diff options
author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-09-16 12:45:01 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-16 12:45:01 -0500 |
commit | 2c2f05c96e021006275a2bc70b9ede70b280616d (patch) | |
tree | db702d7b8fbd14dd8003b1f03c02b77c89d2fced /src/theory/theory_engine.cpp | |
parent | 0534ea1bbee9a3a7049580449ab25025a4f92a9a (diff) |
Dump commands in internal code using command printing functions. (#5040)
This is work towards migrating commands to the new API. Internal code that creates command objects just for dumping is replaced with direct calls to functions that print the those commands.
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 |