diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 91 |
1 files changed, 31 insertions, 60 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 7ff073cf3..b5167ffe4 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -31,6 +31,8 @@ #include "options/quantifiers_options.h" #include "options/theory_options.h" #include "preprocessing/assertion_pipeline.h" +#include "printer/printer.h" +#include "smt/dump.h" #include "smt/logic_exception.h" #include "smt/term_formula_removal.h" #include "theory/arith/arith_ite_utils.h" @@ -211,17 +213,18 @@ TheoryEngine::TheoryEngine(context::Context* context, context::UserContext* userContext, ResourceManager* rm, RemoveTermFormulas& iteRemover, - const LogicInfo& logicInfo) + const LogicInfo& logicInfo, + OutputManager& outMgr) : d_propEngine(nullptr), d_context(context), d_userContext(userContext), d_logicInfo(logicInfo), + d_outMgr(outMgr), d_pnm(nullptr), d_lazyProof( - d_pnm != nullptr - ? new LazyCDProof( - d_pnm, nullptr, d_userContext, "TheoryEngine::LazyCDProof") - : nullptr), + d_pnm != nullptr ? new LazyCDProof( + d_pnm, nullptr, d_userContext, "TheoryEngine::LazyCDProof") + : nullptr), d_tepg(new TheoryEngineProofGenerator(d_pnm, d_userContext)), d_sharedTerms(this, context), d_tc(nullptr), @@ -231,8 +234,6 @@ TheoryEngine::TheoryEngine(context::Context* context, d_preRegistrationVisitor(this, context), d_sharedTermsVisitor(d_sharedTerms), d_eager_model_building(false), - d_possiblePropagations(context), - d_hasPropagated(context), d_inConflict(context, false), d_inSatMode(false), d_hasShutDown(false), @@ -285,11 +286,8 @@ TheoryEngine::~TheoryEngine() { void TheoryEngine::interrupt() { d_interrupted = true; } void TheoryEngine::preRegister(TNode preprocessed) { - - Debug("theory") << "TheoryEngine::preRegister( " << preprocessed << ")" << std::endl; - if(Dump.isOn("missed-t-propagations")) { - d_possiblePropagations.push_back(preprocessed); - } + Debug("theory") << "TheoryEngine::preRegister( " << preprocessed << ")" + << std::endl; d_preregisterQueue.push(preprocessed); if (!d_inPreregister) { @@ -400,26 +398,28 @@ void TheoryEngine::printAssertions(const char* tag) { void TheoryEngine::dumpAssertions(const char* tag) { if (Dump.isOn(tag)) { - Dump(tag) << CommentCommand("Starting completeness check"); + const Printer& printer = d_outMgr.getPrinter(); + std::ostream& out = d_outMgr.getDumpOut(); + printer.toStreamCmdComment(out, "Starting completeness check"); for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { Theory* theory = d_theoryTable[theoryId]; if (theory && d_logicInfo.isTheoryEnabled(theoryId)) { - Dump(tag) << CommentCommand("Completeness check"); - Dump(tag) << PushCommand(); + printer.toStreamCmdComment(out, "Completeness check"); + printer.toStreamCmdPush(out); // Dump the shared terms if (d_logicInfo.isSharingEnabled()) { - Dump(tag) << CommentCommand("Shared terms"); + printer.toStreamCmdComment(out, "Shared terms"); context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end(); for (unsigned i = 0; it != it_end; ++ it, ++i) { stringstream ss; ss << (*it); - Dump(tag) << CommentCommand(ss.str()); + printer.toStreamCmdComment(out, ss.str()); } } // Dump the assertions - Dump(tag) << CommentCommand("Assertions"); + printer.toStreamCmdComment(out, "Assertions"); context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); for (; it != it_end; ++ it) { // Get the assertion @@ -428,17 +428,17 @@ void TheoryEngine::dumpAssertions(const char* tag) { if ((*it).d_isPreregistered) { - Dump(tag) << CommentCommand("Preregistered"); + printer.toStreamCmdComment(out, "Preregistered"); } else { - Dump(tag) << CommentCommand("Shared assertion"); + printer.toStreamCmdComment(out, "Shared assertion"); } - Dump(tag) << AssertCommand(assertionNode.toExpr()); + printer.toStreamCmdAssert(out, assertionNode); } - Dump(tag) << CheckSatCommand(); + printer.toStreamCmdCheckSat(out); - Dump(tag) << PopCommand(); + printer.toStreamCmdPop(out); } } } @@ -516,12 +516,6 @@ void TheoryEngine::check(Theory::Effort effort) { // Do the checking CVC4_FOR_EACH_THEORY; - if(Dump.isOn("missed-t-conflicts")) { - Dump("missed-t-conflicts") - << CommentCommand("Completeness check for T-conflicts; expect sat") - << CheckSatCommand(); - } - Debug("theory") << "TheoryEngine::check(" << effort << "): running propagation after the initial check" << endl; // We are still satisfiable, propagate as much as possible @@ -622,25 +616,6 @@ void TheoryEngine::propagate(Theory::Effort effort) // Propagate for each theory using the statement above CVC4_FOR_EACH_THEORY; - - if(Dump.isOn("missed-t-propagations")) { - for(unsigned i = 0; i < d_possiblePropagations.size(); ++i) { - Node atom = d_possiblePropagations[i]; - bool value; - if(d_propEngine->hasValue(atom, value)) { - continue; - } - // Doesn't have a value, check it (and the negation) - if(d_hasPropagated.find(atom) == d_hasPropagated.end()) { - Dump("missed-t-propagations") - << CommentCommand("Completeness check for T-propagations; expect invalid") - << EchoCommand(atom.toString()) - << QueryCommand(atom.toExpr()) - << EchoCommand(atom.notNode().toString()) - << QueryCommand(atom.notNode().toExpr()); - } - } - } } Node TheoryEngine::getNextDecisionRequest() @@ -1134,14 +1109,6 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { // spendResource(); - if(Dump.isOn("t-propagations")) { - Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid") - << QueryCommand(literal.toExpr()); - } - if(Dump.isOn("missed-t-propagations")) { - d_hasPropagated.insert(literal); - } - // Get the atom bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; @@ -1484,8 +1451,10 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma, if(Dump.isOn("t-lemmas")) { // we dump the negation of the lemma, to show validity of the lemma Node n = lemma.negate(); - Dump("t-lemmas") << CommentCommand("theory lemma: expect valid") - << CheckSatCommand(n.toExpr()); + const Printer& printer = d_outMgr.getPrinter(); + std::ostream& out = d_outMgr.getDumpOut(); + printer.toStreamCmdComment(out, "theory lemma: expect valid"); + printer.toStreamCmdCheckSat(out, n); } bool removable = isLemmaPropertyRemovable(p); bool preprocess = isLemmaPropertyPreprocess(p); @@ -1621,8 +1590,10 @@ void TheoryEngine::conflict(theory::TrustNode tconflict, TheoryId theoryId) d_inConflict = true; if(Dump.isOn("t-conflicts")) { - Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat") - << CheckSatCommand(conflict.toExpr()); + const Printer& printer = d_outMgr.getPrinter(); + std::ostream& out = d_outMgr.getDumpOut(); + printer.toStreamCmdComment(out, "theory conflict: expect unsat"); + printer.toStreamCmdCheckSat(out, conflict); } // In the multiple-theories case, we need to reconstruct the conflict |