From 7f851ea2e2b40f7e5d6e0c0fbe4e9c6ea0450209 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 25 Jan 2021 11:11:02 -0600 Subject: [PATCH] Ensure uses of ground terms in triggers are preprocessed and registered (#5808) This ensures ground terms in triggers are preprocessed and registered in the master equality engine. This avoids cases where our E-matching algorithm is incomplete where it should not be. Positive impact (+222-69) on SMT-LIB, 30 second timeout --- src/theory/quantifiers/ematching/trigger.cpp | 97 ++++++++++++++++++- src/theory/quantifiers/ematching/trigger.h | 38 +++++++- test/regress/CMakeLists.txt | 2 + .../quantifiers/min-ppgt-em-incomplete.smt2 | 25 +++++ .../quantifiers/min-ppgt-em-incomplete2.smt2 | 37 +++++++ 5 files changed, 194 insertions(+), 5 deletions(-) create mode 100644 test/regress/regress1/quantifiers/min-ppgt-em-incomplete.smt2 create mode 100644 test/regress/regress1/quantifiers/min-ppgt-em-incomplete2.smt2 diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 34f413b71..ecd8164d5 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/ematching/trigger.h" #include "expr/node_algorithm.h" +#include "expr/skolem_manager.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/ematching/candidate_generator.h" #include "theory/quantifiers/ematching/ho_trigger.h" @@ -56,7 +57,14 @@ void TriggerTermInfo::init( Node q, Node n, int reqPol, Node reqPolEq ){ Trigger::Trigger(QuantifiersEngine* qe, Node q, std::vector& nodes) : d_quantEngine(qe), d_quant(q) { - d_nodes.insert( d_nodes.begin(), nodes.begin(), nodes.end() ); + // We must ensure that the ground subterms of the trigger have been + // preprocessed. + Valuation& val = qe->getValuation(); + for (const Node& n : nodes) + { + Node np = ensureGroundTermPreprocessed(val, n, d_groundTerms); + d_nodes.push_back(np); + } if (Trace.isOn("trigger")) { quantifiers::QuantAttributes* qa = d_quantEngine->getQuantAttributes(); @@ -92,7 +100,6 @@ Trigger::Trigger(QuantifiersEngine* qe, Node q, std::vector& nodes) ++(qe->d_statistics.d_multi_triggers); } - // Notice() << "Trigger : " << (*this) << " for " << q << std::endl; Trace("trigger-debug") << "Finished making trigger." << std::endl; } @@ -117,6 +124,26 @@ Node Trigger::getInstPattern() const uint64_t Trigger::addInstantiations() { + uint64_t gtAddedLemmas = 0; + if (!d_groundTerms.empty()) + { + // for each ground term t that does not exist in the equality engine, we + // add a purification lemma of the form (k = t). + eq::EqualityEngine* ee = d_quantEngine->getEqualityQuery()->getEngine(); + for (const Node& gt : d_groundTerms) + { + if (!ee->hasTerm(gt)) + { + SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); + Node k = sm->mkPurifySkolem(gt, "gt"); + Node eq = k.eqNode(gt); + Trace("trigger-gt-lemma") + << "Trigger: ground term purify lemma: " << eq << std::endl; + d_quantEngine->addLemma(eq); + gtAddedLemmas++; + } + } + } uint64_t addedLemmas = d_mg->addInstantiations(d_quant, d_quantEngine, this); if (Debug.isOn("inst-trigger")) { @@ -126,7 +153,7 @@ uint64_t Trigger::addInstantiations() << " lemmas, trigger was " << d_nodes << std::endl; } } - return addedLemmas; + return gtAddedLemmas + addedLemmas; } bool Trigger::sendInstantiation(InstMatch& m) @@ -999,6 +1026,70 @@ int Trigger::getActiveScore() { return d_mg->getActiveScore( d_quantEngine ); } +Node Trigger::ensureGroundTermPreprocessed(Valuation& val, + Node n, + std::vector& gts) +{ + NodeManager* nm = NodeManager::currentNM(); + std::unordered_map visited; + std::unordered_map::iterator it; + std::vector visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + it = visited.find(cur); + if (it == visited.end()) + { + if (cur.getNumChildren() == 0) + { + visited[cur] = cur; + } + else if (!quantifiers::TermUtil::hasInstConstAttr(cur)) + { + // cur has no INST_CONSTANT, thus is ground. + Node vcur = val.getPreprocessedTerm(cur); + gts.push_back(vcur); + visited[cur] = vcur; + } + else + { + visited[cur] = Node::null(); + visit.push_back(cur); + visit.insert(visit.end(), cur.begin(), cur.end()); + } + } + else if (it->second.isNull()) + { + Node ret = cur; + bool childChanged = false; + std::vector children; + if (cur.getMetaKind() == metakind::PARAMETERIZED) + { + children.push_back(cur.getOperator()); + } + for (const Node& cn : cur) + { + it = visited.find(cn); + Assert(it != visited.end()); + Assert(!it->second.isNull()); + childChanged = childChanged || cn != it->second; + children.push_back(it->second); + } + if (childChanged) + { + ret = nm->mkNode(cur.getKind(), children); + } + visited[cur] = ret; + } + } while (!visit.empty()); + Assert(visited.find(n) != visited.end()); + Assert(!visited.find(n)->second.isNull()); + return visited[n]; +} + void Trigger::debugPrint(const char* c) const { Trace(c) << "TRIGGER( " << d_nodes << " )" << std::endl; diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index 201d4258b..9fbf41674 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -20,8 +20,9 @@ #include #include "expr/node.h" -#include "theory/quantifiers/inst_match.h" #include "options/quantifiers_options.h" +#include "theory/quantifiers/inst_match.h" +#include "theory/valuation.h" namespace CVC4 { namespace theory { @@ -414,8 +415,41 @@ class Trigger { * Instantiate::addInstantiation(...). */ virtual bool sendInstantiation(InstMatch& m); + /** + * Ensure that all ground subterms of n have been preprocessed. This makes + * calls to the provided valuation to obtain the preprocessed form of these + * terms. The preprocessed form of each ground subterm is added to gts. + * + * As an optimization, this method does not preprocess terms with no + * arguments, e.g. variables and constants are not preprocessed (as they + * should not change after preprocessing), nor are they added to gts. + * + * @param val The valuation to use for looking up preprocessed terms. + * @param n The node to process, which is in inst-constant form (free + * variables have been substituted by corresponding INST_CONSTANT). + * @param gts The set of preprocessed ground subterms of n. + * @return The converted form of n where all ground subterms have been + * replaced by their preprocessed form. + */ + static Node ensureGroundTermPreprocessed(Valuation& val, + Node n, + std::vector& gts); /** The nodes comprising this trigger. */ - std::vector< Node > d_nodes; + std::vector d_nodes; + /** + * The preprocessed ground terms in the nodes of the trigger, which as an + * optimization omits variables and constant subterms. These terms are + * important since we must ensure that the quantifier-free solvers are + * aware of these terms. In particular, when adding instantiations for + * a trigger P(f(a), x), we first check if f(a) is a term in the master + * equality engine. If it is not, then we add the lemma k = f(a) where k + * is the purification skolem for f(a). This ensures that f(a) will be + * registered as a term in the master equality engine on the next + * instantiation round. This is particularly important for cases where + * P(f(a), x) is matched with P(f(b), c), where a=b in the current context. + * This example would fail to match when f(a) is not registered. + */ + std::vector d_groundTerms; /** The quantifiers engine associated with this trigger. */ QuantifiersEngine* d_quantEngine; /** The quantified formula this trigger is for. */ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index da4c6633b..cf4b0386d 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1762,6 +1762,8 @@ set(regress_1_tests regress1/quantifiers/javafe.ast.StmtVec.009.smt2 regress1/quantifiers/lia-witness-div-pp.smt2 regress1/quantifiers/lra-vts-inf.smt2 + regress1/quantifiers/min-ppgt-em-incomplete.smt2 + regress1/quantifiers/min-ppgt-em-incomplete2.smt2 regress1/quantifiers/mix-coeff.smt2 regress1/quantifiers/mutualrec2.cvc regress1/quantifiers/nested9_true-unreach-call.i_575.smt2 diff --git a/test/regress/regress1/quantifiers/min-ppgt-em-incomplete.smt2 b/test/regress/regress1/quantifiers/min-ppgt-em-incomplete.smt2 new file mode 100644 index 000000000..2f86a2764 --- /dev/null +++ b/test/regress/regress1/quantifiers/min-ppgt-em-incomplete.smt2 @@ -0,0 +1,25 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-sort S 0) +(declare-datatypes ((Y 0) (St 0)) (((err)) ((t (|v#t| S) (|l#t| Int))))) +(declare-sort Q 0) +(declare-datatypes ((T 0) (TArray 0)) (((b (B Bool)) (D (add Int)) (Vec (vec TArray))) ((zValueArray (R Q))))) +(declare-sort U 0) +(declare-datatypes ((Sm 0)) (((m (cm U))))) +(declare-fun O (Y) S) +(declare-fun s (T T) Bool) +(declare-fun j (Q Int) T) +(declare-fun K (S Int Y) S) +(declare-fun r () Int) +(declare-fun c () Int) +(declare-fun h (U St Int) T) +(declare-fun a () Sm) +(declare-fun e () T) +(declare-fun l () T) +(declare-fun n () Y) +(assert (forall ((v T) (v2 T)) (! (or (= v v2) (not (s v v2))) :qid Q1))) +(assert (B (b (s l (j (R (vec (h (cm a) (t (K (O err) 0 n) 1) (add (D 1))))) r))))) +(assert (forall ((i Int)) (! (not (s e (j (R (vec (j (R (vec l)) c))) i))) :qid Q2))) +(assert (exists ((z Int)) (! (B (b (s e (j (R (vec (j (R (vec (j (R (vec (h (cm a) (t (K (O err) 0 n) 1) (add (D 1))))) r))) c))) z)))) :qid Q3))) +(check-sat) + diff --git a/test/regress/regress1/quantifiers/min-ppgt-em-incomplete2.smt2 b/test/regress/regress1/quantifiers/min-ppgt-em-incomplete2.smt2 new file mode 100644 index 000000000..8f31750b2 --- /dev/null +++ b/test/regress/regress1/quantifiers/min-ppgt-em-incomplete2.smt2 @@ -0,0 +1,37 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-sort U 0) +(declare-datatypes ((D 0) (T@t 0)) (((err)) ((t (|v#t| U) (|l#t| Int))))) +(declare-sort V 0) +(declare-datatypes ((T 0) (TArray 0)) (((E) (b (B Bool)) (A (add Int)) (Vec (vec TArray))) ((Var (R V) (|l#Var| Int))))) +(declare-sort B 0) +(declare-datatypes ((M 0)) (((Mem (cm B))))) +(declare-fun mc (D) U) +(declare-fun eq (T T) Bool) +(declare-fun s (V Int) T) +(declare-fun sto (V Int T) V) +(declare-fun sel (B T@t Int) T) +(declare-fun c () T) +(declare-fun in () M) +(declare-fun rdv () T) +(declare-fun ivp () T) +(declare-fun ex () T) +(declare-fun cdv () T) +(assert (forall ((z T) (y T)) (! (or (= z y) (not (eq z y))) :qid Q1))) +(assert (forall ((?x0 V) (?x1 Int) (?x2 T)) (! (= ?x2 (s (sto ?x0 ?x1 ?x2) ?x1)) :qid Q2))) +(declare-fun k1 () Bool) +(declare-fun k2 () Bool) +(assert (and +(is-Vec ex) +(not + (and + (not (= ex E)) + (or + (not (= rdv (b false))) + (not (= ivp (Vec (Var (sto (R (vec cdv)) (|l#Var| (vec cdv)) c) 0)))) + (not (= rdv (b k1))) + (not (B (b k2)))))))) +(assert (= k1 (not (forall ((j Int)) (! (not (eq c (s (R (vec ivp)) j))) :qid Q3))))) +(assert (= k2 (not (forall (($i_0 Int)) (! (not (B (b (eq c (s (R (vec (s (R (vec (s (R (vec (sel (cm in) (t (mc err) 1) (add (A 0))))) 0))) 0))) $i_0))))) :qid Q4))))) +(check-sat) + -- 2.30.2