Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Implementation of the propositional engine of cvc5.
11 : : */
12 : :
13 : : #include "prop/prop_engine.h"
14 : :
15 : : #include <utility>
16 : :
17 : : #include "base/check.h"
18 : : #include "base/output.h"
19 : : #include "expr/skolem_manager.h"
20 : : #include "options/base_options.h"
21 : : #include "options/decision_options.h"
22 : : #include "options/main_options.h"
23 : : #include "options/options.h"
24 : : #include "options/proof_options.h"
25 : : #include "options/prop_options.h"
26 : : #include "options/smt_options.h"
27 : : #include "proof/proof_node_algorithm.h"
28 : : #include "prop/cnf_stream.h"
29 : : #include "prop/proof_cnf_stream.h"
30 : : #include "prop/prop_proof_manager.h"
31 : : #include "prop/sat_solver.h"
32 : : #include "prop/sat_solver_factory.h"
33 : : #include "prop/theory_proxy.h"
34 : : #include "smt/env.h"
35 : : #include "theory/output_channel.h"
36 : : #include "theory/theory_engine.h"
37 : : #include "util/resource_manager.h"
38 : : #include "util/result.h"
39 : :
40 : : namespace cvc5::internal {
41 : : namespace prop {
42 : :
43 : : /** Keeps a boolean flag scoped */
44 : : class ScopedBool
45 : : {
46 : : private:
47 : : bool d_original;
48 : : bool& d_reference;
49 : :
50 : : public:
51 : 32412 : ScopedBool(bool& reference) : d_reference(reference)
52 : : {
53 : 32412 : d_original = reference;
54 : 32412 : }
55 : :
56 : 32412 : ~ScopedBool() { d_reference = d_original; }
57 : : };
58 : :
59 : 28722 : PropEngine::PropEngine(Env& env, TheoryEngine* te)
60 : : : EnvObj(env),
61 : 28722 : d_inCheckSat(false),
62 : 28722 : d_theoryEngine(te),
63 : 28722 : d_skdm(new SkolemDefManager(d_env.getContext(), d_env.getUserContext())),
64 : 28722 : d_theoryProxy(nullptr),
65 : 28722 : d_satSolver(nullptr),
66 : 28722 : d_cnfStream(nullptr),
67 : 28722 : d_theoryLemmaPg(d_env, d_env.getUserContext(), "PropEngine::ThLemmaPg"),
68 : 28722 : d_ppm(nullptr),
69 : 28722 : d_interrupted(false),
70 : 28722 : d_assumptions(userContext()),
71 : 28722 : d_localLemmas(userContext()),
72 : 86166 : d_stats(statisticsRegistry())
73 : : {
74 [ + - ]: 28722 : Trace("prop") << "Constructing the PropEngine" << std::endl;
75 : 28722 : context::UserContext* userContext = d_env.getUserContext();
76 : :
77 : : // CNF stream, SAT solver and theory proxy required pointers to each other,
78 : : // make the theory proxy first
79 : 28722 : d_theoryProxy = new TheoryProxy(d_env, this, d_theoryEngine, d_skdm.get());
80 : :
81 : 28722 : const auto factory = SatSolverFactory::getFactory(options().prop.satSolver);
82 : 28722 : d_satSolver = factory(
83 : : env, statisticsRegistry(), env.getResourceManager(), d_theoryProxy, "");
84 : :
85 : : // create CnfStream with new SAT solver
86 : 57444 : d_cnfStream = new CnfStream(env,
87 : 28722 : d_satSolver,
88 : 57444 : d_theoryProxy,
89 : : userContext,
90 : : FormulaLitPolicy::TRACK,
91 [ + - ]: 28722 : "prop");
92 : :
93 : : // connect theory proxy
94 : 28722 : d_theoryProxy->finishInit(d_satSolver, d_cnfStream);
95 : : // if proof producing at all
96 [ + + ]: 28722 : if (options().smt.produceProofs)
97 : : {
98 : : PropPfManager* ppm =
99 : 15194 : new PropPfManager(env, d_satSolver, *d_cnfStream, d_assumptions);
100 : 15194 : d_ppm.reset(ppm);
101 : 15194 : d_satSolver->attachProofManager(ppm);
102 : : }
103 : 28722 : }
104 : :
105 : 28722 : void PropEngine::finishInit()
106 : : {
107 : : // Make sure that true/false are not free assumptions in the proof.
108 [ + + ]: 28722 : if (d_ppm)
109 : : {
110 : 15194 : NodeManager* nm = nodeManager();
111 : 30388 : d_ppm->convertAndAssert(theory::InferenceId::INPUT,
112 : 30388 : nm->mkConst(true),
113 : : false,
114 : : false,
115 : : true,
116 : : nullptr);
117 : 30388 : d_ppm->convertAndAssert(theory::InferenceId::INPUT,
118 : 30388 : nm->mkConst(false).notNode(),
119 : : false,
120 : : false,
121 : : true,
122 : : nullptr);
123 : : }
124 : 28722 : }
125 : :
126 : 57418 : PropEngine::~PropEngine()
127 : : {
128 [ + - ]: 28709 : Trace("prop") << "Destructing the PropEngine" << std::endl;
129 [ + - ]: 28709 : delete d_cnfStream;
130 [ + - ]: 28709 : delete d_satSolver;
131 [ + - ]: 28709 : delete d_theoryProxy;
132 : 57418 : }
133 : :
134 : 434801 : TrustNode PropEngine::preprocess(TNode node,
135 : : std::vector<theory::SkolemLemma>& newLemmas)
136 : : {
137 : 434801 : return d_theoryProxy->preprocess(node, newLemmas);
138 : : }
139 : :
140 : 1342 : TrustNode PropEngine::removeItes(TNode node,
141 : : std::vector<theory::SkolemLemma>& newLemmas)
142 : : {
143 : 1342 : return d_theoryProxy->removeItes(node, newLemmas);
144 : : }
145 : :
146 : 52594 : void PropEngine::notifyTopLevelSubstitution(const Node& lhs,
147 : : const Node& rhs) const
148 : : {
149 : 52594 : d_theoryProxy->notifyTopLevelSubstitution(lhs, rhs);
150 [ + + ]: 52594 : if (isOutputOn(OutputTag::SUBS))
151 : : {
152 : 2 : Node eq = SkolemManager::getOriginalForm(lhs.eqNode(rhs));
153 : 2 : output(OutputTag::SUBS) << "(substitution " << eq << ")" << std::endl;
154 : 2 : }
155 [ - + ][ - + ]: 157782 : AssertEqual(lhs.getType(), rhs.getType());
[ - - ]
156 : 52594 : }
157 : :
158 : 40622 : void PropEngine::assertInputFormulas(
159 : : const std::vector<Node>& assertions,
160 : : std::unordered_map<size_t, Node>& skolemMap)
161 : : {
162 [ - + ][ - + ]: 40622 : Assert(!d_inCheckSat) << "Sat solver in solve()!";
[ - - ]
163 : : // now presolve with prop proof manager so proof logging is on. This must be
164 : : // done *before* the PropEngine checkSat call because when asserting formulas
165 : : // to the theory engine lemmas may already be generated.
166 [ + + ]: 40622 : if (d_ppm != nullptr)
167 : : {
168 : 21208 : d_ppm->presolve();
169 : : }
170 : 40622 : d_theoryProxy->notifyInputFormulas(assertions, skolemMap);
171 : 40622 : int64_t natomsPre = d_cnfStream->d_stats.d_numAtoms.get();
172 [ + + ]: 510164 : for (const Node& node : assertions)
173 : : {
174 [ + - ]: 469558 : Trace("prop") << "assertFormula(" << node << ")" << std::endl;
175 : 469574 : assertInternal(theory::InferenceId::INPUT, node, false, false, true);
176 : : }
177 : 40606 : int64_t natomsPost = d_cnfStream->d_stats.d_numAtoms.get();
178 [ - + ][ - + ]: 40606 : Assert(natomsPost >= natomsPre);
[ - - ]
179 : 40606 : d_stats.d_numInputAtoms += (natomsPost - natomsPre);
180 : 40606 : }
181 : :
182 : 886235 : void PropEngine::assertLemma(theory::InferenceId id,
183 : : TrustNode tlemma,
184 : : theory::LemmaProperty p)
185 : : {
186 : 886235 : bool removable = isLemmaPropertyRemovable(p);
187 : 886235 : bool local = isLemmaPropertyLocal(p);
188 : 886235 : bool inprocess = isLemmaPropertyInprocess(p);
189 : :
190 : : // call preprocessor
191 : 886235 : std::vector<theory::SkolemLemma> ppLemmas;
192 : 886236 : TrustNode tplemma = d_theoryProxy->preprocessLemma(tlemma, ppLemmas);
193 : :
194 : : // do final checks on the lemmas we are about to send
195 : 886234 : if (d_env.isTheoryProofProducing()
196 [ + + ][ + + ]: 886234 : && options().proof.proofCheck == options::ProofCheckMode::EAGER)
[ + + ]
197 : : {
198 [ - + ][ - + ]: 4771 : Assert(tplemma.getGenerator() != nullptr);
[ - - ]
199 : : // ensure closed, make the proof node eagerly here to debug
200 : 4771 : tplemma.debugCheckClosed(
201 : : options(), "te-proof-debug", "TheoryEngine::lemma");
202 [ + + ]: 4781 : for (theory::SkolemLemma& lem : ppLemmas)
203 : : {
204 [ - + ][ - + ]: 10 : Assert(lem.d_lemma.getGenerator() != nullptr);
[ - - ]
205 : 10 : lem.d_lemma.debugCheckClosed(
206 : : options(), "te-proof-debug", "TheoryEngine::lemma_new");
207 : : }
208 : : }
209 : :
210 [ - + ]: 886234 : if (TraceIsOn("te-lemma"))
211 : : {
212 : 0 : Trace("te-lemma") << "Lemma, output: " << tplemma.getProven() << std::endl;
213 [ - - ]: 0 : for (const theory::SkolemLemma& lem : ppLemmas)
214 : : {
215 : 0 : Trace("te-lemma") << "Lemma, new lemma: " << lem.d_lemma.getProven()
216 : 0 : << " (skolem is " << lem.d_skolem << ")" << std::endl;
217 : : }
218 [ - - ]: 0 : Trace("te-lemma") << "removable = " << removable << std::endl;
219 : : }
220 : :
221 : : // now, assert the lemmas
222 : 886234 : assertLemmasInternal(id, tplemma, ppLemmas, removable, inprocess, local);
223 : 886235 : }
224 : :
225 : 921799 : void PropEngine::assertTrustedLemmaInternal(theory::InferenceId id,
226 : : TrustNode trn,
227 : : bool removable,
228 : : bool local)
229 : : {
230 : 921799 : Node node = trn.getNode();
231 [ - + ]: 921799 : if (local)
232 : : {
233 : : // if local, filter here
234 [ - - ]: 0 : if (d_localLemmas.find(node) != d_localLemmas.end())
235 : : {
236 : 0 : return;
237 : : }
238 : 0 : d_localLemmas.insert(node);
239 : : }
240 [ + - ]: 921799 : Trace("prop::lemmas") << "assertLemma(" << node << ")" << std::endl;
241 [ + + ]: 921799 : if (isOutputOn(OutputTag::LEMMAS))
242 : : {
243 : 1 : output(OutputTag::LEMMAS) << "(lemma ";
244 : : // use original form of the lemma here
245 : 1 : output(OutputTag::LEMMAS) << SkolemManager::getOriginalForm(node);
246 : 1 : output(OutputTag::LEMMAS) << " :source " << id;
247 : 1 : output(OutputTag::LEMMAS) << ")" << std::endl;
248 : : }
249 : 921799 : bool negated = trn.getKind() == TrustNodeKind::CONFLICT;
250 : : // should have a proof generator if the theory engine is proof producing
251 [ + + ][ + - ]: 921799 : Assert(!d_env.isTheoryProofProducing() || trn.getGenerator() != nullptr);
[ - + ][ - + ]
[ - - ]
252 : : // if we are producing proofs for the SAT solver but not for theory engine,
253 : : // then we need to prevent the lemma of being added as an assumption (since
254 : : // the generator will be null). We use the default proof generator for lemmas.
255 [ + + ]: 1331354 : if (d_env.isSatProofProducing() && !d_env.isTheoryProofProducing()
256 [ + + ][ + + ]: 1331354 : && !trn.getGenerator())
[ + + ]
257 : : {
258 [ + + ]: 90 : Node actualNode = negated ? node.notNode() : node;
259 : 90 : d_theoryLemmaPg.addTrustedStep(actualNode, TrustId::THEORY_LEMMA, {}, {});
260 : 90 : trn = TrustNode::mkReplaceGenTrustNode(trn, &d_theoryLemmaPg);
261 : 90 : }
262 : 921799 : assertInternal(id, node, negated, removable, false, trn.getGenerator());
263 [ + - ]: 921799 : }
264 : :
265 : 1391357 : void PropEngine::assertInternal(theory::InferenceId id,
266 : : TNode node,
267 : : bool negated,
268 : : bool removable,
269 : : bool input,
270 : : ProofGenerator* pg)
271 : : {
272 : 1391357 : bool addAssumption = false;
273 [ + + ]: 1391357 : if (isProofEnabled())
274 : : {
275 : 839243 : if (input
276 [ + + ][ + + ]: 839243 : && options().smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS)
[ + + ]
277 : : {
278 : : // use the proof CNF stream to ensure the literal
279 : 115068 : d_ppm->ensureLiteral(node);
280 : 115068 : addAssumption = true;
281 : : }
282 : : else
283 : : {
284 : 724175 : d_ppm->convertAndAssert(id, node, negated, removable, input, pg);
285 : : }
286 : : }
287 : 552114 : else if (input
288 [ + + ][ - + ]: 552114 : && options().smt.unsatCoresMode
[ - + ]
289 : : == options::UnsatCoresMode::ASSUMPTIONS)
290 : : {
291 : 0 : d_cnfStream->ensureLiteral(node);
292 : 0 : addAssumption = true;
293 : : }
294 : : else
295 : : {
296 : 552130 : d_cnfStream->convertAndAssert(node, removable, negated);
297 : : }
298 [ + + ]: 1391341 : if (addAssumption)
299 : : {
300 [ - + ]: 115068 : if (negated)
301 : : {
302 : 0 : d_assumptions.push_back(node.notNode());
303 : : }
304 : : else
305 : : {
306 : 115068 : d_assumptions.push_back(node);
307 : : }
308 : : }
309 : 1391341 : }
310 : :
311 : 1317938 : void PropEngine::assertLemmasInternal(
312 : : theory::InferenceId id,
313 : : TrustNode trn,
314 : : const std::vector<theory::SkolemLemma>& ppLemmas,
315 : : bool removable,
316 : : bool inprocess,
317 : : bool local)
318 : : {
319 : : // notify skolem definitions first to ensure that the computation of
320 : : // when a literal contains a skolem is accurate in the calls below.
321 [ + - ]: 1317938 : Trace("prop") << "Notify skolem definitions..." << std::endl;
322 [ + + ]: 1353503 : for (const theory::SkolemLemma& lem : ppLemmas)
323 : : {
324 : 35565 : d_theoryProxy->notifySkolemDefinition(lem.getProven(), lem.d_skolem);
325 : : }
326 : : // Assert to the SAT solver first
327 [ + - ]: 1317938 : Trace("prop") << "Push to SAT..." << std::endl;
328 [ + + ]: 1317938 : if (!trn.isNull())
329 : : {
330 : : // inprocess
331 : 886234 : if (inprocess
332 [ + + ][ + + ]: 886234 : && options().theory.lemmaInprocess != options::LemmaInprocessMode::NONE)
[ + + ]
333 : : {
334 : 3 : trn = d_theoryProxy->inprocessLemma(trn);
335 : : }
336 : 886234 : assertTrustedLemmaInternal(id, trn, removable, local);
337 : : }
338 [ + + ]: 1353503 : for (const theory::SkolemLemma& lem : ppLemmas)
339 : : {
340 : 35565 : assertTrustedLemmaInternal(theory::InferenceId::THEORY_PP_SKOLEM_LEM,
341 : 35565 : lem.d_lemma,
342 : : removable,
343 : : local);
344 : : }
345 : : // Note that this order is important for theories that send lemmas during
346 : : // preregistration, as it impacts the order in which lemmas are processed
347 : : // by default by the decision engine. In particular, sending to the SAT
348 : : // solver first means that lemmas sent during preregistration in response to
349 : : // the current lemma are processed after that lemma. This makes a difference
350 : : // e.g. for string reduction lemmas, where preregistration lemmas are
351 : : // introduced for skolems that appear in reductions. Moving the above
352 : : // block after the one below has mixed performance on SMT-LIB strings logics.
353 [ + - ]: 1317938 : Trace("prop") << "Notify assertions..." << std::endl;
354 : : // also add to the decision engine, where notice we don't need proofs
355 [ + + ]: 1317938 : if (!trn.isNull())
356 : : {
357 : : // notify the theory proxy of the lemma
358 : 886234 : d_theoryProxy->notifyAssertion(trn.getProven(), TNode::null(), true, local);
359 : : }
360 [ + + ]: 1353503 : for (const theory::SkolemLemma& lem : ppLemmas)
361 : : {
362 : 35565 : d_theoryProxy->notifyAssertion(lem.getProven(), lem.d_skolem, true, local);
363 : : }
364 [ + - ]: 1317938 : Trace("prop") << "Finish " << trn << std::endl;
365 : 1317938 : }
366 : :
367 : 269814 : void PropEngine::notifyExplainedPropagation(TrustNode texp)
368 : : {
369 [ + + ]: 269814 : if (d_ppm != nullptr)
370 : : {
371 : 158564 : d_ppm->notifyExplainedPropagation(texp);
372 : : }
373 : 269814 : }
374 : :
375 : 166864 : void PropEngine::preferPhase(TNode n, bool phase)
376 : : {
377 [ + - ]: 166864 : Trace("prop") << "preferPhase(" << n << ", " << phase << ")" << std::endl;
378 : :
379 [ - + ][ - + ]: 166864 : Assert(n.getType().isBoolean());
[ - - ]
380 : 166864 : SatLiteral lit = d_cnfStream->getLiteral(n);
381 [ + + ]: 166864 : d_satSolver->preferPhase(phase ? lit : ~lit);
382 : 166864 : }
383 : :
384 : 206711 : bool PropEngine::isDecision(Node lit) const
385 : : {
386 [ - + ][ - + ]: 206711 : Assert(isSatLiteral(lit));
[ - - ]
387 : 206711 : return d_satSolver->isDecision(d_cnfStream->getLiteral(lit).getSatVariable());
388 : : }
389 : :
390 : 0 : std::vector<Node> PropEngine::getPropDecisions() const
391 : : {
392 : 0 : std::vector<Node> decisions;
393 : 0 : std::vector<SatLiteral> miniDecisions = d_satSolver->getDecisions();
394 [ - - ]: 0 : for (SatLiteral d : miniDecisions)
395 : : {
396 : 0 : decisions.push_back(d_cnfStream->getNode(d));
397 : : }
398 : 0 : return decisions;
399 : 0 : }
400 : :
401 : 0 : std::vector<Node> PropEngine::getPropOrderHeap() const
402 : : {
403 : 0 : return d_satSolver->getOrderHeap();
404 : : }
405 : :
406 : 16 : bool PropEngine::isFixed(TNode lit) const
407 : : {
408 [ + - ]: 16 : if (isSatLiteral(lit))
409 : : {
410 : 16 : return d_satSolver->isFixed(d_cnfStream->getLiteral(lit).getSatVariable());
411 : : }
412 : 0 : return false;
413 : : }
414 : :
415 : 0 : void PropEngine::printSatisfyingAssignment()
416 : : {
417 : : const CnfStream::NodeToLiteralMap& transCache =
418 : 0 : d_cnfStream->getTranslationCache();
419 [ - - ]: 0 : Trace("prop-value") << "Literal | Value | Expr" << std::endl
420 : 0 : << "----------------------------------------"
421 : 0 : << "-----------------" << std::endl;
422 : 0 : for (CnfStream::NodeToLiteralMap::const_iterator i = transCache.begin(),
423 : 0 : end = transCache.end();
424 [ - - ]: 0 : i != end;
425 : 0 : ++i)
426 : : {
427 : 0 : std::pair<Node, SatLiteral> curr = *i;
428 : 0 : SatLiteral l = curr.second;
429 [ - - ]: 0 : if (!l.isNegated())
430 : : {
431 : 0 : Node n = curr.first;
432 : 0 : SatValue value = d_satSolver->modelValue(l);
433 [ - - ]: 0 : Trace("prop-value") << "'" << l << "' " << value << " " << n << std::endl;
434 : 0 : }
435 : 0 : }
436 : 0 : }
437 : 934 : void PropEngine::outputIncompleteReason(UnknownExplanation uexp,
438 : : theory::IncompleteId iid)
439 : : {
440 [ + + ]: 934 : if (isOutputOn(OutputTag::INCOMPLETE))
441 : : {
442 : 4 : output(OutputTag::INCOMPLETE) << "(incomplete ";
443 : 4 : output(OutputTag::INCOMPLETE) << uexp;
444 [ + - ]: 4 : if (iid != theory::IncompleteId::UNKNOWN)
445 : : {
446 : 4 : output(OutputTag::INCOMPLETE) << " " << iid;
447 : : }
448 : 4 : output(OutputTag::INCOMPLETE) << ")" << std::endl;
449 : : }
450 : 934 : }
451 : :
452 : 32412 : Result PropEngine::checkSat()
453 : : {
454 [ - + ][ - + ]: 32412 : Assert(!d_inCheckSat) << "Sat solver in solve()!";
[ - - ]
455 [ + - ]: 32412 : Trace("prop") << "PropEngine::checkSat()" << std::endl;
456 : :
457 : : // Mark that we are in the checkSat
458 : 32412 : ScopedBool scopedBool(d_inCheckSat);
459 : 32412 : d_inCheckSat = true;
460 : :
461 [ - + ]: 32412 : if (options().base.preprocessOnly)
462 : : {
463 : 0 : outputIncompleteReason(UnknownExplanation::REQUIRES_FULL_CHECK);
464 : 0 : return Result(Result::UNKNOWN, UnknownExplanation::REQUIRES_FULL_CHECK);
465 : : }
466 : :
467 : : // Note this currently ignores conflicts (a dangerous practice).
468 : 32412 : d_theoryProxy->presolve();
469 : :
470 : : // add the assumptions
471 : 32412 : std::vector<SatLiteral> assumptions;
472 [ + + ]: 160538 : for (const Node& node : d_assumptions)
473 : : {
474 : 128126 : assumptions.push_back(d_cnfStream->getLiteral(node));
475 : : }
476 : :
477 : : // now log preprocessing
478 [ + + ]: 32412 : if (d_ppm != nullptr)
479 : : {
480 : 17560 : d_ppm->logPreprocessing();
481 : : }
482 : :
483 : : // Reset the interrupted flag
484 : 32412 : d_interrupted = false;
485 : :
486 : : // Check the problem
487 : : SatValue result;
488 [ + + ]: 32412 : if (assumptions.empty())
489 : : {
490 : 24877 : result = d_satSolver->solve();
491 : : }
492 : : else
493 : : {
494 : 7535 : result = d_satSolver->solve(assumptions);
495 : : }
496 : :
497 : 32396 : ResourceManager* rm = resourceManager();
498 : 32396 : bool wasInterrupted = result == SAT_VALUE_UNKNOWN;
499 : : // If a resource limit expires during a full theory check, the SAT solver may
500 : : // still return SAT before observing its termination callback. In that case,
501 : : // the candidate model may not have been fully checked by the theories.
502 [ + + ][ + - ]: 32396 : if (result == SAT_VALUE_TRUE && (d_interrupted || rm->out()))
[ - + ][ - + ]
503 : : {
504 : 0 : wasInterrupted = true;
505 : 0 : result = SAT_VALUE_UNKNOWN;
506 : : }
507 : :
508 : 32396 : d_theoryProxy->postsolve(result);
509 : :
510 [ + + ]: 32396 : if (wasInterrupted)
511 : : {
512 : 82 : UnknownExplanation why = UnknownExplanation::INTERRUPTED;
513 [ + + ]: 82 : if (rm->outOfTime())
514 : : {
515 : 80 : why = UnknownExplanation::TIMEOUT;
516 : : }
517 [ + + ]: 82 : if (rm->outOfResources())
518 : : {
519 : 2 : why = UnknownExplanation::RESOURCEOUT;
520 : : }
521 : 82 : outputIncompleteReason(why);
522 : 82 : return Result(Result::UNKNOWN, why);
523 : : }
524 : :
525 : 32314 : if (result == SAT_VALUE_TRUE && TraceIsOn("prop"))
526 : : {
527 : 0 : printSatisfyingAssignment();
528 : : }
529 : :
530 [ + - ]: 32314 : Trace("prop") << "PropEngine::checkSat() => " << result << std::endl;
531 [ + + ]: 32314 : if (result == SAT_VALUE_TRUE)
532 : : {
533 [ + + ]: 13709 : if (d_theoryProxy->isModelUnsound())
534 : : {
535 : 832 : outputIncompleteReason(UnknownExplanation::INCOMPLETE,
536 : 832 : d_theoryProxy->getModelUnsoundId());
537 : 832 : return Result(Result::UNKNOWN, UnknownExplanation::INCOMPLETE);
538 : : }
539 : : }
540 [ + + ]: 18605 : else if (d_theoryProxy->isRefutationUnsound())
541 : : {
542 : 20 : outputIncompleteReason(UnknownExplanation::INCOMPLETE,
543 : 20 : d_theoryProxy->getRefutationUnsoundId());
544 : 20 : return Result(Result::UNKNOWN, UnknownExplanation::INCOMPLETE);
545 : : }
546 : :
547 [ + + ]: 31462 : if (d_ppm != nullptr)
548 : : {
549 : 17459 : d_ppm->postsolve(result);
550 : : }
551 : :
552 [ + + ]: 31462 : return Result(result == SAT_VALUE_TRUE ? Result::SAT : Result::UNSAT);
553 : 32428 : }
554 : :
555 : 96566 : Node PropEngine::getValue(TNode node) const
556 : : {
557 [ - + ][ - + ]: 96566 : Assert(node.getType().isBoolean());
[ - - ]
558 [ - + ][ - + ]: 96566 : Assert(d_cnfStream->hasLiteral(node));
[ - - ]
559 : :
560 : 96566 : SatLiteral lit = d_cnfStream->getLiteral(node);
561 : :
562 : 96566 : SatValue v = d_satSolver->value(lit);
563 [ + + ]: 96566 : if (v == SAT_VALUE_TRUE)
564 : : {
565 : 192616 : return nodeManager()->mkConst(true);
566 : : }
567 [ + + ]: 258 : else if (v == SAT_VALUE_FALSE)
568 : : {
569 : 416 : return nodeManager()->mkConst(false);
570 : : }
571 : : else
572 : : {
573 [ - + ][ - + ]: 50 : Assert(v == SAT_VALUE_UNKNOWN);
[ - - ]
574 : 50 : return Node::null();
575 : : }
576 : : }
577 : :
578 : 58615483 : bool PropEngine::isSatLiteral(TNode node) const
579 : : {
580 : 58615483 : return d_cnfStream->hasLiteral(node);
581 : : }
582 : :
583 : 22704421 : bool PropEngine::hasValue(TNode node, bool& value) const
584 : : {
585 [ - + ][ - + ]: 22704421 : Assert(node.getType().isBoolean());
[ - - ]
586 : 22704421 : Assert(d_cnfStream->hasLiteral(node)) << node;
587 : :
588 : 22704421 : SatLiteral lit = d_cnfStream->getLiteral(node);
589 : :
590 : 22704421 : SatValue v = d_satSolver->value(lit);
591 [ + + ]: 22704421 : if (v == SAT_VALUE_TRUE)
592 : : {
593 : 13693352 : value = true;
594 : 13693352 : return true;
595 : : }
596 [ + + ]: 9011069 : else if (v == SAT_VALUE_FALSE)
597 : : {
598 : 316550 : value = false;
599 : 316550 : return true;
600 : : }
601 : : else
602 : : {
603 [ - + ][ - + ]: 8694519 : Assert(v == SAT_VALUE_UNKNOWN);
[ - - ]
604 : 8694519 : return false;
605 : : }
606 : : }
607 : :
608 : 28899 : void PropEngine::getBooleanVariables(std::vector<TNode>& outputVariables) const
609 : : {
610 : 28899 : d_cnfStream->getBooleanVariables(outputVariables);
611 : 28899 : }
612 : :
613 : 421356 : Node PropEngine::ensureLiteral(TNode n)
614 : : {
615 : : // must preprocess
616 : 421356 : Node preprocessed = getPreprocessedTerm(n);
617 [ + - ]: 842712 : Trace("ensureLiteral") << "ensureLiteral preprocessed: " << preprocessed
618 : 421356 : << std::endl;
619 [ + + ]: 421356 : if (isProofEnabled())
620 : : {
621 : 233374 : d_ppm->ensureLiteral(preprocessed);
622 : : }
623 : : else
624 : : {
625 : 187982 : d_cnfStream->ensureLiteral(preprocessed);
626 : : }
627 : 421356 : return preprocessed;
628 : 0 : }
629 : :
630 : 431704 : Node PropEngine::getPreprocessedTerm(TNode n)
631 : : {
632 : : // must preprocess
633 : 431704 : std::vector<theory::SkolemLemma> newLemmas;
634 : 431704 : TrustNode tpn = d_theoryProxy->preprocess(n, newLemmas);
635 : : // send lemmas corresponding to the skolems introduced by preprocessing n
636 : 431704 : TrustNode trnNull;
637 : 431704 : assertLemmasInternal(theory::InferenceId::THEORY_PP_SKOLEM_LEM,
638 : : trnNull,
639 : : newLemmas,
640 : : false,
641 : : false,
642 : : false);
643 [ + + ]: 863408 : return tpn.isNull() ? Node(n) : tpn.getNode();
644 : 431704 : }
645 : :
646 : 4194 : Node PropEngine::getPreprocessedTerm(TNode n,
647 : : std::vector<Node>& skAsserts,
648 : : std::vector<Node>& sks)
649 : : {
650 : : // get the preprocessed form of the term
651 : 4194 : Node pn = getPreprocessedTerm(n);
652 : : // initialize the set of skolems and assertions to process
653 : 4194 : std::vector<Node> toProcessAsserts;
654 : 4194 : std::vector<Node> toProcess;
655 : 4194 : d_theoryProxy->getSkolems(pn, toProcessAsserts, toProcess);
656 : 4194 : size_t index = 0;
657 : : // until fixed point is reached
658 [ + + ]: 8461 : while (index < toProcess.size())
659 : : {
660 : 4267 : Node ka = toProcessAsserts[index];
661 : 4267 : Node k = toProcess[index];
662 : 4267 : index++;
663 [ + + ]: 4267 : if (std::find(sks.begin(), sks.end(), k) != sks.end())
664 : : {
665 : : // already added the skolem to the list
666 : 2246 : continue;
667 : : }
668 : : // must preprocess lemmas as well
669 : 2021 : Node kap = getPreprocessedTerm(ka);
670 : 2021 : skAsserts.push_back(kap);
671 : 2021 : sks.push_back(k);
672 : : // get the skolems in the preprocessed form of the lemma ka
673 : 2021 : d_theoryProxy->getSkolems(kap, toProcessAsserts, toProcess);
674 [ + + ][ + + ]: 6513 : }
675 : : // return the preprocessed term
676 : 8388 : return pn;
677 : 4194 : }
678 : :
679 : 4339 : void PropEngine::push()
680 : : {
681 [ - + ][ - + ]: 4339 : Assert(!d_inCheckSat) << "Sat solver in solve()!";
[ - - ]
682 : 4339 : d_satSolver->push();
683 [ + - ]: 4339 : Trace("prop") << "push()" << std::endl;
684 : 4339 : }
685 : :
686 : 4338 : void PropEngine::pop()
687 : : {
688 [ - + ][ - + ]: 4338 : Assert(!d_inCheckSat) << "Sat solver in solve()!";
[ - - ]
689 : 4338 : d_satSolver->pop();
690 [ + - ]: 4338 : Trace("prop") << "pop()" << std::endl;
691 : 4338 : }
692 : :
693 : 31972 : void PropEngine::resetTrail()
694 : : {
695 : 31972 : d_satSolver->resetTrail();
696 [ + - ]: 31972 : Trace("prop") << "resetTrail()" << std::endl;
697 : 31972 : }
698 : :
699 : 28672 : uint32_t PropEngine::getAssertionLevel() const
700 : : {
701 : 28672 : return d_satSolver->getAssertionLevel();
702 : : }
703 : :
704 : 0 : bool PropEngine::isRunning() const { return d_inCheckSat; }
705 : 269557 : void PropEngine::interrupt()
706 : : {
707 [ + + ]: 269557 : if (!d_inCheckSat)
708 : : {
709 : 261519 : return;
710 : : }
711 : :
712 : 8038 : d_interrupted = true;
713 : 8038 : d_satSolver->interrupt();
714 [ + - ]: 8038 : Trace("prop") << "interrupt()" << std::endl;
715 : : }
716 : :
717 : 4787 : void PropEngine::spendResource(Resource r)
718 : : {
719 : 4787 : d_env.getResourceManager()->spendResource(r);
720 : 4787 : }
721 : :
722 : 0 : bool PropEngine::properExplanation(TNode node, TNode expl) const
723 : : {
724 [ - - ]: 0 : if (!d_cnfStream->hasLiteral(node))
725 : : {
726 [ - - ]: 0 : Trace("properExplanation")
727 : 0 : << "properExplanation(): Failing because node "
728 : 0 : << "being explained doesn't have a SAT literal ?!" << std::endl
729 : 0 : << "properExplanation(): The node is: " << node << std::endl;
730 : 0 : return false;
731 : : }
732 : :
733 : 0 : SatLiteral nodeLit = d_cnfStream->getLiteral(node);
734 : :
735 : 0 : for (TNode::kinded_iterator i = expl.begin(Kind::AND),
736 : 0 : i_end = expl.end(Kind::AND);
737 [ - - ]: 0 : i != i_end;
738 : 0 : ++i)
739 : : {
740 [ - - ]: 0 : if (!d_cnfStream->hasLiteral(*i))
741 : : {
742 [ - - ]: 0 : Trace("properExplanation")
743 : 0 : << "properExplanation(): Failing because one of explanation "
744 : 0 : << "nodes doesn't have a SAT literal" << std::endl
745 : 0 : << "properExplanation(): The explanation node is: " << *i
746 : 0 : << std::endl;
747 : 0 : return false;
748 : : }
749 : :
750 : 0 : SatLiteral iLit = d_cnfStream->getLiteral(*i);
751 : :
752 [ - - ]: 0 : if (iLit == nodeLit)
753 : : {
754 [ - - ]: 0 : Trace("properExplanation")
755 : 0 : << "properExplanation(): Failing because the node" << std::endl
756 : 0 : << "properExplanation(): " << node << std::endl
757 : 0 : << "properExplanation(): cannot be made to explain itself!"
758 : 0 : << std::endl;
759 : 0 : return false;
760 : : }
761 [ - - ][ - - ]: 0 : }
762 : :
763 : 0 : return true;
764 : : }
765 : :
766 : 7 : void PropEngine::checkProof(const context::CDList<Node>& assertions)
767 : : {
768 [ - + ]: 7 : if (!d_env.isSatProofProducing())
769 : : {
770 : 0 : return;
771 : : }
772 : 7 : return d_ppm->checkProof(assertions);
773 : : }
774 : :
775 : 8148 : std::shared_ptr<ProofNode> PropEngine::getProof(bool connectCnf)
776 : : {
777 [ - + ]: 8148 : if (!d_env.isSatProofProducing())
778 : : {
779 : 0 : return nullptr;
780 : : }
781 [ + - ]: 16296 : Trace("sat-proof") << "PropEngine::getProof: getting proof with cnfStream's "
782 : 0 : "lazycdproof cxt lvl "
783 : 8148 : << userContext()->getLevel() << "\n";
784 : 8148 : return d_ppm->getProof(connectCnf);
785 : : }
786 : :
787 : 6 : std::vector<std::shared_ptr<ProofNode>> PropEngine::getProofLeaves(
788 : : modes::ProofComponent pc)
789 : : {
790 : 6 : return d_ppm->getProofLeaves(pc);
791 : : }
792 : :
793 : 1812713 : bool PropEngine::isProofEnabled() const { return d_ppm != nullptr; }
794 : :
795 : 3467 : void PropEngine::getUnsatCore(std::vector<Node>& core)
796 : : {
797 [ + + ]: 3467 : if (options().smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS)
798 : : {
799 [ + - ]: 6268 : Trace("unsat-core") << "PropEngine::getUnsatCore: via unsat assumptions"
800 : 3134 : << std::endl;
801 : 3134 : std::vector<SatLiteral> unsat_assumptions;
802 : 3134 : d_satSolver->getUnsatAssumptions(unsat_assumptions);
803 [ + + ]: 21020 : for (const SatLiteral& lit : unsat_assumptions)
804 : : {
805 : 17886 : core.push_back(d_cnfStream->getNode(lit));
806 : : }
807 : 3134 : }
808 : : else
809 : : {
810 [ + - ]: 333 : Trace("unsat-core") << "PropEngine::getUnsatCore: via proof" << std::endl;
811 : : // otherwise, it is just the free assumptions of the proof. Note that we
812 : : // need to connect the SAT proof to the CNF proof becuase we need the
813 : : // preprocessed input as leaves, not the clauses derived from them.
814 : 333 : std::shared_ptr<ProofNode> pfn = getProof();
815 [ + - ]: 333 : Trace("unsat-core") << "Proof is " << *pfn.get() << std::endl;
816 : 333 : expr::getFreeAssumptions(pfn.get(), core);
817 [ + - ]: 333 : Trace("unsat-core") << "Core is " << core << std::endl;
818 : 333 : }
819 : 3467 : }
820 : :
821 : 10 : std::vector<Node> PropEngine::getUnsatCoreLemmas()
822 : : {
823 [ - + ][ - + ]: 10 : Assert(d_env.isSatProofProducing());
[ - - ]
824 : 10 : std::vector<Node> lems = d_ppm->getUnsatCoreLemmas();
825 [ - + ]: 10 : if (isOutputOn(OutputTag::UNSAT_CORE_LEMMAS))
826 : : {
827 : 0 : output(OutputTag::UNSAT_CORE_LEMMAS)
828 : 0 : << ";; unsat core lemmas start" << std::endl;
829 : 0 : std::stringstream ss;
830 [ - - ]: 0 : for (const Node& lem : lems)
831 : : {
832 : 0 : output(OutputTag::UNSAT_CORE_LEMMAS) << "(unsat-core-lemma ";
833 : : output(OutputTag::UNSAT_CORE_LEMMAS)
834 : 0 : << SkolemManager::getOriginalForm(lem);
835 : 0 : uint64_t timestamp = 0;
836 : 0 : theory::InferenceId id = d_ppm->getInferenceIdFor(lem, timestamp);
837 [ - - ]: 0 : if (id != theory::InferenceId::NONE)
838 : : {
839 : 0 : output(OutputTag::UNSAT_CORE_LEMMAS) << " :source " << id;
840 : : }
841 : 0 : output(OutputTag::UNSAT_CORE_LEMMAS) << " :timestamp " << timestamp;
842 : 0 : output(OutputTag::UNSAT_CORE_LEMMAS) << ")" << std::endl;
843 : : // for trace below
844 : 0 : ss << id << ", " << timestamp << std::endl;
845 : : }
846 : 0 : output(OutputTag::UNSAT_CORE_LEMMAS)
847 : 0 : << ";; unsat core lemmas end" << std::endl;
848 : : // print in csv form for debugging
849 [ - - ]: 0 : Trace("ocl-timestamp") << "TIMESTAMPS" << std::endl;
850 : 0 : Trace("ocl-timestamp") << ss.str() << std::endl;
851 : 0 : }
852 : 10 : return lems;
853 : 0 : }
854 : :
855 : 20 : std::vector<Node> PropEngine::getLearnedZeroLevelLiterals(
856 : : modes::LearnedLitType ltype) const
857 : : {
858 : 20 : return d_theoryProxy->getLearnedZeroLevelLiterals(ltype);
859 : : }
860 : :
861 : 7 : std::vector<Node> PropEngine::getLearnedZeroLevelLiteralsForRestart() const
862 : : {
863 : 7 : return d_theoryProxy->getLearnedZeroLevelLiteralsForRestart();
864 : : }
865 : :
866 : 0 : modes::LearnedLitType PropEngine::getLiteralType(const Node& lit) const
867 : : {
868 : 0 : return d_theoryProxy->getLiteralType(lit);
869 : : }
870 : :
871 : 28722 : PropEngine::Statistics::Statistics(StatisticsRegistry& sr)
872 : 28722 : : d_numInputAtoms(sr.registerInt("prop::PropEngine::numInputAtoms"))
873 : : {
874 : 28722 : }
875 : :
876 : : } // namespace prop
877 : : } // namespace cvc5::internal
|
