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