From d47a8708171f1cf488fe9ce05f56f2566db53093 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 12 Feb 2021 03:45:29 -0600 Subject: Simplify and fix decision engine's handling of skolem definitions (#5888) This PR changes the front end of prop engine to distinguish input formulas from skolem definitions, which is required by the decision engine. This PR breaks the dependency of PropEngine on the AssertionsPipeline, as now the determining of whether an input formula is a skolem definition is handled externally, in SmtSolver. With this PR, we should not be required to satisfy skolem definitions that are not relevant based on the techniques already implemented in the decision engine. Currently, we are not distinguishing input formulas from skolem definitions properly, meaning we assert more literals than we need to. This also simplifies related interfaces within decision engine. We should test this PR with --decision=justification on SMT-LIB. --- src/prop/prop_engine.cpp | 119 ++++++++++++++++++++++++---------------------- src/prop/prop_engine.h | 48 +++++++++++++++++-- src/prop/theory_proxy.cpp | 6 +-- 3 files changed, 108 insertions(+), 65 deletions(-) (limited to 'src/prop') diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index da19480f9..e99e11eb2 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -171,40 +171,25 @@ theory::TrustNode PropEngine::removeItes( } void PropEngine::notifyPreprocessedAssertions( - const preprocessing::AssertionPipeline& ap) + const std::vector& assertions) { // 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 ppLemmas; - std::vector ppSkolems; - for (const std::pair& 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); + d_theoryEngine->notifyPreprocessedAssertions(assertions); } void PropEngine::assertFormula(TNode node) { Assert(!d_inCheckSat) << "Sat solver in solve()!"; Debug("prop") << "assertFormula(" << node << ")" << endl; - if (isProofEnabled()) - { - d_pfCnfStream->convertAndAssert(node, false, false, nullptr); - // register in proof manager - d_ppm->registerAssertion(node); - } - else - { - d_cnfStream->convertAndAssert(node, false, false, true); - } + d_decisionEngine->addAssertion(node); + assertInternal(node, false, false, true); +} + +void PropEngine::assertSkolemDefinition(TNode node, TNode skolem) +{ + Assert(!d_inCheckSat) << "Sat solver in solve()!"; + Debug("prop") << "assertFormula(" << node << ")" << endl; + d_decisionEngine->addSkolemDefinition(node, skolem); + assertInternal(node, false, false, true); } void PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p) @@ -243,42 +228,66 @@ void PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p) } // now, assert the lemmas - assertLemmaInternal(tplemma, removable); - for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i) - { - assertLemmaInternal(ppLemmas[i], removable); - } - - // assert to decision engine - if (!removable) - { - // also add to the decision engine, where notice we don't need proofs - std::vector assertions; - assertions.push_back(tplemma.getProven()); - std::vector ppLemmasF; - for (const theory::TrustNode& tnl : ppLemmas) - { - ppLemmasF.push_back(tnl.getProven()); - } - d_decisionEngine->addAssertions(assertions, ppLemmasF, ppSkolems); - } + assertLemmasInternal(tplemma, ppLemmas, ppSkolems, removable); } -void PropEngine::assertLemmaInternal(theory::TrustNode trn, bool removable) +void PropEngine::assertTrustedLemmaInternal(theory::TrustNode trn, + bool removable) { Node node = trn.getNode(); - bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT; Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; + bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT; + Assert(!isProofEnabled() || trn.getGenerator() != nullptr); + assertInternal(trn.getNode(), negated, removable, false, trn.getGenerator()); +} + +void PropEngine::assertInternal( + TNode node, bool negated, bool removable, bool input, ProofGenerator* pg) +{ // Assert as (possibly) removable if (isProofEnabled()) { - Assert(trn.getGenerator()); - d_pfCnfStream->convertAndAssert( - node, negated, removable, trn.getGenerator()); + d_pfCnfStream->convertAndAssert(node, negated, removable, pg); + // if input, register the assertion + if (input) + { + d_ppm->registerAssertion(node); + } } else { - d_cnfStream->convertAndAssert(node, removable, negated); + d_cnfStream->convertAndAssert(node, removable, negated, input); + } +} +void PropEngine::assertLemmasInternal( + theory::TrustNode trn, + const std::vector& ppLemmas, + const std::vector& ppSkolems, + bool removable) +{ + if (!trn.isNull()) + { + assertTrustedLemmaInternal(trn, removable); + } + for (const theory::TrustNode& tnl : ppLemmas) + { + assertTrustedLemmaInternal(tnl, removable); + } + // assert to decision engine + if (!removable) + { + // also add to the decision engine, where notice we don't need proofs + if (!trn.isNull()) + { + // notify the theory proxy of the lemma + d_decisionEngine->addAssertion(trn.getProven()); + } + Assert(ppSkolems.size() == ppLemmas.size()); + for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i) + { + Node lem = ppLemmas[i].getProven(); + d_decisionEngine->addSkolemDefinition(lem, ppSkolems[i]); + } } } @@ -441,10 +450,8 @@ Node PropEngine::getPreprocessedTerm(TNode n) std::vector newSkolems; theory::TrustNode tpn = d_theoryProxy->preprocess(n, newLemmas, newSkolems); // send lemmas corresponding to the skolems introduced by preprocessing n - for (const theory::TrustNode& tnl : newLemmas) - { - assertLemma(tnl, theory::LemmaProperty::NONE); - } + theory::TrustNode trnNull; + assertLemmasInternal(trnNull, newLemmas, newSkolems, false); return tpn.isNull() ? Node(n) : tpn.getNode(); } diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index f7561d945..ac90d0c36 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -26,7 +26,6 @@ #include "base/modal_exception.h" #include "expr/node.h" #include "options/options.h" -#include "preprocessing/assertion_pipeline.h" #include "proof/proof_manager.h" #include "prop/minisat/core/Solver.h" #include "prop/minisat/minisat.h" @@ -127,16 +126,31 @@ class PropEngine /** * 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. + * theory engine of the given assertions. Notice this vector includes + * both the input formulas and the skolem definitions. */ - void notifyPreprocessedAssertions(const preprocessing::AssertionPipeline& ap); + void notifyPreprocessedAssertions(const std::vector& assertions); /** * Converts the given formula to CNF and assert the CNF to the SAT solver. - * The formula is asserted permanently for the current context. + * The formula is asserted permanently for the current context. Note the + * formula should correspond to an input formula and not a lemma introduced + * by term formula removal (which instead should use the interface below). * @param node the formula to assert */ void assertFormula(TNode node); + /** + * Same as above, but node corresponds to the skolem definition of the given + * skolem. + * @param node the formula to assert + * @param skolem the skolem that this lemma defines. + * + * For example, if k is introduced by ITE removal of (ite C x y), then node + * is the formula (ite C (= k x) (= k y)). It is important to distinguish + * these kinds of lemmas from input assertions, as the justification decision + * heuristic treates them specially. + */ + void assertSkolemDefinition(TNode node, TNode skolem); /** * Converts the given formula to CNF and assert the CNF to the SAT solver. @@ -304,7 +318,31 @@ class PropEngine * @param removable whether this lemma can be quietly removed based * on an activity heuristic */ - void assertLemmaInternal(theory::TrustNode trn, bool removable); + void assertTrustedLemmaInternal(theory::TrustNode trn, bool removable); + /** + * Assert node as a formula to the CNF stream + * @param node The formula to assert + * @param negated Whether to assert the negation of node + * @param removable Whether the formula is removable + * @param input Whether the formula came from the input + * @param pg Pointer to a proof generator that can provide a proof of node + * (or its negation if negated is true). + */ + void assertInternal(TNode node, + bool negated, + bool removable, + bool input, + ProofGenerator* pg = nullptr); + /** + * Assert lemmas internal, where trn is a trust node corresponding to a + * formula to assert to the CNF stream, ppLemmas and ppSkolems are the + * skolem definitions and skolems obtained from preprocessing it, and + * removable is whether the lemma is removable. + */ + void assertLemmasInternal(theory::TrustNode trn, + const std::vector& ppLemmas, + const std::vector& ppSkolems, + bool removable); /** * Indicates that the SAT solver is currently solving something and we should diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 06e729714..beb2651bf 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -156,16 +156,14 @@ void TheoryProxy::spendResource(ResourceManager::Resource r) d_theoryEngine->spendResource(r); } -bool TheoryProxy::isDecisionRelevant(SatVariable var) { - return d_decisionEngine->isRelevant(var); -} +bool TheoryProxy::isDecisionRelevant(SatVariable var) { return true; } bool TheoryProxy::isDecisionEngineDone() { return d_decisionEngine->isDone(); } SatValue TheoryProxy::getDecisionPolarity(SatVariable var) { - return d_decisionEngine->getPolarity(var); + return SAT_VALUE_UNKNOWN; } CnfStream* TheoryProxy::getCnfStream() { return d_cnfStream; } -- cgit v1.2.3