From: Andrew Reynolds Date: Wed, 18 May 2022 13:42:48 +0000 (-0500) Subject: Make skolem definition manager robust to definitions for already asserted skolems... X-Git-Tag: cvc5-1.0.1~118 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7f5e1dab306669d09fe1c6a13dc181d07c2af358;p=cvc5.git Make skolem definition manager robust to definitions for already asserted skolems (#8749) It makes the skolem definition manager more robust so that skolem definitions can be added for skolems that have already appeared in asserted literals. This was the initial motivation for the change in ordering. As a result, fixes #8347 and fixes cvc5/cvc5-projects#512. It also optimizes this class in a few ways. It also comments more on the change to PropEngine introduced here: #8301 which led to performance degradation on a set of string benchmarks of interest. --- diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index ca93843c2..1e7267064 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -289,11 +289,16 @@ void PropEngine::assertLemmasInternal( const std::vector& ppLemmas, bool removable) { - // 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. + // Assert to decision engine first. + // Note that this order is important for theories that send lemmas during + // preregistration, as it impacts the order in which lemmas are processed + // by default by the decision engine. In particular, sending to the SAT + // solver first means that lemmas sent during preregistration in response to + // the current lemma are processed after that lemma. This makes a difference + // e.g. for string reduction lemmas, where preregistration lemmas are + // introduced for skolems that appear in reductions. Moving this + // block after the one below has mixed (trending negative) performance on + // SMT-LIB strings logics. if (!removable) { // also add to the decision engine, where notice we don't need proofs diff --git a/src/prop/skolem_def_manager.cpp b/src/prop/skolem_def_manager.cpp index 73bb62afd..013a6f023 100644 --- a/src/prop/skolem_def_manager.cpp +++ b/src/prop/skolem_def_manager.cpp @@ -35,9 +35,6 @@ 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); } } @@ -50,34 +47,28 @@ TNode SkolemDefManager::getDefinitionForSkolem(TNode skolem) const } void SkolemDefManager::notifyAsserted(TNode literal, - std::vector& activatedSkolems, - bool useDefs) + std::vector& activatedSkolems) { - 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.size() == d_skDefs.size()) { - if (d_skActive.find(k) != d_skActive.end()) + // already activated all skolems + return; + } + std::unordered_set defs; + getSkolems(literal, defs, true); + Trace("sk-defs") << "notifyAsserted: " << literal << " has skolems " << defs + << std::endl; + for (const Node& d : defs) + { + if (d_skActive.find(d) != d_skActive.end()) { // already active continue; } - d_skActive.insert(k); - Trace("sk-defs") << "...activate " << k << std::endl; - if (useDefs) - { - // add its definition to the activated list - NodeNodeMap::const_iterator it = d_skDefs.find(k); - Assert(it != d_skDefs.end()); - activatedSkolems.push_back(it->second); - } - else - { - // add to the activated list - activatedSkolems.push_back(k); - } + d_skActive.insert(d); + Trace("sk-defs") << "...activate " << d << std::endl; + // add its definition to the activated list + activatedSkolems.push_back(d); } } @@ -107,12 +98,22 @@ bool SkolemDefManager::hasSkolems(TNode n) if (cur.getNumChildren() == 0) { visit.pop_back(); - bool hasSkolem = false; - if (cur.isVar()) + Kind ck = cur.getKind(); + // We have skolems if we are a skolem that has a definition, or + // we are a Boolean term variable. For Boolean term variables, we do + // not make this test depend on whether the skolem has a definition, + // since that is prone to change if the Boolean term variable was + // introduced in a lemma prior to its definition being introduced. + // This is for example the case in strings reduction for Booleans, + // ground term purification for E-matching, etc. + if (ck == kind::SKOLEM) + { + d_hasSkolems[cur] = (d_skDefs.find(cur) != d_skDefs.end()); + } + else { - hasSkolem = (d_skDefs.find(cur) != d_skDefs.end()); + d_hasSkolems[cur] = (ck == kind::BOOLEAN_TERM_VARIABLE); } - d_hasSkolems[cur] = hasSkolem; } else { @@ -152,8 +153,11 @@ bool SkolemDefManager::hasSkolems(TNode n) return d_hasSkolems[n]; } -void SkolemDefManager::getSkolems(TNode n, std::unordered_set& skolems) +void SkolemDefManager::getSkolems(TNode n, + std::unordered_set& skolems, + bool useDefs) { + NodeNodeMap::const_iterator itd; std::unordered_set visited; std::unordered_set::iterator it; std::vector visit; @@ -174,9 +178,10 @@ void SkolemDefManager::getSkolems(TNode n, std::unordered_set& skolems) visited.insert(cur); if (cur.isVar()) { - if (d_skDefs.find(cur) != d_skDefs.end()) + itd = d_skDefs.find(cur); + if (itd != d_skDefs.end()) { - skolems.insert(cur); + skolems.insert(useDefs ? itd->second : Node(cur)); } continue; } diff --git a/src/prop/skolem_def_manager.h b/src/prop/skolem_def_manager.h index 1a8ed93cb..a6bb756e5 100644 --- a/src/prop/skolem_def_manager.h +++ b/src/prop/skolem_def_manager.h @@ -68,13 +68,9 @@ class SkolemDefManager * is active in the SAT context if it appears in an asserted literal. * * @param literal The literal that became asserted - * @param activatedSkolems The list to add skolems to - * @param useDefs If this flag is true, we add the skolem definition for - * skolems to activatedSkolems instead of the skolem itself. + * @param activatedDefs The list to add skolem definitions to */ - void notifyAsserted(TNode literal, - std::vector& activatedSkolems, - bool useDefs = false); + void notifyAsserted(TNode literal, std::vector& activatedDefs); /** * Get the set of skolems maintained by this class that occur in node n, @@ -82,8 +78,12 @@ class SkolemDefManager * * @param n The node to traverse * @param skolems The set where the skolems are added + * @param useDefs Whether to add definitions for the skolems instead of the + * skolems */ - void getSkolems(TNode n, std::unordered_set& skolems); + void getSkolems(TNode n, + std::unordered_set& skolems, + bool useDefs = false); /** * Does n have skolems having definitions managed by this class? Should call * this method *after* notifying skolem definitions for all potential @@ -94,7 +94,7 @@ class SkolemDefManager private: /** skolems to definitions (user-context dependent) */ NodeNodeMap d_skDefs; - /** set of active skolems (SAT-context dependent) */ + /** set of active skolem definitions (SAT-context dependent) */ NodeSet d_skActive; /** Cache for hasSkolems */ NodeBoolMap d_hasSkolems; diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 6c6c114ff..71720ddc6 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -163,10 +163,13 @@ void TheoryProxy::theoryCheck(theory::Theory::Effort effort) { // Assertion makes all skolems in assertion active, // which triggers their definitions to becoming active. std::vector activeSkolemDefs; - d_skdm->notifyAsserted(assertion, activeSkolemDefs, true); - // notify the decision engine of the skolem definitions that have become - // active due to the assertion. - d_decisionEngine->notifyActiveSkolemDefs(activeSkolemDefs); + d_skdm->notifyAsserted(assertion, activeSkolemDefs); + if (!activeSkolemDefs.empty()) + { + // notify the decision engine of the skolem definitions that have become + // active due to the assertion. + d_decisionEngine->notifyActiveSkolemDefs(activeSkolemDefs); + } } } if (!d_stopSearch.get()) diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 1eee1ea34..30e901bd1 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -1095,6 +1095,7 @@ set(regress_0_tests regress0/quantifiers/nested-inf.smt2 regress0/quantifiers/partial-trigger.smt2 regress0/quantifiers/proj-issue152-2-non-std-nterm-ext-rew.smt2 + regress0/quantifiers/proj-issue512-has-skolem.smt2 regress0/quantifiers/pure_dt_cbqi.smt2 regress0/quantifiers/qarray-sel-over-store.smt2 regress0/quantifiers/qbv-inequality2.smt2 @@ -2595,6 +2596,7 @@ set(regress_1_tests regress1/strings/issue7677-test-const-rv.smt2 regress1/strings/issue7918-learned-rewrite.smt2 regress1/strings/issue8094-witness-model.smt2 + regress1/strings/issue8347-has-skolem.smt2 regress1/strings/issue8434-nterm-str-rw.smt2 regress1/strings/kaluza-fl.smt2 regress1/strings/loop002.smt2 diff --git a/test/regress/cli/regress0/quantifiers/proj-issue512-has-skolem.smt2 b/test/regress/cli/regress0/quantifiers/proj-issue512-has-skolem.smt2 new file mode 100644 index 000000000..140e20734 --- /dev/null +++ b/test/regress/cli/regress0/quantifiers/proj-issue512-has-skolem.smt2 @@ -0,0 +1,6 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :fmf-bound true) +(declare-fun x (Bool Bool) Bool) +(assert (forall ((x4 Bool)) (x x4 (x false false)))) +(check-sat) diff --git a/test/regress/cli/regress1/strings/issue8347-has-skolem.smt2 b/test/regress/cli/regress1/strings/issue8347-has-skolem.smt2 new file mode 100644 index 000000000..68b096a1a --- /dev/null +++ b/test/regress/cli/regress1/strings/issue8347-has-skolem.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --strings-exp -i +; EXPECT: sat +(set-logic ALL) +(declare-fun uf6_2 (Bool Bool Bool Bool Bool Bool) Bool) +(declare-fun str2 () String) +(declare-fun str6 () String) +(assert (str.in_re str2 re.allchar)) +(assert (str.<= str2 str6)) +(check-sat) +(assert (uf6_2 true false true false false (str.<= str2 str6))) +(push)