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