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