diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/decision/decision_engine.cpp | 7 | ||||
-rw-r--r-- | src/decision/decision_engine.h | 8 | ||||
-rw-r--r-- | src/decision/decision_strategy.h | 13 | ||||
-rw-r--r-- | src/decision/justification_heuristic.cpp | 19 | ||||
-rw-r--r-- | src/decision/justification_heuristic.h | 5 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 54 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 32 | ||||
-rw-r--r-- | src/smt/smt_solver.cpp | 7 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 51 |
9 files changed, 128 insertions, 68 deletions
diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index 6ebd73a5f..ec8943f4a 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -113,8 +113,9 @@ SatValue DecisionEngine::getPolarity(SatVariable var) } } -void DecisionEngine::addAssertions( - const preprocessing::AssertionPipeline& assertions) +void DecisionEngine::addAssertions(const std::vector<Node>& assertions, + const std::vector<Node>& ppLemmas, + const std::vector<Node>& ppSkolems) { // new assertions, reset whatever result we knew d_result = SAT_VALUE_UNKNOWN; @@ -126,7 +127,7 @@ void DecisionEngine::addAssertions( for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i) { - d_needIteSkolemMap[i]->addAssertions(assertions); + d_needIteSkolemMap[i]->addAssertions(assertions, ppLemmas, ppSkolems); } } diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index 52e1e2d1a..afa16397d 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -24,7 +24,6 @@ #include "base/output.h" #include "decision/decision_strategy.h" #include "expr/node.h" -#include "preprocessing/assertion_pipeline.h" #include "prop/cnf_stream.h" #include "prop/prop_engine.h" #include "prop/sat_solver_types.h" @@ -142,9 +141,12 @@ class DecisionEngine { // External World helping us help the Strategies /** - * Add a list of assertions from an AssertionPipeline. + * Add a list of assertions, as well as lemmas coming from preprocessing + * (ppLemmas) and pairwise the skolems they constrain (ppSkolems). */ - void addAssertions(const preprocessing::AssertionPipeline& assertions); + void addAssertions(const std::vector<Node>& assertions, + const std::vector<Node>& ppLemmas, + const std::vector<Node>& ppSkolems); // Interface for Strategies to use stuff stored in Decision Engine // (which was possibly requested by them on initialization) diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h index f7c28299d..ebddc659d 100644 --- a/src/decision/decision_strategy.h +++ b/src/decision/decision_strategy.h @@ -19,7 +19,9 @@ #ifndef CVC4__DECISION__DECISION_STRATEGY_H #define CVC4__DECISION__DECISION_STRATEGY_H -#include "preprocessing/assertion_pipeline.h" +#include <vector> + +#include "expr/node.h" #include "prop/sat_solver_types.h" #include "smt/term_formula_removal.h" @@ -58,8 +60,13 @@ public: bool needIteSkolemMap() override { return true; } - virtual void addAssertions( - const preprocessing::AssertionPipeline& assertions) = 0; + /** + * Add a list of assertions, as well as lemmas coming from preprocessing + * (ppLemmas) and pairwise the skolems they constrain (ppSkolems). + */ + virtual void addAssertions(const std::vector<Node>& assertions, + const std::vector<Node>& ppLemmas, + const std::vector<Node>& ppSkolems) = 0; };/* class ITEDecisionStrategy */ class RelevancyStrategy : public ITEDecisionStrategy { diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index baf0056e9..afbff18c1 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -164,15 +164,14 @@ inline void computeXorIffDesiredValues } } -void JustificationHeuristic::addAssertions( - const preprocessing::AssertionPipeline &assertions) +void JustificationHeuristic::addAssertions(const std::vector<Node>& assertions, + const std::vector<Node>& ppLemmas, + const std::vector<Node>& ppSkolems) { - size_t assertionsEnd = assertions.getRealAssertionsEnd(); - + Assert(ppSkolems.size() == ppLemmas.size()); Trace("decision") << "JustificationHeuristic::addAssertions()" << " size = " << assertions.size() - << " assertionsEnd = " << assertionsEnd << std::endl; // Save all assertions locally, including the assertions generated by term @@ -198,13 +197,11 @@ void JustificationHeuristic::addAssertions( } // Save mapping between ite skolems and ite assertions - for (const std::pair<const Node, unsigned> &i : assertions.getIteSkolemMap()) + for (size_t i = 0, nlemmas = ppLemmas.size(); i < nlemmas; i++) { - Trace("decision::jh::ite") << " jh-ite: " << (i.first) << " maps to " - << assertions[(i.second)] << std::endl; - Assert(i.second >= assertionsEnd && i.second < assertions.size()); - - d_skolemAssertions[i.first] = assertions[i.second]; + Trace("decision::jh::ite") << " jh-ite: " << ppSkolems[i] << " maps to " + << ppLemmas[i] << std::endl; + d_skolemAssertions[ppSkolems[i]] = ppLemmas[i]; } // Automatic weight computation diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 5ecb5eb08..81b08f1a6 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -121,8 +121,9 @@ public: prop::SatLiteral getNext(bool &stopSearch) override; - void addAssertions( - const preprocessing::AssertionPipeline &assertions) override; + void addAssertions(const std::vector<Node>& assertions, + const std::vector<Node>& ppLemmas, + const std::vector<Node>& ppSkolems) override; private: /* getNext with an option to specify threshold */ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 26d1e615b..8c1e452e7 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -123,6 +123,28 @@ PropEngine::~PropEngine() { delete d_theoryProxy; } +void PropEngine::notifyPreprocessedAssertions( + const preprocessing::AssertionPipeline& ap) +{ + // notify the theory engine of preprocessed assertions + d_theoryEngine->notifyPreprocessedAssertions(ap.ref()); + + // Add assertions to decision engine, which manually extracts what assertions + // corresponded to term formula removal. Note that alternatively we could + // delay all theory preprocessing and term formula removal to this point, in + // which case this method could simply take a vector of Node and not rely on + // assertion pipeline or its ITE skolem map. + std::vector<Node> ppLemmas; + std::vector<Node> ppSkolems; + for (const std::pair<const Node, unsigned>& i : ap.getIteSkolemMap()) + { + Assert(i.second >= ap.getRealAssertionsEnd() && i.second < ap.size()); + ppSkolems.push_back(i.first); + ppLemmas.push_back(ap[i.second]); + } + d_decisionEngine->addAssertions(ap.ref(), ppLemmas, ppSkolems); +} + void PropEngine::assertFormula(TNode node) { Assert(!d_inCheckSat) << "Sat solver in solve()!"; Debug("prop") << "assertFormula(" << node << ")" << endl; @@ -130,18 +152,42 @@ void PropEngine::assertFormula(TNode node) { d_cnfStream->convertAndAssert(node, false, false, true); } -void PropEngine::assertLemma(TNode node, bool negated, bool removable) +void PropEngine::assertLemma(theory::TrustNode trn, bool removable) { + Node node = trn.getNode(); + bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT; Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; // Assert as (possibly) removable d_cnfStream->convertAndAssert(node, removable, negated); } -void PropEngine::addAssertionsToDecisionEngine( - const preprocessing::AssertionPipeline& assertions) +void PropEngine::assertLemmas(theory::TrustNode lem, + std::vector<theory::TrustNode>& ppLemmas, + std::vector<Node>& ppSkolems, + bool removable) { - d_decisionEngine->addAssertions(assertions); + Assert(ppSkolems.size() == ppLemmas.size()); + // assert the lemmas + assertLemma(lem, removable); + for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i) + { + assertLemma(ppLemmas[i], removable); + } + + // assert to decision engine + if (!removable) + { + // also add to the decision engine, where notice we don't need proofs + std::vector<Node> assertions; + assertions.push_back(lem.getProven()); + std::vector<Node> ppLemmasF; + for (const theory::TrustNode& tnl : ppLemmas) + { + ppLemmasF.push_back(tnl.getProven()); + } + d_decisionEngine->addAssertions(assertions, ppLemmasF, ppSkolems); + } } void PropEngine::requirePhase(TNode n, bool phase) { diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index e4d536c29..061324947 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -88,6 +88,13 @@ class PropEngine void shutdown() {} /** + * Notify preprocessed assertions. This method is called just before the + * assertions are asserted to this prop engine. This method notifies the + * decision engine and the theory engine of the assertions in ap. + */ + void notifyPreprocessedAssertions(const preprocessing::AssertionPipeline& ap); + + /** * Converts the given formula to CNF and assert the CNF to the SAT solver. * The formula is asserted permanently for the current context. * @param node the formula to assert @@ -99,19 +106,28 @@ class PropEngine * The formula can be removed by the SAT solver after backtracking lower * than the (SAT and SMT) level at which it was asserted. * - * @param node the formula to assert - * @param negated whether the node should be considered to be negated - * at the top level (or not) + * @param trn the trust node storing the formula to assert * @param removable whether this lemma can be quietly removed based - * on an activity heuristic (or not) + * on an activity heuristic */ - void assertLemma(TNode node, bool negated, bool removable); + void assertLemma(theory::TrustNode trn, bool removable); /** - * Pass a list of assertions from an AssertionPipeline to the decision engine. + * Assert lemma trn with preprocessing lemmas ppLemmas which correspond + * to lemmas for skolems in ppSkolems. + * + * @param trn the trust node storing the formula to assert + * @param ppLemmas the lemmas from preprocessing and term formula removal on + * the proven node of trn + * @param ppSkolem the skolem that each lemma in ppLemma constrains. It should + * be the case that ppLemmas.size()==ppSkolems.size(). + * @param removable whether this lemma can be quietly removed based + * on an activity heuristic */ - void addAssertionsToDecisionEngine( - const preprocessing::AssertionPipeline& assertions); + void assertLemmas(theory::TrustNode trn, + std::vector<theory::TrustNode>& ppLemmas, + std::vector<Node>& ppSkolems, + bool removable); /** * If ever n is decided upon, it must be in the given phase. This diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 26a2ff3e1..c18dfe8ac 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -224,14 +224,11 @@ void SmtSolver::processAssertions(Assertions& as) // process the assertions with the preprocessor bool noConflict = d_pp.process(as); - // notify theory engine new preprocessed assertions - d_theoryEngine->notifyPreprocessedAssertions(ap.ref()); - // Push the formula to decision engine if (noConflict) { - Chat() << "pushing to decision engine..." << endl; - d_propEngine->addAssertionsToDecisionEngine(ap); + Chat() << "notifying theory engine and decision engine..." << std::endl; + d_propEngine->notifyPreprocessedAssertions(ap); } // end: INVARIANT to maintain: no reordering of assertions or diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 84212fa1b..fa8960446 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -31,7 +31,6 @@ #include "options/options.h" #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" @@ -1495,26 +1494,18 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma, } } - // must use an assertion pipeline due to decision engine below - AssertionPipeline lemmas; - // make the assertion pipeline - lemmas.push_back(lemmap); - lemmas.updateRealAssertionsEnd(); Assert(newSkolems.size() == newLemmas.size()); - for (size_t i = 0, nsize = newLemmas.size(); i < nsize; i++) - { - // store skolem mapping here - IteSkolemMap& imap = lemmas.getIteSkolemMap(); - imap[newSkolems[i]] = lemmas.size(); - lemmas.push_back(newLemmas[i].getNode()); - } // If specified, we must add this lemma to the set of those that need to be // justified, where note we pass all auxiliary lemmas in lemmas, since these // by extension must be justified as well. if (d_relManager != nullptr && isLemmaPropertyNeedsJustify(p)) { - d_relManager->notifyPreprocessedAssertions(lemmas.ref()); + d_relManager->notifyPreprocessedAssertion(tlemma.getProven()); + for (const theory::TrustNode& tnl : newLemmas) + { + d_relManager->notifyPreprocessedAssertion(tnl.getProven()); + } } // do final checks on the lemmas we are about to send @@ -1531,32 +1522,34 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma, } } - // now, send the lemmas to the prop engine - Trace("te-lemma") << "Lemma, output: " << tlemma.getProven() << std::endl; - d_propEngine->assertLemma(tlemma.getProven(), false, removable); - for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i) + if (Trace.isOn("te-lemma")) { - Trace("te-lemma") << "Lemma, new lemma: " << newLemmas[i].getProven() - << std::endl; - d_propEngine->assertLemma(newLemmas[i].getProven(), false, removable); + Trace("te-lemma") << "Lemma, output: " << tlemma.getProven() << std::endl; + for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i) + { + Trace("te-lemma") << "Lemma, new lemma: " << newLemmas[i].getProven() + << " (skolem is " << newSkolems[i] << ")" << std::endl; + } } - // assert to decision engine - if (!removable) - { - d_propEngine->addAssertionsToDecisionEngine(lemmas); - } + // now, send the lemmas to the prop engine + d_propEngine->assertLemmas(tlemma, newLemmas, newSkolems, removable); // Mark that we added some lemmas d_lemmasAdded = true; // Lemma analysis isn't online yet; this lemma may only live for this // user level. - Node retLemma = lemmas[0]; - if (lemmas.size() > 1) + Node retLemma = tlemma.getNode(); + if (!newLemmas.empty()) { + std::vector<Node> lemmas{retLemma}; + for (const theory::TrustNode& tnl : newLemmas) + { + lemmas.push_back(tnl.getProven()); + } // the returned lemma is the conjunction of all additional lemmas. - retLemma = NodeManager::currentNM()->mkNode(kind::AND, lemmas.ref()); + retLemma = NodeManager::currentNM()->mkNode(kind::AND, lemmas); } return theory::LemmaStatus(retLemma, d_userContext->getLevel()); } |