From c274b572b3f634e4f098dff564942d6dc452a22f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 14 Mar 2022 16:02:40 -0500 Subject: [PATCH] Fixes for skolem definition management (#8301) Fixes two issues with how we manage skolem definitions (used for tracking which assertions are relevant for the decision engine). First, the theory proxy must be notified of skolem definitions before we have assertions involving them, or else hasSkolems is wrong. This was previously done incorrectly for lemmas. This PR changes the order in PropEngine::assertLemmasInternal. Second, skolem definitions are local to a solver instance and should not be managed by attributes, moreover they are user-context dependent. This changes it to a local user-context dependent map in Skolem. Fixes #8296. --- src/decision/justification_strategy.cpp | 1 + src/prop/prop_engine.cpp | 22 +++++---- src/prop/skolem_def_manager.cpp | 47 ++++++++----------- src/prop/skolem_def_manager.h | 14 ++++-- test/regress/CMakeLists.txt | 1 + .../issue8296-sk-def-before-assert.smt2 | 12 +++++ 6 files changed, 58 insertions(+), 39 deletions(-) create mode 100644 test/regress/regress0/decision/issue8296-sk-def-before-assert.smt2 diff --git a/src/decision/justification_strategy.cpp b/src/decision/justification_strategy.cpp index bced3d662..6c3ddfd04 100644 --- a/src/decision/justification_strategy.cpp +++ b/src/decision/justification_strategy.cpp @@ -508,6 +508,7 @@ bool JustificationStrategy::needsActiveSkolemDefs() const void JustificationStrategy::notifyActiveSkolemDefs(std::vector& defs) { + Trace("jh-assert") << "notifyActiveSkolemDefs: " << defs << std::endl; Assert(d_jhSkRlvMode == options::JutificationSkolemRlvMode::ASSERT); // assertion processed makes all skolems in assertion active, // which triggers their definitions to becoming relevant diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 4fe7da695..872859346 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -267,15 +267,11 @@ void PropEngine::assertLemmasInternal( const std::vector& ppLemmas, bool removable) { - if (!trn.isNull()) - { - assertTrustedLemmaInternal(trn, removable); - } - for (const theory::SkolemLemma& lem : ppLemmas) - { - assertTrustedLemmaInternal(lem.d_lemma, removable); - } - // assert to decision engine + // Assert to decision engine. Notice this must come before the calls to + // assertTrustedLemmaInternal below, since the decision engine requires + // setting up information about the relevance of skolems before literals + // are potentially asserted to the theory engine, which it listens to for + // tracking active skolem definitions. if (!removable) { // also add to the decision engine, where notice we don't need proofs @@ -289,6 +285,14 @@ void PropEngine::assertLemmasInternal( d_theoryProxy->notifyAssertion(lem.getProven(), lem.d_skolem, true); } } + if (!trn.isNull()) + { + assertTrustedLemmaInternal(trn, removable); + } + for (const theory::SkolemLemma& lem : ppLemmas) + { + assertTrustedLemmaInternal(lem.d_lemma, removable); + } } void PropEngine::requirePhase(TNode n, bool phase) { diff --git a/src/prop/skolem_def_manager.cpp b/src/prop/skolem_def_manager.cpp index 36849424e..b4609ebe8 100644 --- a/src/prop/skolem_def_manager.cpp +++ b/src/prop/skolem_def_manager.cpp @@ -15,14 +15,12 @@ #include "prop/skolem_def_manager.h" -#include "expr/attribute.h" - namespace cvc5 { namespace prop { SkolemDefManager::SkolemDefManager(context::Context* context, context::UserContext* userContext) - : d_skDefs(userContext), d_skActive(context) + : d_skDefs(userContext), d_skActive(context), d_hasSkolems(userContext) { } @@ -37,6 +35,9 @@ void SkolemDefManager::notifySkolemDefinition(TNode skolem, Node def) // equivalent up to purification if (d_skDefs.find(skolem) == d_skDefs.end()) { + // should not have already computed whether the skolem has skolems, or else + // our computation of hasSkolems is wrong after adding this definition + Assert(d_hasSkolems.find(skolem) == d_hasSkolems.end()); d_skDefs.insert(skolem, def); } } @@ -54,6 +55,8 @@ void SkolemDefManager::notifyAsserted(TNode literal, { std::unordered_set skolems; getSkolems(literal, skolems); + Trace("sk-defs") << "notifyAsserted: " << literal << " has skolems " + << skolems << std::endl; for (const Node& k : skolems) { if (d_skActive.find(k) != d_skActive.end()) @@ -62,6 +65,7 @@ void SkolemDefManager::notifyAsserted(TNode literal, continue; } d_skActive.insert(k); + Trace("sk-defs") << "...activate " << k << std::endl; if (useDefs) { // add its definition to the activated list @@ -77,28 +81,20 @@ void SkolemDefManager::notifyAsserted(TNode literal, } } -struct HasSkolemTag -{ -}; -struct HasSkolemComputedTag -{ -}; -/** Attribute true for nodes with skolems in them */ -typedef expr::Attribute HasSkolemAttr; -/** Attribute true for nodes where we have computed the above attribute */ -typedef expr::Attribute HasSkolemComputedAttr; - -bool SkolemDefManager::hasSkolems(TNode n) const +bool SkolemDefManager::hasSkolems(TNode n) { + Trace("sk-defs-debug") << "Compute has skolems for " << n << std::endl; std::unordered_set visited; std::unordered_set::iterator it; + NodeBoolMap::const_iterator itn; std::vector visit; TNode cur; visit.push_back(n); do { cur = visit.back(); - if (cur.getAttribute(HasSkolemComputedAttr())) + itn = d_hasSkolems.find(cur); + if (itn != d_hasSkolems.end()) { visit.pop_back(); // already computed @@ -116,8 +112,7 @@ bool SkolemDefManager::hasSkolems(TNode n) const { hasSkolem = (d_skDefs.find(cur) != d_skDefs.end()); } - cur.setAttribute(HasSkolemAttr(), hasSkolem); - cur.setAttribute(HasSkolemComputedAttr(), true); + d_hasSkolems[cur] = hasSkolem; } else { @@ -133,7 +128,7 @@ bool SkolemDefManager::hasSkolems(TNode n) const visit.pop_back(); bool hasSkolem; if (cur.getMetaKind() == kind::metakind::PARAMETERIZED - && cur.getOperator().getAttribute(HasSkolemAttr())) + && d_hasSkolems[cur.getOperator()]) { hasSkolem = true; } @@ -142,24 +137,22 @@ bool SkolemDefManager::hasSkolems(TNode n) const hasSkolem = false; for (TNode i : cur) { - Assert(i.getAttribute(HasSkolemComputedAttr())); - if (i.getAttribute(HasSkolemAttr())) + Assert(d_hasSkolems.find(i) != d_hasSkolems.end()); + if (d_hasSkolems[i]) { hasSkolem = true; break; } } } - cur.setAttribute(HasSkolemAttr(), hasSkolem); - cur.setAttribute(HasSkolemComputedAttr(), true); + d_hasSkolems[cur] = hasSkolem; } } while (!visit.empty()); - Assert(n.getAttribute(HasSkolemComputedAttr())); - return n.getAttribute(HasSkolemAttr()); + Assert(d_hasSkolems.find(n) != d_hasSkolems.end()); + return d_hasSkolems[n]; } -void SkolemDefManager::getSkolems(TNode n, - std::unordered_set& skolems) const +void SkolemDefManager::getSkolems(TNode n, std::unordered_set& skolems) { std::unordered_set visited; std::unordered_set::iterator it; diff --git a/src/prop/skolem_def_manager.h b/src/prop/skolem_def_manager.h index d3b59f895..59213302e 100644 --- a/src/prop/skolem_def_manager.h +++ b/src/prop/skolem_def_manager.h @@ -22,6 +22,7 @@ #include #include +#include "context/cdhashmap.h" #include "context/cdhashset.h" #include "context/cdinsert_hashmap.h" #include "context/context.h" @@ -42,6 +43,7 @@ namespace prop { class SkolemDefManager { using NodeNodeMap = context::CDInsertHashMap; + using NodeBoolMap = context::CDHashMap; using NodeSet = context::CDHashSet; public: @@ -81,15 +83,21 @@ class SkolemDefManager * @param n The node to traverse * @param skolems The set where the skolems are added */ - void getSkolems(TNode n, std::unordered_set& skolems) const; - /** Does n have skolems having definitions managed by this class? */ - bool hasSkolems(TNode n) const; + void getSkolems(TNode n, std::unordered_set& skolems); + /** + * Does n have skolems having definitions managed by this class? Should call + * this method *after* notifying skolem definitions for all potential + * skolems occurring in n. + */ + bool hasSkolems(TNode n); private: /** skolems to definitions (user-context dependent) */ NodeNodeMap d_skDefs; /** set of active skolems (SAT-context dependent) */ NodeSet d_skActive; + /** Cache for hasSkolems */ + NodeBoolMap d_hasSkolems; }; } // namespace prop diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 05b16abb4..67073033d 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -575,6 +575,7 @@ set(regress_0_tests regress0/decision/error20.delta01.smtv1.smt2 regress0/decision/error20.smtv1.smt2 regress0/decision/error3.delta01.smtv1.smt2 + regress0/decision/issue8296-sk-def-before-assert.smt2 regress0/decision/pp-regfile.delta01.smtv1.smt2 regress0/decision/pp-regfile.delta02.smtv1.smt2 regress0/decision/quant-ex1.smt2 diff --git a/test/regress/regress0/decision/issue8296-sk-def-before-assert.smt2 b/test/regress/regress0/decision/issue8296-sk-def-before-assert.smt2 new file mode 100644 index 000000000..3665d6a55 --- /dev/null +++ b/test/regress/regress0/decision/issue8296-sk-def-before-assert.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: -i +; EXPECT: sat +; EXPECT: sat +(set-logic ALL) +(set-option :miniscope-quant false) +(declare-fun i2 () Int) +(declare-fun v6 () Bool) +(declare-sort S2 0) +(assert (exists ((q521 S2)) (exists ((q523 Int)) (exists ((q524 S2)) (forall ((q525 Bool)) (or (= q524 q521) (= q523 (abs i2)) (and v6 (= q525 (= 0 (abs i2)))))))))) +(check-sat) +(assert (= 1 (abs i2))) +(check-sat) -- 2.30.2