Fix remove term formula policy for terms beneath quantifiers (#5497)
[cvc5.git] / src / theory / theory_engine.cpp
1 /********************* */
2 /*! \file theory_engine.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Dejan Jovanovic, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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.\endverbatim
11 **
12 ** \brief The theory engine
13 **
14 ** The theory engine.
15 **/
16
17 #include "theory/theory_engine.h"
18
19 #include <list>
20 #include <vector>
21
22 #include "base/map_util.h"
23 #include "decision/decision_engine.h"
24 #include "expr/attribute.h"
25 #include "expr/lazy_proof.h"
26 #include "expr/node.h"
27 #include "expr/node_builder.h"
28 #include "expr/node_visitor.h"
29 #include "options/bv_options.h"
30 #include "options/options.h"
31 #include "options/quantifiers_options.h"
32 #include "options/theory_options.h"
33 #include "preprocessing/assertion_pipeline.h"
34 #include "printer/printer.h"
35 #include "smt/dump.h"
36 #include "smt/logic_exception.h"
37 #include "smt/term_formula_removal.h"
38 #include "theory/arith/arith_ite_utils.h"
39 #include "theory/bv/theory_bv_utils.h"
40 #include "theory/care_graph.h"
41 #include "theory/combination_care_graph.h"
42 #include "theory/decision_manager.h"
43 #include "theory/quantifiers/first_order_model.h"
44 #include "theory/quantifiers/fmf/model_engine.h"
45 #include "theory/quantifiers/theory_quantifiers.h"
46 #include "theory/quantifiers_engine.h"
47 #include "theory/relevance_manager.h"
48 #include "theory/rewriter.h"
49 #include "theory/theory.h"
50 #include "theory/theory_engine_proof_generator.h"
51 #include "theory/theory_id.h"
52 #include "theory/theory_model.h"
53 #include "theory/theory_traits.h"
54 #include "theory/uf/equality_engine.h"
55 #include "util/resource_manager.h"
56
57 using namespace std;
58
59 using namespace CVC4::preprocessing;
60 using namespace CVC4::theory;
61
62 namespace CVC4 {
63
64 /* -------------------------------------------------------------------------- */
65
66 namespace theory {
67
68 /**
69 * IMPORTANT: The order of the theories is important. For example, strings
70 * depends on arith, quantifiers needs to come as the very last.
71 * Do not change this order.
72 */
73
74 #define CVC4_FOR_EACH_THEORY \
75 CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BUILTIN) \
76 CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BOOL) \
77 CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_UF) \
78 CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_ARITH) \
79 CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BV) \
80 CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_FP) \
81 CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_ARRAYS) \
82 CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_DATATYPES) \
83 CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_SEP) \
84 CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_SETS) \
85 CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BAGS) \
86 CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_STRINGS) \
87 CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_QUANTIFIERS)
88
89 } // namespace theory
90
91 /* -------------------------------------------------------------------------- */
92
93 inline void flattenAnd(Node n, std::vector<TNode>& out){
94 Assert(n.getKind() == kind::AND);
95 for(Node::iterator i=n.begin(), i_end=n.end(); i != i_end; ++i){
96 Node curr = *i;
97 if(curr.getKind() == kind::AND){
98 flattenAnd(curr, out);
99 }else{
100 out.push_back(curr);
101 }
102 }
103 }
104
105 inline Node flattenAnd(Node n){
106 std::vector<TNode> out;
107 flattenAnd(n, out);
108 return NodeManager::currentNM()->mkNode(kind::AND, out);
109 }
110
111 /**
112 * Compute the string for a given theory id. In this module, we use
113 * THEORY_SAT_SOLVER as an id, which is not a normal id but maps to
114 * THEORY_LAST. Thus, we need our own string conversion here.
115 *
116 * @param id The theory id
117 * @return The string corresponding to the theory id
118 */
119 std::string getTheoryString(theory::TheoryId id)
120 {
121 if (id == theory::THEORY_SAT_SOLVER)
122 {
123 return "THEORY_SAT_SOLVER";
124 }
125 else
126 {
127 std::stringstream ss;
128 ss << id;
129 return ss.str();
130 }
131 }
132
133 void TheoryEngine::finishInit()
134 {
135 // NOTE: This seems to be required since
136 // theory::TheoryTraits<THEORY>::isParametric cannot be accessed without
137 // using the CVC4_FOR_EACH_THEORY_STATEMENT macro. -AJR
138 std::vector<theory::Theory*> paraTheories;
139 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
140 #undef CVC4_FOR_EACH_THEORY_STATEMENT
141 #endif
142 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
143 if (theory::TheoryTraits<THEORY>::isParametric \
144 && d_logicInfo.isTheoryEnabled(THEORY)) \
145 { \
146 paraTheories.push_back(theoryOf(THEORY)); \
147 }
148 // Collect the parametric theories, which are given to the theory combination
149 // manager below
150 CVC4_FOR_EACH_THEORY;
151
152 // Initialize the theory combination architecture
153 if (options::tcMode() == options::TcMode::CARE_GRAPH)
154 {
155 d_tc.reset(new CombinationCareGraph(*this, paraTheories, d_pnm));
156 }
157 else
158 {
159 Unimplemented() << "TheoryEngine::finishInit: theory combination mode "
160 << options::tcMode() << " not supported";
161 }
162 // create the relevance filter if any option requires it
163 if (options::relevanceFilter())
164 {
165 d_relManager.reset(
166 new RelevanceManager(d_userContext, theory::Valuation(this)));
167 }
168
169 // initialize the quantifiers engine
170 if (d_logicInfo.isQuantified())
171 {
172 // initialize the quantifiers engine
173 d_quantEngine = new QuantifiersEngine(this, *d_decManager.get(), d_pnm);
174 }
175 // initialize the theory combination manager, which decides and allocates the
176 // equality engines to use for all theories.
177 d_tc->finishInit();
178 // get pointer to the shared solver
179 d_sharedSolver = d_tc->getSharedSolver();
180
181 // set the core equality engine on quantifiers engine
182 if (d_logicInfo.isQuantified())
183 {
184 d_quantEngine->setMasterEqualityEngine(d_tc->getCoreEqualityEngine());
185 }
186
187 // finish initializing the theories by linking them with the appropriate
188 // utilities and then calling their finishInit method.
189 for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
190 Theory* t = d_theoryTable[theoryId];
191 if (t == nullptr)
192 {
193 continue;
194 }
195 // setup the pointers to the utilities
196 const EeTheoryInfo* eeti = d_tc->getEeTheoryInfo(theoryId);
197 Assert(eeti != nullptr);
198 // the theory's official equality engine is the one specified by the
199 // equality engine manager
200 t->setEqualityEngine(eeti->d_usedEe);
201 // set the quantifiers engine
202 t->setQuantifiersEngine(d_quantEngine);
203 // set the decision manager for the theory
204 t->setDecisionManager(d_decManager.get());
205 // finish initializing the theory
206 t->finishInit();
207 }
208
209 // finish initializing the quantifiers engine
210 if (d_logicInfo.isQuantified())
211 {
212 d_quantEngine->finishInit();
213 }
214 }
215
216 ProofNodeManager* TheoryEngine::getProofNodeManager() const { return d_pnm; }
217
218 TheoryEngine::TheoryEngine(context::Context* context,
219 context::UserContext* userContext,
220 ResourceManager* rm,
221 RemoveTermFormulas& iteRemover,
222 const LogicInfo& logicInfo,
223 OutputManager& outMgr,
224 ProofNodeManager* pnm)
225 : d_propEngine(nullptr),
226 d_context(context),
227 d_userContext(userContext),
228 d_logicInfo(logicInfo),
229 d_outMgr(outMgr),
230 d_pnm(pnm),
231 d_lazyProof(
232 d_pnm != nullptr
233 ? new LazyCDProof(
234 d_pnm, nullptr, d_userContext, "TheoryEngine::LazyCDProof")
235 : nullptr),
236 d_tepg(new TheoryEngineProofGenerator(d_pnm, d_userContext)),
237 d_tc(nullptr),
238 d_sharedSolver(nullptr),
239 d_quantEngine(nullptr),
240 d_decManager(new DecisionManager(userContext)),
241 d_relManager(nullptr),
242 d_preRegistrationVisitor(this, context),
243 d_eager_model_building(false),
244 d_inConflict(context, false),
245 d_inSatMode(false),
246 d_hasShutDown(false),
247 d_incomplete(context, false),
248 d_propagationMap(context),
249 d_propagationMapTimestamp(context, 0),
250 d_propagatedLiterals(context),
251 d_propagatedLiteralsIndex(context, 0),
252 d_atomRequests(context),
253 d_tpp(*this, iteRemover, userContext, d_pnm),
254 d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
255 d_true(),
256 d_false(),
257 d_interrupted(false),
258 d_resourceManager(rm),
259 d_inPreregister(false),
260 d_factsAsserted(context, false),
261 d_attr_handle(),
262 d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0)
263 {
264 for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST;
265 ++ theoryId)
266 {
267 d_theoryTable[theoryId] = NULL;
268 d_theoryOut[theoryId] = NULL;
269 }
270
271 smtStatisticsRegistry()->registerStat(&d_combineTheoriesTime);
272 d_true = NodeManager::currentNM()->mkConst<bool>(true);
273 d_false = NodeManager::currentNM()->mkConst<bool>(false);
274
275 smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded);
276 }
277
278 TheoryEngine::~TheoryEngine() {
279 Assert(d_hasShutDown);
280
281 for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
282 if(d_theoryTable[theoryId] != NULL) {
283 delete d_theoryTable[theoryId];
284 delete d_theoryOut[theoryId];
285 }
286 }
287
288 delete d_quantEngine;
289
290 smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime);
291 smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded);
292 }
293
294 void TheoryEngine::interrupt() { d_interrupted = true; }
295 void TheoryEngine::preRegister(TNode preprocessed) {
296 Debug("theory") << "TheoryEngine::preRegister( " << preprocessed << ")"
297 << std::endl;
298 d_preregisterQueue.push(preprocessed);
299
300 if (!d_inPreregister) {
301 // We're in pre-register
302 d_inPreregister = true;
303
304 // Process the pre-registration queue
305 while (!d_preregisterQueue.empty()) {
306 // Get the next atom to pre-register
307 preprocessed = d_preregisterQueue.front();
308 d_preregisterQueue.pop();
309
310 // the atom should not have free variables
311 Debug("theory") << "TheoryEngine::preRegister: " << preprocessed
312 << std::endl;
313 Assert(!expr::hasFreeVar(preprocessed));
314 // should not have witness
315 Assert(!expr::hasSubtermKind(kind::WITNESS, preprocessed));
316
317 // Pre-register the terms in the atom
318 theory::TheoryIdSet theories = NodeVisitor<PreRegisterVisitor>::run(
319 d_preRegistrationVisitor, preprocessed);
320 theories = TheoryIdSetUtil::setRemove(THEORY_BOOL, theories);
321 // Remove the top theory, if any more that means multiple theories were
322 // involved
323 bool multipleTheories =
324 TheoryIdSetUtil::setRemove(Theory::theoryOf(preprocessed), theories);
325 if (Configuration::isAssertionBuild())
326 {
327 TheoryId i;
328 // This should never throw an exception, since theories should be
329 // guaranteed to be initialized.
330 // These checks don't work with finite model finding, because it
331 // uses Rational constants to represent cardinality constraints,
332 // even though arithmetic isn't actually involved.
333 if (!options::finiteModelFind())
334 {
335 while ((i = TheoryIdSetUtil::setPop(theories)) != THEORY_LAST)
336 {
337 if (!d_logicInfo.isTheoryEnabled(i))
338 {
339 LogicInfo newLogicInfo = d_logicInfo.getUnlockedCopy();
340 newLogicInfo.enableTheory(i);
341 newLogicInfo.lock();
342 std::stringstream ss;
343 ss << "The logic was specified as " << d_logicInfo.getLogicString()
344 << ", which doesn't include " << i
345 << ", but found a term in that theory." << std::endl
346 << "You might want to extend your logic to "
347 << newLogicInfo.getLogicString() << std::endl;
348 throw LogicException(ss.str());
349 }
350 }
351 }
352 }
353
354 // pre-register with the shared solver, which also handles
355 // calling prepregister on individual theories.
356 Assert(d_sharedSolver != nullptr);
357 d_sharedSolver->preRegisterShared(preprocessed, multipleTheories);
358 }
359
360 // Leaving pre-register
361 d_inPreregister = false;
362 }
363 }
364
365 void TheoryEngine::printAssertions(const char* tag) {
366 if (Trace.isOn(tag)) {
367
368 for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
369 Theory* theory = d_theoryTable[theoryId];
370 if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
371 Trace(tag) << "--------------------------------------------" << endl;
372 Trace(tag) << "Assertions of " << theory->getId() << ": " << endl;
373 {
374 context::CDList<Assertion>::const_iterator it = theory->facts_begin(),
375 it_end =
376 theory->facts_end();
377 for (unsigned i = 0; it != it_end; ++it, ++i)
378 {
379 if ((*it).d_isPreregistered)
380 {
381 Trace(tag) << "[" << i << "]: ";
382 }
383 else
384 {
385 Trace(tag) << "(" << i << "): ";
386 }
387 Trace(tag) << (*it).d_assertion << endl;
388 }
389 }
390
391 if (d_logicInfo.isSharingEnabled()) {
392 Trace(tag) << "Shared terms of " << theory->getId() << ": " << endl;
393 context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end();
394 for (unsigned i = 0; it != it_end; ++ it, ++i) {
395 Trace(tag) << "[" << i << "]: " << (*it) << endl;
396 }
397 }
398 }
399 }
400 }
401 }
402
403 void TheoryEngine::dumpAssertions(const char* tag) {
404 if (Dump.isOn(tag)) {
405 const Printer& printer = d_outMgr.getPrinter();
406 std::ostream& out = d_outMgr.getDumpOut();
407 printer.toStreamCmdComment(out, "Starting completeness check");
408 for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
409 Theory* theory = d_theoryTable[theoryId];
410 if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
411 printer.toStreamCmdComment(out, "Completeness check");
412 printer.toStreamCmdPush(out);
413
414 // Dump the shared terms
415 if (d_logicInfo.isSharingEnabled()) {
416 printer.toStreamCmdComment(out, "Shared terms");
417 context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end();
418 for (unsigned i = 0; it != it_end; ++ it, ++i) {
419 stringstream ss;
420 ss << (*it);
421 printer.toStreamCmdComment(out, ss.str());
422 }
423 }
424
425 // Dump the assertions
426 printer.toStreamCmdComment(out, "Assertions");
427 context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
428 for (; it != it_end; ++ it) {
429 // Get the assertion
430 Node assertionNode = (*it).d_assertion;
431 // Purify all the terms
432
433 if ((*it).d_isPreregistered)
434 {
435 printer.toStreamCmdComment(out, "Preregistered");
436 }
437 else
438 {
439 printer.toStreamCmdComment(out, "Shared assertion");
440 }
441 printer.toStreamCmdAssert(out, assertionNode);
442 }
443 printer.toStreamCmdCheckSat(out);
444
445 printer.toStreamCmdPop(out);
446 }
447 }
448 }
449 }
450
451 /**
452 * Check all (currently-active) theories for conflicts.
453 * @param effort the effort level to use
454 */
455 void TheoryEngine::check(Theory::Effort effort) {
456 // spendResource();
457
458 // Reset the interrupt flag
459 d_interrupted = false;
460
461 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
462 #undef CVC4_FOR_EACH_THEORY_STATEMENT
463 #endif
464 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
465 if (theory::TheoryTraits<THEORY>::hasCheck \
466 && d_logicInfo.isTheoryEnabled(THEORY)) \
467 { \
468 theoryOf(THEORY)->check(effort); \
469 if (d_inConflict) \
470 { \
471 Debug("conflict") << THEORY << " in conflict. " << std::endl; \
472 break; \
473 } \
474 }
475
476 // Do the checking
477 try {
478
479 // Mark the output channel unused (if this is FULL_EFFORT, and nothing
480 // is done by the theories, no additional check will be needed)
481 d_outputChannelUsed = false;
482
483 // Mark the lemmas flag (no lemmas added)
484 d_lemmasAdded = false;
485
486 Debug("theory") << "TheoryEngine::check(" << effort << "): d_factsAsserted = " << (d_factsAsserted ? "true" : "false") << endl;
487
488 // If in full effort, we have a fake new assertion just to jumpstart the checking
489 if (Theory::fullEffort(effort)) {
490 d_factsAsserted = true;
491 // Reset round for the relevance manager, which notice only sets a flag
492 // to indicate that its information must be recomputed.
493 if (d_relManager != nullptr)
494 {
495 d_relManager->resetRound();
496 }
497 d_tc->resetRound();
498 }
499
500 // Check until done
501 while (d_factsAsserted && !d_inConflict && !d_lemmasAdded) {
502
503 Debug("theory") << "TheoryEngine::check(" << effort << "): running check" << endl;
504
505 Trace("theory::assertions") << endl;
506 if (Trace.isOn("theory::assertions")) {
507 printAssertions("theory::assertions");
508 }
509
510 if(Theory::fullEffort(effort)) {
511 Trace("theory::assertions::fulleffort") << endl;
512 if (Trace.isOn("theory::assertions::fulleffort")) {
513 printAssertions("theory::assertions::fulleffort");
514 }
515 }
516
517 // Note that we've discharged all the facts
518 d_factsAsserted = false;
519
520 // Do the checking
521 CVC4_FOR_EACH_THEORY;
522
523 Debug("theory") << "TheoryEngine::check(" << effort << "): running propagation after the initial check" << endl;
524
525 // We are still satisfiable, propagate as much as possible
526 propagate(effort);
527
528 // We do combination if all has been processed and we are in fullcheck
529 if (Theory::fullEffort(effort) && d_logicInfo.isSharingEnabled() && !d_factsAsserted && !d_lemmasAdded && !d_inConflict) {
530 // Do the combination
531 Debug("theory") << "TheoryEngine::check(" << effort << "): running combination" << endl;
532 {
533 TimerStat::CodeTimer combineTheoriesTimer(d_combineTheoriesTime);
534 d_tc->combineTheories();
535 }
536 if(d_logicInfo.isQuantified()){
537 d_quantEngine->notifyCombineTheories();
538 }
539 }
540 }
541
542 // Must consult quantifiers theory for last call to ensure sat, or otherwise add a lemma
543 if( Theory::fullEffort(effort) && ! d_inConflict && ! needCheck() ) {
544 Trace("theory::assertions-model") << endl;
545 if (Trace.isOn("theory::assertions-model")) {
546 printAssertions("theory::assertions-model");
547 }
548 // reset the model in the combination engine
549 d_tc->resetModel();
550 //checks for theories requiring the model go at last call
551 for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
552 if( theoryId!=THEORY_QUANTIFIERS ){
553 Theory* theory = d_theoryTable[theoryId];
554 if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
555 if( theory->needsCheckLastEffort() ){
556 if (!d_tc->buildModel())
557 {
558 break;
559 }
560 theory->check(Theory::EFFORT_LAST_CALL);
561 }
562 }
563 }
564 }
565 if (!d_inConflict)
566 {
567 if(d_logicInfo.isQuantified()) {
568 // quantifiers engine must check at last call effort
569 d_quantEngine->check(Theory::EFFORT_LAST_CALL);
570 }
571 }
572 if (!d_inConflict && !needCheck())
573 {
574 // If d_eager_model_building is false, then we only mark that we
575 // are in "SAT mode". We build the model later only if the user asks
576 // for it via getBuiltModel.
577 d_inSatMode = true;
578 if (d_eager_model_building)
579 {
580 d_tc->buildModel();
581 }
582 }
583 }
584
585 Debug("theory") << "TheoryEngine::check(" << effort << "): done, we are " << (d_inConflict ? "unsat" : "sat") << (d_lemmasAdded ? " with new lemmas" : " with no new lemmas");
586 Debug("theory") << ", need check = " << (needCheck() ? "YES" : "NO") << endl;
587
588 if( Theory::fullEffort(effort) && !d_inConflict && !needCheck()) {
589 // Do post-processing of model from the theories (e.g. used for THEORY_SEP
590 // to construct heap model)
591 d_tc->postProcessModel(d_incomplete.get());
592 }
593 } catch(const theory::Interrupted&) {
594 Trace("theory") << "TheoryEngine::check() => interrupted" << endl;
595 }
596 // If fulleffort, check all theories
597 if(Dump.isOn("theory::fullcheck") && Theory::fullEffort(effort)) {
598 if (!d_inConflict && !needCheck()) {
599 dumpAssertions("theory::fullcheck");
600 }
601 }
602 }
603
604 void TheoryEngine::propagate(Theory::Effort effort)
605 {
606 // Reset the interrupt flag
607 d_interrupted = false;
608
609 // Definition of the statement that is to be run by every theory
610 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
611 #undef CVC4_FOR_EACH_THEORY_STATEMENT
612 #endif
613 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
614 if (theory::TheoryTraits<THEORY>::hasPropagate && d_logicInfo.isTheoryEnabled(THEORY)) { \
615 theoryOf(THEORY)->propagate(effort); \
616 }
617
618 // Reset the interrupt flag
619 d_interrupted = false;
620
621 // Propagate for each theory using the statement above
622 CVC4_FOR_EACH_THEORY;
623 }
624
625 Node TheoryEngine::getNextDecisionRequest()
626 {
627 return d_decManager->getNextDecisionRequest();
628 }
629
630 bool TheoryEngine::properConflict(TNode conflict) const {
631 bool value;
632 if (conflict.getKind() == kind::AND) {
633 for (unsigned i = 0; i < conflict.getNumChildren(); ++ i) {
634 if (! getPropEngine()->hasValue(conflict[i], value)) {
635 Debug("properConflict") << "Bad conflict is due to unassigned atom: "
636 << conflict[i] << endl;
637 return false;
638 }
639 if (! value) {
640 Debug("properConflict") << "Bad conflict is due to false atom: "
641 << conflict[i] << endl;
642 return false;
643 }
644 if (conflict[i] != Rewriter::rewrite(conflict[i])) {
645 Debug("properConflict") << "Bad conflict is due to atom not in normal form: "
646 << conflict[i] << " vs " << Rewriter::rewrite(conflict[i]) << endl;
647 return false;
648 }
649 }
650 } else {
651 if (! getPropEngine()->hasValue(conflict, value)) {
652 Debug("properConflict") << "Bad conflict is due to unassigned atom: "
653 << conflict << endl;
654 return false;
655 }
656 if(! value) {
657 Debug("properConflict") << "Bad conflict is due to false atom: "
658 << conflict << endl;
659 return false;
660 }
661 if (conflict != Rewriter::rewrite(conflict)) {
662 Debug("properConflict") << "Bad conflict is due to atom not in normal form: "
663 << conflict << " vs " << Rewriter::rewrite(conflict) << endl;
664 return false;
665 }
666 }
667 return true;
668 }
669
670 TheoryModel* TheoryEngine::getModel()
671 {
672 Assert(d_tc != nullptr);
673 TheoryModel* m = d_tc->getModel();
674 Assert(m != nullptr);
675 return m;
676 }
677
678 TheoryModel* TheoryEngine::getBuiltModel()
679 {
680 Assert(d_tc != nullptr);
681 // If this method was called, we should be in SAT mode, and produceModels
682 // should be true.
683 AlwaysAssert(options::produceModels());
684 if (!d_inSatMode)
685 {
686 // not available, perhaps due to interuption.
687 return nullptr;
688 }
689 // must build model at this point
690 if (!d_tc->buildModel())
691 {
692 return nullptr;
693 }
694 return d_tc->getModel();
695 }
696
697 bool TheoryEngine::buildModel()
698 {
699 Assert(d_tc != nullptr);
700 return d_tc->buildModel();
701 }
702
703 bool TheoryEngine::getSynthSolutions(
704 std::map<Node, std::map<Node, Node>>& sol_map)
705 {
706 if (d_quantEngine)
707 {
708 return d_quantEngine->getSynthSolutions(sol_map);
709 }
710 // we are not in a quantified logic, there is no synthesis solution
711 return false;
712 }
713
714 bool TheoryEngine::presolve() {
715 // Reset the interrupt flag
716 d_interrupted = false;
717
718 // Reset the decision manager. This clears its decision strategies that are
719 // no longer valid in this user context.
720 d_decManager->presolve();
721
722 try {
723 // Definition of the statement that is to be run by every theory
724 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
725 #undef CVC4_FOR_EACH_THEORY_STATEMENT
726 #endif
727 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
728 if (theory::TheoryTraits<THEORY>::hasPresolve) { \
729 theoryOf(THEORY)->presolve(); \
730 if(d_inConflict) { \
731 return true; \
732 } \
733 }
734
735 // Presolve for each theory using the statement above
736 CVC4_FOR_EACH_THEORY;
737 } catch(const theory::Interrupted&) {
738 Trace("theory") << "TheoryEngine::presolve() => interrupted" << endl;
739 }
740 // return whether we have a conflict
741 return false;
742 }/* TheoryEngine::presolve() */
743
744 void TheoryEngine::postsolve() {
745 // no longer in SAT mode
746 d_inSatMode = false;
747 // Reset the interrupt flag
748 d_interrupted = false;
749 bool CVC4_UNUSED wasInConflict = d_inConflict;
750
751 try {
752 // Definition of the statement that is to be run by every theory
753 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
754 #undef CVC4_FOR_EACH_THEORY_STATEMENT
755 #endif
756 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
757 if (theory::TheoryTraits<THEORY>::hasPostsolve) \
758 { \
759 theoryOf(THEORY)->postsolve(); \
760 Assert(!d_inConflict || wasInConflict) \
761 << "conflict raised during postsolve()"; \
762 }
763
764 // Postsolve for each theory using the statement above
765 CVC4_FOR_EACH_THEORY;
766 } catch(const theory::Interrupted&) {
767 Trace("theory") << "TheoryEngine::postsolve() => interrupted" << endl;
768 }
769 }/* TheoryEngine::postsolve() */
770
771
772 void TheoryEngine::notifyRestart() {
773 // Reset the interrupt flag
774 d_interrupted = false;
775
776 // Definition of the statement that is to be run by every theory
777 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
778 #undef CVC4_FOR_EACH_THEORY_STATEMENT
779 #endif
780 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
781 if (theory::TheoryTraits<THEORY>::hasNotifyRestart && d_logicInfo.isTheoryEnabled(THEORY)) { \
782 theoryOf(THEORY)->notifyRestart(); \
783 }
784
785 // notify each theory using the statement above
786 CVC4_FOR_EACH_THEORY;
787 }
788
789 void TheoryEngine::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
790 // Reset the interrupt flag
791 d_interrupted = false;
792
793 // Definition of the statement that is to be run by every theory
794 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
795 #undef CVC4_FOR_EACH_THEORY_STATEMENT
796 #endif
797 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
798 if (theory::TheoryTraits<THEORY>::hasPpStaticLearn) { \
799 theoryOf(THEORY)->ppStaticLearn(in, learned); \
800 }
801
802 // static learning for each theory using the statement above
803 CVC4_FOR_EACH_THEORY;
804 }
805
806 bool TheoryEngine::isRelevant(Node lit) const
807 {
808 if (d_relManager != nullptr)
809 {
810 return d_relManager->isRelevant(lit);
811 }
812 // otherwise must assume its relevant
813 return true;
814 }
815
816 void TheoryEngine::shutdown() {
817 // Set this first; if a Theory shutdown() throws an exception,
818 // at least the destruction of the TheoryEngine won't confound
819 // matters.
820 d_hasShutDown = true;
821
822 // Shutdown all the theories
823 for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) {
824 if(d_theoryTable[theoryId]) {
825 theoryOf(theoryId)->shutdown();
826 }
827 }
828 }
829
830 theory::Theory::PPAssertStatus TheoryEngine::solve(
831 TrustNode tliteral, TrustSubstitutionMap& substitutionOut)
832 {
833 // Reset the interrupt flag
834 d_interrupted = false;
835
836 TNode literal = tliteral.getNode();
837 TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
838 Trace("theory::solve") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl;
839
840 if(! d_logicInfo.isTheoryEnabled(Theory::theoryOf(atom)) &&
841 Theory::theoryOf(atom) != THEORY_SAT_SOLVER) {
842 stringstream ss;
843 ss << "The logic was specified as " << d_logicInfo.getLogicString()
844 << ", which doesn't include " << Theory::theoryOf(atom)
845 << ", but got a preprocessing-time fact for that theory." << endl
846 << "The fact:" << endl
847 << literal;
848 throw LogicException(ss.str());
849 }
850
851 Theory::PPAssertStatus solveStatus =
852 theoryOf(atom)->ppAssert(tliteral, substitutionOut);
853 Trace("theory::solve") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << endl;
854 return solveStatus;
855 }
856
857 TrustNode TheoryEngine::preprocess(TNode assertion)
858 {
859 return d_tpp.theoryPreprocess(assertion);
860 }
861
862 void TheoryEngine::notifyPreprocessedAssertions(
863 const std::vector<Node>& assertions) {
864 // call all the theories
865 for (TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST;
866 ++theoryId) {
867 if (d_theoryTable[theoryId]) {
868 theoryOf(theoryId)->ppNotifyAssertions(assertions);
869 }
870 }
871 if (d_relManager != nullptr)
872 {
873 d_relManager->notifyPreprocessedAssertions(assertions);
874 }
875 }
876
877 bool TheoryEngine::markPropagation(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) {
878
879 // What and where we are asserting
880 NodeTheoryPair toAssert(assertion, toTheoryId, d_propagationMapTimestamp);
881 // What and where it came from
882 NodeTheoryPair toExplain(originalAssertion, fromTheoryId, d_propagationMapTimestamp);
883
884 // See if the theory already got this literal
885 PropagationMap::const_iterator find = d_propagationMap.find(toAssert);
886 if (find != d_propagationMap.end()) {
887 // The theory already knows this
888 Trace("theory::assertToTheory") << "TheoryEngine::markPropagation(): already there" << endl;
889 return false;
890 }
891
892 Trace("theory::assertToTheory") << "TheoryEngine::markPropagation(): marking [" << d_propagationMapTimestamp << "] " << assertion << ", " << toTheoryId << " from " << originalAssertion << ", " << fromTheoryId << endl;
893
894 // Mark the propagation
895 d_propagationMap[toAssert] = toExplain;
896 d_propagationMapTimestamp = d_propagationMapTimestamp + 1;
897
898 return true;
899 }
900
901
902 void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) {
903
904 Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << originalAssertion << "," << toTheoryId << ", " << fromTheoryId << ")" << endl;
905
906 Assert(toTheoryId != fromTheoryId);
907 if(toTheoryId != THEORY_SAT_SOLVER &&
908 ! d_logicInfo.isTheoryEnabled(toTheoryId)) {
909 stringstream ss;
910 ss << "The logic was specified as " << d_logicInfo.getLogicString()
911 << ", which doesn't include " << toTheoryId
912 << ", but got an asserted fact to that theory." << endl
913 << "The fact:" << endl
914 << assertion;
915 throw LogicException(ss.str());
916 }
917
918 if (d_inConflict) {
919 return;
920 }
921
922 // If sharing is disabled, things are easy
923 if (!d_logicInfo.isSharingEnabled()) {
924 Assert(assertion == originalAssertion);
925 if (fromTheoryId == THEORY_SAT_SOLVER) {
926 // Send to the apropriate theory
927 theory::Theory* toTheory = theoryOf(toTheoryId);
928 // We assert it, and we know it's preregistereed
929 toTheory->assertFact(assertion, true);
930 // Mark that we have more information
931 d_factsAsserted = true;
932 } else {
933 Assert(toTheoryId == THEORY_SAT_SOLVER);
934 // Check for propositional conflict
935 bool value;
936 if (d_propEngine->hasValue(assertion, value)) {
937 if (!value) {
938 Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict (no sharing)" << endl;
939 Trace("dtview::conflict")
940 << ":THEORY-CONFLICT: " << assertion << std::endl;
941 d_inConflict = true;
942 } else {
943 return;
944 }
945 }
946 d_propagatedLiterals.push_back(assertion);
947 }
948 return;
949 }
950
951 // If sending to the shared terms database, it's also simple
952 if (toTheoryId == THEORY_BUILTIN) {
953 Assert(assertion.getKind() == kind::EQUAL
954 || (assertion.getKind() == kind::NOT
955 && assertion[0].getKind() == kind::EQUAL))
956 << "atom should be an EQUALity, not `" << assertion << "'";
957 if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
958 // assert to the shared solver
959 bool polarity = assertion.getKind() != kind::NOT;
960 TNode atom = polarity ? assertion : assertion[0];
961 d_sharedSolver->assertSharedEquality(atom, polarity, assertion);
962 }
963 return;
964 }
965
966 // Things from the SAT solver are already normalized, so they go
967 // directly to the apropriate theory
968 if (fromTheoryId == THEORY_SAT_SOLVER) {
969 // We know that this is normalized, so just send it off to the theory
970 if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
971 // Is it preregistered
972 bool preregistered = d_propEngine->isSatLiteral(assertion) && Theory::theoryOf(assertion) == toTheoryId;
973 // We assert it
974 theoryOf(toTheoryId)->assertFact(assertion, preregistered);
975 // Mark that we have more information
976 d_factsAsserted = true;
977 }
978 return;
979 }
980
981 // Propagations to the SAT solver are just enqueued for pickup by
982 // the SAT solver later
983 if (toTheoryId == THEORY_SAT_SOLVER) {
984 if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
985 // Enqueue for propagation to the SAT solver
986 d_propagatedLiterals.push_back(assertion);
987 // Check for propositional conflicts
988 bool value;
989 if (d_propEngine->hasValue(assertion, value) && !value) {
990 Trace("theory::propagate")
991 << "TheoryEngine::assertToTheory(" << assertion << ", "
992 << toTheoryId << ", " << fromTheoryId << "): conflict (sharing)"
993 << endl;
994 Trace("dtview::conflict")
995 << ":THEORY-CONFLICT: " << assertion << std::endl;
996 d_inConflict = true;
997 }
998 }
999 return;
1000 }
1001
1002 Assert(assertion.getKind() == kind::EQUAL
1003 || (assertion.getKind() == kind::NOT
1004 && assertion[0].getKind() == kind::EQUAL));
1005
1006 // Normalize
1007 Node normalizedLiteral = Rewriter::rewrite(assertion);
1008
1009 // See if it rewrites false directly -> conflict
1010 if (normalizedLiteral.isConst()) {
1011 if (!normalizedLiteral.getConst<bool>()) {
1012 // Mark the propagation for explanations
1013 if (markPropagation(normalizedLiteral, originalAssertion, toTheoryId, fromTheoryId)) {
1014 // special case, trust node has no proof generator
1015 TrustNode trnn = TrustNode::mkTrustConflict(normalizedLiteral);
1016 // Get the explanation (conflict will figure out where it came from)
1017 conflict(trnn, toTheoryId);
1018 } else {
1019 Unreachable();
1020 }
1021 return;
1022 }
1023 }
1024
1025 // Try and assert (note that we assert the non-normalized one)
1026 if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
1027 // Check if has been pre-registered with the theory
1028 bool preregistered = d_propEngine->isSatLiteral(assertion) && Theory::theoryOf(assertion) == toTheoryId;
1029 // Assert away
1030 theoryOf(toTheoryId)->assertFact(assertion, preregistered);
1031 d_factsAsserted = true;
1032 }
1033
1034 return;
1035 }
1036
1037 void TheoryEngine::assertFact(TNode literal)
1038 {
1039 Trace("theory") << "TheoryEngine::assertFact(" << literal << ")" << endl;
1040
1041 // spendResource();
1042
1043 // If we're in conflict, nothing to do
1044 if (d_inConflict) {
1045 return;
1046 }
1047
1048 // Get the atom
1049 bool polarity = literal.getKind() != kind::NOT;
1050 TNode atom = polarity ? literal : literal[0];
1051
1052 if (d_logicInfo.isSharingEnabled()) {
1053 // If any shared terms, it's time to do sharing work
1054 d_sharedSolver->preNotifySharedFact(atom);
1055
1056 // If it's an equality, assert it to the shared term manager, even though the terms are not
1057 // yet shared. As the terms become shared later, the shared terms manager will then add them
1058 // to the assert the equality to the interested theories
1059 if (atom.getKind() == kind::EQUAL) {
1060 // Assert it to the the owning theory
1061 assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
1062 // Shared terms manager will assert to interested theories directly, as
1063 // the terms become shared
1064 assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ THEORY_SAT_SOLVER);
1065
1066 // Now, let's check for any atom triggers from lemmas
1067 AtomRequests::atom_iterator it = d_atomRequests.getAtomIterator(atom);
1068 while (!it.done()) {
1069 const AtomRequests::Request& request = it.get();
1070 Node toAssert =
1071 polarity ? (Node)request.d_atom : request.d_atom.notNode();
1072 Debug("theory::atoms") << "TheoryEngine::assertFact(" << literal << "): sending requested " << toAssert << endl;
1073 assertToTheory(
1074 toAssert, literal, request.d_toTheory, THEORY_SAT_SOLVER);
1075 it.next();
1076 }
1077
1078 } else {
1079 // Not an equality, just assert to the appropriate theory
1080 assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
1081 }
1082 } else {
1083 // Assert the fact to the appropriate theory directly
1084 assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
1085 }
1086 }
1087
1088 bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
1089 Debug("theory::propagate") << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << endl;
1090
1091 Trace("dtview::prop") << std::string(d_context->getLevel(), ' ')
1092 << ":THEORY-PROP: " << literal << endl;
1093
1094 // spendResource();
1095
1096 // Get the atom
1097 bool polarity = literal.getKind() != kind::NOT;
1098 TNode atom = polarity ? literal : literal[0];
1099
1100 if (d_logicInfo.isSharingEnabled() && atom.getKind() == kind::EQUAL) {
1101 if (d_propEngine->isSatLiteral(literal)) {
1102 // We propagate SAT literals to SAT
1103 assertToTheory(literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory);
1104 }
1105 if (theory != THEORY_BUILTIN) {
1106 // Assert to the shared terms database
1107 assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ theory);
1108 }
1109 } else {
1110 // Just send off to the SAT solver
1111 Assert(d_propEngine->isSatLiteral(literal));
1112 assertToTheory(literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory);
1113 }
1114
1115 return !d_inConflict;
1116 }
1117
1118 const LogicInfo& TheoryEngine::getLogicInfo() const { return d_logicInfo; }
1119
1120 bool TheoryEngine::getSepHeapTypes(TypeNode& locType, TypeNode& dataType) const
1121 {
1122 if (d_sepLocType.isNull())
1123 {
1124 return false;
1125 }
1126 locType = d_sepLocType;
1127 dataType = d_sepDataType;
1128 return true;
1129 }
1130
1131 void TheoryEngine::declareSepHeap(TypeNode locT, TypeNode dataT)
1132 {
1133 Theory* tsep = theoryOf(THEORY_SEP);
1134 if (tsep == nullptr)
1135 {
1136 Assert(false) << "TheoryEngine::declareSepHeap called without the "
1137 "separation logic theory enabled";
1138 return;
1139 }
1140
1141 // Definition of the statement that is to be run by every theory
1142 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
1143 #undef CVC4_FOR_EACH_THEORY_STATEMENT
1144 #endif
1145 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
1146 theoryOf(THEORY)->declareSepHeap(locT, dataT);
1147
1148 // notify each theory using the statement above
1149 CVC4_FOR_EACH_THEORY;
1150
1151 // remember the types we have set
1152 d_sepLocType = locT;
1153 d_sepDataType = dataT;
1154 }
1155
1156 theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
1157 Assert(a.getType().isComparableTo(b.getType()));
1158 return d_sharedSolver->getEqualityStatus(a, b);
1159 }
1160
1161 Node TheoryEngine::getModelValue(TNode var) {
1162 if (var.isConst())
1163 {
1164 // the model value of a constant must be itself
1165 return var;
1166 }
1167 Assert(d_sharedSolver->isShared(var));
1168 return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var);
1169 }
1170
1171
1172 Node TheoryEngine::ensureLiteral(TNode n) {
1173 Trace("ensureLiteral") << "ensureLiteral rewriting: " << n << std::endl;
1174 Node rewritten = Rewriter::rewrite(n);
1175 Trace("ensureLiteral") << " got: " << rewritten << std::endl;
1176 std::vector<TrustNode> newLemmas;
1177 std::vector<Node> newSkolems;
1178 TrustNode tpn = d_tpp.preprocess(n, newLemmas, newSkolems, true);
1179 // send lemmas corresponding to the skolems introduced by preprocessing n
1180 for (const TrustNode& tnl : newLemmas)
1181 {
1182 Trace("ensureLiteral") << " lemma: " << tnl.getNode() << std::endl;
1183 lemma(tnl, LemmaProperty::NONE);
1184 }
1185 Node preprocessed = tpn.isNull() ? rewritten : tpn.getNode();
1186 Trace("ensureLiteral") << "ensureLiteral preprocessed: " << preprocessed
1187 << std::endl;
1188 d_propEngine->ensureLiteral(preprocessed);
1189 return preprocessed;
1190 }
1191
1192
1193 void TheoryEngine::printInstantiations( std::ostream& out ) {
1194 if( d_quantEngine ){
1195 d_quantEngine->printInstantiations( out );
1196 }else{
1197 out << "Internal error : instantiations not available when quantifiers are not present." << std::endl;
1198 Assert(false);
1199 }
1200 }
1201
1202 void TheoryEngine::printSynthSolution( std::ostream& out ) {
1203 if( d_quantEngine ){
1204 d_quantEngine->printSynthSolution( out );
1205 }else{
1206 out << "Internal error : synth solution not available when quantifiers are not present." << std::endl;
1207 Assert(false);
1208 }
1209 }
1210
1211 void TheoryEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) {
1212 if( d_quantEngine ){
1213 d_quantEngine->getInstantiatedQuantifiedFormulas( qs );
1214 }else{
1215 Assert(false);
1216 }
1217 }
1218
1219 void TheoryEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
1220 if( d_quantEngine ){
1221 d_quantEngine->getInstantiationTermVectors( q, tvecs );
1222 }else{
1223 Assert(false);
1224 }
1225 }
1226
1227 void TheoryEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) {
1228 if( d_quantEngine ){
1229 d_quantEngine->getInstantiationTermVectors( insts );
1230 }else{
1231 Assert(false);
1232 }
1233 }
1234
1235 TrustNode TheoryEngine::getExplanation(TNode node)
1236 {
1237 Debug("theory::explain") << "TheoryEngine::getExplanation(" << node
1238 << "): current propagation index = "
1239 << d_propagationMapTimestamp << endl;
1240 bool polarity = node.getKind() != kind::NOT;
1241 TNode atom = polarity ? node : node[0];
1242
1243 // If we're not in shared mode, explanations are simple
1244 if (!d_logicInfo.isSharingEnabled())
1245 {
1246 Debug("theory::explain")
1247 << "TheoryEngine::getExplanation: sharing is NOT enabled. "
1248 << " Responsible theory is: " << theoryOf(atom)->getId() << std::endl;
1249
1250 TrustNode texplanation = theoryOf(atom)->explain(node);
1251 Node explanation = texplanation.getNode();
1252 Debug("theory::explain") << "TheoryEngine::getExplanation(" << node
1253 << ") => " << explanation << endl;
1254 if (isProofEnabled())
1255 {
1256 texplanation.debugCheckClosed(
1257 "te-proof-exp", "texplanation no share", false);
1258 // check if no generator, if so, add THEORY_LEMMA
1259 if (texplanation.getGenerator() == nullptr)
1260 {
1261 Node proven = texplanation.getProven();
1262 TheoryId tid = theoryOf(atom)->getId();
1263 Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(tid);
1264 d_lazyProof->addStep(proven, PfRule::THEORY_LEMMA, {}, {proven, tidn});
1265 texplanation =
1266 TrustNode::mkTrustPropExp(node, explanation, d_lazyProof.get());
1267 }
1268 }
1269 return texplanation;
1270 }
1271
1272 Debug("theory::explain") << "TheoryEngine::getExplanation: sharing IS enabled"
1273 << std::endl;
1274
1275 // Initial thing to explain
1276 NodeTheoryPair toExplain(node, THEORY_SAT_SOLVER, d_propagationMapTimestamp);
1277 Assert(d_propagationMap.find(toExplain) != d_propagationMap.end());
1278
1279 NodeTheoryPair nodeExplainerPair = d_propagationMap[toExplain];
1280 Debug("theory::explain")
1281 << "TheoryEngine::getExplanation: explainer for node "
1282 << nodeExplainerPair.d_node
1283 << " is theory: " << nodeExplainerPair.d_theory << std::endl;
1284
1285 // Create the workplace for explanations
1286 std::vector<NodeTheoryPair> vec{d_propagationMap[toExplain]};
1287 // Process the explanation
1288 TrustNode texplanation = getExplanation(vec);
1289 Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => "
1290 << texplanation.getNode() << endl;
1291 return texplanation;
1292 }
1293
1294 struct AtomsCollect {
1295
1296 std::vector<TNode> d_atoms;
1297 std::unordered_set<TNode, TNodeHashFunction> d_visited;
1298
1299 public:
1300
1301 typedef void return_type;
1302
1303 bool alreadyVisited(TNode current, TNode parent) {
1304 // Check if already visited
1305 if (d_visited.find(current) != d_visited.end()) return true;
1306 // Don't visit non-boolean
1307 if (!current.getType().isBoolean()) return true;
1308 // New node
1309 return false;
1310 }
1311
1312 void visit(TNode current, TNode parent) {
1313 if (Theory::theoryOf(current) != theory::THEORY_BOOL) {
1314 d_atoms.push_back(current);
1315 }
1316 d_visited.insert(current);
1317 }
1318
1319 void start(TNode node) {}
1320 void done(TNode node) {}
1321
1322 std::vector<TNode> getAtoms() const {
1323 return d_atoms;
1324 }
1325 };
1326
1327 void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId atomsTo) {
1328 for (unsigned i = 0; i < atoms.size(); ++ i) {
1329
1330 // Non-equality atoms are either owned by theory or they don't make sense
1331 if (atoms[i].getKind() != kind::EQUAL) {
1332 continue;
1333 }
1334
1335 // The equality
1336 Node eq = atoms[i];
1337 // Simple normalization to not repeat stuff
1338 if (eq[0] > eq[1]) {
1339 eq = eq[1].eqNode(eq[0]);
1340 }
1341
1342 // Rewrite the equality
1343 Node eqNormalized = Rewriter::rewrite(atoms[i]);
1344
1345 Debug("theory::atoms") << "TheoryEngine::ensureLemmaAtoms(): " << eq << " with nf " << eqNormalized << endl;
1346
1347 // If the equality is a boolean constant, we send immediately
1348 if (eqNormalized.isConst()) {
1349 if (eqNormalized.getConst<bool>()) {
1350 assertToTheory(eq, eqNormalized, /** to */ atomsTo, /** Sat solver */ theory::THEORY_SAT_SOLVER);
1351 } else {
1352 assertToTheory(eq.notNode(), eqNormalized.notNode(), /** to */ atomsTo, /** Sat solver */ theory::THEORY_SAT_SOLVER);
1353 }
1354 continue;
1355 }else if( eqNormalized.getKind() != kind::EQUAL){
1356 Assert(eqNormalized.getKind() == kind::BOOLEAN_TERM_VARIABLE
1357 || (eqNormalized.getKind() == kind::NOT
1358 && eqNormalized[0].getKind() == kind::BOOLEAN_TERM_VARIABLE));
1359 // this happens for Boolean term equalities V = true that are rewritten to V, we should skip
1360 // TODO : revisit this
1361 continue;
1362 }
1363
1364 // If the normalization did the just flips, keep the flip
1365 if (eqNormalized[0] == eq[1] && eqNormalized[1] == eq[0]) {
1366 eq = eqNormalized;
1367 }
1368
1369 // Check if the equality is already known by the sat solver
1370 if (d_propEngine->isSatLiteral(eqNormalized)) {
1371 bool value;
1372 if (d_propEngine->hasValue(eqNormalized, value)) {
1373 if (value) {
1374 assertToTheory(eq, eqNormalized, atomsTo, theory::THEORY_SAT_SOLVER);
1375 continue;
1376 } else {
1377 assertToTheory(eq.notNode(), eqNormalized.notNode(), atomsTo, theory::THEORY_SAT_SOLVER);
1378 continue;
1379 }
1380 }
1381 }
1382
1383 // If the theory is asking about a different form, or the form is ok but if will go to a different theory
1384 // then we must figure it out
1385 if (eqNormalized != eq || Theory::theoryOf(eq) != atomsTo) {
1386 // If you get eqNormalized, send atoms[i] to atomsTo
1387 d_atomRequests.add(eqNormalized, eq, atomsTo);
1388 }
1389 }
1390 }
1391
1392 theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma,
1393 theory::LemmaProperty p,
1394 theory::TheoryId atomsTo,
1395 theory::TheoryId from)
1396 {
1397 // For resource-limiting (also does a time check).
1398 // spendResource();
1399 Assert(tlemma.getKind() == TrustNodeKind::LEMMA
1400 || tlemma.getKind() == TrustNodeKind::CONFLICT);
1401 // get the node
1402 Node node = tlemma.getNode();
1403 Node lemma = tlemma.getProven();
1404 Trace("te-lemma") << "Lemma, input: " << lemma << std::endl;
1405
1406 Assert(!expr::hasFreeVar(lemma));
1407
1408 // when proofs are enabled, we ensure the trust node has a generator by
1409 // adding a trust step to the lazy proof maintained by this class
1410 if (isProofEnabled())
1411 {
1412 // ensure proof: set THEORY_LEMMA if no generator is provided
1413 if (tlemma.getGenerator() == nullptr)
1414 {
1415 // internal lemmas should have generators
1416 Assert(from != THEORY_LAST);
1417 // add theory lemma step to proof
1418 Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(from);
1419 d_lazyProof->addStep(lemma, PfRule::THEORY_LEMMA, {}, {lemma, tidn});
1420 // update the trust node
1421 tlemma = TrustNode::mkTrustLemma(lemma, d_lazyProof.get());
1422 }
1423 // ensure closed
1424 tlemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_initial");
1425 }
1426
1427 // Do we need to check atoms
1428 if (atomsTo != theory::THEORY_LAST) {
1429 Debug("theory::atoms") << "TheoryEngine::lemma(" << node << ", " << atomsTo << ")" << endl;
1430 AtomsCollect collectAtoms;
1431 NodeVisitor<AtomsCollect>::run(collectAtoms, node);
1432 ensureLemmaAtoms(collectAtoms.getAtoms(), atomsTo);
1433 }
1434
1435 if(Dump.isOn("t-lemmas")) {
1436 // we dump the negation of the lemma, to show validity of the lemma
1437 Node n = lemma.negate();
1438 const Printer& printer = d_outMgr.getPrinter();
1439 std::ostream& out = d_outMgr.getDumpOut();
1440 printer.toStreamCmdComment(out, "theory lemma: expect valid");
1441 printer.toStreamCmdCheckSat(out, n);
1442 }
1443 bool removable = isLemmaPropertyRemovable(p);
1444 bool preprocess = isLemmaPropertyPreprocess(p);
1445
1446 // ensure closed
1447 tlemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_initial");
1448
1449 // call preprocessor
1450 std::vector<TrustNode> newLemmas;
1451 std::vector<Node> newSkolems;
1452 TrustNode tplemma =
1453 d_tpp.preprocess(lemma, newLemmas, newSkolems, preprocess);
1454 // the preprocessed lemma
1455 Node lemmap;
1456 if (tplemma.isNull())
1457 {
1458 lemmap = lemma;
1459 }
1460 else
1461 {
1462 Assert(tplemma.getKind() == TrustNodeKind::REWRITE);
1463 lemmap = tplemma.getNode();
1464
1465 // must update the trust lemma
1466 if (lemmap != lemma)
1467 {
1468 // process the preprocessing
1469 if (isProofEnabled())
1470 {
1471 Assert(d_lazyProof != nullptr);
1472 // add the original proof to the lazy proof
1473 d_lazyProof->addLazyStep(tlemma.getProven(), tlemma.getGenerator());
1474 // only need to do anything if lemmap changed in a non-trivial way
1475 if (!CDProof::isSame(lemmap, lemma))
1476 {
1477 d_lazyProof->addLazyStep(tplemma.getProven(),
1478 tplemma.getGenerator(),
1479 PfRule::PREPROCESS_LEMMA,
1480 true,
1481 "TheoryEngine::lemma_pp");
1482 // ---------- from d_lazyProof -------------- from theory preprocess
1483 // lemma lemma = lemmap
1484 // ------------------------------------------ EQ_RESOLVE
1485 // lemmap
1486 std::vector<Node> pfChildren;
1487 pfChildren.push_back(lemma);
1488 pfChildren.push_back(tplemma.getProven());
1489 d_lazyProof->addStep(lemmap, PfRule::EQ_RESOLVE, pfChildren, {});
1490 }
1491 }
1492 tlemma = TrustNode::mkTrustLemma(lemmap, d_lazyProof.get());
1493 }
1494 }
1495
1496 // must use an assertion pipeline due to decision engine below
1497 AssertionPipeline lemmas;
1498 // make the assertion pipeline
1499 lemmas.push_back(lemmap);
1500 lemmas.updateRealAssertionsEnd();
1501 Assert(newSkolems.size() == newLemmas.size());
1502 for (size_t i = 0, nsize = newLemmas.size(); i < nsize; i++)
1503 {
1504 // store skolem mapping here
1505 IteSkolemMap& imap = lemmas.getIteSkolemMap();
1506 imap[newSkolems[i]] = lemmas.size();
1507 lemmas.push_back(newLemmas[i].getNode());
1508 }
1509
1510 // If specified, we must add this lemma to the set of those that need to be
1511 // justified, where note we pass all auxiliary lemmas in lemmas, since these
1512 // by extension must be justified as well.
1513 if (d_relManager != nullptr && isLemmaPropertyNeedsJustify(p))
1514 {
1515 d_relManager->notifyPreprocessedAssertions(lemmas.ref());
1516 }
1517
1518 // do final checks on the lemmas we are about to send
1519 if (isProofEnabled())
1520 {
1521 Assert(tlemma.getGenerator() != nullptr);
1522 // ensure closed, make the proof node eagerly here to debug
1523 tlemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma");
1524 for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i)
1525 {
1526 Assert(newLemmas[i].getGenerator() != nullptr);
1527 newLemmas[i].debugCheckClosed("te-proof-debug",
1528 "TheoryEngine::lemma_new");
1529 }
1530 }
1531
1532 // now, send the lemmas to the prop engine
1533 Trace("te-lemma") << "Lemma, output: " << tlemma.getProven() << std::endl;
1534 d_propEngine->assertLemma(tlemma.getProven(), false, removable);
1535 for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i)
1536 {
1537 Trace("te-lemma") << "Lemma, new lemma: " << newLemmas[i].getProven()
1538 << std::endl;
1539 d_propEngine->assertLemma(newLemmas[i].getProven(), false, removable);
1540 }
1541
1542 // assert to decision engine
1543 if (!removable)
1544 {
1545 d_propEngine->addAssertionsToDecisionEngine(lemmas);
1546 }
1547
1548 // Mark that we added some lemmas
1549 d_lemmasAdded = true;
1550
1551 // Lemma analysis isn't online yet; this lemma may only live for this
1552 // user level.
1553 Node retLemma = lemmas[0];
1554 if (lemmas.size() > 1)
1555 {
1556 // the returned lemma is the conjunction of all additional lemmas.
1557 retLemma = NodeManager::currentNM()->mkNode(kind::AND, lemmas.ref());
1558 }
1559 return theory::LemmaStatus(retLemma, d_userContext->getLevel());
1560 }
1561
1562 void TheoryEngine::conflict(theory::TrustNode tconflict, TheoryId theoryId)
1563 {
1564 Assert(tconflict.getKind() == TrustNodeKind::CONFLICT);
1565 TNode conflict = tconflict.getNode();
1566 Trace("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", "
1567 << theoryId << ")" << endl;
1568 Trace("te-proof-debug") << "Check closed conflict" << std::endl;
1569 // doesn't require proof generator, yet, since THEORY_LEMMA is added below
1570 tconflict.debugCheckClosed(
1571 "te-proof-debug", "TheoryEngine::conflict_initial", false);
1572
1573 Trace("dtview::conflict") << ":THEORY-CONFLICT: " << conflict << std::endl;
1574
1575 // Mark that we are in conflict
1576 d_inConflict = true;
1577
1578 if(Dump.isOn("t-conflicts")) {
1579 const Printer& printer = d_outMgr.getPrinter();
1580 std::ostream& out = d_outMgr.getDumpOut();
1581 printer.toStreamCmdComment(out, "theory conflict: expect unsat");
1582 printer.toStreamCmdCheckSat(out, conflict);
1583 }
1584
1585 // In the multiple-theories case, we need to reconstruct the conflict
1586 if (d_logicInfo.isSharingEnabled()) {
1587 // Create the workplace for explanations
1588 std::vector<NodeTheoryPair> vec;
1589 vec.push_back(
1590 NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp));
1591
1592 // Process the explanation
1593 TrustNode tncExp = getExplanation(vec);
1594 Trace("te-proof-debug")
1595 << "Check closed conflict explained with sharing" << std::endl;
1596 tncExp.debugCheckClosed("te-proof-debug",
1597 "TheoryEngine::conflict_explained_sharing");
1598 Node fullConflict = tncExp.getNode();
1599
1600 if (isProofEnabled())
1601 {
1602 Trace("te-proof-debug") << "Process conflict: " << conflict << std::endl;
1603 Trace("te-proof-debug") << "Conflict " << tconflict << " from "
1604 << tconflict.identifyGenerator() << std::endl;
1605 Trace("te-proof-debug") << "Explanation " << tncExp << " from "
1606 << tncExp.identifyGenerator() << std::endl;
1607 Assert(d_lazyProof != nullptr);
1608 if (tconflict.getGenerator() != nullptr)
1609 {
1610 d_lazyProof->addLazyStep(tconflict.getProven(),
1611 tconflict.getGenerator());
1612 }
1613 else
1614 {
1615 // add theory lemma step
1616 Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId);
1617 Node conf = tconflict.getProven();
1618 d_lazyProof->addStep(conf, PfRule::THEORY_LEMMA, {}, {conf, tidn});
1619 }
1620 // store the explicit step, which should come from a different
1621 // generator, e.g. d_tepg.
1622 Node proven = tncExp.getProven();
1623 Assert(tncExp.getGenerator() != d_lazyProof.get());
1624 Trace("te-proof-debug") << "add lazy step " << tncExp.identifyGenerator()
1625 << " for " << proven << std::endl;
1626 d_lazyProof->addLazyStep(proven, tncExp.getGenerator());
1627 pfgEnsureClosed(proven,
1628 d_lazyProof.get(),
1629 "te-proof-debug",
1630 "TheoryEngine::conflict_during");
1631 Node fullConflictNeg = fullConflict.notNode();
1632 std::vector<Node> children;
1633 children.push_back(proven);
1634 std::vector<Node> args;
1635 args.push_back(fullConflictNeg);
1636 if (conflict == d_false)
1637 {
1638 AlwaysAssert(proven == fullConflictNeg);
1639 }
1640 else
1641 {
1642 if (fullConflict != conflict)
1643 {
1644 // ------------------------- explained ---------- from theory
1645 // fullConflict => conflict ~conflict
1646 // ------------------------------------------ MACRO_SR_PRED_TRANSFORM
1647 // ~fullConflict
1648 children.push_back(conflict.notNode());
1649 args.push_back(mkMethodId(MethodId::SB_LITERAL));
1650 d_lazyProof->addStep(
1651 fullConflictNeg, PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
1652 }
1653 }
1654 }
1655 // pass the processed trust node
1656 TrustNode tconf =
1657 TrustNode::mkTrustConflict(fullConflict, d_lazyProof.get());
1658 Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl;
1659 Assert(properConflict(fullConflict));
1660 Trace("te-proof-debug")
1661 << "Check closed conflict with sharing" << std::endl;
1662 tconf.debugCheckClosed("te-proof-debug", "TheoryEngine::conflict:sharing");
1663 lemma(tconf, LemmaProperty::REMOVABLE);
1664 } else {
1665 // When only one theory, the conflict should need no processing
1666 Assert(properConflict(conflict));
1667 // pass the trust node that was sent from the theory
1668 lemma(tconflict, LemmaProperty::REMOVABLE, THEORY_LAST, theoryId);
1669 }
1670 }
1671
1672 theory::TrustNode TheoryEngine::getExplanation(
1673 std::vector<NodeTheoryPair>& explanationVector)
1674 {
1675 Assert(explanationVector.size() == 1);
1676 Node conclusion = explanationVector[0].d_node;
1677 std::shared_ptr<LazyCDProof> lcp;
1678 if (isProofEnabled())
1679 {
1680 Trace("te-proof-exp") << "=== TheoryEngine::getExplanation " << conclusion
1681 << std::endl;
1682 lcp.reset(new LazyCDProof(
1683 d_pnm, nullptr, nullptr, "TheoryEngine::LazyCDProof::getExplanation"));
1684 }
1685 unsigned i = 0; // Index of the current literal we are processing
1686
1687 std::unique_ptr<std::set<Node>> inputAssertions = nullptr;
1688 // the overall explanation
1689 std::set<TNode> exp;
1690 // vector of trust nodes to explain at the end
1691 std::vector<std::pair<TheoryId, TrustNode>> texplains;
1692 // cache of nodes we have already explained by some theory
1693 std::unordered_map<Node, size_t, NodeHashFunction> cache;
1694
1695 while (i < explanationVector.size()) {
1696 // Get the current literal to explain
1697 NodeTheoryPair toExplain = explanationVector[i];
1698
1699 Debug("theory::explain")
1700 << "[i=" << i << "] TheoryEngine::explain(): processing ["
1701 << toExplain.d_timestamp << "] " << toExplain.d_node << " sent from "
1702 << toExplain.d_theory << endl;
1703
1704 if (cache.find(toExplain.d_node) != cache.end()
1705 && cache[toExplain.d_node] < toExplain.d_timestamp)
1706 {
1707 ++i;
1708 continue;
1709 }
1710 cache[toExplain.d_node] = toExplain.d_timestamp;
1711
1712 // If a true constant or a negation of a false constant we can ignore it
1713 if ((toExplain.d_node.isConst() && toExplain.d_node.getConst<bool>())
1714 || (toExplain.d_node.getKind() == kind::NOT
1715 && toExplain.d_node[0].isConst()
1716 && !toExplain.d_node[0].getConst<bool>()))
1717 {
1718 ++ i;
1719 // if we are building a proof
1720 if (lcp != nullptr)
1721 {
1722 Trace("te-proof-exp")
1723 << "- explain " << toExplain.d_node << " trivially..." << std::endl;
1724 // ------------------MACRO_SR_PRED_INTRO
1725 // toExplain.d_node
1726 std::vector<Node> children;
1727 std::vector<Node> args;
1728 args.push_back(toExplain.d_node);
1729 lcp->addStep(
1730 toExplain.d_node, PfRule::MACRO_SR_PRED_INTRO, children, args);
1731 }
1732 continue;
1733 }
1734
1735 // If from the SAT solver, keep it
1736 if (toExplain.d_theory == THEORY_SAT_SOLVER)
1737 {
1738 Debug("theory::explain") << "\tLiteral came from THEORY_SAT_SOLVER. Kepping it." << endl;
1739 exp.insert(explanationVector[i++].d_node);
1740 // it will be a free assumption in the proof
1741 Trace("te-proof-exp") << "- keep " << toExplain.d_node << std::endl;
1742 continue;
1743 }
1744
1745 // If an and, expand it
1746 if (toExplain.d_node.getKind() == kind::AND)
1747 {
1748 Debug("theory::explain")
1749 << "TheoryEngine::explain(): expanding " << toExplain.d_node
1750 << " got from " << toExplain.d_theory << endl;
1751 size_t nchild = toExplain.d_node.getNumChildren();
1752 for (size_t k = 0; k < nchild; ++k)
1753 {
1754 NodeTheoryPair newExplain(
1755 toExplain.d_node[k], toExplain.d_theory, toExplain.d_timestamp);
1756 explanationVector.push_back(newExplain);
1757 }
1758 if (lcp != nullptr)
1759 {
1760 Trace("te-proof-exp")
1761 << "- AND expand " << toExplain.d_node << std::endl;
1762 // delay explanation, use a dummy trust node
1763 TrustNode tnAndExp = TrustNode::mkTrustPropExp(
1764 toExplain.d_node, toExplain.d_node, nullptr);
1765 texplains.push_back(
1766 std::pair<TheoryId, TrustNode>(THEORY_LAST, tnAndExp));
1767 }
1768 ++ i;
1769 continue;
1770 }
1771
1772 // See if it was sent to the theory by another theory
1773 PropagationMap::const_iterator find = d_propagationMap.find(toExplain);
1774 if (find != d_propagationMap.end()) {
1775 Debug("theory::explain")
1776 << "\tTerm was propagated by another theory (theory = "
1777 << getTheoryString((*find).second.d_theory) << ")" << std::endl;
1778 // There is some propagation, check if its a timely one
1779 if ((*find).second.d_timestamp < toExplain.d_timestamp)
1780 {
1781 Debug("theory::explain")
1782 << "\tRelevant timetsamp, pushing " << (*find).second.d_node
1783 << "to index = " << explanationVector.size() << std::endl;
1784 explanationVector.push_back((*find).second);
1785 ++i;
1786
1787 if (lcp != nullptr)
1788 {
1789 if (!CDProof::isSame(toExplain.d_node, (*find).second.d_node))
1790 {
1791 Trace("te-proof-exp")
1792 << "- t-explained cached: " << toExplain.d_node << " by "
1793 << (*find).second.d_node << std::endl;
1794 // delay explanation, use a dummy trust node that says that
1795 // (*find).second.d_node explains toExplain.d_node.
1796 TrustNode tnRewExp = TrustNode::mkTrustPropExp(
1797 toExplain.d_node, (*find).second.d_node, nullptr);
1798 texplains.push_back(
1799 std::pair<TheoryId, TrustNode>(THEORY_LAST, tnRewExp));
1800 }
1801 }
1802 continue;
1803 }
1804 }
1805 // It was produced by the theory, so ask for an explanation
1806 TrustNode texplanation =
1807 d_sharedSolver->explain(toExplain.d_node, toExplain.d_theory);
1808 if (lcp != nullptr)
1809 {
1810 texplanation.debugCheckClosed("te-proof-exp", "texplanation", false);
1811 Trace("te-proof-exp")
1812 << "- t-explained[" << toExplain.d_theory << "]: " << toExplain.d_node
1813 << " by " << texplanation.getNode() << std::endl;
1814 // if not a trivial explanation
1815 if (!CDProof::isSame(texplanation.getNode(), toExplain.d_node))
1816 {
1817 // We add it to the list of theory explanations, to be processed at
1818 // the end of this method. We wait to explain here because it may
1819 // be that a later explanation may preempt the need for proving this
1820 // step. For instance, if the conclusion lit is later added as an
1821 // assumption in the final explanation. This avoids cyclic proofs.
1822 texplains.push_back(
1823 std::pair<TheoryId, TrustNode>(toExplain.d_theory, texplanation));
1824 }
1825 }
1826 Node explanation = texplanation.getNode();
1827
1828 Debug("theory::explain")
1829 << "TheoryEngine::explain(): got explanation " << explanation
1830 << " got from " << toExplain.d_theory << endl;
1831 Assert(explanation != toExplain.d_node)
1832 << "wasn't sent to you, so why are you explaining it trivially";
1833 // Mark the explanation
1834 NodeTheoryPair newExplain(
1835 explanation, toExplain.d_theory, toExplain.d_timestamp);
1836 explanationVector.push_back(newExplain);
1837
1838 ++ i;
1839 }
1840
1841 // make the explanation node
1842 Node expNode;
1843 if (exp.size() == 0)
1844 {
1845 // Normalize to true
1846 expNode = NodeManager::currentNM()->mkConst<bool>(true);
1847 }
1848 else if (exp.size() == 1)
1849 {
1850 // All the same, or just one
1851 expNode = *exp.begin();
1852 }
1853 else
1854 {
1855 NodeBuilder<> conjunction(kind::AND);
1856 std::set<TNode>::const_iterator it = exp.begin();
1857 std::set<TNode>::const_iterator it_end = exp.end();
1858 while (it != it_end)
1859 {
1860 conjunction << *it;
1861 ++it;
1862 }
1863 expNode = conjunction;
1864 }
1865 // if we are building a proof, go back through the explanations and
1866 // build the proof
1867 if (lcp != nullptr)
1868 {
1869 if (Trace.isOn("te-proof-exp"))
1870 {
1871 Trace("te-proof-exp") << "Explanation is:" << std::endl;
1872 for (const Node& e : exp)
1873 {
1874 Trace("te-proof-exp") << " " << e << std::endl;
1875 }
1876 Trace("te-proof-exp") << "=== Replay explanations..." << std::endl;
1877 }
1878 // Now, go back and add the necessary steps of theory explanations, i.e.
1879 // add those that prove things that aren't in the final explanation. We
1880 // iterate in reverse order so that most recent steps take priority. This
1881 // avoids cyclic proofs in the lazy proof we are building (lcp).
1882 for (std::vector<std::pair<TheoryId, TrustNode>>::reverse_iterator
1883 it = texplains.rbegin(),
1884 itEnd = texplains.rend();
1885 it != itEnd;
1886 ++it)
1887 {
1888 TrustNode trn = it->second;
1889 Assert(trn.getKind() == TrustNodeKind::PROP_EXP);
1890 Node proven = trn.getProven();
1891 Assert(proven.getKind() == kind::IMPLIES);
1892 Node tConc = proven[1];
1893 Trace("te-proof-exp") << "- Process " << trn << std::endl;
1894 if (exp.find(tConc) != exp.end())
1895 {
1896 // already added to proof
1897 Trace("te-proof-exp") << "...already added" << std::endl;
1898 continue;
1899 }
1900 Node symTConc = CDProof::getSymmFact(tConc);
1901 if (!symTConc.isNull())
1902 {
1903 if (exp.find(symTConc) != exp.end())
1904 {
1905 // symmetric direction
1906 Trace("te-proof-exp") << "...already added (SYMM)" << std::endl;
1907 continue;
1908 }
1909 }
1910 // remember that we've explained this formula, to avoid cycles in lcp
1911 exp.insert(tConc);
1912 TheoryId ttid = it->first;
1913 Node tExp = proven[0];
1914 if (ttid == THEORY_LAST)
1915 {
1916 if (tConc == tExp)
1917 {
1918 // dummy trust node, do AND expansion
1919 Assert(tConc.getKind() == kind::AND);
1920 // tConc[0] ... tConc[n]
1921 // ---------------------- AND_INTRO
1922 // tConc
1923 std::vector<Node> pfChildren;
1924 pfChildren.insert(pfChildren.end(), tConc.begin(), tConc.end());
1925 lcp->addStep(tConc, PfRule::AND_INTRO, pfChildren, {});
1926 Trace("te-proof-exp") << "...via AND_INTRO" << std::endl;
1927 continue;
1928 }
1929 // otherwise should hold by rewriting
1930 Assert(Rewriter::rewrite(tConc) == Rewriter::rewrite(tExp));
1931 // tExp
1932 // ---- MACRO_SR_PRED_TRANSFORM
1933 // tConc
1934 lcp->addStep(tConc, PfRule::MACRO_SR_PRED_TRANSFORM, {tExp}, {tConc});
1935 Trace("te-proof-exp") << "...via MACRO_SR_PRED_TRANSFORM" << std::endl;
1936 continue;
1937 }
1938 if (tExp == tConc)
1939 {
1940 // trivial
1941 Trace("te-proof-exp") << "...trivial" << std::endl;
1942 continue;
1943 }
1944 // ------------- Via theory
1945 // tExp tExp => tConc
1946 // ---------------------------------MODUS_PONENS
1947 // tConc
1948 if (trn.getGenerator() != nullptr)
1949 {
1950 Trace("te-proof-exp") << "...via theory generator" << std::endl;
1951 lcp->addLazyStep(proven, trn.getGenerator());
1952 }
1953 else
1954 {
1955 Trace("te-proof-exp") << "...via trust THEORY_LEMMA" << std::endl;
1956 // otherwise, trusted theory lemma
1957 Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(it->first);
1958 lcp->addStep(proven, PfRule::THEORY_LEMMA, {}, {proven, tidn});
1959 }
1960 std::vector<Node> pfChildren;
1961 pfChildren.push_back(trn.getNode());
1962 pfChildren.push_back(proven);
1963 lcp->addStep(tConc, PfRule::MODUS_PONENS, pfChildren, {});
1964 }
1965 // store in the proof generator
1966 TrustNode trn = d_tepg->mkTrustExplain(conclusion, expNode, lcp);
1967 // return the trust node
1968 return trn;
1969 }
1970
1971 return theory::TrustNode::mkTrustLemma(expNode, nullptr);
1972 }
1973
1974 bool TheoryEngine::isProofEnabled() const { return d_pnm != nullptr; }
1975
1976 void TheoryEngine::setUserAttribute(const std::string& attr,
1977 Node n,
1978 const std::vector<Node>& node_values,
1979 const std::string& str_value)
1980 {
1981 Trace("te-attr") << "set user attribute " << attr << " " << n << endl;
1982 if( d_attr_handle.find( attr )!=d_attr_handle.end() ){
1983 for( size_t i=0; i<d_attr_handle[attr].size(); i++ ){
1984 d_attr_handle[attr][i]->setUserAttribute(attr, n, node_values, str_value);
1985 }
1986 } else {
1987 //unhandled exception?
1988 }
1989 }
1990
1991 void TheoryEngine::handleUserAttribute(const char* attr, Theory* t) {
1992 Trace("te-attr") << "Handle user attribute " << attr << " " << t << endl;
1993 std::string str( attr );
1994 d_attr_handle[ str ].push_back( t );
1995 }
1996
1997 void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) {
1998 for(TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
1999 Theory* theory = d_theoryTable[theoryId];
2000 if(theory && d_logicInfo.isTheoryEnabled(theoryId)) {
2001 for(context::CDList<Assertion>::const_iterator it = theory->facts_begin(),
2002 it_end = theory->facts_end();
2003 it != it_end;
2004 ++it) {
2005 Node assertion = (*it).d_assertion;
2006 if (!isRelevant(assertion))
2007 {
2008 // not relevant, skip
2009 continue;
2010 }
2011 Node val = d_tc->getModel()->getValue(assertion);
2012 if (val != d_true)
2013 {
2014 std::stringstream ss;
2015 ss << " " << theoryId
2016 << " has an asserted fact that the model doesn't satisfy." << endl
2017 << "The fact: " << assertion << endl
2018 << "Model value: " << val << endl;
2019 if (hardFailure)
2020 {
2021 if (val == d_false)
2022 {
2023 // Always an error if it is false
2024 InternalError() << ss.str();
2025 }
2026 else
2027 {
2028 // Otherwise just a warning. Notice this case may happen for
2029 // assertions with unevaluable operators, e.g. transcendental
2030 // functions. It also may happen for separation logic, where
2031 // check-model support is limited.
2032 Warning() << ss.str();
2033 }
2034 }
2035 }
2036 }
2037 }
2038 }
2039 }
2040
2041 std::pair<bool, Node> TheoryEngine::entailmentCheck(options::TheoryOfMode mode,
2042 TNode lit)
2043 {
2044 TNode atom = (lit.getKind() == kind::NOT) ? lit[0] : lit;
2045 if( atom.getKind()==kind::AND || atom.getKind()==kind::OR || atom.getKind()==kind::IMPLIES ){
2046 //Boolean connective, recurse
2047 std::vector< Node > children;
2048 bool pol = (lit.getKind()!=kind::NOT);
2049 bool is_conjunction = pol==(lit.getKind()==kind::AND);
2050 for( unsigned i=0; i<atom.getNumChildren(); i++ ){
2051 Node ch = atom[i];
2052 if( pol==( lit.getKind()==kind::IMPLIES && i==0 ) ){
2053 ch = atom[i].negate();
2054 }
2055 std::pair<bool, Node> chres = entailmentCheck(mode, ch);
2056 if( chres.first ){
2057 if( !is_conjunction ){
2058 return chres;
2059 }else{
2060 children.push_back( chres.second );
2061 }
2062 }else if( !chres.first && is_conjunction ){
2063 return std::pair<bool, Node>(false, Node::null());
2064 }
2065 }
2066 if( is_conjunction ){
2067 return std::pair<bool, Node>(true, NodeManager::currentNM()->mkNode(kind::AND, children));
2068 }else{
2069 return std::pair<bool, Node>(false, Node::null());
2070 }
2071 }else if( atom.getKind()==kind::ITE || ( atom.getKind()==kind::EQUAL && atom[0].getType().isBoolean() ) ){
2072 bool pol = (lit.getKind()!=kind::NOT);
2073 for( unsigned r=0; r<2; r++ ){
2074 Node ch = atom[0];
2075 if( r==1 ){
2076 ch = ch.negate();
2077 }
2078 std::pair<bool, Node> chres = entailmentCheck(mode, ch);
2079 if( chres.first ){
2080 Node ch2 = atom[ atom.getKind()==kind::ITE ? r+1 : 1 ];
2081 if( pol==( atom.getKind()==kind::ITE ? true : r==1 ) ){
2082 ch2 = ch2.negate();
2083 }
2084 std::pair<bool, Node> chres2 = entailmentCheck(mode, ch2);
2085 if( chres2.first ){
2086 return std::pair<bool, Node>(true, NodeManager::currentNM()->mkNode(kind::AND, chres.second, chres2.second));
2087 }else{
2088 break;
2089 }
2090 }
2091 }
2092 return std::pair<bool, Node>(false, Node::null());
2093 }else{
2094 //it is a theory atom
2095 theory::TheoryId tid = theory::Theory::theoryOf(mode, atom);
2096 theory::Theory* th = theoryOf(tid);
2097
2098 Assert(th != NULL);
2099 Trace("theory-engine-entc") << "Entailment check : " << lit << std::endl;
2100
2101 std::pair<bool, Node> chres = th->entailmentCheck(lit);
2102 return chres;
2103 }
2104 }
2105
2106 void TheoryEngine::spendResource(ResourceManager::Resource r)
2107 {
2108 d_resourceManager->spendResource(r);
2109 }
2110
2111 }/* CVC4 namespace */