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
#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"
Trigger::Trigger(QuantifiersEngine* qe, Node q, std::vector<Node>& 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();
++(qe->d_statistics.d_multi_triggers);
}
- // Notice() << "Trigger : " << (*this) << " for " << q << std::endl;
Trace("trigger-debug") << "Finished making trigger." << std::endl;
}
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"))
{
<< " lemmas, trigger was " << d_nodes << std::endl;
}
}
- return addedLemmas;
+ return gtAddedLemmas + addedLemmas;
}
bool Trigger::sendInstantiation(InstMatch& m)
return d_mg->getActiveScore( d_quantEngine );
}
+Node Trigger::ensureGroundTermPreprocessed(Valuation& val,
+ Node n,
+ std::vector<Node>& gts)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ std::unordered_map<TNode, Node, TNodeHashFunction> visited;
+ std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ std::vector<TNode> 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<Node> 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;
#include <map>
#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 {
* 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<Node>& gts);
/** The nodes comprising this trigger. */
- std::vector< Node > d_nodes;
+ std::vector<Node> 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<Node> d_groundTerms;
/** The quantifiers engine associated with this trigger. */
QuantifiersEngine* d_quantEngine;
/** The quantified formula this trigger is for. */
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
--- /dev/null
+(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)
+
--- /dev/null
+(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)
+
projects / cvc5.git / commitdiff