From: Andrew Reynolds Date: Fri, 8 Oct 2021 20:23:15 +0000 (-0500) Subject: Add argument to distinguish lemmas and input assertions (#7326) X-Git-Tag: cvc5-1.0.0~1099 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7fe20b85b18ae99461c4de339c9109fe68ca48f2;p=cvc5.git Add argument to distinguish lemmas and input assertions (#7326) Work towards virtual clause deletion, where lemmas will be SAT-context dependent. This adds an argument to the decision engine so it can distinguish lemmas from input assertions. --- diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index 3011ad6ec..88f8c6c50 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -42,8 +42,12 @@ prop::SatLiteral DecisionEngine::getNext(bool& stopSearch) DecisionEngineEmpty::DecisionEngineEmpty(Env& env) : DecisionEngine(env) {} bool DecisionEngineEmpty::isDone() { return false; } -void DecisionEngineEmpty::addAssertion(TNode assertion) {} -void DecisionEngineEmpty::addSkolemDefinition(TNode lem, TNode skolem) {} +void DecisionEngineEmpty::addAssertion(TNode assertion, bool isLemma) {} +void DecisionEngineEmpty::addSkolemDefinition(TNode lem, + TNode skolem, + bool isLemma) +{ +} prop::SatLiteral DecisionEngineEmpty::getNextInternal(bool& stopSearch) { return undefSatLiteral; diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index d0092ab1c..3755509b8 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -54,12 +54,12 @@ class DecisionEngine : protected EnvObj * Notify this class that assertion is an (input) assertion, not corresponding * to a skolem definition. */ - virtual void addAssertion(TNode assertion) = 0; + virtual void addAssertion(TNode assertion, bool isLemma) = 0; /** * Notify this class that lem is the skolem definition for skolem, which is * a part of the current assertions. */ - virtual void addSkolemDefinition(TNode lem, TNode skolem) = 0; + virtual void addSkolemDefinition(TNode lem, TNode skolem, bool isLemma) = 0; /** * Notify this class that the list of lemmas defs are now active in the * current SAT context. @@ -93,8 +93,8 @@ class DecisionEngineEmpty : public DecisionEngine public: DecisionEngineEmpty(Env& env); bool isDone() override; - void addAssertion(TNode assertion) override; - void addSkolemDefinition(TNode lem, TNode skolem) override; + void addAssertion(TNode assertion, bool isLemma) override; + void addSkolemDefinition(TNode lem, TNode skolem, bool isLemma) override; protected: prop::SatLiteral getNextInternal(bool& stopSearch) override; diff --git a/src/decision/decision_engine_old.cpp b/src/decision/decision_engine_old.cpp index c61069cae..120fc730b 100644 --- a/src/decision/decision_engine_old.cpp +++ b/src/decision/decision_engine_old.cpp @@ -72,7 +72,7 @@ SatLiteral DecisionEngineOld::getNextInternal(bool& stopSearch) return d_decisionStopOnly ? undefSatLiteral : ret; } -void DecisionEngineOld::addAssertion(TNode assertion) +void DecisionEngineOld::addAssertion(TNode assertion, bool isLemma) { // new assertions, reset whatever result we knew d_result = SAT_VALUE_UNKNOWN; @@ -82,7 +82,9 @@ void DecisionEngineOld::addAssertion(TNode assertion) } } -void DecisionEngineOld::addSkolemDefinition(TNode lem, TNode skolem) +void DecisionEngineOld::addSkolemDefinition(TNode lem, + TNode skolem, + bool isLemma) { // new assertions, reset whatever result we knew d_result = SAT_VALUE_UNKNOWN; diff --git a/src/decision/decision_engine_old.h b/src/decision/decision_engine_old.h index f1a340ca0..5f33a5ecc 100644 --- a/src/decision/decision_engine_old.h +++ b/src/decision/decision_engine_old.h @@ -92,12 +92,12 @@ class DecisionEngineOld : public decision::DecisionEngine * Notify this class that assertion is an (input) assertion, not corresponding * to a skolem definition. */ - void addAssertion(TNode assertion) override; + void addAssertion(TNode assertion, bool isLemma) override; /** * Notify this class that lem is the skolem definition for skolem, which is * a part of the current assertions. */ - void addSkolemDefinition(TNode lem, TNode skolem) override; + void addSkolemDefinition(TNode lem, TNode skolem, bool isLemma) override; // Interface for Strategies to use stuff stored in Decision Engine // (which was possibly requested by them on initialization) diff --git a/src/decision/justification_strategy.cpp b/src/decision/justification_strategy.cpp index e577e6912..d65936964 100644 --- a/src/decision/justification_strategy.cpp +++ b/src/decision/justification_strategy.cpp @@ -478,7 +478,7 @@ prop::SatValue JustificationStrategy::lookupValue(TNode n) bool JustificationStrategy::isDone() { return !refreshCurrentAssertion(); } -void JustificationStrategy::addAssertion(TNode assertion) +void JustificationStrategy::addAssertion(TNode assertion, bool isLemma) { Trace("jh-assert") << "addAssertion " << assertion << std::endl; std::vector toProcess; @@ -486,7 +486,9 @@ void JustificationStrategy::addAssertion(TNode assertion) insertToAssertionList(toProcess, false); } -void JustificationStrategy::addSkolemDefinition(TNode lem, TNode skolem) +void JustificationStrategy::addSkolemDefinition(TNode lem, + TNode skolem, + bool isLemma) { Trace("jh-assert") << "addSkolemDefinition " << lem << " / " << skolem << std::endl; diff --git a/src/decision/justification_strategy.h b/src/decision/justification_strategy.h index 366c26c22..60446a0e7 100644 --- a/src/decision/justification_strategy.h +++ b/src/decision/justification_strategy.h @@ -145,12 +145,12 @@ class JustificationStrategy : public DecisionEngine * Notify this class that assertion is an (input) assertion, not corresponding * to a skolem definition. */ - void addAssertion(TNode assertion) override; + void addAssertion(TNode assertion, bool isLemma) override; /** * Notify this class that lem is the skolem definition for skolem, which is * a part of the current assertions. */ - void addSkolemDefinition(TNode lem, TNode skolem) override; + void addSkolemDefinition(TNode lem, TNode skolem, bool isLemma) override; /** * Notify this class that the list of lemmas defs are now active in the * current SAT context. This is triggered when a literal lit is sent to diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 6f8bbe997..0e911a495 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -194,7 +194,7 @@ void PropEngine::assertInputFormulas( { skolem = it->second; } - d_theoryProxy->notifyAssertion(assertions[i], skolem); + d_theoryProxy->notifyAssertion(assertions[i], skolem, false); } for (const Node& node : assertions) { @@ -310,11 +310,11 @@ void PropEngine::assertLemmasInternal( if (!trn.isNull()) { // notify the theory proxy of the lemma - d_theoryProxy->notifyAssertion(trn.getProven()); + d_theoryProxy->notifyAssertion(trn.getProven(), TNode::null(), true); } for (const theory::SkolemLemma& lem : ppLemmas) { - d_theoryProxy->notifyAssertion(lem.getProven(), lem.d_skolem); + d_theoryProxy->notifyAssertion(lem.getProven(), lem.d_skolem, true); } } } diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 254388a49..ff00acc51 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -62,16 +62,16 @@ void TheoryProxy::presolve() d_theoryEngine->presolve(); } -void TheoryProxy::notifyAssertion(Node a, TNode skolem) +void TheoryProxy::notifyAssertion(Node a, TNode skolem, bool isLemma) { if (skolem.isNull()) { - d_decisionEngine->addAssertion(a); + d_decisionEngine->addAssertion(a, isLemma); } else { d_skdm->notifySkolemDefinition(skolem, a); - d_decisionEngine->addSkolemDefinition(a, skolem); + d_decisionEngine->addSkolemDefinition(a, skolem, isLemma); } } diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 67d3c0668..decae3f2a 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -68,8 +68,13 @@ class TheoryProxy : public Registrar /** Presolve, which calls presolve for the modules managed by this class */ void presolve(); - /** Notify a lemma, possibly corresponding to a skolem definition */ - void notifyAssertion(Node lem, TNode skolem = TNode::null()); + /** + * Notify a lemma or input assertion, possibly corresponding to a skolem + * definition. + */ + void notifyAssertion(Node lem, + TNode skolem = TNode::null(), + bool isLemma = false); void theoryCheck(theory::Theory::Effort effort);