* Higher-order instantiation.
* Add missing files.
* Document inst match generators, make collectHoVarApplyTerms iterative.
* More documentation.
* More documentation.
* More documentation.
* More documentation
* Refactoring, documentation.
* More documentation.
* Fix comment, reference issue.
* More documentation. Fix ho trigger for the changes from master.
* Minor
* More documentation.
* More documentation.
* More
* More documentation, make indexing and lookup in TriggerTrie iterative instead of recursive.
* More
* Minor improvements to comments.
* Remove an unimplemented optimization from an old version of cached multi-trigger matching. Update and improve documentation in inst match generator.
* Improve documentation for ho_trigger.
* Update ho trigger to not access now private member of TermDb.
* Address comments.
* Address
* Clang format
theory/quantifiers/fun_def_engine.h \
theory/quantifiers/fun_def_process.cpp \
theory/quantifiers/fun_def_process.h \
+ theory/quantifiers/ho_trigger.cpp \
+ theory/quantifiers/ho_trigger.h \
theory/quantifiers/inst_match.cpp \
theory/quantifiers/inst_match.h \
theory/quantifiers/inst_match_generator.cpp \
QCF_PARTIAL,
};
-enum UserPatMode {
- /** use but do not trust */
+/** User pattern mode.
+*
+* These modes determine how user provided patterns (triggers) are
+* used during E-matching. The modes vary on when instantiation based on
+* user-provided triggers is combined with instantiation based on
+* automatically selected triggers.
+*/
+enum UserPatMode
+{
+ /** First instantiate based on user-provided triggers. If no instantiations
+ * are produced, use automatically selected triggers.
+ */
USER_PAT_MODE_USE,
- /** default, if patterns are supplied for a quantifier, use only those */
+ /** Default, if triggers are supplied for a quantifier, use only those. */
USER_PAT_MODE_TRUST,
- /** resort to user patterns only when necessary */
+ /** Resort to user triggers only when no instantiations are
+ * produced by automatically selected triggers
+ */
USER_PAT_MODE_RESORT,
- /** ignore user patterns */
+ /** Ignore user patterns. */
USER_PAT_MODE_IGNORE,
- /** interleave use/resort for user patterns */
+ /** Interleave use/resort modes for quantified formulas with user patterns. */
USER_PAT_MODE_INTERLEAVE,
};
+/** Trigger selection mode.
+*
+* These modes are used for determining which terms to select
+* as triggers for quantified formulas, when necessary, during E-matching.
+* In the following, note the following terminology. A trigger is a set of terms,
+* where a single trigger is a singleton set and a multi-trigger is a set of more
+* than one term.
+*
+* TRIGGER_SEL_MIN selects single triggers of minimal term size.
+* TRIGGER_SEL_MAX selects single triggers of maximal term size.
+*
+* For example, consider the quantified formula :
+* forall xy. P( f( g( x, y ) ) ) V Q( f( x ), y )
+*
+* TRIGGER_SEL_MIN will select g( x, y ) and Q( f( x ), y ).
+* TRIGGER_SEL_MAX will select P( f( g( x ) ) ) and Q( f( x ), y ).
+*
+* The remaining three trigger selections make a difference for multi-triggers
+* only. For quantified formulas that require multi-triggers, we build a set of
+* partial triggers that don't contain all variables, call this set S. Then,
+* multi-triggers are built by taking a random subset of S that collectively
+* contains all variables.
+*
+* Consider the quantified formula :
+* forall xyz. P( h( x ), y ) V Q( y, z )
+*
+* For TRIGGER_SEL_ALL and TRIGGER_SEL_MIN_SINGLE_ALL,
+* S = { h( x ), P( h( x ), y ), Q( y, z ) }.
+* For TRIGGER_SEL_MIN_SINGLE_MAX,
+* S = { P( h( x ), y ), Q( y, z ) }.
+*
+* Furthermore, TRIGGER_SEL_MIN_SINGLE_ALL and TRIGGER_SEL_MIN_SINGLE_MAX, when
+* selecting single triggers, only select terms of minimal size.
+*/
enum TriggerSelMode {
/** only consider minimal terms for triggers */
TRIGGER_SEL_MIN,
--- /dev/null
+/********************* */
+/*! \file ho_trigger.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of higher-order trigger class
+ **/
+
+#include <stack>
+
+#include "theory/quantifiers/ho_trigger.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/theory_engine.h"
+#include "theory/uf/equality_engine.h"
+#include "theory/uf/theory_uf_rewriter.h"
+#include "util/hash.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace inst {
+
+HigherOrderTrigger::HigherOrderTrigger(
+ QuantifiersEngine* qe,
+ Node q,
+ std::vector<Node>& nodes,
+ std::map<Node, std::vector<Node> >& ho_apps)
+ : Trigger(qe, q, nodes), d_ho_var_apps(ho_apps)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ // process the higher-order variable applications
+ for (std::pair<const Node, std::vector<Node> >& as : d_ho_var_apps)
+ {
+ Node n = as.first;
+ d_ho_var_list.push_back(n);
+ TypeNode tn = n.getType();
+ Assert(tn.isFunction());
+ if (Trace.isOn("ho-quant-trigger"))
+ {
+ Trace("ho-quant-trigger") << " have " << as.second.size();
+ Trace("ho-quant-trigger") << " patterns with variable operator " << n
+ << ":" << std::endl;
+ for (unsigned j = 0; j < as.second.size(); j++)
+ {
+ Trace("ho-quant-trigger") << " " << as.second[j] << std::endl;
+ }
+ }
+ if (d_ho_var_types.find(tn) == d_ho_var_types.end())
+ {
+ Trace("ho-quant-trigger") << " type " << tn
+ << " needs higher-order matching." << std::endl;
+ d_ho_var_types.insert(tn);
+ }
+ // make the bound variable lists
+ d_ho_var_bvl[n] = nm->getBoundVarListForFunctionType(tn);
+ for (const Node& nc : d_ho_var_bvl[n])
+ {
+ d_ho_var_bvs[n].push_back(nc);
+ }
+ }
+}
+
+HigherOrderTrigger::~HigherOrderTrigger() {}
+void HigherOrderTrigger::collectHoVarApplyTerms(
+ Node q, TNode n, std::map<Node, std::vector<Node> >& apps)
+{
+ std::vector<Node> ns;
+ ns.push_back(n);
+ collectHoVarApplyTerms(q, ns, apps);
+}
+
+void HigherOrderTrigger::collectHoVarApplyTerms(
+ Node q, std::vector<Node>& ns, std::map<Node, std::vector<Node> >& apps)
+{
+ std::unordered_set<TNode, TNodeHashFunction> visited;
+ // whether the visited node is a child of a HO_APPLY chain
+ std::unordered_map<TNode, bool, TNodeHashFunction> withinApply;
+ std::stack<TNode> visit;
+ TNode cur;
+ for (unsigned i = 0; i < ns.size(); i++)
+ {
+ visit.push(ns[i]);
+ withinApply[ns[i]] = false;
+ do
+ {
+ cur = visit.top();
+ visit.pop();
+
+ if (visited.find(cur) == visited.end())
+ {
+ visited.insert(cur);
+ bool curWithinApply = withinApply[cur];
+ if (!curWithinApply)
+ {
+ TNode op;
+ if (cur.getKind() == kind::APPLY_UF)
+ {
+ // could be a fully applied function variable
+ op = cur.getOperator();
+ }
+ else if (cur.getKind() == kind::HO_APPLY)
+ {
+ op = cur;
+ while (op.getKind() == kind::HO_APPLY)
+ {
+ op = op[0];
+ }
+ }
+ if (!op.isNull())
+ {
+ if (op.getKind() == kind::INST_CONSTANT)
+ {
+ Assert(quantifiers::TermUtil::getInstConstAttr(cur) == q);
+ Trace("ho-quant-trigger-debug")
+ << "Ho variable apply term : " << cur << " with head " << op
+ << std::endl;
+ Node app = cur;
+ if (app.getKind() == kind::APPLY_UF)
+ {
+ // for consistency, convert to HO_APPLY if fully applied
+ app = uf::TheoryUfRewriter::getHoApplyForApplyUf(app);
+ }
+ apps[op].push_back(cur);
+ }
+ if (cur.getKind() == kind::HO_APPLY)
+ {
+ curWithinApply = true;
+ }
+ }
+ }
+ else
+ {
+ if (cur.getKind() != HO_APPLY)
+ {
+ curWithinApply = false;
+ }
+ }
+ // do not look in nested quantifiers
+ if (cur.getKind() != FORALL)
+ {
+ for (unsigned i = 0, size = cur.getNumChildren(); i < size; i++)
+ {
+ withinApply[cur[i]] = curWithinApply && i == 0;
+ visit.push(cur[i]);
+ }
+ }
+ }
+ } while (!visit.empty());
+ }
+}
+
+int HigherOrderTrigger::addInstantiations(InstMatch& baseMatch)
+{
+ // call the base class implementation
+ int addedFoLemmas = Trigger::addInstantiations(baseMatch);
+ // also adds predicate lemms to force app completion
+ int addedHoLemmas = addHoTypeMatchPredicateLemmas();
+ return addedHoLemmas + addedFoLemmas;
+}
+
+bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
+{
+ if (options::hoMatching())
+ {
+ // get substitution corresponding to m
+ std::vector<TNode> vars;
+ std::vector<TNode> subs;
+ for (unsigned i = 0, size = d_f[0].getNumChildren(); i < size; i++)
+ {
+ subs.push_back(m.d_vals[i]);
+ vars.push_back(
+ d_quantEngine->getTermUtil()->getInstantiationConstant(d_f, i));
+ }
+
+ Trace("ho-unif-debug") << "Run higher-order unification..." << std::endl;
+
+ // get the substituted form of all variable-operator ho application terms
+ std::map<TNode, std::vector<Node> > ho_var_apps_subs;
+ for (std::pair<const Node, std::vector<Node> >& ha : d_ho_var_apps)
+ {
+ TNode var = ha.first;
+ for (unsigned j = 0, size = ha.second.size(); j < size; j++)
+ {
+ TNode app = ha.second[j];
+ Node sapp =
+ app.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
+ ho_var_apps_subs[var].push_back(sapp);
+ Trace("ho-unif-debug") << " app[" << var << "] : " << app << " -> "
+ << sapp << std::endl;
+ }
+ }
+
+ // compute argument vectors for each variable
+ d_lchildren.clear();
+ d_arg_to_arg_rep.clear();
+ d_arg_vector.clear();
+ EqualityQuery* eq = d_quantEngine->getEqualityQuery();
+ for (std::pair<const TNode, std::vector<Node> >& ha : ho_var_apps_subs)
+ {
+ TNode var = ha.first;
+ unsigned vnum = var.getAttribute(InstVarNumAttribute());
+ Node value = m.d_vals[vnum];
+ Trace("ho-unif-debug") << " val[" << var << "] = " << value << std::endl;
+
+ Trace("ho-unif-debug2") << "initialize lambda information..."
+ << std::endl;
+ // initialize the lambda children
+ d_lchildren[vnum].push_back(value);
+ std::map<TNode, std::vector<Node> >::iterator ithb =
+ d_ho_var_bvs.find(var);
+ Assert(ithb != d_ho_var_bvs.end());
+ d_lchildren[vnum].insert(
+ d_lchildren[vnum].end(), ithb->second.begin(), ithb->second.end());
+
+ Trace("ho-unif-debug2") << "compute fixed arguments..." << std::endl;
+ // compute for each argument if it is only applied to a fixed value modulo
+ // equality
+ std::map<unsigned, Node> fixed_vals;
+ for (unsigned i = 0; i < ha.second.size(); i++)
+ {
+ std::vector<TNode> args;
+ Node f = uf::TheoryUfRewriter::decomposeHoApply(ha.second[i], args);
+ // Assert( f==value );
+ for (unsigned k = 0, size = args.size(); k < size; k++)
+ {
+ Node val = args[k];
+ std::map<unsigned, Node>::iterator itf = fixed_vals.find(k);
+ if (itf == fixed_vals.end())
+ {
+ fixed_vals[k] = val;
+ }
+ else if (!itf->second.isNull())
+ {
+ if (!eq->areEqual(itf->second, args[k]))
+ {
+ if (!d_quantEngine->getTermDatabase()->isEntailed(
+ itf->second.eqNode(args[k]), true, eq))
+ {
+ fixed_vals[k] = Node::null();
+ }
+ }
+ }
+ }
+ }
+ if (Trace.isOn("ho-unif-debug"))
+ {
+ for (std::map<unsigned, Node>::iterator itf = fixed_vals.begin();
+ itf != fixed_vals.end();
+ ++itf)
+ {
+ Trace("ho-unif-debug") << " arg[" << var << "][" << itf->first
+ << "] : " << itf->second << std::endl;
+ }
+ }
+
+ // now construct argument vectors
+ Trace("ho-unif-debug2") << "compute argument vectors..." << std::endl;
+ std::map<Node, unsigned> arg_to_rep;
+ for (unsigned index = 0, size = ithb->second.size(); index < size;
+ index++)
+ {
+ Node bv_at_index = ithb->second[index];
+ std::map<unsigned, Node>::iterator itf = fixed_vals.find(index);
+ Trace("ho-unif-debug") << " * arg[" << var << "][" << index << "]";
+ if (itf != fixed_vals.end())
+ {
+ if (!itf->second.isNull())
+ {
+ Node r = eq->getRepresentative(itf->second);
+ std::map<Node, unsigned>::iterator itfr = arg_to_rep.find(r);
+ if (itfr != arg_to_rep.end())
+ {
+ d_arg_to_arg_rep[vnum][index] = itfr->second;
+ // function applied to equivalent values at multiple arguments,
+ // can permute variables
+ d_arg_vector[vnum][itfr->second].push_back(bv_at_index);
+ Trace("ho-unif-debug") << " = { self } ++ arg[" << var << "]["
+ << itfr->second << "]" << std::endl;
+ }
+ else
+ {
+ arg_to_rep[r] = index;
+ // function applied to single value, can either use variable or
+ // value at this argument position
+ d_arg_vector[vnum][index].push_back(bv_at_index);
+ d_arg_vector[vnum][index].push_back(itf->second);
+ if (!options::hoMatchingVarArgPriority())
+ {
+ std::reverse(d_arg_vector[vnum][index].begin(),
+ d_arg_vector[vnum][index].end());
+ }
+ Trace("ho-unif-debug") << " = { self, " << itf->second << " } "
+ << std::endl;
+ }
+ }
+ else
+ {
+ // function is applied to disequal values, can only use variable at
+ // this argument position
+ d_arg_vector[vnum][index].push_back(bv_at_index);
+ Trace("ho-unif-debug") << " = { self } (disequal)" << std::endl;
+ }
+ }
+ else
+ {
+ // argument is irrelevant to matching, assume identity variable
+ d_arg_vector[vnum][index].push_back(bv_at_index);
+ Trace("ho-unif-debug") << " = { self } (irrelevant)" << std::endl;
+ }
+ }
+ Trace("ho-unif-debug2") << "finished." << std::endl;
+ }
+
+ return sendInstantiation(m, 0);
+ }
+ else
+ {
+ // do not run higher-order matching
+ return d_quantEngine->addInstantiation(d_f, m);
+ }
+}
+
+// recursion depth limited by number of arguments of higher order variables
+// occurring as pattern operators (very small)
+bool HigherOrderTrigger::sendInstantiation(InstMatch& m, unsigned var_index)
+{
+ if (var_index == d_ho_var_list.size())
+ {
+ // we now have an instantiation to try
+ return d_quantEngine->addInstantiation(d_f, m);
+ }
+ else
+ {
+ Node var = d_ho_var_list[var_index];
+ unsigned vnum = var.getAttribute(InstVarNumAttribute());
+ Assert(vnum < m.d_vals.size());
+ Node value = m.d_vals[vnum];
+ Assert(d_lchildren[vnum][0] == value);
+ Assert(d_ho_var_bvl.find(var) != d_ho_var_bvl.end());
+
+ // now, recurse on arguments to enumerate equivalent matching lambda
+ // expressions
+ bool ret =
+ sendInstantiationArg(m, var_index, vnum, 0, d_ho_var_bvl[var], false);
+
+ // reset the value
+ m.d_vals[vnum] = value;
+
+ return ret;
+ }
+}
+
+bool HigherOrderTrigger::sendInstantiationArg(InstMatch& m,
+ unsigned var_index,
+ unsigned vnum,
+ unsigned arg_index,
+ Node lbvl,
+ bool arg_changed)
+{
+ if (arg_index == lbvl.getNumChildren())
+ {
+ // construct the lambda
+ if (arg_changed)
+ {
+ Node body =
+ NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_lchildren[vnum]);
+ Node lam = NodeManager::currentNM()->mkNode(kind::LAMBDA, lbvl, body);
+ m.d_vals[vnum] = lam;
+ Trace("ho-unif-debug2") << " try " << vnum << " -> " << lam << std::endl;
+ }
+ return sendInstantiation(m, var_index + 1);
+ }
+ else
+ {
+ std::map<unsigned, unsigned>::iterator itr =
+ d_arg_to_arg_rep[vnum].find(arg_index);
+ unsigned rindex =
+ itr != d_arg_to_arg_rep[vnum].end() ? itr->second : arg_index;
+ std::map<unsigned, std::vector<Node> >::iterator itv =
+ d_arg_vector[vnum].find(rindex);
+ Assert(itv != d_arg_vector[vnum].end());
+ Node prev = lbvl[arg_index];
+ bool ret = false;
+ // try each argument in the vector
+ for (unsigned i = 0, size = itv->second.size(); i < size; i++)
+ {
+ bool new_arg_changed = arg_changed || prev != itv->second[i];
+ d_lchildren[vnum][arg_index + 1] = itv->second[i];
+ if (sendInstantiationArg(
+ m, var_index, vnum, arg_index + 1, lbvl, new_arg_changed))
+ {
+ ret = true;
+ break;
+ }
+ }
+ // clean up
+ d_lchildren[vnum][arg_index + 1] = prev;
+ return ret;
+ }
+}
+
+int HigherOrderTrigger::addHoTypeMatchPredicateLemmas()
+{
+ unsigned numLemmas = 0;
+ if (!d_ho_var_types.empty())
+ {
+ // this forces expansion of APPLY_UF terms to curried HO_APPLY chains
+ unsigned size = d_quantEngine->getTermDatabase()->getNumOperators();
+ for (unsigned j = 0; j < size; j++)
+ {
+ Node f = d_quantEngine->getTermDatabase()->getOperator(j);
+ if (f.isVar())
+ {
+ TypeNode tn = f.getType();
+ if (d_ho_var_types.find(tn) != d_ho_var_types.end())
+ {
+ Node u = d_quantEngine->getTermUtil()->getHoTypeMatchPredicate(tn);
+ Node au = NodeManager::currentNM()->mkNode(kind::APPLY_UF, u, f);
+ if (d_quantEngine->addLemma(au))
+ {
+ // this forces f to be a first-class member of the quantifier-free
+ // equality engine,
+ // which in turn forces the quantifier-free theory solver to expand
+ // it to HO_APPLY
+ Trace("ho-quant") << "Added ho match predicate lemma : " << au
+ << std::endl;
+ numLemmas++;
+ }
+ }
+ }
+ }
+ }
+ return numLemmas;
+}
+
+} /* CVC4::theory::inst namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file ho_trigger.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief higher-order trigger class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H
+#define __CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H
+
+#include <map>
+#include <unordered_set>
+
+#include "expr/node.h"
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/inst_match.h"
+#include "theory/quantifiers/trigger.h"
+
+namespace CVC4 {
+namespace theory {
+namespace inst {
+
+class Trigger;
+
+/** HigherOrder trigger
+ *
+ * This extends the trigger class with techniques that post-process
+ * instantiations, specified by InstMatch objects, according to a variant of
+ * Huet's algorithm. For details, see Chapter 16 of the Handbook of Automated
+ * Reasoning (vol. 2), by Gilles Dowek.
+ *
+ * The main difference between HigherOrderTrigger and Trigger is the function
+ * sendInstantiation(...). Recall that this function is called when its
+ * underlying IMGenerator generates an InstMatch m using E-matching technique.
+ * We enumerate additional instantiations based on m, when the domain of m
+ * contains variables of function type.
+ *
+ * Examples below (f, x, y are universal variables):
+ *
+ * (EX1): (f x y) matches (k 0 1) in standard E-matching with:
+ *
+ * f -> k, x -> 0, y -> 1
+ *
+ * This match is extended to four possible solutions by this class:
+ *
+ * f -> \ xy. (k x y), x -> 0, y -> 1
+ * f -> \ xy. (k 0 y), x -> 0, y -> 1
+ * f -> \ xy. (k x 1), x -> 0, y -> 1
+ * f -> \ xy. (k 0 1), x -> 0, y -> 1
+ *
+ *
+ * (EX2): Similarly, (f x y) matches (k 0 0) with possible solutions:
+ *
+ * f -> \ xy. (k x x), x -> 0, y -> 0
+ * f -> \ xy. (k y x), x -> 0, y -> 0
+ * f -> \ xy. (k 0 x), x -> 0, y -> 0
+ * f -> \ xy. (k x y), x -> 0, y -> 0
+ * f -> \ xy. (k y y), x -> 0, y -> 0
+ * f -> \ xy. (k 0 y), x -> 0, y -> 0
+ * f -> \ xy. (k x 0), x -> 0, y -> 0
+ * f -> \ xy. (k y 0), x -> 0, y -> 0
+ * f -> \ xy. (k 0 0), x -> 0, y -> 0
+ *
+ *
+ * (EX3): (f x y), (f x z) simultaneously match (k 0 1), (k 0 2) with possible
+ * solutions:
+ *
+ * f -> \ xy. (k x y), x -> 0, y -> 1, z -> 2
+ * f -> \ xy. (k 0 y), x -> 0, y -> 1, z -> 2
+ *
+ *
+ * This class enumerates the lists above until one instantiation of that form is
+ * successfully added via a call to Instantiate::addInstantiation(...)
+ *
+ *
+ * It also implements a way of forcing APPLY_UF to expand to curried HO_APPLY to
+ * handle a corner case where there are no matchable ground terms
+ * (addHoTypeMatchPredicateLemmas).
+ *
+ */
+class HigherOrderTrigger : public Trigger
+{
+ friend class Trigger;
+
+ private:
+ HigherOrderTrigger(QuantifiersEngine* qe,
+ Node q,
+ std::vector<Node>& nodes,
+ std::map<Node, std::vector<Node> >& ho_apps);
+ virtual ~HigherOrderTrigger();
+
+ public:
+ /** Collect higher order var apply terms
+ *
+ * Collect all top-level HO_APPLY terms in n whose head is a variable in
+ * quantified formula q. Append all such terms in apps.
+ */
+ static void collectHoVarApplyTerms(Node q,
+ TNode n,
+ std::map<Node, std::vector<Node> >& apps);
+ /** Collect higher order var apply terms
+ *
+ * Collect all top-level HO_APPLY terms in terms ns whose head is a variable
+ * in quantified formula q, store in apps.
+ */
+ static void collectHoVarApplyTerms(Node q,
+ std::vector<Node>& ns,
+ std::map<Node, std::vector<Node> >& apps);
+ /** add all available instantiations, based on the current context
+ *
+ * Extends Trigger::addInstantiations to also send
+ * lemmas based on addHoTypeMatchPredicateLemmas.
+ */
+ virtual int addInstantiations(InstMatch& baseMatch) override;
+
+ protected:
+ /**
+ * Map from function-typed variables to their applications in the quantified
+ * formula d_f (member of Trigger).
+ */
+ std::map<Node, std::vector<Node> > d_ho_var_apps;
+ /**
+ * List of all function-typed variables that occur as the head of function
+ * applications in d_f.
+ */
+ std::vector<Node> d_ho_var_list;
+ /**
+ * Cached bound variables and bound variable list for each variable of
+ * function type. These are used for constructing lambda terms in
+ * instantiations.
+ */
+ std::map<TNode, std::vector<Node> > d_ho_var_bvs;
+ std::map<TNode, Node> d_ho_var_bvl;
+ /** the set of types of ho variables */
+ std::unordered_set<TypeNode, TypeNodeHashFunction> d_ho_var_types;
+ /** add higher-order type predicate lemmas
+ *
+ * Adds lemmas of the form P( f ), where P is the predicate
+ * returned by TermUtil::getHoTypeMatchPredicate( f.getType() ).
+ * These lemmas force certain functions f of type tn to appear as
+ * first-class terms in the quantifier-free UF solver, where recall a
+ * first-class term is one that occurs as an (external) term in its equality
+ * engine. These functions f are all operators that have at least one
+ * term f(t1...tn) indexed by TermDabatase and are such that
+ * f's type is the same as a function-typed variable we
+ * are considering in this class (in d_ho_var_apps).
+ *
+ * TODO: we may eliminate this based on how github issue #1115 is resolved.
+ */
+ int addHoTypeMatchPredicateLemmas();
+ /** send instantiation
+ *
+ * Sends an instantiation that is equivalent to m via
+ * Instantiate::addInstantiation(...). This method may modify m based on
+ * imitations and projections (Huet's algorithm), if m was generated by
+ * matching ground terms to function applications with variable heads.
+ * See examples (EX1)-(EX3) above.
+ */
+ virtual bool sendInstantiation(InstMatch& m);
+
+ private:
+ //-------------------- current information about the match
+ /**
+ * Map from variable position to the arguments of the lambda we generated
+ * for that variable.
+ *
+ * For example (EX4), take a quantified formula:
+ * forall x f1 y f2. (...)
+ * Say we generated the match:
+ * x -> 0
+ * f1 -> k1
+ * y -> 1
+ * f2 -> k2
+ * z -> 0
+ * where we matched
+ * (f1 x y) with (k1 0 1) and
+ * (f2 x z) with (k2 0 0)
+ * Then the algorithm implemented by this class may modify the match to:
+ * x -> 0
+ * f1 -> (\ x1 x2. (k1 x1 1))
+ * y -> 1
+ * f2 -> (\ x1 x2. (k2 0 x1))
+ * z -> 0
+ *
+ * In the above (modified) match, the contents of d_lchildren are:
+ * 1 -> { k1, x1, 1 }
+ * 3 -> { k2, 0, x1 }
+ */
+ std::map<unsigned, std::vector<Node> > d_lchildren;
+ /** map from variable position to the representative variable position.
+ * Used when two argument positions of a match are mapped to equal terms.
+ *
+ * In the above example (EX4), the first and second arguments of
+ * the match for f2 are equal. Thus, in the above example,
+ * we have that d_arg_to_arg_rep is:
+ * 1 -> { 0 -> 0, 1 -> 1 }
+ * 3 -> { 0 -> 0, 1 -> 0 }
+ * In other words, the first argument
+ */
+ std::map<unsigned, std::map<unsigned, unsigned> > d_arg_to_arg_rep;
+ /** map from representative argument positions to the equivalence class
+ * of argument positions. In the above example (EX4), d_arg_vector is:
+ * 1 -> { 0 -> { 0 }, 1 -> { 1 } }
+ * 3 -> { 0 -> { 0, 1 } }
+ */
+ std::map<unsigned, std::map<unsigned, std::vector<Node> > > d_arg_vector;
+ //-------------------- end current information about the match
+
+ /** higher-order pattern unification algorithm
+ *
+ * Sends an instantiation that is equivalent to m via
+ * d_quantEngine->addInstantiation(...),
+ * based on Huet's algorithm.
+ *
+ * This is a helper function of sendInstantiation( m ) above.
+ *
+ * var_index is the index of the variable in m that we are currently processing
+ * i.e. we are processing the var_index^{th} higher-order variable.
+ *
+ * For example, say we are processing the match from (EX4) above.
+ * when var_index = 0,1, we are processing possibilities for
+ * instantiation of f1,f2 respectively.
+ */
+ bool sendInstantiation(InstMatch& m, unsigned var_index);
+ /** higher-order pattern unification algorithm
+ * Sends an instantiation that is equivalent to m via
+ * d_quantEngine->addInstantiation(...).
+ * This is a helper function of sendInstantiation( m, var_index ) above.
+ *
+ * var_index is the index of the variable in m that we are currently
+ * processing
+ * i.e. we are processing the var_index^{th} higher-order variable.
+ * vnum maps var_index to the actual variable number in m
+ * arg_index is the argument of the lambda term we are currently considering
+ * lbvl is the bound variable list associated with the term in m we are
+ * currently modifying
+ * arg_changed is whether we have modified m.
+ *
+ * For example, say we have modified our match from (EX4) to:
+ * x -> 0
+ * f1 -> (\ x1 x2. (k1 x1 1))
+ * y -> 1
+ * f2 -> (\ x1 x2. (k2 0 ?))
+ * z -> 0
+ * That is, we are currently considering possibilities for the second
+ * argument of the body for f2.
+ * Then:
+ * var_index = 1,
+ * vnum = 3 (f2 is the 3^rd variable of our quantified formula)
+ * arg_index = 1,
+ * lbvl is d_ho_var_bvl[f2], and
+ * arg_changed is true, since we modified at least one previous
+ * argument of f1 or f2.
+ */
+ bool sendInstantiationArg(InstMatch& m,
+ unsigned var_index,
+ unsigned vnum,
+ unsigned arg_index,
+ Node lbvl,
+ bool arg_changed);
+};
+
+} /* CVC4::theory::inst namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H */
namespace theory {
namespace inst {
+bool IMGenerator::sendInstantiation(Trigger* tparent, InstMatch& m)
+{
+ return tparent->sendInstantiation(m);
+}
+
InstMatchGenerator::InstMatchGenerator( Node pat ){
d_cg = NULL;
d_needsReset = true;
- d_active_add = false;
+ d_active_add = true;
Assert( quantifiers::TermUtil::hasInstConstAttr(pat) );
d_pattern = pat;
d_match_pattern = pat;
InstMatchGenerator::InstMatchGenerator() {
d_cg = NULL;
d_needsReset = true;
- d_active_add = false;
+ d_active_add = true;
d_next = NULL;
d_matchPolicy = MATCH_GEN_DEFAULT;
d_independent_gen = false;
d_match_pattern_op = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
//now, collect children of d_match_pattern
- for( unsigned i=0; i<d_match_pattern.getNumChildren(); i++ ){
- Node qa = quantifiers::TermUtil::getInstConstAttr(d_match_pattern[i]);
- if( !qa.isNull() ){
- InstMatchGenerator * cimg = Trigger::getInstMatchGenerator( q, d_match_pattern[i] );
- if( cimg ){
- d_children.push_back( cimg );
- d_children_index.push_back( i );
- d_children_types.push_back( 1 );
- }else{
- if( d_match_pattern[i].getKind()==INST_CONSTANT && qa==q ){
- d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute());
- d_children_types.push_back( 0 );
+ if (d_match_pattern.getKind() == INST_CONSTANT)
+ {
+ d_var_num[0] = d_match_pattern.getAttribute(InstVarNumAttribute());
+ }
+ else
+ {
+ for (unsigned i = 0, size = d_match_pattern.getNumChildren(); i < size;
+ i++)
+ {
+ Node qa = quantifiers::TermUtil::getInstConstAttr(d_match_pattern[i]);
+ if (!qa.isNull())
+ {
+ InstMatchGenerator* cimg =
+ getInstMatchGenerator(q, d_match_pattern[i]);
+ if (cimg)
+ {
+ d_children.push_back(cimg);
+ d_children_index.push_back(i);
+ d_children_types.push_back(1);
}else{
- d_children_types.push_back( -1 );
+ if (d_match_pattern[i].getKind() == INST_CONSTANT && qa == q)
+ {
+ d_var_num[i] =
+ d_match_pattern[i].getAttribute(InstVarNumAttribute());
+ d_children_types.push_back(0);
+ }
+ else
+ {
+ d_children_types.push_back(-1);
+ }
}
}
- }else{
- d_children_types.push_back( -1 );
+ else
+ {
+ d_children_types.push_back(-1);
+ }
}
}
- if( d_match_pattern.getKind()==INST_CONSTANT ){
- d_var_num[0] = d_match_pattern.getAttribute(InstVarNumAttribute());
- }
//create candidate generator
if( Trigger::isAtomicTrigger( d_match_pattern ) ){
}
/** get match (not modulo equality) */
-int InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngine* qe ){
+int InstMatchGenerator::getMatch(
+ Node f, Node t, InstMatch& m, QuantifiersEngine* qe, Trigger* tparent)
+{
Trace("matching") << "Matching " << t << " against pattern " << d_match_pattern << " ("
<< m << ")" << ", " << d_children.size() << ", pattern is " << d_pattern << std::endl;
Assert( !d_match_pattern.isNull() );
}
if( success ){
Trace("matching-debug2") << "Continue next " << d_next << std::endl;
- ret_val = continueNextMatch( f, m, qe );
+ ret_val = continueNextMatch(f, m, qe, tparent);
}
}
if( ret_val<0 ){
}
}
-int InstMatchGenerator::continueNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){
+int InstMatchGenerator::continueNextMatch(Node f,
+ InstMatch& m,
+ QuantifiersEngine* qe,
+ Trigger* tparent)
+{
if( d_next!=NULL ){
- return d_next->getNextMatch( f, m, qe );
+ return d_next->getNextMatch(f, m, qe, tparent);
}else{
if( d_active_add ){
- return qe->addInstantiation( f, m ) ? 1 : -1;
+ return sendInstantiation(tparent, m) ? 1 : -1;
}else{
return 1;
}
return !d_curr_first_candidate.isNull();
}
-int InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){
+int InstMatchGenerator::getNextMatch(Node f,
+ InstMatch& m,
+ QuantifiersEngine* qe,
+ Trigger* tparent)
+{
if( d_needsReset ){
Trace("matching") << "Reset not done yet, must do the reset..." << std::endl;
reset( d_eq_class, qe );
if( d_curr_exclude_match.find( t )==d_curr_exclude_match.end() ){
Assert( t.getType().isComparableTo( d_match_pattern_type ) );
Trace("matching-summary") << "Try " << d_match_pattern << " : " << t << std::endl;
- success = getMatch( f, t, m, qe );
+ success = getMatch(f, t, m, qe, tparent);
if( d_independent_gen && success<0 ){
Assert( d_eq_class.isNull() );
d_curr_exclude_match[t] = true;
return success;
}
-
-
-int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){
+int InstMatchGenerator::addInstantiations(Node f,
+ InstMatch& baseMatch,
+ QuantifiersEngine* qe,
+ Trigger* tparent)
+{
//try to add instantiation for each match produced
int addedLemmas = 0;
InstMatch m( f );
- while( getNextMatch( f, m, qe )>0 ){
+ while (getNextMatch(f, m, qe, tparent) > 0)
+ {
if( !d_active_add ){
m.add( baseMatch );
- if( qe->addInstantiation( f, m ) ){
+ if (sendInstantiation(tparent, m))
+ {
addedLemmas++;
if( qe->inConflict() ){
break;
return oinit;
}
+InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Node q, Node n)
+{
+ if (n.getKind() == INST_CONSTANT)
+ {
+ return NULL;
+ }
+ Trace("var-trigger-debug") << "Is " << n << " a variable trigger?"
+ << std::endl;
+ if (Trigger::isBooleanTermTrigger(n))
+ {
+ VarMatchGeneratorBooleanTerm* vmg =
+ new VarMatchGeneratorBooleanTerm(n[0], n[1]);
+ Trace("var-trigger") << "Boolean term trigger : " << n << ", var = " << n[0]
+ << std::endl;
+ return vmg;
+ }
+ Node x;
+ if (options::purifyTriggers())
+ {
+ x = Trigger::getInversionVariable(n);
+ }
+ if (!x.isNull())
+ {
+ Node s = Trigger::getInversion(n, x);
+ VarMatchGeneratorTermSubs* vmg = new VarMatchGeneratorTermSubs(x, s);
+ Trace("var-trigger") << "Term substitution trigger : " << n
+ << ", var = " << x << ", subs = " << s << std::endl;
+ return vmg;
+ }
+ return new InstMatchGenerator(n);
+}
+
VarMatchGeneratorBooleanTerm::VarMatchGeneratorBooleanTerm( Node var, Node comp ) :
InstMatchGenerator(), d_comp( comp ), d_rm_prev( false ) {
d_var_num[0] = var.getAttribute(InstVarNumAttribute());
}
-int VarMatchGeneratorBooleanTerm::getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) {
+int VarMatchGeneratorBooleanTerm::getNextMatch(Node q,
+ InstMatch& m,
+ QuantifiersEngine* qe,
+ Trigger* tparent)
+{
int ret_val = -1;
if( !d_eq_class.isNull() ){
Node s = NodeManager::currentNM()->mkConst(qe->getEqualityQuery()->areEqual( d_eq_class, d_pattern ));
if( !m.set( qe, d_var_num[0], s ) ){
return -1;
}else{
- ret_val = continueNextMatch( q, m, qe );
+ ret_val = continueNextMatch(q, m, qe, tparent);
if( ret_val>0 ){
return ret_val;
}
d_var_type = d_var.getType();
}
-int VarMatchGeneratorTermSubs::getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) {
+int VarMatchGeneratorTermSubs::getNextMatch(Node q,
+ InstMatch& m,
+ QuantifiersEngine* qe,
+ Trigger* tparent)
+{
int ret_val = -1;
if( !d_eq_class.isNull() ){
Trace("var-trigger-matching") << "Matching " << d_eq_class << " against " << d_var << " in " << d_subs << std::endl;
if( !m.set( qe, d_var_num[0], s ) ){
return -1;
}else{
- ret_val = continueNextMatch( q, m, qe );
+ ret_val = continueNextMatch(q, m, qe, tparent);
if( ret_val>0 ){
return ret_val;
}
Trace("multi-trigger-linear") << "Make children for linear multi trigger." << std::endl;
for( unsigned i=0; i<pats_ordered.size(); i++ ){
Trace("multi-trigger-linear") << "...make for " << pats_ordered[i] << std::endl;
- InstMatchGenerator * cimg = Trigger::getInstMatchGenerator( q, pats_ordered[i] );
+ InstMatchGenerator* cimg = getInstMatchGenerator(q, pats_ordered[i]);
Assert( cimg!=NULL );
d_children.push_back( cimg );
if( i==0 ){ //TODO : improve
}
}
-int InstMatchGeneratorMultiLinear::getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) {
+int InstMatchGeneratorMultiLinear::getNextMatch(Node q,
+ InstMatch& m,
+ QuantifiersEngine* qe,
+ Trigger* tparent)
+{
Trace("multi-trigger-linear-debug") << "InstMatchGeneratorMultiLinear::getNextMatch : reset " << std::endl;
if( options::multiTriggerLinear() ){
//reset everyone
}
Trace("multi-trigger-linear-debug") << "InstMatchGeneratorMultiLinear::getNextMatch : continue match " << std::endl;
Assert( d_next!=NULL );
- int ret_val = continueNextMatch( q, m, qe );
+ int ret_val = continueNextMatch(q, m, qe, tparent);
if( ret_val>0 ){
Trace("multi-trigger-linear") << "Successful multi-trigger instantiation." << std::endl;
if( options::multiTriggerLinear() ){
// now, restrict everyone
for( unsigned i=0; i<d_children.size(); i++ ){
- Node mi = d_children[i]->d_curr_matched;
+ Node mi = d_children[i]->getCurrentMatch();
Trace("multi-trigger-linear") << " child " << i << " match : " << mi << std::endl;
d_children[i]->excludeMatch( mi );
}
/** constructors */
-InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ) :
-d_f( q ){
+InstMatchGeneratorMulti::InstMatchGeneratorMulti(Node q,
+ std::vector<Node>& pats,
+ QuantifiersEngine* qe)
+ : d_quant(q)
+{
Trace("multi-trigger-cache") << "Making smart multi-trigger for " << q << std::endl;
std::map< Node, std::vector< Node > > var_contains;
qe->getTermUtil()->getVarContains( q, pats, var_contains );
for( unsigned i=0; i<pats.size(); i++ ){
Node n = pats[i];
//make the match generator
- d_children.push_back( InstMatchGenerator::mkInstMatchGenerator(q, n, qe ) );
+ InstMatchGenerator* img =
+ InstMatchGenerator::mkInstMatchGenerator(q, n, qe);
+ img->setActiveAdd(false);
+ d_children.push_back(img);
//compute unique/shared variables
std::vector< int > unique_vars;
std::map< int, bool > shared_vars;
return true;
}
-int InstMatchGeneratorMulti::addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ){
+int InstMatchGeneratorMulti::addInstantiations(Node q,
+ InstMatch& baseMatch,
+ QuantifiersEngine* qe,
+ Trigger* tparent)
+{
int addedLemmas = 0;
Trace("multi-trigger-cache") << "Process smart multi trigger" << std::endl;
for( unsigned i=0; i<d_children.size(); i++ ){
Trace("multi-trigger-cache") << "Calculate matches " << i << std::endl;
std::vector< InstMatch > newMatches;
InstMatch m( q );
- while( d_children[i]->getNextMatch( q, m, qe )>0 ){
+ while (d_children[i]->getNextMatch(q, m, qe, tparent) > 0)
+ {
//m.makeRepresentative( qe );
newMatches.push_back( InstMatch( &m ) );
m.clear();
Trace("multi-trigger-cache") << "Made " << newMatches.size() << " new matches for index " << i << std::endl;
for( unsigned j=0; j<newMatches.size(); j++ ){
Trace("multi-trigger-cache2") << "...processing " << j << " / " << newMatches.size() << ", #lemmas = " << addedLemmas << std::endl;
- processNewMatch( qe, newMatches[j], i, addedLemmas );
+ processNewMatch(qe, tparent, newMatches[j], i, addedLemmas);
if( qe->inConflict() ){
return addedLemmas;
}
return addedLemmas;
}
-void InstMatchGeneratorMulti::processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas ){
+void InstMatchGeneratorMulti::processNewMatch(QuantifiersEngine* qe,
+ Trigger* tparent,
+ InstMatch& m,
+ int fromChildIndex,
+ int& addedLemmas)
+{
//see if these produce new matches
- d_children_trie[fromChildIndex].addInstMatch( qe, d_f, m );
+ d_children_trie[fromChildIndex].addInstMatch(qe, d_quant, m);
//possibly only do the following if we know that new matches will be produced?
//the issue is that instantiations are filtered in quantifiers engine, and so there is no guarentee that
// we can safely skip the following lines, even when we have already produced this match.
Trace("multi-trigger-cache-debug") << "Child " << fromChildIndex << " produced match " << m << std::endl;
//process new instantiations
int childIndex = (fromChildIndex+1)%(int)d_children.size();
- std::vector< IndexedTrie > unique_var_tries;
- processNewInstantiations( qe, m, addedLemmas, d_children_trie[childIndex].getTrie(),
- unique_var_tries, 0, childIndex, fromChildIndex, true );
+ processNewInstantiations(qe,
+ tparent,
+ m,
+ addedLemmas,
+ d_children_trie[childIndex].getTrie(),
+ 0,
+ childIndex,
+ fromChildIndex,
+ true);
}
-void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr,
- std::vector< IndexedTrie >& unique_var_tries,
- int trieIndex, int childIndex, int endChildIndex, bool modEq ){
+void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
+ Trigger* tparent,
+ InstMatch& m,
+ int& addedLemmas,
+ InstMatchTrie* tr,
+ int trieIndex,
+ int childIndex,
+ int endChildIndex,
+ bool modEq)
+{
Assert( !qe->inConflict() );
if( childIndex==endChildIndex ){
- //now, process unique variables
- processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, 0 );
+ // m is an instantiation
+ if (sendInstantiation(tparent, m))
+ {
+ addedLemmas++;
+ Trace("multi-trigger-cache-debug") << "-> Produced instantiation " << m
+ << std::endl;
+ }
}else if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){
int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex];
- //Node curr_ic = qe->getTermUtil()->getInstantiationConstant( d_f, curr_index );
+ // Node curr_ic = qe->getTermUtil()->getInstantiationConstant( d_quant,
+ // curr_index );
Node n = m.get( curr_index );
if( n.isNull() ){
- //if( d_var_to_node[ curr_index ].size()==1 ){ //FIXME
- // //unique variable(s), defer calculation
- // unique_var_tries.push_back( IndexedTrie( std::pair< int, int >( childIndex, trieIndex ), tr ) );
- // int newChildIndex = (childIndex+1)%(int)d_children.size();
- // processNewInstantiations( qe, m, d_children_trie[newChildIndex].getTrie(), unique_var_tries,
- // 0, newChildIndex, endChildIndex, modEq );
- //}else{
- //shared and non-set variable, add to InstMatch
- for( std::map< Node, InstMatchTrie >::iterator it = tr->d_data.begin(); it != tr->d_data.end(); ++it ){
- InstMatch mn( &m );
- mn.setValue( curr_index, it->first);
- processNewInstantiations( qe, mn, addedLemmas, &(it->second), unique_var_tries,
- trieIndex+1, childIndex, endChildIndex, modEq );
- if( qe->inConflict() ){
- break;
- }
+ // add to InstMatch
+ for (std::pair<const Node, InstMatchTrie>& d : tr->d_data)
+ {
+ InstMatch mn(&m);
+ mn.setValue(curr_index, d.first);
+ processNewInstantiations(qe,
+ tparent,
+ mn,
+ addedLemmas,
+ &(d.second),
+ trieIndex + 1,
+ childIndex,
+ endChildIndex,
+ modEq);
+ if (qe->inConflict())
+ {
+ break;
}
- //}
- }else{
- //shared and set variable, try to merge
- std::map< Node, InstMatchTrie >::iterator it = tr->d_data.find( n );
- if( it!=tr->d_data.end() ){
- processNewInstantiations( qe, m, addedLemmas, &(it->second), unique_var_tries,
- trieIndex+1, childIndex, endChildIndex, modEq );
}
- if( modEq ){
- //check modulo equality for other possible instantiations
- if( qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
- eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
- qe->getEqualityQuery()->getEngine() );
- while( !eqc.isFinished() ){
- Node en = (*eqc);
- if( en!=n ){
- std::map< Node, InstMatchTrie >::iterator itc = tr->d_data.find( en );
- if( itc!=tr->d_data.end() ){
- processNewInstantiations( qe, m, addedLemmas, &(itc->second), unique_var_tries,
- trieIndex+1, childIndex, endChildIndex, modEq );
- if( qe->inConflict() ){
- break;
- }
+ }
+ // shared and set variable, try to merge
+ std::map<Node, InstMatchTrie>::iterator it = tr->d_data.find(n);
+ if (it != tr->d_data.end())
+ {
+ processNewInstantiations(qe,
+ tparent,
+ m,
+ addedLemmas,
+ &(it->second),
+ trieIndex + 1,
+ childIndex,
+ endChildIndex,
+ modEq);
+ }
+ if (modEq)
+ {
+ // check modulo equality for other possible instantiations
+ if (qe->getEqualityQuery()->getEngine()->hasTerm(n))
+ {
+ eq::EqClassIterator eqc(
+ qe->getEqualityQuery()->getEngine()->getRepresentative(n),
+ qe->getEqualityQuery()->getEngine());
+ while (!eqc.isFinished())
+ {
+ Node en = (*eqc);
+ if (en != n)
+ {
+ std::map<Node, InstMatchTrie>::iterator itc = tr->d_data.find(en);
+ if (itc != tr->d_data.end())
+ {
+ processNewInstantiations(qe,
+ tparent,
+ m,
+ addedLemmas,
+ &(itc->second),
+ trieIndex + 1,
+ childIndex,
+ endChildIndex,
+ modEq);
+ if (qe->inConflict())
+ {
+ break;
}
}
- ++eqc;
}
+ ++eqc;
}
}
}
}else{
int newChildIndex = (childIndex+1)%(int)d_children.size();
- processNewInstantiations( qe, m, addedLemmas, d_children_trie[newChildIndex].getTrie(), unique_var_tries,
- 0, newChildIndex, endChildIndex, modEq );
- }
-}
-
-void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas,
- std::vector< IndexedTrie >& unique_var_tries,
- int uvtIndex, InstMatchTrie* tr, int trieIndex ){
- if( uvtIndex<(int)unique_var_tries.size() ){
- int childIndex = unique_var_tries[uvtIndex].first.first;
- if( !tr ){
- tr = unique_var_tries[uvtIndex].second;
- trieIndex = unique_var_tries[uvtIndex].first.second;
- }
- if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){
- int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex];
- //Node curr_ic = qe->getTermUtil()->getInstantiationConstant( d_f, curr_index );
- //unique non-set variable, add to InstMatch
- for( std::map< Node, InstMatchTrie >::iterator it = tr->d_data.begin(); it != tr->d_data.end(); ++it ){
- InstMatch mn( &m );
- mn.setValue( curr_index, it->first);
- processNewInstantiations2( qe, mn, addedLemmas, unique_var_tries, uvtIndex, &(it->second), trieIndex+1 );
- if( qe->inConflict() ){
- break;
- }
- }
- }else{
- processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, uvtIndex+1 );
- }
- }else{
- //m is an instantiation
- if( qe->addInstantiation( d_f, m ) ){
- addedLemmas++;
- Trace("multi-trigger-cache-debug") << "-> Produced instantiation " << m << std::endl;
- }
+ processNewInstantiations(qe,
+ tparent,
+ m,
+ addedLemmas,
+ d_children_trie[newChildIndex].getTrie(),
+ 0,
+ newChildIndex,
+ endChildIndex,
+ modEq);
}
}
-InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat, QuantifiersEngine* qe ) : d_f( q ), d_match_pattern( pat ) {
+InstMatchGeneratorSimple::InstMatchGeneratorSimple(Node q,
+ Node pat,
+ QuantifiersEngine* qe)
+ : d_quant(q), d_match_pattern(pat)
+{
if( d_match_pattern.getKind()==NOT ){
d_match_pattern = d_match_pattern[0];
d_pol = false;
void InstMatchGeneratorSimple::resetInstantiationRound( QuantifiersEngine* qe ) {
}
-
-int InstMatchGeneratorSimple::addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ){
+int InstMatchGeneratorSimple::addInstantiations(Node q,
+ InstMatch& baseMatch,
+ QuantifiersEngine* qe,
+ Trigger* tparent)
+{
int addedLemmas = 0;
quantifiers::TermArgTrie* tat;
if( d_eqc.isNull() ){
return addedLemmas;
}
-void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ){
+void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
+ QuantifiersEngine* qe,
+ int& addedLemmas,
+ unsigned argIndex,
+ quantifiers::TermArgTrie* tat)
+{
Debug("simple-trigger-debug") << "Add inst " << argIndex << " " << d_match_pattern << std::endl;
- if( argIndex==(int)d_match_pattern.getNumChildren() ){
+ if (argIndex == d_match_pattern.getNumChildren())
+ {
Assert( !tat->d_data.empty() );
TNode t = tat->getNodeData();
Debug("simple-trigger") << "Actual term is " << t << std::endl;
m.setValue( it->second, t[it->first] );
}
}
- if( qe->addInstantiation( d_f, m ) ){
+ // we do not need the trigger parent for simple triggers (no post-processing
+ // required)
+ if (qe->addInstantiation(d_quant, m))
+ {
addedLemmas++;
Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl;
}
namespace inst {
-/** base class for producing InstMatch objects */
+class Trigger;
+
+/** IMGenerator class
+*
+* Virtual base class for generating InstMatch objects, which correspond to
+* quantifier instantiations. The main use of this class is as a backend utility
+* to Trigger (see theory/quantifiers/trigger.h).
+*
+* Some functions below take as argument a pointer to the current quantifiers
+* engine, which is used for making various queries about what terms and
+* equalities exist in the current context.
+*
+* Some functions below take a pointer to a parent Trigger object, which is used
+* to post-process and finalize the instantiations through
+* sendInstantiation(...), where the parent trigger will make calls to
+* qe->getInstantiate()->addInstantiation(...). The latter function is the entry
+* point in which instantiate lemmas are enqueued to be sent on the output
+* channel.
+*/
class IMGenerator {
public:
virtual ~IMGenerator() {}
- /** reset instantiation round (call this at beginning of instantiation round) */
- virtual void resetInstantiationRound( QuantifiersEngine* qe ) = 0;
- /** reset, eqc is the equivalence class to search in (any if eqc=null) */
- virtual bool reset( Node eqc, QuantifiersEngine* qe ) = 0;
- /** get the next match. must call reset( eqc ) before this function. */
- virtual int getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) = 0;
- /** add instantiations directly */
- virtual int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ) = 0;
- /** set active add */
- virtual void setActiveAdd( bool val ) {}
- /** get active score */
+ /** Reset instantiation round.
+ *
+ * Called once at beginning of an instantiation round.
+ */
+ virtual void resetInstantiationRound(QuantifiersEngine* qe) {}
+ /** Reset.
+ *
+ * eqc is the equivalence class to search in (any if eqc=null).
+ * Returns true if this generator can produce instantiations, and false
+ * otherwise. An example of when it returns false is if it can be determined
+ * that no appropriate matchable terms occur based on eqc.
+ */
+ virtual bool reset(Node eqc, QuantifiersEngine* qe) { return true; }
+ /** Get the next match.
+ *
+ * Must call reset( eqc ) before this function. This constructs an
+ * instantiation, which it populates in data structure m,
+ * based on the current context using the implemented matching algorithm.
+ *
+ * q is the quantified formula we are adding instantiations for
+ * m is the InstMatch object we are generating
+ *
+ * Returns a value >0 if an instantiation was successfully generated
+ */
+ virtual int getNextMatch(Node q,
+ InstMatch& m,
+ QuantifiersEngine* qe,
+ Trigger* tparent)
+ {
+ return 0;
+ }
+ /** add instantiations
+ *
+ * This add all available instantiations for q based on the current context
+ * using the implemented matching algorithm. It typically is implemented as a
+ * fixed point of getNextMatch above.
+ *
+ * baseMatch is a mapping of default values that should be used for variables
+ * that are not bound by this (not frequently used). (TODO remove #1389)
+ *
+ * It returns the number of instantiations added using calls to calls to
+ * Instantiate::addInstantiation(...).
+ */
+ virtual int addInstantiations(Node q,
+ InstMatch& baseMatch,
+ QuantifiersEngine* qe,
+ Trigger* tparent)
+ {
+ return 0;
+ }
+ /** get active score
+ *
+ * A heuristic value indicating how active this generator is.
+ */
virtual int getActiveScore( QuantifiersEngine * qe ) { return 0; }
+ protected:
+ /** send instantiation
+ *
+ * This method sends instantiation, specified by m, to the parent trigger
+ * object, which will in turn make a call to
+ * Instantiate::addInstantiation(...). This method returns true if a
+ * call to Instantiate::addInstantiation(...) was successfully made,
+ * indicating that an instantiation was enqueued in the quantifier engine's
+ * lemma cache.
+ */
+ bool sendInstantiation(Trigger* tparent, InstMatch& m);
};/* class IMGenerator */
class CandidateGenerator;
+/** InstMatchGenerator class
+*
+* This is the default generator class for non-simple single triggers, that is,
+* triggers composed of a single term with nested term applications.
+* For example, { f( y, f( x, a ) ) } and { f( g( x ), a ) } are non-simple
+* triggers.
+*
+* Handling non-simple triggers is done by constructing a linked list of
+* InstMatchGenerator classes (see mkInstMatchGenerator), where each
+* InstMatchGenerator has a "d_next" pointer. If d_next is NULL,
+* then this is the end of the InstMatchGenerator and the last
+* InstMatchGenerator is responsible for finalizing the instantiation.
+*
+* For (EX1), for the trigger f( y, f( x, a ) ), we construct the linked list:
+*
+* [ f( y, f( x, a ) ) ] -> [ f( x, a ) ] -> NULL
+*
+* In a call to getNextMatch,
+* if we match against a ground term f( b, c ), then the first InstMatchGenerator
+* in this list binds y to b, and tells the InstMatchGenerator [ f( x, a ) ] to
+* match f-applications in the equivalence class of c.
+*
+* CVC4 employs techniques that ensure that the number of instantiations
+* is worst-case polynomial wrt the number of ground terms.
+* Consider the axiom/pattern/context (EX2) :
+*
+* axiom : forall x1 x2 x3 x4. F[ x1...x4 ]
+*
+* trigger : P( f( x1 ), f( x2 ), f( x3 ), f( x4 ) )
+*
+* ground context : ~P( a, a, a, a ), a = f( c_1 ) = ... = f( c_100 )
+*
+* If E-matching were applied exhaustively, then x1, x2, x3, x4 would be
+* instantiated with all combinations of c_1, ... c_100, giving 100^4
+* instantiations.
+*
+* Instead, we enforce that at most 1 instantiation is produced for a
+* ( pattern, ground term ) pair per round. Meaning, only one instantiation is
+* generated when matching P( a, a, a, a ) against the generator
+* [P( f( x1 ), f( x2 ), f( x3 ), f( x4 ) )]. For details, see Section 3 of
+* Reynolds, Vampire 2016.
+*
+* To enforce these policies, we use a flag "d_active_add" which dictates the
+* behavior of the last element in the linked list. If d_active_add is
+* true -> a call to getNextMatch(...) returns 1 only if adding the
+* instantiation via a call to IMGenerator::sendInstantiation(...)
+* successfully enqueues a lemma via a call to
+* Instantiate::addInstantiation(...). This call may fail e.g. if we
+* have already added the instantiation, or the instantiation is
+* entailed.
+* false -> a call to getNextMatch(...) returns 1 whenever an m is
+* constructed, where typically the caller would use m.
+* This is important since a return value >0 signals that the current matched
+* terms should be flushed. Consider the above example (EX1), where
+* [ f(y,f(x,a)) ] is being matched against f(b,c),
+* [ f(x,a) ] is being matched against f(d,a) where c=f(d,a)
+* A successfully added instantiation { x->d, y->b } here signals we should
+* not produce further instantiations that match f(y,f(x,a)) with f(b,c).
+*
+* A number of special cases of triggers are covered by this generator (see
+* implementation of initialize), including :
+* Literal triggers, e.g. x >= a, ~x = y
+* Selector triggers, e.g. head( x )
+* Triggers with invertible subterms, e.g. f( x+1 )
+* Variable triggers, e.g. x
+*
+* All triggers above can be in the context of an equality, e.g.
+* { f( y, f( x, a ) ) = b } is a trigger that matches f( y, f( x, a ) ) to
+* ground terms in the equivalence class of b.
+* { ~f( y, f( x, a ) ) = b } is a trigger that matches f( y, f( x, a ) ) to any
+* ground terms not in the equivalence class of b.
+*/
class InstMatchGenerator : public IMGenerator {
-protected:
- bool d_needsReset;
- /** candidate generator */
- CandidateGenerator* d_cg;
- /** policy to use for matching */
- int d_matchPolicy;
- /** children generators */
- std::vector< InstMatchGenerator* > d_children;
- std::vector< int > d_children_index;
- /** the next generator in order */
- InstMatchGenerator* d_next;
- /** eq class */
- Node d_eq_class;
- Node d_eq_class_rel;
- /** variable numbers */
- std::map< int, int > d_var_num;
- /** excluded matches */
- std::map< Node, bool > d_curr_exclude_match;
- /** first candidate */
- Node d_curr_first_candidate;
- /** indepdendent generate (failures should be cached) */
- bool d_independent_gen;
- /** initialize pattern */
- void initialize( Node q, QuantifiersEngine* qe, std::vector< InstMatchGenerator * > & gens );
- /** children types 0 : variable, 1 : child term, -1 : ground term */
- std::vector< int > d_children_types;
- /** continue */
- int continueNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe );
-public:
- enum {
- //options for producing matches
- MATCH_GEN_DEFAULT = 0,
- //others (internally used)
- MATCH_GEN_INTERNAL_ERROR,
- };
public:
- /** get the match against ground term or formula t.
- d_match_pattern and t should have the same shape.
- only valid for use where !d_match_pattern.isNull().
- */
- int getMatch( Node q, Node t, InstMatch& m, QuantifiersEngine* qe );
+ /** destructor */
+ virtual ~InstMatchGenerator() throw();
+ enum
+ {
+ // options for producing matches
+ MATCH_GEN_DEFAULT = 0,
+ // others (internally used)
+ MATCH_GEN_INTERNAL_ERROR,
+ };
- /** constructors */
- InstMatchGenerator( Node pat );
- InstMatchGenerator();
- /** destructor */
- virtual ~InstMatchGenerator() throw();
- /** The pattern we are producing matches for.
- If null, this is a multi trigger that is merging matches from d_children.
- */
- Node d_pattern;
- /** match pattern */
- Node d_match_pattern;
- /** match pattern type */
- TypeNode d_match_pattern_type;
- /** match pattern op */
- Node d_match_pattern_op;
- /** what matched */
- Node d_curr_matched;
-public:
- /** reset instantiation round (call this whenever equivalence classes have changed) */
- void resetInstantiationRound( QuantifiersEngine* qe );
- /** reset, eqc is the equivalence class to search in (any if eqc=null) */
- bool reset( Node eqc, QuantifiersEngine* qe );
- /** get the next match. must call reset( eqc ) before this function. */
- int getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe );
- /** add instantiations */
- int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe );
+ /** Reset instantiation round. */
+ void resetInstantiationRound(QuantifiersEngine* qe) override;
+ /** Reset. */
+ bool reset(Node eqc, QuantifiersEngine* qe) override;
+ /** Get the next match. */
+ int getNextMatch(Node q,
+ InstMatch& m,
+ QuantifiersEngine* qe,
+ Trigger* tparent) override;
+ /** Add instantiations. */
+ int addInstantiations(Node q,
+ InstMatch& baseMatch,
+ QuantifiersEngine* qe,
+ Trigger* tparent) override;
- bool d_active_add;
- void setActiveAdd( bool val );
- int getActiveScore( QuantifiersEngine * qe );
- void excludeMatch( Node n ) { d_curr_exclude_match[n] = true; }
- void setIndependent() { d_independent_gen = true; }
+ /** set active add flag (true by default)
+ *
+ * If active add is true, we call sendInstantiation in calls to getNextMatch,
+ * instead of returning the match. This is necessary so that we can ensure
+ * policies that are dependent upon knowing when instantiations are
+ * successfully added to the output channel through
+ * Instantiate::addInstantiation(...).
+ */
+ void setActiveAdd(bool val);
+ /** Get active score for this inst match generator
+ *
+ * See Trigger::getActiveScore for details.
+ */
+ int getActiveScore(QuantifiersEngine* qe);
+ /** exclude match
+ *
+ * Exclude matching d_match_pattern with Node n on subsequent calls to
+ * getNextMatch.
+ */
+ void excludeMatch(Node n) { d_curr_exclude_match[n] = true; }
+ /** Get current match.
+ * Returns the term we are currently matching.
+ */
+ Node getCurrentMatch() { return d_curr_matched; }
+ /** set that this match generator is independent
+ *
+ * A match generator is indepndent when this generator fails to produce a
+ * match in a call to getNextMatch, the overall matching fails.
+ */
+ void setIndependent() { d_independent_gen = true; }
+ //-------------------------------construction of inst match generators
+ /** mkInstMatchGenerator for single triggers, calls the method below */
+ static InstMatchGenerator* mkInstMatchGenerator(Node q,
+ Node pat,
+ QuantifiersEngine* qe);
+ /** mkInstMatchGenerator for the multi trigger case
+ *
+ * This linked list of InstMatchGenerator classes with one
+ * InstMatchGeneratorMultiLinear at the head and a list of trailing
+ * InstMatchGenerators corresponding to each unique subterm of pats with
+ * free variables.
+ */
+ static InstMatchGenerator* mkInstMatchGeneratorMulti(Node q,
+ std::vector<Node>& pats,
+ QuantifiersEngine* qe);
+ /** mkInstMatchGenerator
+ *
+ * This generates a linked list of InstMatchGenerators for each unique
+ * subterm of pats with free variables.
+ *
+ * q is the quantified formula associated with the generator we are making
+ * pats is a set of terms we are making InstMatchGenerator nodes for
+ * qe is a pointer to the quantifiers engine (used for querying necessary
+ * information during initialization) pat_map_init maps from terms to
+ * generators we have already made for them.
+ *
+ * It calls initialize(...) for all InstMatchGenerators generated by this call.
+ */
+ static InstMatchGenerator* mkInstMatchGenerator(
+ Node q,
+ std::vector<Node>& pats,
+ QuantifiersEngine* qe,
+ std::map<Node, InstMatchGenerator*>& pat_map_init);
+ //-------------------------------end construction of inst match generators
- static InstMatchGenerator* mkInstMatchGenerator( Node q, Node pat, QuantifiersEngine* qe );
- static InstMatchGenerator* mkInstMatchGeneratorMulti( Node q, std::vector< Node >& pats, QuantifiersEngine* qe );
- static InstMatchGenerator* mkInstMatchGenerator( Node q, std::vector< Node >& pats, QuantifiersEngine* qe,
- std::map< Node, InstMatchGenerator * >& pat_map_init );
+protected:
+ /** constructors
+ *
+ * These are intentionally private, and are called during linked list
+ * construction in mkInstMatchGenerator.
+ */
+ InstMatchGenerator(Node pat);
+ InstMatchGenerator();
+ /** The pattern we are producing matches for.
+ *
+ * This term and d_match_pattern can be different since this
+ * term may involve information regarding phase and (dis)equality entailment,
+ * or other special cases of Triggers.
+ *
+ * For example, for the trigger for P( x ) = false, which matches P( x ) with
+ * P( t ) in the equivalence class of false,
+ * P( x ) = false is d_pattern
+ * P( x ) is d_match_pattern
+ * Another example, for pure theory triggers like head( x ), we have
+ * head( x ) is d_pattern
+ * x is d_match_pattern
+ * since head( x ) can match any (List) datatype term x.
+ *
+ * If null, this is a multi trigger that is merging matches from d_children,
+ * which is used in InstMatchGeneratorMulti.
+ */
+ Node d_pattern;
+ /** The match pattern
+ * This is the term that is matched against ground terms,
+ * see examples above.
+ */
+ Node d_match_pattern;
+ /** The current term we are matching. */
+ Node d_curr_matched;
+ /** do we need to call reset on this generator? */
+ bool d_needsReset;
+ /** candidate generator
+ * This is the back-end utility for InstMatchGenerator.
+ * It generates a stream of candidate terms to match against d_match_pattern
+ * below, dependending upon what kind of term we are matching
+ * (e.g. a matchable term, a variable, a relation, etc.).
+ */
+ CandidateGenerator* d_cg;
+ /** policy to use for matching
+ * This is one of MATCH_GEN_* above.
+ * TODO: this can be simplified/removed (#1283).
+ */
+ int d_matchPolicy;
+ /** children generators
+ * These match generators correspond to the children of the term
+ * we are matching with this generator.
+ * For example [ f( x, a ) ] is a child of [ f( y, f( x, a ) ) ]
+ * in the example (EX1) above.
+ */
+ std::vector<InstMatchGenerator*> d_children;
+ /** for each child, the index in the term
+ * For example [ f( x, a ) ] has index 1 in [ f( y, f( x, a ) ) ]
+ * in the example (EX1) above, indicating it is the 2nd child
+ * of the term.
+ */
+ std::vector<int> d_children_index;
+ /** children types 0 : variable, 1 : child term, -1 : ground term */
+ std::vector<int> d_children_types;
+ /** The next generator in the linked list
+ * that this generator is a part of.
+ */
+ InstMatchGenerator* d_next;
+ /** The equivalence class we are currently matching in. */
+ Node d_eq_class;
+ /** If non-null, then this is a relational trigger of the form x ~
+ * d_eq_class_rel. */
+ Node d_eq_class_rel;
+ /** For each child index of this node, the variable numbers of the children.
+ * For example, if this is generator is for the term f( x3, a, x1, x2 )
+ * the quantified formula
+ * forall x1 x2 x3. (...).
+ * Then d_var_num[0] = 2, d_var_num[2] = 0 and d_var_num[3] = 1.
+ */
+ std::map<int, int> d_var_num;
+ /** Excluded matches
+ * Stores the terms we are not allowed to match.
+ * These can for instance be specified by the smt2
+ * extended syntax (! ... :no-pattern).
+ */
+ std::map<Node, bool> d_curr_exclude_match;
+ /** Current first candidate
+ * Used in a key fail-quickly optimization which generates
+ * the first candidate term to match during reset().
+ */
+ Node d_curr_first_candidate;
+ /** Indepdendent generate
+ * If this flag is true, failures to match should be cached.
+ */
+ bool d_independent_gen;
+ /** active add flag, described above. */
+ bool d_active_add;
+ /** cached value of d_match_pattern.getType() */
+ TypeNode d_match_pattern_type;
+ /** the match operator for d_match_pattern
+ *
+ * See TermDatabase::getMatchOperator for details on match operators.
+ */
+ Node d_match_pattern_op;
+ /** get the match against ground term or formula t.
+ *
+ * d_match_pattern and t should have the same shape, that is,
+ * their match operator (see TermDatabase::getMatchOperator) is the same.
+ * only valid for use where !d_match_pattern.isNull().
+ */
+ int getMatch(
+ Node q, Node t, InstMatch& m, QuantifiersEngine* qe, Trigger* tparent);
+ /** Initialize this generator.
+ *
+ * q is the quantified formula associated with this generator.
+ *
+ * This constructs the appropriate information about what
+ * patterns we are matching and children generators.
+ *
+ * It may construct new (child) generators needed to implement
+ * the matching algorithm for this term. For each new generator
+ * constructed in this way, it adds them to gens.
+ */
+ void initialize(Node q,
+ QuantifiersEngine* qe,
+ std::vector<InstMatchGenerator*>& gens);
+ /** Continue next match
+ *
+ * This is called during getNextMatch when the current generator in the linked
+ * list succesfully satisfies its matching constraint. This function either
+ * calls getNextMatch of the next element in the linked list, or finalizes the
+ * match (calling sendInstantiation(...) if active add is true, or returning a
+ * value >0 if active add is false). Its return value has the same semantics
+ * as getNextMatch.
+ */
+ int continueNextMatch(Node q,
+ InstMatch& m,
+ QuantifiersEngine* qe,
+ Trigger* tparent);
+ /** Get inst match generator
+ *
+ * Gets the InstMatchGenerator that implements the
+ * appropriate matching algorithm for n within q
+ * within a linked list of InstMatchGenerators.
+ */
+ static InstMatchGenerator* getInstMatchGenerator(Node q, Node n);
};/* class InstMatchGenerator */
-//match generator for boolean term ITEs
+/** match generator for Boolean term ITEs
+* This handles the special case of triggers that look like ite( x, BV1, BV0 ).
+*/
class VarMatchGeneratorBooleanTerm : public InstMatchGenerator {
public:
VarMatchGeneratorBooleanTerm( Node var, Node comp );
virtual ~VarMatchGeneratorBooleanTerm() throw() {}
- Node d_comp;
- bool d_rm_prev;
- /** reset instantiation round (call this at beginning of instantiation round) */
- void resetInstantiationRound( QuantifiersEngine* qe ){}
- /** reset, eqc is the equivalence class to search in (any if eqc=null) */
- bool reset( Node eqc, QuantifiersEngine* qe ){
+ /** Reset */
+ bool reset(Node eqc, QuantifiersEngine* qe) override
+ {
d_eq_class = eqc;
return true;
}
- /** get the next match. must call reset( eqc ) before this function. */
- int getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe );
- /** add instantiations directly */
- int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ){ return 0; }
+ /** Get the next match. */
+ int getNextMatch(Node q,
+ InstMatch& m,
+ QuantifiersEngine* qe,
+ Trigger* tparent) override;
+
+ private:
+ /** stores the true branch of the Boolean ITE */
+ Node d_comp;
+ /** stores whether we have written a value for var in the current match. */
+ bool d_rm_prev;
};
-//match generator for purified terms (matched term is substituted into d_subs)
+/** match generator for purified terms
+* This handles the special case of invertible terms like x+1 (see
+* Trigger::getTermInversionVariable).
+*/
class VarMatchGeneratorTermSubs : public InstMatchGenerator {
public:
VarMatchGeneratorTermSubs( Node var, Node subs );
virtual ~VarMatchGeneratorTermSubs() throw() {}
+ /** Reset */
+ bool reset(Node eqc, QuantifiersEngine* qe) override
+ {
+ d_eq_class = eqc;
+ return true;
+ }
+ /** Get the next match. */
+ int getNextMatch(Node q,
+ InstMatch& m,
+ QuantifiersEngine* qe,
+ Trigger* tparent) override;
+
+ private:
+ /** variable we are matching (x in the example x+1). */
TNode d_var;
+ /** cache of d_var.getType() */
TypeNode d_var_type;
+ /** The substitution for what we match (x-1 in the example x+1). */
Node d_subs;
+ /** stores whether we have written a value for d_var in the current match. */
bool d_rm_prev;
- /** reset instantiation round (call this at beginning of instantiation round) */
- void resetInstantiationRound( QuantifiersEngine* qe ){}
- /** reset, eqc is the equivalence class to search in (any if eqc=null) */
- bool reset( Node eqc, QuantifiersEngine* qe ){
- d_eq_class = eqc;
- return true;
- }
- /** get the next match. must call reset( eqc ) before this function. */
- int getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe );
- /** add instantiations directly */
- int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe ) { return 0; }
};
-
-/** smart multi-trigger implementation */
+/** InstMatchGeneratorMultiLinear class
+*
+* This is the default implementation of multi-triggers.
+*
+* Handling multi-triggers using this class is done by constructing a linked
+* list of InstMatchGenerator classes (see mkInstMatchGeneratorMulti), with one
+* InstMatchGeneratorMultiLinear at the head and a list of trailing
+* InstMatchGenerators.
+*
+* CVC4 employs techniques that ensure that the number of instantiations
+* is worst-case polynomial wrt the number of ground terms, where this class
+* lifts this policy to multi-triggers. In particular consider
+*
+* multi-trigger : { f( x1 ), f( x2 ), f( x3 ), f( x4 ) }
+*
+* For this multi-trigger, we insist that for each i=1...4, and each ground term
+* t, there is at most 1 instantiation added as a result of matching
+* ( f( x1 ), f( x2 ), f( x3 ), f( x4 ) )
+* against ground terms of the form
+* ( s_1, s_2, s_3, s_4 ) where t = s_i for i=1,...,4.
+* Meaning we add instantiations for the multi-trigger
+* ( f( x1 ), f( x2 ), f( x3 ), f( x4 ) ) based on matching pairwise against:
+* ( f( c_i11 ), f( c_i21 ), f( c_i31 ), f( c_i41 ) )
+* ( f( c_i12 ), f( c_i22 ), f( c_i32 ), f( c_i42 ) )
+* ( f( c_i13 ), f( c_i23 ), f( c_i33 ), f( c_i43 ) )
+* Where we require c_i{jk} != c_i{jl} for each i=1...4, k != l.
+*
+* For example, we disallow adding instantiations based on matching against both
+* ( f( c_1 ), f( c_2 ), f( c_4 ), f( c_6 ) ) and
+* ( f( c_1 ), f( c_3 ), f( c_5 ), f( c_7 ) )
+* against ( f( x1 ), f( x2 ), f( x3 ), f( x4 ) ), since f( c_1 ) is matched
+* against f( x1 ) twice.
+*
+* This policy can be disabled by --no-multi-trigger-linear.
+*
+*/
class InstMatchGeneratorMultiLinear : public InstMatchGenerator {
-private:
- int resetChildren( QuantifiersEngine* qe );
-public:
- /** constructors */
- InstMatchGeneratorMultiLinear( Node q, std::vector< Node >& pats, QuantifiersEngine* qe );
+ friend class InstMatchGenerator;
+
+ public:
/** destructor */
virtual ~InstMatchGeneratorMultiLinear() throw();
- /** reset, eqc is the equivalence class to search in (any if eqc=null) */
- bool reset( Node eqc, QuantifiersEngine* qe );
- /** get the next match. must call reset( eqc ) before this function.*/
- int getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe );
-};/* class InstMatchGeneratorMulti */
+ /** Reset. */
+ bool reset(Node eqc, QuantifiersEngine* qe) override;
+ /** Get the next match. */
+ int getNextMatch(Node q,
+ InstMatch& m,
+ QuantifiersEngine* qe,
+ Trigger* tparent) override;
-/** smart multi-trigger implementation */
+ protected:
+ /** reset the children of this generator */
+ int resetChildren(QuantifiersEngine* qe);
+ /** constructor */
+ InstMatchGeneratorMultiLinear(Node q,
+ std::vector<Node>& pats,
+ QuantifiersEngine* qe);
+};/* class InstMatchGeneratorMulti */
+
+/** InstMatchGeneratorMulti
+*
+* This is an earlier implementation of multi-triggers
+* that is enabled by --multi-trigger-cache.
+* This generator takes the product of instantiations
+* found by single trigger matching, and does
+* not have the guarantee that the number of
+* instantiations is polynomial wrt the number of
+* ground terms.
+*/
class InstMatchGeneratorMulti : public IMGenerator {
-private:
+ public:
+ /** constructors */
+ InstMatchGeneratorMulti(Node q,
+ std::vector<Node>& pats,
+ QuantifiersEngine* qe);
+ /** destructor */
+ virtual ~InstMatchGeneratorMulti() throw();
+
+ /** Reset instantiation round. */
+ void resetInstantiationRound(QuantifiersEngine* qe) override;
+ /** Reset. */
+ bool reset(Node eqc, QuantifiersEngine* qe) override;
+ /** Add instantiations. */
+ int addInstantiations(Node q,
+ InstMatch& baseMatch,
+ QuantifiersEngine* qe,
+ Trigger* tparent) override;
+
+ private:
/** indexed trie */
typedef std::pair< std::pair< int, int >, InstMatchTrie* > IndexedTrie;
- /** process new match */
- void processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas );
- /** process new instantiations */
- void processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr,
- std::vector< IndexedTrie >& unique_var_tries,
- int trieIndex, int childIndex, int endChildIndex, bool modEq );
- /** process new instantiations 2 */
- void processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas,
- std::vector< IndexedTrie >& unique_var_tries,
- int uvtIndex, InstMatchTrie* tr = NULL, int trieIndex = 0 );
-private:
- /** var contains (variable indices) for each pattern node */
+ /** process new match
+ *
+ * Called during addInstantiations(...).
+ * Indicates we produced a match m for child fromChildIndex
+ * addedLemmas is how many instantiations we succesfully send
+ * via IMGenerator::sendInstantiation(...) calls.
+ */
+ void processNewMatch(QuantifiersEngine* qe,
+ Trigger* tparent,
+ InstMatch& m,
+ int fromChildIndex,
+ int& addedLemmas);
+ /** helper for process new match
+ * tr is the inst match trie (term index) we are currently traversing.
+ * trieIndex is depth we are in trie tr.
+ * childIndex is the index of the term in the multi trigger we are currently
+ * processing.
+ * endChildIndex is the index of the term in the multi trigger that generated
+ * a new term, and hence we will end when the product
+ * computed by this function returns to.
+ * modEq is whether we are matching modulo equality.
+ */
+ void processNewInstantiations(QuantifiersEngine* qe,
+ Trigger* tparent,
+ InstMatch& m,
+ int& addedLemmas,
+ InstMatchTrie* tr,
+ int trieIndex,
+ int childIndex,
+ int endChildIndex,
+ bool modEq);
+ /** Map from pattern nodes to indices of variables they contain. */
std::map< Node, std::vector< int > > d_var_contains;
- /** variable indices contained to pattern nodes */
+ /** Map from variable indices to pattern nodes that contain them. */
std::map< int, std::vector< Node > > d_var_to_node;
- /** quantifier to use */
- Node d_f;
- /** policy to use for matching */
- int d_matchPolicy;
- /** children generators */
+ /** quantified formula we are producing matches for */
+ Node d_quant;
+ /** children generators
+ * These are inst match generators for each term in the multi trigger.
+ */
std::vector< InstMatchGenerator* > d_children;
- /** order */
+ /** variable orderings
+ * Stores a heuristically determined variable ordering (unique
+ * variables first) for each term in the multi trigger.
+ */
std::map< unsigned, InstMatchTrie::ImtIndexOrder* > d_imtio;
- /** inst match tries for each child */
+ /** inst match tries for each child node
+ * This data structure stores all InstMatch objects generated
+ * by matching for each term in the multi trigger.
+ */
std::vector< InstMatchTrieOrdered > d_children_trie;
- /** calculate matches */
- void calculateMatches( QuantifiersEngine* qe );
-public:
- /** constructors */
- InstMatchGeneratorMulti( Node q, std::vector< Node >& pats, QuantifiersEngine* qe );
- /** destructor */
- virtual ~InstMatchGeneratorMulti() throw();
- /** reset instantiation round (call this whenever equivalence classes have changed) */
- void resetInstantiationRound( QuantifiersEngine* qe );
- /** reset, eqc is the equivalence class to search in (any if eqc=null) */
- bool reset( Node eqc, QuantifiersEngine* qe );
- /** get the next match. must call reset( eqc ) before this function. (not implemented) */
- int getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) { return -1; }
- /** add instantiations */
- int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe );
};/* class InstMatchGeneratorMulti */
-/** smart (single)-trigger implementation */
+/** InstMatchGeneratorSimple class
+*
+* This is the default generator class for simple single triggers.
+* For example, { f( x, a ) }, { f( x, x ) } and { f( x, y ) } are simple single
+* triggers. In practice, around 70-90% of triggers are simple single triggers.
+*
+* Notice that simple triggers also can have an attached polarity.
+* For example, { P( x ) = false }, { f( x, y ) = a } and { ~f( a, x ) = b } are
+* simple single triggers.
+*
+* The implementation traverses the term indices in TermDatabase for adding
+* instantiations, which is more efficient than the techniques required for
+* handling non-simple single triggers.
+*
+* In contrast to other instantiation generators, it does not call
+* IMGenerator::sendInstantiation and for performance reasons instead calls
+* qe->getInstantiate()->addInstantiation(...) directly.
+*/
class InstMatchGeneratorSimple : public IMGenerator {
-private:
- /** quantifier for match term */
- Node d_f;
- /** match term */
+ public:
+ /** constructors */
+ InstMatchGeneratorSimple(Node q, Node pat, QuantifiersEngine* qe);
+ /** destructor */
+ ~InstMatchGeneratorSimple() throw() {}
+ /** Reset instantiation round. */
+ void resetInstantiationRound(QuantifiersEngine* qe) override;
+ /** Add instantiations. */
+ int addInstantiations(Node q,
+ InstMatch& baseMatch,
+ QuantifiersEngine* qe,
+ Trigger* tparent) override;
+ /** Get active score. */
+ int getActiveScore(QuantifiersEngine* qe) override;
+
+ private:
+ /** quantified formula for the trigger term */
+ Node d_quant;
+ /** the trigger term */
Node d_match_pattern;
- /** equivalence class */
+ /** equivalence class polarity information
+ *
+ * This stores the required polarity/equivalence class with this trigger.
+ * If d_eqc is non-null, we only produce matches { x->t } such that
+ * our context does not entail
+ * ( d_match_pattern*{ x->t } = d_eqc) if d_pol = true, or
+ * ( d_match_pattern*{ x->t } != d_eqc) if d_pol = false.
+ * where * denotes application of substitution.
+ */
bool d_pol;
Node d_eqc;
- /** match pattern arg types */
+ /** Match pattern arg types.
+ * Cached values of d_match_pattern[i].getType().
+ */
std::vector< TypeNode > d_match_pattern_arg_types;
- /** operator */
+ /** The match operator d_match_pattern (see TermDb::getMatchOperator). */
Node d_op;
- /** to indicies */
+ /** Map from child number to variable index. */
std::map< int, int > d_var_num;
- /** add instantiations */
- void addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat );
-public:
- /** constructors */
- InstMatchGeneratorSimple( Node q, Node pat, QuantifiersEngine* qe );
- /** destructor */
- ~InstMatchGeneratorSimple() throw() {}
- /** reset instantiation round (call this whenever equivalence classes have changed) */
- void resetInstantiationRound( QuantifiersEngine* qe );
- /** reset, eqc is the equivalence class to search in (any if eqc=null) */
- bool reset( Node eqc, QuantifiersEngine* qe ) { return true; }
- /** get the next match. must call reset( eqc ) before this function. (not implemented) */
- int getNextMatch( Node q, InstMatch& m, QuantifiersEngine* qe ) { return -1; }
- /** add instantiations */
- int addInstantiations( Node q, InstMatch& baseMatch, QuantifiersEngine* qe );
- /** get active score */
- int getActiveScore( QuantifiersEngine * qe );
+ /** add instantiations, helper function.
+ *
+ * m is the current match we are building,
+ * addedLemmas is the number of lemmas we have added via calls to
+ * qe->getInstantiate()->aaddInstantiation(...),
+ * argIndex is the argument index in d_match_pattern we are currently
+ * matching,
+ * tat is the term index we are currently traversing.
+ */
+ void addInstantiations(InstMatch& m,
+ QuantifiersEngine* qe,
+ int& addedLemmas,
+ unsigned argIndex,
+ quantifiers::TermArgTrie* tat);
};/* class InstMatchGeneratorSimple */
-
}
}
}
#include "theory/quantifiers/trigger.h"
#include "theory/quantifiers/candidate_generator.h"
+#include "theory/quantifiers/ho_trigger.h"
#include "theory/quantifiers/inst_match_generator.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
#include "theory/uf/equality_engine.h"
#include "util/hash.h"
-
using namespace std;
using namespace CVC4::kind;
using namespace CVC4::context;
d_mg = new InstMatchGeneratorSimple( f, d_nodes[0], qe );
}else{
d_mg = InstMatchGenerator::mkInstMatchGenerator( f, d_nodes[0], qe );
- d_mg->setActiveAdd(true);
}
}else{
if( options::multiTriggerCache() ){
d_mg = new InstMatchGeneratorMulti( f, d_nodes, qe );
}else{
d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti( f, d_nodes, qe );
- d_mg->setActiveAdd(true);
}
- //d_mg = InstMatchGenerator::mkInstMatchGenerator( d_nodes, qe );
- //d_mg->setActiveAdd();
}
if( d_nodes.size()==1 ){
if( isSimpleTrigger( d_nodes[0] ) ){
}
++(qe->d_statistics.d_multi_triggers);
}
+
//Notice() << "Trigger : " << (*this) << " for " << f << std::endl;
Trace("trigger-debug") << "Finished making trigger." << std::endl;
}
d_mg->reset( eqc, d_quantEngine );
}
-bool Trigger::getNextMatch( Node f, InstMatch& m ){
- int retVal = d_mg->getNextMatch( f, m, d_quantEngine );
- return retVal>0;
-}
-
Node Trigger::getInstPattern(){
return NodeManager::currentNM()->mkNode( INST_PATTERN, d_nodes );
}
-int Trigger::addInstantiations( InstMatch& baseMatch ){
- int addedLemmas = d_mg->addInstantiations( d_f, baseMatch, d_quantEngine );
+int Trigger::addInstantiations(InstMatch& baseMatch)
+{
+ int addedLemmas =
+ d_mg->addInstantiations(d_f, baseMatch, d_quantEngine, this);
if( addedLemmas>0 ){
- Debug("inst-trigger") << "Added " << addedLemmas << " lemmas, trigger was ";
- for( int i=0; i<(int)d_nodes.size(); i++ ){
- Debug("inst-trigger") << d_nodes[i] << " ";
+ if (Debug.isOn("inst-trigger"))
+ {
+ Debug("inst-trigger") << "Added " << addedLemmas
+ << " lemmas, trigger was ";
+ for (unsigned i = 0; i < d_nodes.size(); i++)
+ {
+ Debug("inst-trigger") << d_nodes[i] << " ";
+ }
+ Debug("inst-trigger") << std::endl;
}
- Debug("inst-trigger") << std::endl;
}
return addedLemmas;
}
+bool Trigger::sendInstantiation(InstMatch& m)
+{
+ return d_quantEngine->addInstantiation(d_f, m);
+}
+
bool Trigger::mkTriggerTerms( Node q, std::vector< Node >& nodes, unsigned n_vars, std::vector< Node >& trNodes ) {
//only take nodes that contribute variables to the trigger when added
std::vector< Node > temp;
}
}
}
- Trigger* t = new Trigger( qe, f, trNodes );
+
+ // check if higher-order
+ Trace("trigger") << "Collect higher-order variable triggers..." << std::endl;
+ std::map<Node, std::vector<Node> > ho_apps;
+ HigherOrderTrigger::collectHoVarApplyTerms(f, trNodes, ho_apps);
+ Trigger* t;
+ if (!ho_apps.empty())
+ {
+ t = new HigherOrderTrigger(qe, f, trNodes, ho_apps);
+ }
+ else
+ {
+ t = new Trigger(qe, f, trNodes);
+ }
+
qe->getTriggerDatabase()->addTrigger( trNodes, t );
return t;
}
}
bool Trigger::isAtomicTriggerKind( Kind k ) {
- return k==APPLY_UF || k==SELECT || k==STORE ||
- k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER ||
- k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON ||
- k==SEP_PTO || k==BITVECTOR_TO_NAT || k==INT_TO_BITVECTOR;
+ return k == APPLY_UF || k == SELECT || k == STORE || k == APPLY_CONSTRUCTOR
+ || k == APPLY_SELECTOR_TOTAL || k == APPLY_TESTER || k == UNION
+ || k == INTERSECTION || k == SUBSET || k == SETMINUS || k == MEMBER
+ || k == SINGLETON || k == SEP_PTO || k == BITVECTOR_TO_NAT
+ || k == INT_TO_BITVECTOR || k == HO_APPLY;
}
bool Trigger::isRelationalTrigger( Node n ) {
if( options::purifyDtTriggers() && t.getKind()==APPLY_SELECTOR_TOTAL ){
return false;
}
+ if (t.getKind() == HO_APPLY && t[0].getKind() == INST_CONSTANT)
+ {
+ return false;
+ }
return true;
}else{
return false;
return Node::null();
}
-void Trigger::getTriggerVariables( Node icn, Node q, std::vector< Node >& t_vars ) {
+void Trigger::getTriggerVariables(Node n, Node q, std::vector<Node>& t_vars)
+{
std::vector< Node > patTerms;
std::map< Node, TriggerTermInfo > tinfo;
- //collect all patterns from icn
+ // collect all patterns from n
std::vector< Node > exclude;
- collectPatTerms( q, icn, patTerms, quantifiers::TRIGGER_SEL_ALL, exclude, tinfo );
+ collectPatTerms(q, n, patTerms, quantifiers::TRIGGER_SEL_ALL, exclude, tinfo);
//collect all variables from all patterns in patTerms, add to t_vars
for( unsigned i=0; i<patTerms.size(); i++ ){
quantifiers::TermUtil::getVarContainsNode( q, patTerms[i], t_vars );
}
}
-InstMatchGenerator* Trigger::getInstMatchGenerator( Node q, Node n ) {
- if( n.getKind()==INST_CONSTANT ){
- return NULL;
- }else{
- Trace("var-trigger-debug") << "Is " << n << " a variable trigger?" << std::endl;
- if( isBooleanTermTrigger( n ) ){
- VarMatchGeneratorBooleanTerm* vmg = new VarMatchGeneratorBooleanTerm( n[0], n[1] );
- Trace("var-trigger") << "Boolean term trigger : " << n << ", var = " << n[0] << std::endl;
- return vmg;
- }else{
- Node x;
- if( options::purifyTriggers() ){
- x = getInversionVariable( n );
- }
- if( !x.isNull() ){
- Node s = getInversion( n, x );
- VarMatchGeneratorTermSubs* vmg = new VarMatchGeneratorTermSubs( x, s );
- Trace("var-trigger") << "Term substitution trigger : " << n << ", var = " << x << ", subs = " << s << std::endl;
- return vmg;
- }else{
- return new InstMatchGenerator( n );
- }
- }
- }
-}
-
int Trigger::getActiveScore() {
return d_mg->getActiveScore( d_quantEngine );
}
-Trigger* TriggerTrie::getTrigger2( std::vector< Node >& nodes ){
- if( nodes.empty() ){
- return d_tr.empty() ? NULL : d_tr[0];
- }else{
- Node n = nodes.back();
- nodes.pop_back();
- if( d_children.find( n )!=d_children.end() ){
- return d_children[n]->getTrigger2( nodes );
- }else{
- return NULL;
- }
- }
-}
-
-void TriggerTrie::addTrigger2( std::vector< Node >& nodes, Trigger* t ){
- if( nodes.empty() ){
- d_tr.push_back( t );
- }else{
- Node n = nodes.back();
- nodes.pop_back();
- if( d_children.find( n )==d_children.end() ){
- d_children[n] = new TriggerTrie;
- }
- d_children[n]->addTrigger2( nodes, t );
- }
-}
-
-
TriggerTrie::TriggerTrie()
{}
}
}
+inst::Trigger* TriggerTrie::getTrigger(std::vector<Node>& nodes)
+{
+ std::vector<Node> temp;
+ temp.insert(temp.begin(), nodes.begin(), nodes.end());
+ std::sort(temp.begin(), temp.end());
+ TriggerTrie* tt = this;
+ for (const Node& n : temp)
+ {
+ std::map<TNode, TriggerTrie*>::iterator itt = tt->d_children.find(n);
+ if (itt == tt->d_children.end())
+ {
+ return NULL;
+ }
+ else
+ {
+ tt = itt->second;
+ }
+ }
+ return tt->d_tr.empty() ? NULL : tt->d_tr[0];
+}
+
+void TriggerTrie::addTrigger(std::vector<Node>& nodes, inst::Trigger* t)
+{
+ std::vector<Node> temp;
+ temp.insert(temp.begin(), nodes.begin(), nodes.end());
+ std::sort(temp.begin(), temp.end());
+ TriggerTrie* tt = this;
+ for (const Node& n : temp)
+ {
+ std::map<TNode, TriggerTrie*>::iterator itt = tt->d_children.find(n);
+ if (itt == tt->d_children.end())
+ {
+ TriggerTrie* ttn = new TriggerTrie;
+ tt->d_children[n] = ttn;
+ tt = ttn;
+ }
+ else
+ {
+ tt = itt->second;
+ }
+ }
+ tt->d_tr.push_back(t);
+}
+
}/* CVC4::theory::inst namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#include "theory/quantifiers/inst_match.h"
#include "options/quantifiers_options.h"
-// Forward declarations for defining the Trigger and TriggerTrie.
namespace CVC4 {
namespace theory {
class IMGenerator;
class InstMatchGenerator;
-}/* CVC4::theory::inst namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-
-namespace CVC4 {
-namespace theory {
-namespace inst {
+/** Information about a node used in a trigger.
+*
+* This information includes:
+* 1. the free variables of the node, and
+* 2. information about which terms are useful for matching.
+*
+* As an example, consider the trigger
+* { f( x ), g( y ), P( y, z ) }
+* for quantified formula
+* forall xy. ( f( x ) != b => ( P( x, g( y ) ) V P( y, z ) ) )
+*
+* Notice that it is only useful to match f( x ) to f-applications not in the
+* equivalence class of b, and P( y, z ) to P-applications not in the equivalence
+* class of true, as such instances will always be entailed by the ground
+* equalities and disequalities the current context. Entailed instances are
+* typically not helpful, and are discarded in Instantiate::addInstantiation(...)
+* unless the option --no-inst-no-entail is enabled. For more details, see page
+* 10 of "Congruence Closure with Free Variables", Barbosa et al., TACAS 2017.
+*
+* This example is referenced for each of the functions below.
+*/
class TriggerTermInfo {
public:
TriggerTermInfo() : d_reqPol(0){}
~TriggerTermInfo(){}
+ /** The free variables in the node
+ *
+ * In the trigger term info for f( x ) in the above example, d_fv = { x }
+ * In the trigger term info for g( y ) in the above example, d_fv = { y }
+ * In the trigger term info for P( y, z ) in the above example, d_fv = { y, z }
+ */
std::vector< Node > d_fv;
+ /** Required polarity: 1 for equality, -1 for disequality, 0 for none
+ *
+ * In the trigger term info for f( x ) in the above example, d_reqPol = -1
+ * In the trigger term info for g( y ) in the above example, d_reqPol = 0
+ * In the trigger term info for P( y, z ) in the above example, d_reqPol = 1
+ */
int d_reqPol;
+ /** Required polarity equal term
+ *
+ * If d_reqPolEq is not null,
+ * if d_reqPol = 1, then this trigger term must be matched to terms in the
+ * equivalence class of d_reqPolEq,
+ * if d_reqPol = -1, then this trigger term must be matched to terms *not* in
+ * the equivalence class of d_reqPolEq.
+ *
+ * This information is typically chosen by analyzing the entailed equalities
+ * and disequalities of quantified formulas.
+ * In the trigger term info for f( x ) in the above example, d_reqPolEq = b
+ * In the trigger term info for g( y ) in the above example,
+ * d_reqPolEq = Node::null()
+ * In the trigger term info for P( y, z ) in the above example,
+ * d_reqPolEq = false
+ */
Node d_reqPolEq;
+ /** Initialize this information class (can be called more than once).
+ * q is the quantified formula that n is a trigger term for
+ * n is the trigger term
+ * reqPol/reqPolEq are described above
+ */
void init( Node q, Node n, int reqPol = 0, Node reqPolEq = Node::null() );
};
-/** A collect of nodes representing a trigger. */
+/** A collection of nodes representing a trigger.
+*
+* This class encapsulates all implementations of E-matching in CVC4.
+* Its primary use is as a utility of the quantifiers module InstantiationEngine
+* (see theory/quantifiers/instantiation_engine.h) which uses Trigger to make
+* appropriate calls to Instantiate::addInstantiation(...)
+* (see theory/instantiate.h) for the instantiate utility of the quantifiers
+* engine (d_quantEngine) associated with this trigger. These calls
+* queue instantiation lemmas to the output channel of TheoryQuantifiers during
+* a full effort check.
+*
+* Concretely, a Trigger* t is used in the following way during a full effort
+* check. Assume that t is associated with quantified formula q (see field d_f).
+* We call :
+*
+* // setup initial information
+* t->resetInstantiationRound();
+* // will produce instantiations based on matching with all terms
+* t->reset( Node::null() );
+* InstMatch baseMatch;
+* // add all instantiations based on E-matching with this trigger and the
+* // current context
+* t->addInstantiations( baseMatch );
+*
+* This will result in (a set of) calls to
+* Instantiate::addInstantiation(q, m1)...Instantiate::addInstantiation(q, mn),
+* where m1...mn are InstMatch objects. These calls add the corresponding
+* instantiation lemma for (q,mi) on the output channel associated with
+* d_quantEngine.
+*
+* The Trigger class is wrapper around an underlying IMGenerator class, which
+* implements various forms of E-matching for its set of nodes (d_nodes), which
+* is refered to in the literature as a "trigger". A trigger is a set of terms
+* whose free variables are the bound variables of a quantified formula q,
+* and that is used to guide instantiations for q (for example, see "Efficient
+* E-Matching for SMT Solvers" by de Moura et al).
+*
+* For example of an instantiation lemma produced by E-matching :
+*
+* quantified formula : forall x. P( x )
+* trigger : P( x )
+* ground context : ~P( a )
+*
+* Then E-matching matches P( x ) and P( a ), resulting in the match { x -> a }
+* which is used to generate the instantiation lemma :
+* (forall x. P( x )) => P( a )
+*
+* Terms that are provided as input to a Trigger class via mkTrigger
+* should be in "instantiation constant form", see TermUtil::getInstConstantNode.
+* Say we have quantified formula q whose AST is the Node
+* (FORALL
+* (BOUND_VAR_LIST x)
+* (NOT (P x))
+* (INST_PATTERN_LIST (INST_PATTERN (P x))))
+* then TermUtil::getInstConstantNode( q, (P x) ) = (P IC) where
+* IC = TermUtil::getInstantiationConstant( q, i ).
+* Trigger expects as input (P IC) to represent the Trigger (P x). This form
+* ensures that references to bound variables are unique to quantified formulas,
+* which is required to ensure the correctness of instantiation lemmas we
+* generate.
+*
+*/
class Trigger {
- public:
- ~Trigger();
+ friend class IMGenerator;
+ public:
+ virtual ~Trigger();
+ /** get the generator associated with this trigger */
IMGenerator* getGenerator() { return d_mg; }
-
- /** reset instantiation round (call this whenever equivalence
- * classes have changed) */
+ /** Reset instantiation round.
+ *
+ * Called once at beginning of an instantiation round.
+ */
void resetInstantiationRound();
- /** reset, eqc is the equivalence class to search in (search in any
- * if eqc=null) */
+ /** Reset the trigger.
+ *
+ * eqc is the equivalence class from which to match ground terms. If eqc is
+ * Node::null(), then we match ground terms from all equivalence classes.
+ */
void reset( Node eqc );
- /** get next match. must call reset( eqc ) once before this function. */
- bool getNextMatch( Node f, InstMatch& m );
- /** return whether this is a multi-trigger */
+ /** add all available instantiations, based on the current context
+ *
+ * This function makes the appropriate calls to d_qe->addInstantiation(...)
+ * based on the current ground terms and equalities in the current context,
+ * via queries to functions in d_qe. This calls the addInstantiations function
+ * of the underlying match generator. It can be extended to
+ * produce instantiations beyond what is produced by the match generator
+ * (for example, see theory/quantifiers/ho_trigger.h).
+ *
+ * baseMatch : a mapping of default values that should be used for variables
+ * that are not bound as a result of matching terms from this
+ * trigger. These default values are not frequently used in
+ * instantiations. (TODO : remove #1389)
+ */
+ virtual int addInstantiations(InstMatch& baseMatch);
+ /** Return whether this is a multi-trigger. */
bool isMultiTrigger() { return d_nodes.size()>1; }
- /** get inst pattern list */
+ /** Get instantiation pattern list associated with this trigger.
+ *
+ * An instantiation pattern list is the node representation of a trigger, in
+ * particular, it is the third argument of quantified formulas which have user
+ * (! ... :pattern) attributes.
+ */
Node getInstPattern();
-
- /** add all available instantiations exhaustively, in any equivalence class
- if limitInst>0, limitInst is the max # of instantiations to try */
- int addInstantiations( InstMatch& baseMatch );
- /** mkTrigger method
- ie : quantifier engine;
- f : forall something ....
- nodes : (multi-)trigger
- keepAll: don't remove unneeded patterns;
- trOption : policy for dealing with triggers that already existed
- (see below)
+ /* A heuristic value indicating how active this generator is.
+ *
+ * This returns the number of ground terms for the match operators in terms
+ * from d_nodes. This score is only used with the experimental option
+ * --trigger-active-sel.
*/
+ int getActiveScore();
+ /** print debug information for the trigger */
+ void debugPrint(const char* c)
+ {
+ Trace(c) << "TRIGGER( ";
+ for (int i = 0; i < (int)d_nodes.size(); i++)
+ {
+ if (i > 0)
+ {
+ Trace(c) << ", ";
+ }
+ Trace(c) << d_nodes[i];
+ }
+ Trace(c) << " )";
+ }
+ /** mkTrigger method
+ *
+ * This makes an instance of a trigger object.
+ * qe : pointer to the quantifier engine;
+ * q : the quantified formula we are making a trigger for
+ * nodes : the nodes comprising the (multi-)trigger
+ * keepAll: don't remove unneeded patterns;
+ * trOption : policy for dealing with triggers that already exist
+ * (see below)
+ * use_n_vars : number of variables that should be bound by the trigger
+ * typically, the number of quantified variables in q.
+ */
enum{
TR_MAKE_NEW, //make new trigger even if it already may exist
TR_GET_OLD, //return a previous trigger if it had already been created
TR_RETURN_NULL //return null if a duplicate is found
};
- //nodes input, trNodes output
- static bool mkTriggerTerms( Node q, std::vector< Node >& nodes, unsigned n_vars, std::vector< Node >& trNodes );
- static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes,
- bool keepAll = true, int trOption = TR_MAKE_NEW, unsigned use_n_vars = 0 );
- static Trigger* mkTrigger( QuantifiersEngine* qe, Node f, Node n, bool keepAll = true,
- int trOption = TR_MAKE_NEW, unsigned use_n_vars = 0 );
+ static Trigger* mkTrigger(QuantifiersEngine* qe,
+ Node q,
+ std::vector<Node>& nodes,
+ bool keepAll = true,
+ int trOption = TR_MAKE_NEW,
+ unsigned use_n_vars = 0);
+ /** single trigger version that calls the above function */
+ static Trigger* mkTrigger(QuantifiersEngine* qe,
+ Node q,
+ Node n,
+ bool keepAll = true,
+ int trOption = TR_MAKE_NEW,
+ unsigned use_n_vars = 0);
+ /** make trigger terms
+ *
+ * This takes a set of eligible trigger terms and stores a subset of them in
+ * trNodes, such that :
+ * (1) the terms in trNodes contain at least n_vars of the quantified
+ * variables in quantified formula q, and
+ * (2) the set trNodes is minimal, i.e. removing one term from trNodes
+ * always violates (1).
+ */
+ static bool mkTriggerTerms(Node q,
+ std::vector<Node>& nodes,
+ unsigned n_vars,
+ std::vector<Node>& trNodes);
+ /** collect pattern terms
+ *
+ * This collects all terms that are eligible for triggers for quantified
+ * formula q in term n and adds them to patTerms.
+ * tstrt : the selection strategy (see options/quantifiers_mode.h),
+ * exclude : a set of terms that *cannot* be selected as triggers,
+ * tinfo : stores the result of the collection, mapping terms to the
+ * information they are associated with,
+ * filterInst : flag that when true, we discard terms that have instances
+ * in the vector we are returning, e.g. we do not return f( x ) if we are
+ * also returning f( f( x ) ). TODO: revisit this (issue #1211)
+ */
static void collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt,
std::vector< Node >& exclude, std::map< Node, TriggerTermInfo >& tinfo,
bool filterInst = false );
- /** is usable trigger */
+ /** Is n a usable trigger in quantified formula q?
+ *
+ * A usable trigger is one that is matchable and contains free variables only
+ * from q.
+ */
static bool isUsableTrigger( Node n, Node q );
+ /** get is usable trigger
+ *
+ * Return the associated node of n that is a usable trigger in quantified
+ * formula q. This may be different than n in several cases :
+ * (1) Polarity information is explicitly converted to equalities, e.g.
+ * getIsUsableTrigger( (not (P x )), q ) may return (= (P x) false)
+ * (2) Relational triggers are put into solved form, e.g.
+ * getIsUsableTrigger( (= (+ x a) 5), q ) may return (= x (- 5 a)).
+ */
static Node getIsUsableTrigger( Node n, Node q );
+ /** Is n a usable atomic trigger?
+ *
+ * A usable atomic trigger is a term that is both a useable trigger and an
+ * atomic trigger.
+ */
static bool isUsableAtomicTrigger( Node n, Node q );
+ /** is n an atomic trigger?
+ *
+ * An atomic trigger is one whose kind is an atomic trigger kind.
+ */
static bool isAtomicTrigger( Node n );
+ /** Is k an atomic trigger kind?
+ *
+ * An atomic trigger kind is one for which term indexing/matching is possible.
+ */
static bool isAtomicTriggerKind( Kind k );
+ /** is n a relational trigger, e.g. like x >= a ? */
static bool isRelationalTrigger( Node n );
+ /** Is k a relational trigger kind? */
static bool isRelationalTriggerKind( Kind k );
+ /** Is k a kind for which counterexample-guided instantiation is possible?
+ *
+ * This typically corresponds to kinds that correspond to operators that
+ * have total interpretations and are a part of the signature of
+ * satisfaction complete theories (see Reynolds et al., CAV 2015).
+ */
static bool isCbqiKind( Kind k );
+ /** is n a simple trigger (see inst_match_generator.h)? */
static bool isSimpleTrigger( Node n );
+ /** is n a Boolean term trigger, e.g. ite( x, BV1, BV0 )? */
static bool isBooleanTermTrigger( Node n );
+ /** is n a pure theory trigger, e.g. head( x )? */
static bool isPureTheoryTrigger( Node n );
+ /** get trigger weight
+ *
+ * Returns 0 for triggers that are easy to process and 1 otherwise.
+ * A trigger is easy to process if it is an atomic trigger, or a relational
+ * trigger of the form x ~ g for ~ \in { =, >=, > }.
+ */
static int getTriggerWeight( Node n );
+ /** Returns whether n is a trigger term with a local theory extension
+ * property from Bansal et al., CAV 2015.
+ */
static bool isLocalTheoryExt( Node n, std::vector< Node >& vars,
std::vector< Node >& patTerms );
- /** return data structure for producing matches for this trigger. */
- static InstMatchGenerator* getInstMatchGenerator( Node q, Node n );
+ /** get the variable associated with an inversion for n
+ *
+ * A term n with an inversion variable x has the following property :
+ * There exists a closed function f such that for all terms t
+ * |= (n = t) <=> (x = f(t))
+ * For example, getInversionVariable( x+1 ) returns x since for all terms t,
+ * |= x+1 = t <=> x = (\y. y-1)(t)
+ * We call f the inversion function for n.
+ */
static Node getInversionVariable( Node n );
- static Node getInversion( Node n, Node x );
- /** get all variables that E-matching can possibly handle */
- static void getTriggerVariables( Node icn, Node f, std::vector< Node >& t_vars );
+ /** Get the body of the inversion function for n whose argument is y.
+ * e.g. getInversion( x+1, y ) returns y-1
+ */
+ static Node getInversion(Node n, Node y);
+ /** get all variables that E-matching can instantiate from a subterm n.
+ *
+ * This returns the union of all free variables in usable triggers that are
+ * subterms of n.
+ */
+ static void getTriggerVariables(Node n, Node f, std::vector<Node>& t_vars);
- void debugPrint( const char * c ) {
- Trace(c) << "TRIGGER( ";
- for( int i=0; i<(int)d_nodes.size(); i++ ){
- if( i>0 ){ Trace(c) << ", "; }
- Trace(c) << d_nodes[i];
- }
- Trace(c) << " )";
- }
- int getActiveScore();
-private:
- /** trigger constructor */
+ protected:
+ /** trigger constructor, intentionally protected (use Trigger::mkTrigger). */
Trigger( QuantifiersEngine* ie, Node f, std::vector< Node >& nodes );
-
- /** is subterm of trigger usable */
+ /** is subterm of trigger usable (helper function for isUsableTrigger) */
static bool isUsable( Node n, Node q );
+ /** returns an equality that is equivalent to the equality eq and
+ * is a usable trigger for q if one exists, otherwise returns Node::null().
+ */
static Node getIsUsableEq( Node q, Node eq );
+ /** returns whether n1 == n2 is a usable (relational) trigger for q. */
static bool isUsableEqTerms( Node q, Node n1, Node n2 );
- /** collect all APPLY_UF pattern terms for f in n */
+ /** recursive helper function for collectPatTerms
+ *
+ * This collects the usable trigger terms in the subterm n of the body of
+ * quantified formula q.
+ * visited : cache of the trigger terms collected for each visited node,
+ * tinfo : cache of trigger term info for each visited node,
+ * tstrat : the selection strategy (see options/quantifiers_mode.h)
+ * exclude : a set of terms that *cannot* be selected as triggers
+ * pol/hasPol : the polarity of node n in q
+ * (see QuantPhaseReq theory/quantifiers/quant_util.h)
+ * epol/hasEPol : the entailed polarity of node n in q
+ * (see QuantPhaseReq theory/quantifiers/quant_util.h)
+ * knowIsUsable : whether we know that n is a usable trigger.
+ *
+ * We add the triggers we collected recursively in n into added.
+ */
static void collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Node > >& visited, std::map< Node, TriggerTermInfo >& tinfo,
quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added,
bool pol, bool hasPol, bool epol, bool hasEPol, bool knowIsUsable = false );
+ /** add an instantiation (called by InstMatchGenerator)
+ *
+ * This calls Instantiate::addInstantiation(...) for instantiations
+ * associated with m. Typically, m is associated with a single instantiation,
+ * but in some cases (e.g. higher-order) we may modify m before calling
+ * Instantiate::addInstantiation(...).
+ */
+ virtual bool sendInstantiation(InstMatch& m);
+ /** The nodes comprising this trigger. */
std::vector< Node > d_nodes;
-
- /** the quantifiers engine */
+ /** The quantifiers engine associated with this trigger. */
QuantifiersEngine* d_quantEngine;
- /** the quantifier this trigger is for */
+ /** The quantified formula this trigger is for. */
Node d_f;
- /** match generators */
+ /** match generator
+ *
+ * This is the back-end utility that implements the underlying matching
+ * algorithm associated with this trigger.
+ */
IMGenerator* d_mg;
}; /* class Trigger */
-/** a trie of triggers */
+/** A trie of triggers.
+*
+* This class is used to cache all Trigger objects that are generated in the
+* current context. We index Triggers in this data structure based on the
+* value of Trigger::d_nodes. When a Trigger is added to this data structure,
+* this Trie assumes responsibility for deleting it.
+*/
class TriggerTrie {
public:
TriggerTrie();
~TriggerTrie();
+ /** get trigger
+ * This returns a Trigger t that is indexed by nodes,
+ * or NULL otherwise.
+ */
+ Trigger* getTrigger(std::vector<Node>& nodes);
+ /** add trigger
+ * This adds t to the trie, indexed by nodes.
+ * In typical use cases, nodes is t->d_nodes.
+ */
+ void addTrigger(std::vector<Node>& nodes, Trigger* t);
- inst::Trigger* getTrigger( std::vector< Node >& nodes ){
- std::vector< Node > temp;
- temp.insert( temp.begin(), nodes.begin(), nodes.end() );
- std::sort( temp.begin(), temp.end() );
- return getTrigger2( temp );
- }
- void addTrigger( std::vector< Node >& nodes, inst::Trigger* t ){
- std::vector< Node > temp;
- temp.insert( temp.begin(), nodes.begin(), nodes.end() );
- std::sort( temp.begin(), temp.end() );
- return addTrigger2( temp, t );
- }
-private:
- inst::Trigger* getTrigger2( std::vector< Node >& nodes );
- void addTrigger2( std::vector< Node >& nodes, inst::Trigger* t );
-
- std::vector< inst::Trigger* > d_tr;
+ private:
+ /** The trigger at this node in the trie. */
+ std::vector<Trigger*> d_tr;
+ /** The children of this node in the trie. */
std::map< TNode, TriggerTrie* > d_children;
};/* class inst::Trigger::TriggerTrie */
projects / cvc5.git / commitdiff