summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/ematching
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/ematching')
-rw-r--r--src/theory/quantifiers/ematching/ho_trigger.cpp475
-rw-r--r--src/theory/quantifiers/ematching/ho_trigger.h278
-rw-r--r--src/theory/quantifiers/ematching/inst_match_generator.cpp1138
-rw-r--r--src/theory/quantifiers/ematching/inst_match_generator.h694
-rw-r--r--src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp613
-rw-r--r--src/theory/quantifiers/ematching/inst_strategy_e_matching.h119
-rw-r--r--src/theory/quantifiers/ematching/instantiation_engine.cpp209
-rw-r--r--src/theory/quantifiers/ematching/instantiation_engine.h98
-rw-r--r--src/theory/quantifiers/ematching/trigger.cpp969
-rw-r--r--src/theory/quantifiers/ematching/trigger.h476
10 files changed, 5069 insertions, 0 deletions
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
new file mode 100644
index 000000000..0e0955119
--- /dev/null
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -0,0 +1,475 @@
+/********************* */
+/*! \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/ematching/ho_trigger.h"
+#include "theory/quantifiers/instantiate.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, Node& n, std::map<Node, std::vector<Node> >& apps)
+{
+ std::vector<Node> ns;
+ ns.push_back(n);
+ collectHoVarApplyTerms(q, ns, apps);
+ Assert(ns.size() == 1);
+ n = ns[0];
+}
+
+void HigherOrderTrigger::collectHoVarApplyTerms(
+ Node q, std::vector<Node>& ns, std::map<Node, std::vector<Node> >& apps)
+{
+ std::unordered_map<TNode, Node, TNodeHashFunction> visited;
+ std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+ // whether the visited node is a child of a HO_APPLY chain
+ std::unordered_map<TNode, bool, TNodeHashFunction> withinApply;
+ std::vector<TNode> visit;
+ TNode cur;
+ for (unsigned i = 0, size = ns.size(); i < size; i++)
+ {
+ visit.push_back(ns[i]);
+ withinApply[ns[i]] = false;
+ do
+ {
+ cur = visit.back();
+ visit.pop_back();
+
+ it = visited.find(cur);
+ if (it == visited.end())
+ {
+ // do not look in nested quantifiers
+ if (cur.getKind() == FORALL)
+ {
+ visited[cur] = cur;
+ }
+ else
+ {
+ bool curWithinApply = withinApply[cur];
+ visited[cur] = Node::null();
+ visit.push_back(cur);
+ for (unsigned j = 0, size = cur.getNumChildren(); j < size; j++)
+ {
+ withinApply[cur[j]] = curWithinApply && j == 0;
+ visit.push_back(cur[j]);
+ }
+ }
+ }
+ else if (it->second.isNull())
+ {
+ // carry the conversion
+ Node ret = cur;
+ bool childChanged = false;
+ std::vector<Node> children;
+ if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
+ {
+ children.push_back(cur.getOperator());
+ }
+ for (const Node& nc : cur)
+ {
+ it = visited.find(nc);
+ Assert(it != visited.end());
+ Assert(!it->second.isNull());
+ childChanged = childChanged || nc != it->second;
+ children.push_back(it->second);
+ }
+ if (childChanged)
+ {
+ ret = NodeManager::currentNM()->mkNode(cur.getKind(), children);
+ }
+ // now, convert and store the application
+ if (!withinApply[cur])
+ {
+ TNode op;
+ if (ret.getKind() == kind::APPLY_UF)
+ {
+ // could be a fully applied function variable
+ op = ret.getOperator();
+ }
+ else if (ret.getKind() == kind::HO_APPLY)
+ {
+ op = ret;
+ while (op.getKind() == kind::HO_APPLY)
+ {
+ op = op[0];
+ }
+ }
+ if (!op.isNull())
+ {
+ if (op.getKind() == kind::INST_CONSTANT)
+ {
+ Assert(quantifiers::TermUtil::getInstConstAttr(ret) == q);
+ Trace("ho-quant-trigger-debug")
+ << "Ho variable apply term : " << ret << " with head " << op
+ << std::endl;
+ if (ret.getKind() == kind::APPLY_UF)
+ {
+ Node prev = ret;
+ // for consistency, convert to HO_APPLY if fully applied
+ ret = uf::TheoryUfRewriter::getHoApplyForApplyUf(ret);
+ }
+ apps[op].push_back(ret);
+ }
+ }
+ }
+ visited[cur] = ret;
+ }
+ } while (!visit.empty());
+
+ // store the conversion
+ Assert(visited.find(ns[i]) != visited.end());
+ ns[i] = visited[ns[i]];
+ }
+}
+
+int HigherOrderTrigger::addInstantiations()
+{
+ // call the base class implementation
+ int addedFoLemmas = Trigger::addInstantiations();
+ // 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;
+ quantifiers::TermUtil* tutil = d_quantEngine->getTermUtil();
+ for (unsigned i = 0, size = d_quant[0].getNumChildren(); i < size; i++)
+ {
+ subs.push_back(m.d_vals[i]);
+ vars.push_back(tutil->getInstantiationConstant(d_quant, 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->getInstantiate()->addInstantiation(d_quant, 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->getInstantiate()->addInstantiation(d_quant, 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 */
diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h
new file mode 100644
index 000000000..41fec5e5f
--- /dev/null
+++ b/src/theory/quantifiers/ematching/ho_trigger.h
@@ -0,0 +1,278 @@
+/********************* */
+/*! \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/ematching/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 x in
+ * quantified formula q. Append all such terms in apps[x].
+ * This method may modify n so that it is in the expected form required for
+ * higher-order matching, in particular, APPLY_UF terms with variable
+ * operators are converted to curried applications of HO_APPLY.
+ */
+ static void collectHoVarApplyTerms(Node q,
+ Node& n,
+ std::map<Node, std::vector<Node> >& apps);
+ /** Collect higher order var apply terms
+ *
+ * Same as above, but with multiple terms ns.
+ */
+ 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() 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.
+ */
+ bool sendInstantiation(InstMatch& m) override;
+
+ 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 */
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
new file mode 100644
index 000000000..c36597e3e
--- /dev/null
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -0,0 +1,1138 @@
+/********************* */
+/*! \file inst_match_generator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Morgan Deters, Tim King
+ ** 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
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+#include "theory/quantifiers/ematching/inst_match_generator.h"
+
+#include "expr/datatype.h"
+#include "options/datatypes_options.h"
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/candidate_generator.h"
+#include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers/ematching/trigger.h"
+#include "theory/quantifiers_engine.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+
+namespace CVC4 {
+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 = true;
+ Assert( quantifiers::TermUtil::hasInstConstAttr(pat) );
+ d_pattern = pat;
+ d_match_pattern = pat;
+ d_match_pattern_type = pat.getType();
+ d_next = NULL;
+ d_independent_gen = false;
+}
+
+InstMatchGenerator::InstMatchGenerator() {
+ d_cg = NULL;
+ d_needsReset = true;
+ d_active_add = true;
+ d_next = NULL;
+ d_independent_gen = false;
+}
+
+InstMatchGenerator::~InstMatchGenerator()
+{
+ for( unsigned i=0; i<d_children.size(); i++ ){
+ delete d_children[i];
+ }
+ delete d_cg;
+}
+
+void InstMatchGenerator::setActiveAdd(bool val){
+ d_active_add = val;
+ if( d_next!=NULL ){
+ d_next->setActiveAdd(val);
+ }
+}
+
+int InstMatchGenerator::getActiveScore( QuantifiersEngine * qe ) {
+ if( d_match_pattern.isNull() ){
+ return -1;
+ }else if( Trigger::isAtomicTrigger( d_match_pattern ) ){
+ Node f = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
+ unsigned ngt = qe->getTermDatabase()->getNumGroundTerms( f );
+ Trace("trigger-active-sel-debug") << "Number of ground terms for " << f << " is " << ngt << std::endl;
+ return ngt;
+ }else if( d_match_pattern.getKind()==INST_CONSTANT ){
+ TypeNode tn = d_match_pattern.getType();
+ unsigned ngtt = qe->getTermDatabase()->getNumTypeGroundTerms( tn );
+ Trace("trigger-active-sel-debug") << "Number of ground terms for " << tn << " is " << ngtt << std::endl;
+ return ngtt;
+// }else if( d_match_pattern_getKind()==EQUAL ){
+
+ }else{
+ return -1;
+ }
+}
+
+void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< InstMatchGenerator * > & gens ){
+ if( !d_pattern.isNull() ){
+ Trace("inst-match-gen") << "Initialize, pattern term is " << d_pattern << std::endl;
+ if( d_match_pattern.getKind()==NOT ){
+ //we want to add the children of the NOT
+ d_match_pattern = d_pattern[0];
+ }
+ if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==GEQ ){
+ //make sure the matching portion of the equality is on the LHS of d_pattern
+ // and record what d_match_pattern is
+ for( unsigned i=0; i<2; i++ ){
+ if( !quantifiers::TermUtil::hasInstConstAttr(d_match_pattern[i]) || d_match_pattern[i].getKind()==INST_CONSTANT ){
+ Node mp = d_match_pattern[1-i];
+ Node mpo = d_match_pattern[i];
+ if( mp.getKind()!=INST_CONSTANT ){
+ if( i==0 ){
+ if( d_match_pattern.getKind()==GEQ ){
+ d_pattern = NodeManager::currentNM()->mkNode( kind::GT, mp, mpo );
+ d_pattern = d_pattern.negate();
+ }else{
+ d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), mp, mpo );
+ }
+ }
+ d_eq_class_rel = mpo;
+ d_match_pattern = mp;
+ }
+ break;
+ }
+ }
+ }else if( d_match_pattern.getKind()==APPLY_SELECTOR_TOTAL && d_match_pattern[0].getKind()==INST_CONSTANT &&
+ options::purifyDtTriggers() && !options::dtSharedSelectors() ){
+ d_match_pattern = d_match_pattern[0];
+ }
+ d_match_pattern_type = d_match_pattern.getType();
+ Trace("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl;
+ d_match_pattern_op = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
+
+ //now, collect children of d_match_pattern
+ if (d_match_pattern.getKind() == INST_CONSTANT)
+ {
+ d_children_types.push_back(
+ 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(-2);
+ }else{
+ if (d_match_pattern[i].getKind() == INST_CONSTANT && qa == q)
+ {
+ d_children_types.push_back(
+ d_match_pattern[i].getAttribute(InstVarNumAttribute()));
+ }
+ else
+ {
+ d_children_types.push_back(-1);
+ }
+ }
+ }
+ else
+ {
+ d_children_types.push_back(-1);
+ }
+ }
+ }
+
+ //create candidate generator
+ if( Trigger::isAtomicTrigger( d_match_pattern ) ){
+ //we will be scanning lists trying to find d_match_pattern.getOperator()
+ d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern );
+ //if matching on disequality, inform the candidate generator not to match on eqc
+ if( d_pattern.getKind()==NOT && d_pattern[0].getKind()==EQUAL ){
+ ((inst::CandidateGeneratorQE*)d_cg)->excludeEqc( d_eq_class_rel );
+ d_eq_class_rel = Node::null();
+ }
+ }else if( d_match_pattern.getKind()==INST_CONSTANT ){
+ if( d_pattern.getKind()==APPLY_SELECTOR_TOTAL ){
+ Expr selectorExpr = qe->getTermDatabase()->getMatchOperator( d_pattern ).toExpr();
+ size_t selectorIndex = Datatype::cindexOf(selectorExpr);
+ const Datatype& dt = Datatype::datatypeOf(selectorExpr);
+ const DatatypeConstructor& c = dt[selectorIndex];
+ Node cOp = Node::fromExpr(c.getConstructor());
+ Trace("inst-match-gen") << "Purify dt trigger " << d_pattern << ", will match terms of op " << cOp << std::endl;
+ d_cg = new inst::CandidateGeneratorQE( qe, cOp );
+ }else{
+ d_cg = new CandidateGeneratorQEAll( qe, d_match_pattern );
+ }
+ }else if( d_match_pattern.getKind()==EQUAL &&
+ d_match_pattern[0].getKind()==INST_CONSTANT && d_match_pattern[1].getKind()==INST_CONSTANT ){
+ //we will be producing candidates via literal matching heuristics
+ if( d_pattern.getKind()!=NOT ){
+ //candidates will be all equalities
+ d_cg = new inst::CandidateGeneratorQELitEq( qe, d_match_pattern );
+ }else{
+ //candidates will be all disequalities
+ d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern );
+ }
+ }else{
+ Trace("inst-match-gen-warn") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
+ }
+ }
+ gens.insert( gens.end(), d_children.begin(), d_children.end() );
+}
+
+/** get match (not modulo equality) */
+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 (d_cg == nullptr)
+ {
+ Trace("matching-fail") << "Internal error for match generator." << std::endl;
+ return -2;
+ }else{
+ EqualityQuery* q = qe->getEqualityQuery();
+ bool success = true;
+ //save previous match
+ //InstMatch prev( &m );
+ std::vector< int > prev;
+ //if t is null
+ Assert( !t.isNull() );
+ Assert( !quantifiers::TermUtil::hasInstConstAttr(t) );
+ Assert( d_match_pattern.getKind()==INST_CONSTANT || t.getKind()==d_match_pattern.getKind() );
+ Assert( !Trigger::isAtomicTrigger( d_match_pattern ) || t.getOperator()==d_match_pattern.getOperator() );
+ //first, check if ground arguments are not equal, or a match is in conflict
+ Trace("matching-debug2") << "Setting immediate matches..." << std::endl;
+ for (unsigned i = 0, size = d_match_pattern.getNumChildren(); i < size; i++)
+ {
+ int ct = d_children_types[i];
+ if (ct >= 0)
+ {
+ Trace("matching-debug2") << "Setting " << ct << " to " << t[i] << "..."
+ << std::endl;
+ bool addToPrev = m.get(ct).isNull();
+ if (!m.set(q, ct, t[i]))
+ {
+ //match is in conflict
+ Trace("matching-fail") << "Match fail: " << m.get(ct) << " and "
+ << t[i] << std::endl;
+ success = false;
+ break;
+ }else if( addToPrev ){
+ Trace("matching-debug2") << "Success." << std::endl;
+ prev.push_back(ct);
+ }
+ }
+ else if (ct == -1)
+ {
+ if( !q->areEqual( d_match_pattern[i], t[i] ) ){
+ Trace("matching-fail") << "Match fail arg: " << d_match_pattern[i] << " and " << t[i] << std::endl;
+ //ground arguments are not equal
+ success = false;
+ break;
+ }
+ }
+ }
+ Trace("matching-debug2") << "Done setting immediate matches, success = " << success << "." << std::endl;
+ //for variable matching
+ if( d_match_pattern.getKind()==INST_CONSTANT ){
+ bool addToPrev = m.get(d_children_types[0]).isNull();
+ if (!m.set(q, d_children_types[0], t))
+ {
+ success = false;
+ }else{
+ if( addToPrev ){
+ prev.push_back(d_children_types[0]);
+ }
+ }
+ //for relational matching
+ }else if( !d_eq_class_rel.isNull() && d_eq_class_rel.getKind()==INST_CONSTANT ){
+ int v = d_eq_class_rel.getAttribute(InstVarNumAttribute());
+ //also must fit match to equivalence class
+ bool pol = d_pattern.getKind()!=NOT;
+ Node pat = d_pattern.getKind()==NOT ? d_pattern[0] : d_pattern;
+ Node t_match;
+ if( pol ){
+ if( pat.getKind()==GT ){
+ t_match = NodeManager::currentNM()->mkNode(MINUS, t, qe->getTermUtil()->d_one);
+ }else{
+ t_match = t;
+ }
+ }else{
+ if( pat.getKind()==EQUAL ){
+ if( t.getType().isBoolean() ){
+ t_match = NodeManager::currentNM()->mkConst( !q->areEqual( qe->getTermUtil()->d_true, t ) );
+ }else{
+ Assert( t.getType().isReal() );
+ t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermUtil()->d_one);
+ }
+ }else if( pat.getKind()==GEQ ){
+ t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermUtil()->d_one);
+ }else if( pat.getKind()==GT ){
+ t_match = t;
+ }
+ }
+ if( !t_match.isNull() ){
+ bool addToPrev = m.get( v ).isNull();
+ if (!m.set(q, v, t_match))
+ {
+ success = false;
+ }else if( addToPrev ){
+ prev.push_back( v );
+ }
+ }
+ }
+ int ret_val = -1;
+ if( success ){
+ Trace("matching-debug2") << "Reset children..." << std::endl;
+ //now, fit children into match
+ //we will be requesting candidates for matching terms for each child
+ for (unsigned i = 0, size = d_children.size(); i < size; i++)
+ {
+ if( !d_children[i]->reset( t[ d_children_index[i] ], qe ) ){
+ success = false;
+ break;
+ }
+ }
+ if( success ){
+ Trace("matching-debug2") << "Continue next " << d_next << std::endl;
+ ret_val = continueNextMatch(f, m, qe, tparent);
+ }
+ }
+ if( ret_val<0 ){
+ for (int& pv : prev)
+ {
+ m.d_vals[pv] = Node::null();
+ }
+ }
+ return ret_val;
+ }
+}
+
+int InstMatchGenerator::continueNextMatch(Node f,
+ InstMatch& m,
+ QuantifiersEngine* qe,
+ Trigger* tparent)
+{
+ if( d_next!=NULL ){
+ return d_next->getNextMatch(f, m, qe, tparent);
+ }else{
+ if( d_active_add ){
+ return sendInstantiation(tparent, m) ? 1 : -1;
+ }else{
+ return 1;
+ }
+ }
+}
+
+/** reset instantiation round */
+void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){
+ if( !d_match_pattern.isNull() ){
+ Trace("matching-debug2") << this << " reset instantiation round." << std::endl;
+ d_needsReset = true;
+ if( d_cg ){
+ d_cg->resetInstantiationRound();
+ }
+ }
+ if( d_next ){
+ d_next->resetInstantiationRound( qe );
+ }
+ d_curr_exclude_match.clear();
+}
+
+bool InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){
+ eqc = qe->getEqualityQuery()->getRepresentative( eqc );
+ Trace("matching-debug2") << this << " reset " << eqc << "." << std::endl;
+ if( !d_eq_class_rel.isNull() && d_eq_class_rel.getKind()!=INST_CONSTANT ){
+ d_eq_class = d_eq_class_rel;
+ }else if( !eqc.isNull() ){
+ d_eq_class = eqc;
+ }
+ //we have a specific equivalence class in mind
+ //we are producing matches for f(E) ~ t, where E is a non-ground vector of terms, and t is a ground term
+ //just look in equivalence class of the RHS
+ d_cg->reset( d_eq_class );
+ d_needsReset = false;
+
+ //generate the first candidate preemptively
+ d_curr_first_candidate = Node::null();
+ Node t;
+ do {
+ t = d_cg->getNextCandidate();
+ if( d_curr_exclude_match.find( t )==d_curr_exclude_match.end() ){
+ d_curr_first_candidate = t;
+ }
+ }while( !t.isNull() && d_curr_first_candidate.isNull() );
+ Trace("matching-summary") << "Reset " << d_match_pattern << " in " << eqc << " returns " << !d_curr_first_candidate.isNull() << "." << std::endl;
+
+ return !d_curr_first_candidate.isNull();
+}
+
+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 );
+ }
+ d_curr_matched = Node::null();
+ Trace("matching") << this << " " << d_match_pattern << " get next match " << m << " in eq class " << d_eq_class << std::endl;
+ int success = -1;
+ Node t = d_curr_first_candidate;
+ do{
+ Trace("matching-debug2") << "Matching candidate : " << t << std::endl;
+ //if t not null, try to fit it into match m
+ if( !t.isNull() ){
+ 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, tparent);
+ if( d_independent_gen && success<0 ){
+ Assert( d_eq_class.isNull() );
+ d_curr_exclude_match[t] = true;
+ }
+ }
+ //get the next candidate term t
+ if( success<0 ){
+ t = d_cg->getNextCandidate();
+ }else{
+ d_curr_first_candidate = d_cg->getNextCandidate();
+ }
+ }
+ }while( success<0 && !t.isNull() );
+ d_curr_matched = t;
+ if( success<0 ){
+ Trace("matching-summary") << "..." << d_match_pattern << " failed, reset." << std::endl;
+ Trace("matching") << this << " failed, reset " << d_eq_class << std::endl;
+ //we failed, must reset
+ reset( d_eq_class, qe );
+ }else{
+ Trace("matching-summary") << "..." << d_match_pattern << " success." << std::endl;
+ }
+ return success;
+}
+
+int InstMatchGenerator::addInstantiations(Node f,
+ QuantifiersEngine* qe,
+ Trigger* tparent)
+{
+ //try to add instantiation for each match produced
+ int addedLemmas = 0;
+ InstMatch m( f );
+ while (getNextMatch(f, m, qe, tparent) > 0)
+ {
+ if( !d_active_add ){
+ if (sendInstantiation(tparent, m))
+ {
+ addedLemmas++;
+ if( qe->inConflict() ){
+ break;
+ }
+ }
+ }else{
+ addedLemmas++;
+ if( qe->inConflict() ){
+ break;
+ }
+ }
+ m.clear();
+ }
+ //return number of lemmas added
+ return addedLemmas;
+}
+
+
+InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( Node q, Node pat, QuantifiersEngine* qe ) {
+ std::vector< Node > pats;
+ pats.push_back( pat );
+ std::map< Node, InstMatchGenerator * > pat_map_init;
+ return mkInstMatchGenerator( q, pats, qe, pat_map_init );
+}
+
+InstMatchGenerator* InstMatchGenerator::mkInstMatchGeneratorMulti( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ) {
+ Assert( pats.size()>1 );
+ InstMatchGeneratorMultiLinear * imgm = new InstMatchGeneratorMultiLinear( q, pats, qe );
+ std::vector< InstMatchGenerator* > gens;
+ imgm->initialize(q, qe, gens);
+ Assert( gens.size()==pats.size() );
+ std::vector< Node > patsn;
+ std::map< Node, InstMatchGenerator * > pat_map_init;
+ for( unsigned i=0; i<gens.size(); i++ ){
+ Node pn = gens[i]->d_match_pattern;
+ patsn.push_back( pn );
+ pat_map_init[pn] = gens[i];
+ }
+ //return mkInstMatchGenerator( q, patsn, qe, pat_map_init );
+ imgm->d_next = mkInstMatchGenerator( q, patsn, qe, pat_map_init );
+ return imgm;
+}
+
+InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( Node q, std::vector< Node >& pats, QuantifiersEngine* qe,
+ std::map< Node, InstMatchGenerator * >& pat_map_init ) {
+ size_t pCounter = 0;
+ InstMatchGenerator* prev = NULL;
+ InstMatchGenerator* oinit = NULL;
+ while( pCounter<pats.size() ){
+ size_t counter = 0;
+ std::vector< InstMatchGenerator* > gens;
+ InstMatchGenerator* init;
+ std::map< Node, InstMatchGenerator * >::iterator iti = pat_map_init.find( pats[pCounter] );
+ if( iti==pat_map_init.end() ){
+ init = new InstMatchGenerator(pats[pCounter]);
+ }else{
+ init = iti->second;
+ }
+ if(pCounter==0){
+ oinit = init;
+ }
+ gens.push_back(init);
+ //chain the resulting match generators together
+ while (counter<gens.size()) {
+ InstMatchGenerator* curr = gens[counter];
+ if( prev ){
+ prev->d_next = curr;
+ }
+ curr->initialize(q, qe, gens);
+ prev = curr;
+ counter++;
+ }
+ pCounter++;
+ }
+ 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_children_types.push_back(var.getAttribute(InstVarNumAttribute()));
+}
+
+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 ));
+ d_eq_class = Node::null();
+ d_rm_prev = m.get(d_children_types[0]).isNull();
+ if (!m.set(qe->getEqualityQuery(), d_children_types[0], s))
+ {
+ return -1;
+ }else{
+ ret_val = continueNextMatch(q, m, qe, tparent);
+ if( ret_val>0 ){
+ return ret_val;
+ }
+ }
+ }
+ if( d_rm_prev ){
+ m.d_vals[d_children_types[0]] = Node::null();
+ d_rm_prev = false;
+ }
+ return ret_val;
+}
+
+VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs( Node var, Node subs ) :
+ InstMatchGenerator(), d_var( var ), d_subs( subs ), d_rm_prev( false ){
+ d_children_types.push_back(d_var.getAttribute(InstVarNumAttribute()));
+ d_var_type = d_var.getType();
+}
+
+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;
+ Node s = d_subs.substitute( d_var, d_eq_class );
+ s = Rewriter::rewrite( s );
+ Trace("var-trigger-matching") << "...got " << s << ", " << s.getKind() << std::endl;
+ d_eq_class = Node::null();
+ //if( s.getType().isSubtypeOf( d_var_type ) ){
+ d_rm_prev = m.get(d_children_types[0]).isNull();
+ if (!m.set(qe->getEqualityQuery(), d_children_types[0], s))
+ {
+ return -1;
+ }else{
+ ret_val = continueNextMatch(q, m, qe, tparent);
+ if( ret_val>0 ){
+ return ret_val;
+ }
+ }
+ }
+ if( d_rm_prev ){
+ m.d_vals[d_children_types[0]] = Node::null();
+ d_rm_prev = false;
+ }
+ return -1;
+}
+
+InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ) {
+ //order patterns to maximize eager matching failures
+ std::map< Node, std::vector< Node > > var_contains;
+ qe->getTermUtil()->getVarContains( q, pats, var_contains );
+ std::map< Node, std::vector< Node > > var_to_node;
+ for( std::map< Node, std::vector< Node > >::iterator it = var_contains.begin(); it != var_contains.end(); ++it ){
+ for( unsigned i=0; i<it->second.size(); i++ ){
+ var_to_node[ it->second[i] ].push_back( it->first );
+ }
+ }
+ std::vector< Node > pats_ordered;
+ std::vector< bool > pats_ordered_independent;
+ std::map< Node, bool > var_bound;
+ while( pats_ordered.size()<pats.size() ){
+ // score is lexographic ( bound vars, shared vars )
+ int score_max_1 = -1;
+ int score_max_2 = -1;
+ int score_index = -1;
+ for( unsigned i=0; i<pats.size(); i++ ){
+ Node p = pats[i];
+ if( std::find( pats_ordered.begin(), pats_ordered.end(), p )==pats_ordered.end() ){
+ int score_1 = 0;
+ int score_2 = 0;
+ for( unsigned j=0; j<var_contains[p].size(); j++ ){
+ Node v = var_contains[p][j];
+ if( var_bound.find( v )!=var_bound.end() ){
+ score_1++;
+ }else if( var_to_node[v].size()>1 ){
+ score_2++;
+ }
+ }
+ if( score_index==-1 || score_1>score_max_1 || ( score_1==score_max_1 && score_2>score_max_2 ) ){
+ score_index = i;
+ score_max_1 = score_1;
+ score_max_2 = score_2;
+ }
+ }
+ }
+ //update the variable bounds
+ Node mp = pats[score_index];
+ for( unsigned i=0; i<var_contains[mp].size(); i++ ){
+ var_bound[var_contains[mp][i]] = true;
+ }
+ pats_ordered.push_back( mp );
+ pats_ordered_independent.push_back( score_max_1==0 );
+ }
+
+ 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 = getInstMatchGenerator(q, pats_ordered[i]);
+ Assert( cimg!=NULL );
+ d_children.push_back( cimg );
+ if( i==0 ){ //TODO : improve
+ cimg->setIndependent();
+ }
+ }
+}
+
+int InstMatchGeneratorMultiLinear::resetChildren( QuantifiersEngine* qe ){
+ for( unsigned i=0; i<d_children.size(); i++ ){
+ if( !d_children[i]->reset( Node::null(), qe ) ){
+ return -2;
+ }
+ }
+ return 1;
+}
+
+bool InstMatchGeneratorMultiLinear::reset( Node eqc, QuantifiersEngine* qe ) {
+ Assert( eqc.isNull() );
+ if( options::multiTriggerLinear() ){
+ return true;
+ }else{
+ return resetChildren( qe )>0;
+ }
+}
+
+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
+ int rc_ret = resetChildren( qe );
+ if( rc_ret<0 ){
+ return rc_ret;
+ }
+ }
+ Trace("multi-trigger-linear-debug") << "InstMatchGeneratorMultiLinear::getNextMatch : continue match " << std::endl;
+ Assert( d_next!=NULL );
+ 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]->getCurrentMatch();
+ Trace("multi-trigger-linear") << " child " << i << " match : " << mi << std::endl;
+ d_children[i]->excludeMatch( mi );
+ }
+ }
+ }
+ return ret_val;
+}
+
+
+/** constructors */
+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 );
+ //convert to indicies
+ for( std::map< Node, std::vector< Node > >::iterator it = var_contains.begin(); it != var_contains.end(); ++it ){
+ Trace("multi-trigger-cache") << "Pattern " << it->first << " contains: ";
+ for( int i=0; i<(int)it->second.size(); i++ ){
+ Trace("multi-trigger-cache") << it->second[i] << " ";
+ int index = it->second[i].getAttribute(InstVarNumAttribute());
+ d_var_contains[ it->first ].push_back( index );
+ d_var_to_node[ index ].push_back( it->first );
+ }
+ Trace("multi-trigger-cache") << std::endl;
+ }
+ for( unsigned i=0; i<pats.size(); i++ ){
+ Node n = pats[i];
+ //make the match generator
+ 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;
+ int numSharedVars = 0;
+ for( unsigned j=0; j<d_var_contains[n].size(); j++ ){
+ if( d_var_to_node[ d_var_contains[n][j] ].size()==1 ){
+ Trace("multi-trigger-cache") << "Var " << d_var_contains[n][j] << " is unique to " << pats[i] << std::endl;
+ unique_vars.push_back( d_var_contains[n][j] );
+ }else{
+ shared_vars[ d_var_contains[n][j] ] = true;
+ numSharedVars++;
+ }
+ }
+ //we use the latest shared variables, then unique variables
+ std::vector< int > vars;
+ unsigned index = i==0 ? pats.size()-1 : (i-1);
+ while( numSharedVars>0 && index!=i ){
+ for( std::map< int, bool >::iterator it = shared_vars.begin(); it != shared_vars.end(); ++it ){
+ if( it->second ){
+ if( std::find( d_var_contains[ pats[index] ].begin(), d_var_contains[ pats[index] ].end(), it->first )!=
+ d_var_contains[ pats[index] ].end() ){
+ vars.push_back( it->first );
+ shared_vars[ it->first ] = false;
+ numSharedVars--;
+ }
+ }
+ }
+ index = index==0 ? (int)(pats.size()-1) : (index-1);
+ }
+ vars.insert( vars.end(), unique_vars.begin(), unique_vars.end() );
+ Trace("multi-trigger-cache") << " Index[" << i << "]: ";
+ for( unsigned j=0; j<vars.size(); j++ ){
+ Trace("multi-trigger-cache") << vars[j] << " ";
+ }
+ Trace("multi-trigger-cache") << std::endl;
+ //make ordered inst match trie
+ d_imtio[i] = new InstMatchTrie::ImtIndexOrder;
+ d_imtio[i]->d_order.insert( d_imtio[i]->d_order.begin(), vars.begin(), vars.end() );
+ d_children_trie.push_back( InstMatchTrieOrdered( d_imtio[i] ) );
+ }
+}
+
+InstMatchGeneratorMulti::~InstMatchGeneratorMulti()
+{
+ for( unsigned i=0; i<d_children.size(); i++ ){
+ delete d_children[i];
+ }
+ for( std::map< unsigned, InstMatchTrie::ImtIndexOrder* >::iterator it = d_imtio.begin(); it != d_imtio.end(); ++it ){
+ delete it->second;
+ }
+}
+
+/** reset instantiation round (call this whenever equivalence classes have changed) */
+void InstMatchGeneratorMulti::resetInstantiationRound( QuantifiersEngine* qe ){
+ for( unsigned i=0; i<d_children.size(); i++ ){
+ d_children[i]->resetInstantiationRound( qe );
+ }
+}
+
+/** reset, eqc is the equivalence class to search in (any if eqc=null) */
+bool InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){
+ for( unsigned i=0; i<d_children.size(); i++ ){
+ if( !d_children[i]->reset( eqc, qe ) ){
+ //return false;
+ }
+ }
+ return true;
+}
+
+int InstMatchGeneratorMulti::addInstantiations(Node q,
+ 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, 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, tparent, newMatches[j], i, addedLemmas);
+ if( qe->inConflict() ){
+ return addedLemmas;
+ }
+ }
+ }
+ return 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_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();
+ processNewInstantiations(qe,
+ tparent,
+ m,
+ addedLemmas,
+ d_children_trie[childIndex].getTrie(),
+ 0,
+ childIndex,
+ fromChildIndex,
+ true);
+}
+
+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 ){
+ // 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_quant,
+ // curr_index );
+ Node n = m.get( curr_index );
+ if( n.isNull() ){
+ // 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;
+ }
+ }
+ }
+ // 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;
+ }
+ }
+ }
+ }else{
+ int newChildIndex = (childIndex+1)%(int)d_children.size();
+ processNewInstantiations(qe,
+ tparent,
+ m,
+ addedLemmas,
+ d_children_trie[newChildIndex].getTrie(),
+ 0,
+ newChildIndex,
+ endChildIndex,
+ modEq);
+ }
+}
+
+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;
+ }else{
+ d_pol = true;
+ }
+ if( d_match_pattern.getKind()==EQUAL ){
+ d_eqc = d_match_pattern[1];
+ d_match_pattern = d_match_pattern[0];
+ Assert( !quantifiers::TermUtil::hasInstConstAttr( d_eqc ) );
+ }
+ Assert( Trigger::isSimpleTrigger( d_match_pattern ) );
+ for( unsigned i=0; i<d_match_pattern.getNumChildren(); i++ ){
+ if( d_match_pattern[i].getKind()==INST_CONSTANT ){
+ if( !options::cbqi() || quantifiers::TermUtil::getInstConstAttr(d_match_pattern[i])==q ){
+ d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute());
+ }else{
+ d_var_num[i] = -1;
+ }
+ }
+ d_match_pattern_arg_types.push_back( d_match_pattern[i].getType() );
+ }
+ d_op = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
+}
+
+void InstMatchGeneratorSimple::resetInstantiationRound( QuantifiersEngine* qe ) {
+
+}
+int InstMatchGeneratorSimple::addInstantiations(Node q,
+ QuantifiersEngine* qe,
+ Trigger* tparent)
+{
+ int addedLemmas = 0;
+ quantifiers::TermArgTrie* tat;
+ if( d_eqc.isNull() ){
+ tat = qe->getTermDatabase()->getTermArgTrie( d_op );
+ }else{
+ if( d_pol ){
+ tat = qe->getTermDatabase()->getTermArgTrie( d_eqc, d_op );
+ }else{
+ Node r = qe->getEqualityQuery()->getRepresentative( d_eqc );
+ //iterate over all classes except r
+ tat = qe->getTermDatabase()->getTermArgTrie( Node::null(), d_op );
+ if( tat ){
+ for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){
+ if( it->first!=r ){
+ InstMatch m( q );
+ addInstantiations( m, qe, addedLemmas, 0, &(it->second) );
+ if( qe->inConflict() ){
+ break;
+ }
+ }
+ }
+ tat = NULL;
+ }
+ }
+ }
+ Debug("simple-trigger-debug") << "Adding instantiations based on " << tat << " from " << d_op << " " << d_eqc << std::endl;
+ if( tat ){
+ InstMatch m( q );
+ addInstantiations( m, qe, addedLemmas, 0, tat );
+ }
+ return addedLemmas;
+}
+
+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 == d_match_pattern.getNumChildren())
+ {
+ Assert( !tat->d_data.empty() );
+ TNode t = tat->getNodeData();
+ Debug("simple-trigger") << "Actual term is " << t << std::endl;
+ //convert to actual used terms
+ for( std::map< int, int >::iterator it = d_var_num.begin(); it != d_var_num.end(); ++it ){
+ if( it->second>=0 ){
+ Debug("simple-trigger") << "...set " << it->second << " " << t[it->first] << std::endl;
+ m.setValue( it->second, t[it->first] );
+ }
+ }
+ // we do not need the trigger parent for simple triggers (no post-processing
+ // required)
+ if (qe->getInstantiate()->addInstantiation(d_quant, m))
+ {
+ addedLemmas++;
+ Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl;
+ }
+ }else{
+ if( d_match_pattern[argIndex].getKind()==INST_CONSTANT ){
+ int v = d_var_num[argIndex];
+ if( v!=-1 ){
+ for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){
+ Node t = it->first;
+ Node prev = m.get( v );
+ //using representatives, just check if equal
+ Assert( t.getType().isComparableTo( d_match_pattern_arg_types[argIndex] ) );
+ if( prev.isNull() || prev==t ){
+ m.setValue( v, t);
+ addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
+ m.setValue( v, prev);
+ if( qe->inConflict() ){
+ break;
+ }
+ }
+ }
+ return;
+ }
+ //inst constant from another quantified formula, treat as ground term TODO: remove this?
+ }
+ Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] );
+ std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r );
+ if( it!=tat->d_data.end() ){
+ addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
+ }
+ }
+}
+
+int InstMatchGeneratorSimple::getActiveScore( QuantifiersEngine * qe ) {
+ Node f = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
+ unsigned ngt = qe->getTermDatabase()->getNumGroundTerms( f );
+ Trace("trigger-active-sel-debug") << "Number of ground terms for (simple) " << f << " is " << ngt << std::endl;
+ return ngt;
+}
+
+
+}/* CVC4::theory::inst namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h
new file mode 100644
index 000000000..6c38db13b
--- /dev/null
+++ b/src/theory/quantifiers/ematching/inst_match_generator.h
@@ -0,0 +1,694 @@
+/********************* */
+/*! \file inst_match_generator.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Morgan Deters, Andrew Reynolds, Tim King
+ ** 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 inst match generator class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
+#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
+
+#include <map>
+#include "theory/quantifiers/inst_match_trie.h"
+
+namespace CVC4 {
+namespace theory {
+
+class QuantifiersEngine;
+namespace quantifiers{
+ class TermArgTrie;
+}
+
+namespace inst {
+
+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/ematching/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.
+ *
+ * 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.
+ *
+ * It returns the number of instantiations added using calls to calls to
+ * Instantiate::addInstantiation(...).
+ */
+ virtual int addInstantiations(Node q,
+ 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 {
+ public:
+ /** destructor */
+ ~InstMatchGenerator() override;
+
+ /** 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,
+ QuantifiersEngine* qe,
+ Trigger* tparent) override;
+
+ /** 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) override;
+ /** 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
+
+ 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;
+ /** 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
+ *
+ * If d_match_pattern is an instantiation constant, then this is a singleton
+ * vector containing the variable number of the d_match_pattern itself.
+ * If d_match_patterm is a term of the form f( t1, ..., tn ), then for each
+ * index i, d_children[i] stores the type of node ti is, where:
+ * >= 0 : variable (indicates its number),
+ * -1 : ground term,
+ * -2 : child 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;
+ /** 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
+* This handles the special case of triggers that look like ite( x, BV1, BV0 ).
+*/
+class VarMatchGeneratorBooleanTerm : public InstMatchGenerator {
+public:
+ VarMatchGeneratorBooleanTerm( Node var, Node comp );
+
+ /** 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:
+ /** 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
+* This handles the special case of invertible terms like x+1 (see
+* Trigger::getTermInversionVariable).
+*/
+class VarMatchGeneratorTermSubs : public InstMatchGenerator {
+public:
+ VarMatchGeneratorTermSubs( Node var, Node subs );
+
+ /** 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;
+};
+
+/** 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 {
+ friend class InstMatchGenerator;
+
+ public:
+ /** Reset. */
+ bool reset(Node eqc, QuantifiersEngine* qe) override;
+ /** Get the next match. */
+ int getNextMatch(Node q,
+ InstMatch& m,
+ QuantifiersEngine* qe,
+ Trigger* tparent) override;
+
+ 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 {
+ public:
+ /** constructors */
+ InstMatchGeneratorMulti(Node q,
+ std::vector<Node>& pats,
+ QuantifiersEngine* qe);
+ /** destructor */
+ ~InstMatchGeneratorMulti() override;
+
+ /** Reset instantiation round. */
+ void resetInstantiationRound(QuantifiersEngine* qe) override;
+ /** Reset. */
+ bool reset(Node eqc, QuantifiersEngine* qe) override;
+ /** Add instantiations. */
+ int addInstantiations(Node q,
+ QuantifiersEngine* qe,
+ Trigger* tparent) override;
+
+ private:
+ /** indexed trie */
+ typedef std::pair< std::pair< int, int >, InstMatchTrie* > IndexedTrie;
+ /** 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;
+ /** Map from variable indices to pattern nodes that contain them. */
+ std::map< int, std::vector< Node > > d_var_to_node;
+ /** 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;
+ /** 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 node
+ * This data structure stores all InstMatch objects generated
+ * by matching for each term in the multi trigger.
+ */
+ std::vector< InstMatchTrieOrdered > d_children_trie;
+};/* class InstMatchGeneratorMulti */
+
+/** 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 {
+ public:
+ /** constructors */
+ InstMatchGeneratorSimple(Node q, Node pat, QuantifiersEngine* qe);
+
+ /** Reset instantiation round. */
+ void resetInstantiationRound(QuantifiersEngine* qe) override;
+ /** Add instantiations. */
+ int addInstantiations(Node q,
+ 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 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.
+ * Cached values of d_match_pattern[i].getType().
+ */
+ std::vector< TypeNode > d_match_pattern_arg_types;
+ /** The match operator d_match_pattern (see TermDb::getMatchOperator). */
+ Node d_op;
+ /** Map from child number to variable index. */
+ std::map< int, int > d_var_num;
+ /** 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 */
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
new file mode 100644
index 000000000..c2c1425f0
--- /dev/null
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -0,0 +1,613 @@
+/********************* */
+/*! \file inst_strategy_e_matching.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Morgan Deters, Tim King
+ ** 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 e matching instantiation strategies
+ **/
+
+#include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
+#include "theory/quantifiers/ematching/inst_match_generator.h"
+#include "theory/quantifiers/quant_relevance.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
+#include "theory/theory_engine.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+using namespace kind;
+using namespace context;
+
+namespace theory {
+
+using namespace inst;
+
+namespace quantifiers {
+
+//priority levels :
+//1 : user patterns (when user-pat!={resort,ignore}), auto-gen patterns (for non-user pattern quantifiers, or when user-pat={resort,ignore})
+//2 : user patterns (when user-pat=resort), auto gen patterns (for user pattern quantifiers when user-pat=use)
+
+// user-pat=interleave alternates between use and resort
+
+struct sortQuantifiersForSymbol {
+ QuantifiersEngine* d_qe;
+ std::map< Node, Node > d_op_map;
+ bool operator() (Node i, Node j) {
+ int nqfsi = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( d_op_map[i] );
+ int nqfsj = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( d_op_map[j] );
+ if( nqfsi<nqfsj ){
+ return true;
+ }else if( nqfsi>nqfsj ){
+ return false;
+ }else{
+ return false;
+ }
+ }
+};
+
+struct sortTriggers {
+ bool operator() (Node i, Node j) {
+ int wi = Trigger::getTriggerWeight( i );
+ int wj = Trigger::getTriggerWeight( j );
+ if( wi==wj ){
+ return i<j;
+ }else{
+ return wi<wj;
+ }
+ }
+};
+
+void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort effort ){
+ Trace("inst-alg-debug") << "reset user triggers" << std::endl;
+ //reset triggers
+ for( std::map< Node, std::vector< Trigger* > >::iterator it = d_user_gen.begin(); it != d_user_gen.end(); ++it ){
+ for( unsigned i=0; i<it->second.size(); i++ ){
+ it->second[i]->resetInstantiationRound();
+ it->second[i]->reset( Node::null() );
+ }
+ }
+ Trace("inst-alg-debug") << "done reset user triggers" << std::endl;
+}
+
+int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
+ if( e==0 ){
+ return STATUS_UNFINISHED;
+ }else{
+ int peffort = d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ? 2 : 1;
+ if( e<peffort ){
+ return STATUS_UNFINISHED;
+ }else if( e==peffort ){
+ d_counter[f]++;
+
+ Trace("inst-alg") << "-> User-provided instantiate " << f << "..." << std::endl;
+ if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ){
+ for( unsigned i=0; i<d_user_gen_wait[f].size(); i++ ){
+ Trigger * t = Trigger::mkTrigger( d_quantEngine, f, d_user_gen_wait[f][i], true, Trigger::TR_RETURN_NULL );
+ if( t ){
+ d_user_gen[f].push_back( t );
+ }
+ }
+ d_user_gen_wait[f].clear();
+ }
+
+ for( unsigned i=0; i<d_user_gen[f].size(); i++ ){
+ bool processTrigger = true;
+ if( processTrigger ){
+ Trace("process-trigger") << " Process (user) ";
+ d_user_gen[f][i]->debugPrint("process-trigger");
+ Trace("process-trigger") << "..." << std::endl;
+ int numInst = d_user_gen[f][i]->addInstantiations();
+ Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl;
+ d_quantEngine->d_statistics.d_instantiations_user_patterns += numInst;
+ if( d_user_gen[f][i]->isMultiTrigger() ){
+ d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
+ }
+ if( d_quantEngine->inConflict() ){
+ break;
+ }
+ }
+ }
+ }
+ }
+ return STATUS_UNKNOWN;
+}
+
+void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){
+ Assert( pat.getKind()==INST_PATTERN );
+ //add to generators
+ bool usable = true;
+ std::vector< Node > nodes;
+ for( unsigned i=0; i<pat.getNumChildren(); i++ ){
+ Node pat_use = Trigger::getIsUsableTrigger( pat[i], q );
+ if( pat_use.isNull() ){
+ Trace("trigger-warn") << "User-provided trigger is not usable : " << pat << " because of " << pat[i] << std::endl;
+ usable = false;
+ break;
+ }else{
+ nodes.push_back( pat_use );
+ }
+ }
+ if( usable ){
+ Trace("user-pat") << "Add user pattern: " << pat << " for " << q << std::endl;
+ //check match option
+ if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ){
+ d_user_gen_wait[q].push_back( nodes );
+ }else{
+ Trigger * t = Trigger::mkTrigger( d_quantEngine, q, nodes, true, Trigger::TR_MAKE_NEW );
+ if( t ){
+ d_user_gen[q].push_back( t );
+ }else{
+ Trace("trigger-warn") << "Failed to construct trigger : " << pat << " due to variable mismatch" << std::endl;
+ }
+ }
+ }
+}
+
+InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe ) : InstStrategy( qe ){
+ //how to select trigger terms
+ d_tr_strategy = options::triggerSelMode();
+ //whether to select new triggers during the search
+ if( options::incrementTriggers() ){
+ d_regenerate_frequency = 3;
+ d_regenerate = true;
+ }else{
+ d_regenerate_frequency = 1;
+ d_regenerate = false;
+ }
+}
+
+void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){
+ Trace("inst-alg-debug") << "reset auto-gen triggers" << std::endl;
+ //reset triggers
+ for( unsigned r=0; r<2; r++ ){
+ for( std::map< Node, std::map< Trigger*, bool > >::iterator it = d_auto_gen_trigger[r].begin(); it != d_auto_gen_trigger[r].end(); ++it ){
+ for( std::map< Trigger*, bool >::iterator itt = it->second.begin(); itt != it->second.end(); ++itt ){
+ itt->first->resetInstantiationRound();
+ itt->first->reset( Node::null() );
+ }
+ }
+ }
+ d_processed_trigger.clear();
+ Trace("inst-alg-debug") << "done reset auto-gen triggers" << std::endl;
+}
+
+int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){
+ UserPatMode upMode = d_quantEngine->getInstUserPatMode();
+ if( hasUserPatterns( f ) && upMode==USER_PAT_MODE_TRUST ){
+ return STATUS_UNKNOWN;
+ }else{
+ int peffort = ( hasUserPatterns( f ) && upMode!=USER_PAT_MODE_IGNORE && upMode!=USER_PAT_MODE_RESORT ) ? 2 : 1;
+ if( e<peffort ){
+ return STATUS_UNFINISHED;
+ }else{
+ Trace("inst-alg") << "-> Auto-gen instantiate " << f << "..." << std::endl;
+ bool gen = false;
+ if( e==peffort ){
+ if( d_counter.find( f )==d_counter.end() ){
+ d_counter[f] = 0;
+ gen = true;
+ }else{
+ d_counter[f]++;
+ gen = d_regenerate && d_counter[f]%d_regenerate_frequency==0;
+ }
+ }else{
+ gen = true;
+ }
+ if( gen ){
+ generateTriggers( f );
+ if( d_counter[f]==0 && d_auto_gen_trigger[0][f].empty() && d_auto_gen_trigger[1][f].empty() && f.getNumChildren()==2 ){
+ Trace("trigger-warn") << "Could not find trigger for " << f << std::endl;
+ }
+ }
+
+ //if( e==4 ){
+ // d_processed_trigger.clear();
+ // d_quantEngine->getEqualityQuery()->setLiberal( true );
+ //}
+ if( options::triggerActiveSelMode()!=TRIGGER_ACTIVE_SEL_ALL ){
+ int max_score = -1;
+ Trigger * max_trigger = NULL;
+ for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[0][f].begin(); itt != d_auto_gen_trigger[0][f].end(); ++itt ){
+ int score = itt->first->getActiveScore();
+ if( options::triggerActiveSelMode()==TRIGGER_ACTIVE_SEL_MIN ){
+ if( score>=0 && ( score<max_score || max_score<0 ) ){
+ max_score = score;
+ max_trigger = itt->first;
+ }
+ }else{
+ if( score>max_score ){
+ max_score = score;
+ max_trigger = itt->first;
+ }
+ }
+ d_auto_gen_trigger[0][f][itt->first] = false;
+ }
+ if( max_trigger!=NULL ){
+ d_auto_gen_trigger[0][f][max_trigger] = true;
+ }
+ }
+
+ bool hasInst = false;
+ for( unsigned r=0; r<2; r++ ){
+ for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[r][f].begin(); itt != d_auto_gen_trigger[r][f].end(); ++itt ){
+ Trigger* tr = itt->first;
+ if( tr ){
+ bool processTrigger = itt->second;
+ if( processTrigger && d_processed_trigger[f].find( tr )==d_processed_trigger[f].end() ){
+ d_processed_trigger[f][tr] = true;
+ Trace("process-trigger") << " Process ";
+ tr->debugPrint("process-trigger");
+ Trace("process-trigger") << "..." << std::endl;
+ int numInst = tr->addInstantiations();
+ hasInst = numInst>0 || hasInst;
+ Trace("process-trigger") << " Done, numInst = " << numInst << "." << std::endl;
+ d_quantEngine->d_statistics.d_instantiations_auto_gen += numInst;
+ if( r==1 ){
+ d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
+ }
+ if( d_quantEngine->inConflict() ){
+ break;
+ }
+ }
+ }
+ }
+ if( d_quantEngine->inConflict() || ( hasInst && options::multiTriggerPriority() ) ){
+ break;
+ }
+ }
+ //if( e==4 ){
+ // d_quantEngine->getEqualityQuery()->setLiberal( false );
+ //}
+ return STATUS_UNKNOWN;
+ }
+ }
+}
+
+void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
+ Trace("auto-gen-trigger-debug") << "Generate triggers for " << f << ", #var=" << f[0].getNumChildren() << "..." << std::endl;
+ if( d_patTerms[0].find( f )==d_patTerms[0].end() ){
+ //determine all possible pattern terms based on trigger term selection strategy d_tr_strategy
+ d_patTerms[0][f].clear();
+ d_patTerms[1][f].clear();
+ bool ntrivTriggers = options::relationalTriggers();
+ std::vector< Node > patTermsF;
+ std::map< Node, inst::TriggerTermInfo > tinfo;
+ //well-defined function: can assume LHS is only trigger
+ if( options::quantFunWellDefined() ){
+ Node hd = QuantAttributes::getFunDefHead( f );
+ if( !hd.isNull() ){
+ hd = d_quantEngine->getTermUtil()
+ ->substituteBoundVariablesToInstConstants(hd, f);
+ patTermsF.push_back( hd );
+ tinfo[hd].init( f, hd );
+ }
+ }
+ //otherwise, use algorithm for collecting pattern terms
+ if( patTermsF.empty() ){
+ Node bd = d_quantEngine->getTermUtil()->getInstConstantBody( f );
+ Trigger::collectPatTerms( f, bd, patTermsF, d_tr_strategy, d_user_no_gen[f], tinfo, true );
+ if( ntrivTriggers ){
+ sortTriggers st;
+ std::sort( patTermsF.begin(), patTermsF.end(), st );
+ }
+ if( Trace.isOn("auto-gen-trigger-debug") ){
+ Trace("auto-gen-trigger-debug") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl;
+ for( unsigned i=0; i<patTermsF.size(); i++ ){
+ Assert( tinfo.find( patTermsF[i] )!=tinfo.end() );
+ Trace("auto-gen-trigger-debug") << " " << patTermsF[i] << std::endl;
+ Trace("auto-gen-trigger-debug2") << " info = [" << tinfo[patTermsF[i]].d_reqPol << ", " << tinfo[patTermsF[i]].d_reqPolEq << ", " << tinfo[patTermsF[i]].d_fv.size() << "]" << std::endl;
+ }
+ Trace("auto-gen-trigger-debug") << std::endl;
+ }
+ }
+ //sort into single/multi triggers, calculate which terms should not be considered
+ std::map< Node, bool > vcMap;
+ std::map< Node, bool > rmPatTermsF;
+ int last_weight = -1;
+ for( unsigned i=0; i<patTermsF.size(); i++ ){
+ Assert( patTermsF[i].getKind()!=NOT );
+ bool newVar = false;
+ for( unsigned j=0; j<tinfo[ patTermsF[i] ].d_fv.size(); j++ ){
+ if( vcMap.find( tinfo[ patTermsF[i] ].d_fv[j] )==vcMap.end() ){
+ vcMap[tinfo[ patTermsF[i] ].d_fv[j]] = true;
+ newVar = true;
+ }
+ }
+ int curr_w = Trigger::getTriggerWeight( patTermsF[i] );
+ if( ntrivTriggers && !newVar && last_weight!=-1 && curr_w>last_weight ){
+ Trace("auto-gen-trigger-debug") << "...exclude expendible non-trivial trigger : " << patTermsF[i] << std::endl;
+ rmPatTermsF[patTermsF[i]] = true;
+ }else{
+ last_weight = curr_w;
+ }
+ }
+ d_num_trigger_vars[f] = vcMap.size();
+ if( d_num_trigger_vars[f]>0 && d_num_trigger_vars[f]<f[0].getNumChildren() ){
+ Trace("auto-gen-trigger-partial") << "Quantified formula : " << f << std::endl;
+ Trace("auto-gen-trigger-partial") << "...does not contain all variables in triggers!!!" << std::endl;
+ if( options::partialTriggers() ){
+ std::vector< Node > vcs[2];
+ for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
+ Node ic = d_quantEngine->getTermUtil()->getInstantiationConstant( f, i );
+ vcs[ vcMap.find( ic )==vcMap.end() ? 0 : 1 ].push_back( f[0][i] );
+ }
+ for( unsigned i=0; i<2; i++ ){
+ d_vc_partition[i][f] = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, vcs[i] );
+ }
+ }else{
+ return;
+ }
+ }
+ for( unsigned i=0; i<patTermsF.size(); i++ ){
+ Node pat = patTermsF[i];
+ if( rmPatTermsF.find( pat )==rmPatTermsF.end() ){
+ Trace("auto-gen-trigger-debug") << "...processing pattern " << pat << std::endl;
+ Node mpat = pat;
+ //process the pattern: if it has a required polarity, consider it
+ Assert( tinfo.find( pat )!=tinfo.end() );
+ int rpol = tinfo[pat].d_reqPol;
+ Node rpoleq = tinfo[pat].d_reqPolEq;
+ unsigned num_fv = tinfo[pat].d_fv.size();
+ Trace("auto-gen-trigger-debug") << "...required polarity for " << pat << " is " << rpol << ", eq=" << rpoleq << std::endl;
+ if( rpol!=0 ){
+ Assert( rpol==1 || rpol==-1 );
+ if( Trigger::isRelationalTrigger( pat ) ){
+ pat = rpol==-1 ? pat.negate() : pat;
+ }else{
+ Assert( Trigger::isAtomicTrigger( pat ) );
+ if( pat.getType().isBoolean() && rpoleq.isNull() ){
+ if( options::literalMatchMode()==LITERAL_MATCH_USE ){
+ pat = NodeManager::currentNM()->mkNode( EQUAL, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate();
+ }else if( options::literalMatchMode()!=LITERAL_MATCH_NONE ){
+ pat = NodeManager::currentNM()->mkNode( EQUAL, pat, NodeManager::currentNM()->mkConst( rpol==1 ) );
+ }
+ }else{
+ Assert( !rpoleq.isNull() );
+ if( rpol==-1 ){
+ if( options::literalMatchMode()!=LITERAL_MATCH_NONE ){
+ //all equivalence classes except rpoleq
+ pat = NodeManager::currentNM()->mkNode( EQUAL, pat, rpoleq ).negate();
+ }
+ }else if( rpol==1 ){
+ if( options::literalMatchMode()==LITERAL_MATCH_AGG ){
+ //only equivalence class rpoleq
+ pat = NodeManager::currentNM()->mkNode( EQUAL, pat, rpoleq );
+ }
+ //all equivalence classes that are not disequal to rpoleq TODO?
+ }
+ }
+ }
+ Trace("auto-gen-trigger-debug") << "...got : " << pat << std::endl;
+ }else{
+ if( Trigger::isRelationalTrigger( pat ) ){
+ //consider both polarities
+ addPatternToPool( f, pat.negate(), num_fv, mpat );
+ }
+ }
+ addPatternToPool( f, pat, num_fv, mpat );
+ }
+ }
+ //tinfo not used below this point
+ d_made_multi_trigger[f] = false;
+ Trace("auto-gen-trigger") << "Single trigger pool for " << f << " : " << std::endl;
+ for( unsigned i=0; i<d_patTerms[0][f].size(); i++ ){
+ Trace("auto-gen-trigger") << " " << d_patTerms[0][f][i] << std::endl;
+ }
+ if( !d_patTerms[1][f].empty() ){
+ Trace("auto-gen-trigger") << "Multi-trigger term pool for " << f << " : " << std::endl;
+ for( unsigned i=0; i<d_patTerms[1][f].size(); i++ ){
+ Trace("auto-gen-trigger") << " " << d_patTerms[1][f][i] << std::endl;
+ }
+ }
+ }
+
+ unsigned rmin = d_patTerms[0][f].empty() ? 1 : 0;
+ unsigned rmax = options::multiTriggerWhenSingle() ? 1 : rmin;
+ for( unsigned r=rmin; r<=rmax; r++ ){
+ std::vector< Node > patTerms;
+ for( int i=0; i<(int)d_patTerms[r][f].size(); i++ ){
+ if( r==1 || d_single_trigger_gen.find( d_patTerms[r][f][i] )==d_single_trigger_gen.end() ){
+ patTerms.push_back( d_patTerms[r][f][i] );
+ }
+ }
+ if( !patTerms.empty() ){
+ Trace("auto-gen-trigger") << "Generate trigger for " << f << std::endl;
+ //sort terms based on relevance
+ if( options::relevantTriggers() ){
+ sortQuantifiersForSymbol sqfs;
+ sqfs.d_qe = d_quantEngine;
+ for( unsigned i=0; i<patTerms.size(); i++ ){
+ Assert( d_pat_to_mpat.find( patTerms[i] )!=d_pat_to_mpat.end() );
+ Assert( d_pat_to_mpat[patTerms[i]].hasOperator() );
+ sqfs.d_op_map[ patTerms[i] ] = d_pat_to_mpat[patTerms[i]].getOperator();
+ }
+ //sort based on # occurrences (this will cause Trigger to select rarer symbols)
+ std::sort( patTerms.begin(), patTerms.end(), sqfs );
+ Debug("relevant-trigger") << "Terms based on relevance: " << std::endl;
+ for( unsigned i=0; i<patTerms.size(); i++ ){
+ Debug("relevant-trigger") << " " << patTerms[i] << " from " << d_pat_to_mpat[patTerms[i]] << " (";
+ Debug("relevant-trigger") << d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( d_pat_to_mpat[patTerms[i]].getOperator() ) << ")" << std::endl;
+ }
+ }
+ //now, generate the trigger...
+ Trigger* tr = NULL;
+ if( d_is_single_trigger[ patTerms[0] ] ){
+ tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], false, Trigger::TR_RETURN_NULL, d_num_trigger_vars[f] );
+ d_single_trigger_gen[ patTerms[0] ] = true;
+ }else{
+ //only generate multi trigger if option set, or if no single triggers exist
+ if( !d_patTerms[0][f].empty() ){
+ if( options::multiTriggerWhenSingle() ){
+ Trace("multi-trigger-debug") << "Resort to choosing multi-triggers..." << std::endl;
+ }else{
+ return;
+ }
+ }
+ //if we are re-generating triggers, shuffle based on some method
+ if( d_made_multi_trigger[f] ){
+ std::random_shuffle( patTerms.begin(), patTerms.end() ); //shuffle randomly
+ }else{
+ d_made_multi_trigger[f] = true;
+ }
+ //will possibly want to get an old trigger
+ tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, false, Trigger::TR_GET_OLD, d_num_trigger_vars[f] );
+ }
+ if( tr ){
+ addTrigger( tr, f );
+ //if we are generating additional triggers...
+ if( !tr->isMultiTrigger() ){
+ unsigned index = 0;
+ if( index<patTerms.size() ){
+ //Notice() << "check add additional" << std::endl;
+ //check if similar patterns exist, and if so, add them additionally
+ unsigned nqfs_curr = 0;
+ if( options::relevantTriggers() ){
+ nqfs_curr = d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[0].getOperator() );
+ }
+ index++;
+ bool success = true;
+ while( success && index<patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){
+ success = false;
+ if( !options::relevantTriggers() ||
+ d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){
+ d_single_trigger_gen[ patTerms[index] ] = true;
+ Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], false, Trigger::TR_RETURN_NULL, d_num_trigger_vars[f] );
+ addTrigger( tr2, f );
+ success = true;
+ }
+ index++;
+ }
+ //Notice() << "done check add additional" << std::endl;
+ }
+ }
+ }
+ }
+ }
+}
+
+void InstStrategyAutoGenTriggers::addPatternToPool( Node q, Node pat, unsigned num_fv, Node mpat ) {
+ d_pat_to_mpat[pat] = mpat;
+ unsigned num_vars = options::partialTriggers() ? d_num_trigger_vars[q] : q[0].getNumChildren();
+ if( num_fv==num_vars && ( options::pureThTriggers() || !Trigger::isPureTheoryTrigger( pat ) ) ){
+ d_patTerms[0][q].push_back( pat );
+ d_is_single_trigger[ pat ] = true;
+ }else{
+ d_patTerms[1][q].push_back( pat );
+ d_is_single_trigger[ pat ] = false;
+ }
+}
+
+
+void InstStrategyAutoGenTriggers::addTrigger( inst::Trigger * tr, Node q ) {
+ if( tr ){
+ if( d_num_trigger_vars[q]<q[0].getNumChildren() ){
+ //partial trigger : generate implication to mark user pattern
+ Node pat =
+ d_quantEngine->getTermUtil()->substituteInstConstantsToBoundVariables(
+ tr->getInstPattern(), q);
+ Node ipl = NodeManager::currentNM()->mkNode(INST_PATTERN_LIST, pat);
+ Node qq = NodeManager::currentNM()->mkNode( FORALL, d_vc_partition[1][q], NodeManager::currentNM()->mkNode( FORALL, d_vc_partition[0][q], q[1] ), ipl );
+ Trace("auto-gen-trigger-partial") << "Make partially specified user pattern: " << std::endl;
+ Trace("auto-gen-trigger-partial") << " " << qq << std::endl;
+ Node lem = NodeManager::currentNM()->mkNode( OR, q.negate(), qq );
+ d_quantEngine->addLemma( lem );
+ }else{
+ unsigned tindex;
+ if( tr->isMultiTrigger() ){
+ //disable all other multi triggers
+ for( std::map< Trigger*, bool >::iterator it = d_auto_gen_trigger[1][q].begin(); it != d_auto_gen_trigger[1][q].end(); ++it ){
+ d_auto_gen_trigger[1][q][ it->first ] = false;
+ }
+ tindex = 1;
+ }else{
+ tindex = 0;
+ }
+ //making it during an instantiation round, so must reset
+ if( d_auto_gen_trigger[tindex][q].find( tr )==d_auto_gen_trigger[tindex][q].end() ){
+ tr->resetInstantiationRound();
+ tr->reset( Node::null() );
+ }
+ d_auto_gen_trigger[tindex][q][tr] = true;
+ }
+ }
+}
+
+bool InstStrategyAutoGenTriggers::hasUserPatterns( Node q ) {
+ if( q.getNumChildren()==3 ){
+ std::map< Node, bool >::iterator it = d_hasUserPatterns.find( q );
+ if( it==d_hasUserPatterns.end() ){
+ bool hasPat = false;
+ for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
+ if( q[2][i].getKind()==INST_PATTERN ){
+ hasPat = true;
+ break;
+ }
+ }
+ d_hasUserPatterns[q] = hasPat;
+ return hasPat;
+ }else{
+ return it->second;
+ }
+ }else{
+ return false;
+ }
+}
+
+void InstStrategyAutoGenTriggers::addUserNoPattern( Node q, Node pat ) {
+ Assert( pat.getKind()==INST_NO_PATTERN && pat.getNumChildren()==1 );
+ if( std::find( d_user_no_gen[q].begin(), d_user_no_gen[q].end(), pat[0] )==d_user_no_gen[q].end() ){
+ Trace("user-pat") << "Add user no-pattern: " << pat[0] << " for " << q << std::endl;
+ d_user_no_gen[q].push_back( pat[0] );
+ }
+}
+
+/* TODO?
+bool InstStrategyLocalTheoryExt::isLocalTheoryExt( Node f ) {
+ std::map< Node, bool >::iterator itq = d_quant.find( f );
+ if( itq==d_quant.end() ){
+ //generate triggers
+ Node bd = d_quantEngine->getTermUtil()->getInstConstantBody( f );
+ std::vector< Node > vars;
+ std::vector< Node > patTerms;
+ bool ret = Trigger::isLocalTheoryExt( bd, vars, patTerms );
+ if( ret ){
+ d_quant[f] = ret;
+ //add all variables to trigger that don't already occur
+ for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
+ Node x = d_quantEngine->getTermUtil()->getInstantiationConstant( f, i );
+ if( std::find( vars.begin(), vars.end(), x )==vars.end() ){
+ patTerms.push_back( x );
+ }
+ }
+ Trace("local-t-ext") << "Local theory extensions trigger for " << f << " : " << std::endl;
+ for( unsigned i=0; i<patTerms.size(); i++ ){
+ Trace("local-t-ext") << " " << patTerms[i] << std::endl;
+ }
+ Trace("local-t-ext") << std::endl;
+ Trigger * tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, true, Trigger::TR_GET_OLD );
+ d_lte_trigger[f] = tr;
+ }else{
+ Trace("local-t-ext") << "No local theory extensions trigger for " << f << "." << std::endl;
+ Trace("local-t-ext-warn") << "WARNING: not local theory extensions : " << f << std::endl;
+ }
+ d_quant[f] = ret;
+ return ret;
+ }else{
+ return itq->second;
+ }
+}
+*/
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
new file mode 100644
index 000000000..8f11dfedf
--- /dev/null
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
@@ -0,0 +1,119 @@
+/********************* */
+/*! \file inst_strategy_e_matching.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Morgan Deters, Andrew Reynolds, Tim King
+ ** 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 E matching instantiation strategies
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__INST_STRATEGY_E_MATCHING_H
+#define __CVC4__INST_STRATEGY_E_MATCHING_H
+
+#include "context/context.h"
+#include "context/context_mm.h"
+#include "theory/quantifiers/ematching/instantiation_engine.h"
+#include "theory/quantifiers/ematching/trigger.h"
+#include "theory/quantifiers_engine.h"
+#include "util/statistics_registry.h"
+#include "options/quantifiers_options.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+//instantiation strategies
+
+class InstStrategyUserPatterns : public InstStrategy{
+private:
+ /** explicitly provided patterns */
+ std::map< Node, std::vector< inst::Trigger* > > d_user_gen;
+ /** waiting to be generated patterns */
+ std::map< Node, std::vector< std::vector< Node > > > d_user_gen_wait;
+ /** counter for quantifiers */
+ std::map< Node, int > d_counter;
+ /** process functions */
+ void processResetInstantiationRound( Theory::Effort effort );
+ int process( Node f, Theory::Effort effort, int e );
+public:
+ InstStrategyUserPatterns( QuantifiersEngine* ie ) :
+ InstStrategy( ie ){}
+ ~InstStrategyUserPatterns(){}
+public:
+ /** add pattern */
+ void addUserPattern( Node q, Node pat );
+ /** get num patterns */
+ int getNumUserGenerators( Node q ) { return (int)d_user_gen[q].size(); }
+ /** get user pattern */
+ inst::Trigger* getUserGenerator( Node q, int i ) { return d_user_gen[q][ i ]; }
+ /** identify */
+ std::string identify() const { return std::string("UserPatterns"); }
+};/* class InstStrategyUserPatterns */
+
+class InstStrategyAutoGenTriggers : public InstStrategy {
+public:
+ enum {
+ RELEVANCE_NONE,
+ RELEVANCE_DEFAULT,
+ };
+private:
+ /** trigger generation strategy */
+ TriggerSelMode d_tr_strategy;
+ /** regeneration */
+ bool d_regenerate;
+ int d_regenerate_frequency;
+ /** (single,multi) triggers for each quantifier */
+ std::map< Node, std::map< inst::Trigger*, bool > > d_auto_gen_trigger[2];
+ std::map< Node, int > d_counter;
+ /** single, multi triggers for each quantifier */
+ std::map< Node, std::vector< Node > > d_patTerms[2];
+ std::map< Node, std::map< Node, bool > > d_patReqPol;
+ /** information about triggers */
+ std::map< Node, bool > d_is_single_trigger;
+ std::map< Node, bool > d_single_trigger_gen;
+ std::map< Node, bool > d_made_multi_trigger;
+ //processed trigger this round
+ std::map< Node, std::map< inst::Trigger*, bool > > d_processed_trigger;
+ //instantiation no patterns
+ std::map< Node, std::vector< Node > > d_user_no_gen;
+ // number of trigger variables per quantifier
+ std::map< Node, unsigned > d_num_trigger_vars;
+ std::map< Node, Node > d_vc_partition[2];
+ std::map< Node, Node > d_pat_to_mpat;
+private:
+ /** process functions */
+ void processResetInstantiationRound( Theory::Effort effort );
+ int process( Node q, Theory::Effort effort, int e );
+ /** generate triggers */
+ void generateTriggers( Node q );
+ void addPatternToPool( Node q, Node pat, unsigned num_fv, Node mpat );
+ void addTrigger( inst::Trigger * tr, Node f );
+ /** has user patterns */
+ bool hasUserPatterns( Node q );
+ /** has user patterns */
+ std::map< Node, bool > d_hasUserPatterns;
+public:
+ InstStrategyAutoGenTriggers( QuantifiersEngine* qe );
+ ~InstStrategyAutoGenTriggers(){}
+public:
+ /** get auto-generated trigger */
+ inst::Trigger* getAutoGenTrigger( Node q );
+ /** identify */
+ std::string identify() const { return std::string("AutoGenTriggers"); }
+ /** add pattern */
+ void addUserNoPattern( Node q, Node pat );
+};/* class InstStrategyAutoGenTriggers */
+
+
+}
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
new file mode 100644
index 000000000..184add8c3
--- /dev/null
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -0,0 +1,209 @@
+/********************* */
+/*! \file instantiation_engine.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Morgan Deters, Tim King
+ ** 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 instantiation engine class
+ **/
+
+#include "theory/quantifiers/ematching/instantiation_engine.h"
+
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers/ematching/trigger.h"
+#include "theory/theory_engine.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace CVC4::theory::inst;
+
+InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe)
+ : QuantifiersModule(qe),
+ d_instStrategies(),
+ d_isup(),
+ d_i_ag(),
+ d_quants() {
+ if (options::eMatching()) {
+ // these are the instantiation strategies for E-matching
+ // user-provided patterns
+ if (options::userPatternsQuant() != USER_PAT_MODE_IGNORE) {
+ d_isup.reset(new InstStrategyUserPatterns(d_quantEngine));
+ d_instStrategies.push_back(d_isup.get());
+ }
+
+ // auto-generated patterns
+ d_i_ag.reset(new InstStrategyAutoGenTriggers(d_quantEngine));
+ d_instStrategies.push_back(d_i_ag.get());
+ }
+}
+
+InstantiationEngine::~InstantiationEngine() {}
+
+void InstantiationEngine::presolve() {
+ for( unsigned i=0; i<d_instStrategies.size(); ++i ){
+ d_instStrategies[i]->presolve();
+ }
+}
+
+void InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
+ unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
+ //iterate over an internal effort level e
+ int e = 0;
+ int eLimit = effort==Theory::EFFORT_LAST_CALL ? 10 : 2;
+ bool finished = false;
+ //while unfinished, try effort level=0,1,2....
+ while( !finished && e<=eLimit ){
+ Debug("inst-engine") << "IE: Prepare instantiation (" << e << ")." << std::endl;
+ finished = true;
+ //instantiate each quantifier
+ for( unsigned i=0; i<d_quants.size(); i++ ){
+ Node q = d_quants[i];
+ Debug("inst-engine-debug") << "IE: Instantiate " << q << "..." << std::endl;
+ //int e_use = d_quantEngine->getRelevance( q )==-1 ? e - 1 : e;
+ int e_use = e;
+ if( e_use>=0 ){
+ Trace("inst-engine-debug") << "inst-engine : " << q << std::endl;
+ //check each instantiation strategy
+ for( unsigned j=0; j<d_instStrategies.size(); j++ ){
+ InstStrategy* is = d_instStrategies[j];
+ Trace("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl;
+ int quantStatus = is->process( q, effort, e_use );
+ Trace("inst-engine-debug") << " -> status is " << quantStatus << ", conflict=" << d_quantEngine->inConflict() << std::endl;
+ if( d_quantEngine->inConflict() ){
+ return;
+ }else if( quantStatus==InstStrategy::STATUS_UNFINISHED ){
+ finished = false;
+ }
+ }
+ }
+ }
+ //do not consider another level if already added lemma at this level
+ if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
+ finished = true;
+ }
+ e++;
+ }
+}
+
+bool InstantiationEngine::needsCheck( Theory::Effort e ){
+ return d_quantEngine->getInstWhenNeedsCheck( e );
+}
+
+void InstantiationEngine::reset_round( Theory::Effort e ){
+ //if not, proceed to instantiation round
+ //reset the instantiation strategies
+ for( unsigned i=0; i<d_instStrategies.size(); ++i ){
+ InstStrategy* is = d_instStrategies[i];
+ is->processResetInstantiationRound( e );
+ }
+}
+
+void InstantiationEngine::check(Theory::Effort e, QEffort quant_e)
+{
+ CodeTimer codeTimer(d_quantEngine->d_statistics.d_ematching_time);
+ if (quant_e == QEFFORT_STANDARD)
+ {
+ double clSet = 0;
+ if( Trace.isOn("inst-engine") ){
+ clSet = double(clock())/double(CLOCKS_PER_SEC);
+ Trace("inst-engine") << "---Instantiation Engine Round, effort = " << e << "---" << std::endl;
+ }
+ //collect all active quantified formulas belonging to this
+ bool quantActive = false;
+ d_quants.clear();
+ for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true );
+ if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
+ quantActive = true;
+ d_quants.push_back( q );
+ }
+ }
+ Trace("inst-engine-debug") << "InstEngine: check: # asserted quantifiers " << d_quants.size() << "/";
+ Trace("inst-engine-debug") << d_quantEngine->getModel()->getNumAssertedQuantifiers() << " " << quantActive << std::endl;
+ if( quantActive ){
+ unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
+ doInstantiationRound( e );
+ if( d_quantEngine->inConflict() ){
+ Assert( d_quantEngine->getNumLemmasWaiting()>lastWaiting );
+ Trace("inst-engine") << "Conflict, added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl;
+ }else if( d_quantEngine->hasAddedLemma() ){
+ Trace("inst-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl;
+ }
+ }else{
+ d_quants.clear();
+ }
+ if( Trace.isOn("inst-engine") ){
+ double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+ Trace("inst-engine") << "Finished instantiation engine, time = " << (clSet2-clSet) << std::endl;
+ }
+ }
+}
+
+bool InstantiationEngine::checkCompleteFor( Node q ) {
+ //TODO?
+ return false;
+}
+
+void InstantiationEngine::preRegisterQuantifier( Node q ) {
+ if( options::strictTriggers() && q.getNumChildren()==3 ){
+ //if strict triggers, take ownership of this quantified formula
+ bool hasPat = false;
+ for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
+ if( q[2][i].getKind()==INST_PATTERN || q[2][i].getKind()==INST_NO_PATTERN ){
+ hasPat = true;
+ break;
+ }
+ }
+ if( hasPat ){
+ d_quantEngine->setOwner( q, this, 1 );
+ }
+ }
+}
+
+void InstantiationEngine::registerQuantifier( Node f ){
+ if( d_quantEngine->hasOwnership( f, this ) ){
+ //for( unsigned i=0; i<d_instStrategies.size(); ++i ){
+ // d_instStrategies[i]->registerQuantifier( f );
+ //}
+ //take into account user patterns
+ if( f.getNumChildren()==3 ){
+ Node subsPat =
+ d_quantEngine->getTermUtil()->substituteBoundVariablesToInstConstants(
+ f[2], f);
+ //add patterns
+ for( int i=0; i<(int)subsPat.getNumChildren(); i++ ){
+ //Notice() << "Add pattern " << subsPat[i] << " for " << f << std::endl;
+ if( subsPat[i].getKind()==INST_PATTERN ){
+ addUserPattern( f, subsPat[i] );
+ }else if( subsPat[i].getKind()==INST_NO_PATTERN ){
+ addUserNoPattern( f, subsPat[i] );
+ }
+ }
+ }
+ }
+}
+
+void InstantiationEngine::addUserPattern(Node q, Node pat) {
+ if (d_isup) {
+ d_isup->addUserPattern(q, pat);
+ }
+}
+
+void InstantiationEngine::addUserNoPattern(Node q, Node pat) {
+ if (d_i_ag) {
+ d_i_ag->addUserNoPattern(q, pat);
+ }
+}
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h
new file mode 100644
index 000000000..18b5ea19c
--- /dev/null
+++ b/src/theory/quantifiers/ematching/instantiation_engine.h
@@ -0,0 +1,98 @@
+/********************* */
+/*! \file instantiation_engine.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Morgan Deters, Tim King
+ ** 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 Instantiation Engine classes
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
+#define __CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
+
+#include <memory>
+
+#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/theory_quantifiers.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class InstStrategyUserPatterns;
+class InstStrategyAutoGenTriggers;
+class InstStrategyFreeVariable;
+
+/** instantiation strategy class */
+class InstStrategy {
+public:
+ enum Status {
+ STATUS_UNFINISHED,
+ STATUS_UNKNOWN,
+ };/* enum Status */
+protected:
+ /** reference to the instantiation engine */
+ QuantifiersEngine* d_quantEngine;
+public:
+ InstStrategy( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
+ virtual ~InstStrategy(){}
+ /** presolve */
+ virtual void presolve() {}
+ /** reset instantiation */
+ virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
+ /** process method, returns a status */
+ virtual int process( Node f, Theory::Effort effort, int e ) = 0;
+ /** identify */
+ virtual std::string identify() const { return std::string("Unknown"); }
+ /** register quantifier */
+ //virtual void registerQuantifier( Node q ) {}
+};/* class InstStrategy */
+
+class InstantiationEngine : public QuantifiersModule {
+ private:
+ /** instantiation strategies */
+ std::vector<InstStrategy*> d_instStrategies;
+ /** user-pattern instantiation strategy */
+ std::unique_ptr<InstStrategyUserPatterns> d_isup;
+ /** auto gen triggers; only kept for destructor cleanup */
+ std::unique_ptr<InstStrategyAutoGenTriggers> d_i_ag;
+
+ typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
+ /** current processing quantified formulas */
+ std::vector<Node> d_quants;
+
+ /** is the engine incomplete for this quantifier */
+ bool isIncomplete(Node q);
+ /** do instantiation round */
+ void doInstantiationRound(Theory::Effort effort);
+
+ public:
+ InstantiationEngine(QuantifiersEngine* qe);
+ ~InstantiationEngine();
+ void presolve();
+ bool needsCheck(Theory::Effort e);
+ void reset_round(Theory::Effort e);
+ void check(Theory::Effort e, QEffort quant_e);
+ bool checkCompleteFor(Node q);
+ void preRegisterQuantifier(Node q);
+ void registerQuantifier(Node q);
+ Node explain(TNode n) { return Node::null(); }
+ /** add user pattern */
+ void addUserPattern(Node q, Node pat);
+ void addUserNoPattern(Node q, Node pat);
+ /** Identify this module */
+ std::string identify() const { return "InstEngine"; }
+}; /* class InstantiationEngine */
+
+}/* CVC4::theory::quantifiers namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
new file mode 100644
index 000000000..b73c3368d
--- /dev/null
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -0,0 +1,969 @@
+/********************* */
+/*! \file trigger.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Morgan Deters, Tim King
+ ** 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 trigger class
+ **/
+
+#include "theory/quantifiers/ematching/trigger.h"
+
+#include "theory/arith/arith_msum.h"
+#include "theory/quantifiers/candidate_generator.h"
+#include "theory/quantifiers/ematching/ho_trigger.h"
+#include "theory/quantifiers/ematching/inst_match_generator.h"
+#include "theory/quantifiers/instantiate.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 "util/hash.h"
+
+using namespace std;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+
+namespace CVC4 {
+namespace theory {
+namespace inst {
+
+void TriggerTermInfo::init( Node q, Node n, int reqPol, Node reqPolEq ){
+ if( d_fv.empty() ){
+ quantifiers::TermUtil::getVarContainsNode( q, n, d_fv );
+ }
+ if( d_reqPol==0 ){
+ d_reqPol = reqPol;
+ d_reqPolEq = reqPolEq;
+ }else{
+ //determined a ground (dis)equality must hold or else q is a tautology?
+ }
+ d_weight = Trigger::getTriggerWeight(n);
+}
+
+/** trigger class constructor */
+Trigger::Trigger(QuantifiersEngine* qe, Node q, std::vector<Node>& nodes)
+ : d_quantEngine(qe), d_quant(q)
+{
+ d_nodes.insert( d_nodes.begin(), nodes.begin(), nodes.end() );
+ Trace("trigger") << "Trigger for " << q << ": " << std::endl;
+ for( unsigned i=0; i<d_nodes.size(); i++ ){
+ Trace("trigger") << " " << d_nodes[i] << std::endl;
+ }
+ if( d_nodes.size()==1 ){
+ if( isSimpleTrigger( d_nodes[0] ) ){
+ d_mg = new InstMatchGeneratorSimple(q, d_nodes[0], qe);
+ }else{
+ d_mg = InstMatchGenerator::mkInstMatchGenerator(q, d_nodes[0], qe);
+ }
+ }else{
+ if( options::multiTriggerCache() ){
+ d_mg = new InstMatchGeneratorMulti(q, d_nodes, qe);
+ }else{
+ d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti(q, d_nodes, qe);
+ }
+ }
+ if( d_nodes.size()==1 ){
+ if( isSimpleTrigger( d_nodes[0] ) ){
+ ++(qe->d_statistics.d_triggers);
+ }else{
+ ++(qe->d_statistics.d_simple_triggers);
+ }
+ }else{
+ Trace("multi-trigger") << "Trigger for " << q << ": " << std::endl;
+ for( unsigned i=0; i<d_nodes.size(); i++ ){
+ Trace("multi-trigger") << " " << d_nodes[i] << std::endl;
+ }
+ ++(qe->d_statistics.d_multi_triggers);
+ }
+
+ // Notice() << "Trigger : " << (*this) << " for " << q << std::endl;
+ Trace("trigger-debug") << "Finished making trigger." << std::endl;
+}
+
+Trigger::~Trigger() {
+ delete d_mg;
+}
+
+void Trigger::resetInstantiationRound(){
+ d_mg->resetInstantiationRound( d_quantEngine );
+}
+
+void Trigger::reset( Node eqc ){
+ d_mg->reset( eqc, d_quantEngine );
+}
+
+Node Trigger::getInstPattern(){
+ return NodeManager::currentNM()->mkNode( INST_PATTERN, d_nodes );
+}
+
+int Trigger::addInstantiations()
+{
+ int addedLemmas = d_mg->addInstantiations(d_quant, d_quantEngine, this);
+ if( addedLemmas>0 ){
+ 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;
+ }
+ }
+ return addedLemmas;
+}
+
+bool Trigger::sendInstantiation(InstMatch& m)
+{
+ return d_quantEngine->getInstantiate()->addInstantiation(d_quant, 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;
+ temp.insert( temp.begin(), nodes.begin(), nodes.end() );
+ std::map< Node, bool > vars;
+ std::map< Node, std::vector< Node > > patterns;
+ size_t varCount = 0;
+ std::map< Node, std::vector< Node > > varContains;
+ quantifiers::TermUtil::getVarContains( q, temp, varContains );
+ for( unsigned i=0; i<temp.size(); i++ ){
+ bool foundVar = false;
+ for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){
+ Node v = varContains[ temp[i] ][j];
+ Assert( quantifiers::TermUtil::getInstConstAttr(v)==q );
+ if( vars.find( v )==vars.end() ){
+ varCount++;
+ vars[ v ] = true;
+ foundVar = true;
+ }
+ }
+ if( foundVar ){
+ trNodes.push_back( temp[i] );
+ for( unsigned j=0; j<varContains[ temp[i] ].size(); j++ ){
+ Node v = varContains[ temp[i] ][j];
+ patterns[ v ].push_back( temp[i] );
+ }
+ }
+ if( varCount==n_vars ){
+ break;
+ }
+ }
+ if( varCount<n_vars ){
+ Trace("trigger-debug") << "Don't consider trigger since it does not contain specified number of variables." << std::endl;
+ for( unsigned i=0; i<nodes.size(); i++) {
+ Trace("trigger-debug") << nodes[i] << " ";
+ }
+ Trace("trigger-debug") << std::endl;
+
+ //do not generate multi-trigger if it does not contain all variables
+ return false;
+ }else{
+ //now, minimize the trigger
+ for( unsigned i=0; i<trNodes.size(); i++ ){
+ bool keepPattern = false;
+ Node n = trNodes[i];
+ for( unsigned j=0; j<varContains[ n ].size(); j++ ){
+ Node v = varContains[ n ][j];
+ if( patterns[v].size()==1 ){
+ keepPattern = true;
+ break;
+ }
+ }
+ if( !keepPattern ){
+ //remove from pattern vector
+ for( unsigned j=0; j<varContains[ n ].size(); j++ ){
+ Node v = varContains[ n ][j];
+ for( unsigned k=0; k<patterns[v].size(); k++ ){
+ if( patterns[v][k]==n ){
+ patterns[v].erase( patterns[v].begin() + k, patterns[v].begin() + k + 1 );
+ break;
+ }
+ }
+ }
+ //remove from trigger nodes
+ trNodes.erase( trNodes.begin() + i, trNodes.begin() + i + 1 );
+ i--;
+ }
+ }
+ }
+ return true;
+}
+
+Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, bool keepAll, int trOption, unsigned use_n_vars ){
+ std::vector< Node > trNodes;
+ if( !keepAll ){
+ unsigned n_vars = use_n_vars==0 ? f[0].getNumChildren() : use_n_vars;
+ if( !mkTriggerTerms( f, nodes, n_vars, trNodes ) ){
+ return NULL;
+ }
+ }else{
+ trNodes.insert( trNodes.begin(), nodes.begin(), nodes.end() );
+ }
+
+ //check for duplicate?
+ if( trOption!=TR_MAKE_NEW ){
+ Trigger* t = qe->getTriggerDatabase()->getTrigger( trNodes );
+ if( t ){
+ if( trOption==TR_GET_OLD ){
+ //just return old trigger
+ return t;
+ }else{
+ return NULL;
+ }
+ }
+ }
+
+ // check if higher-order
+ Trace("trigger-debug") << "Collect higher-order variable triggers..."
+ << std::endl;
+ std::map<Node, std::vector<Node> > ho_apps;
+ HigherOrderTrigger::collectHoVarApplyTerms(f, trNodes, ho_apps);
+ Trace("trigger") << "...got " << ho_apps.size()
+ << " higher-order applications." << std::endl;
+ 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;
+}
+
+Trigger* Trigger::mkTrigger( QuantifiersEngine* qe, Node f, Node n, bool keepAll, int trOption, unsigned use_n_vars ){
+ std::vector< Node > nodes;
+ nodes.push_back( n );
+ return mkTrigger( qe, f, nodes, keepAll, trOption, use_n_vars );
+}
+
+bool Trigger::isUsable( Node n, Node q ){
+ if( quantifiers::TermUtil::getInstConstAttr(n)==q ){
+ if( isAtomicTrigger( n ) ){
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( !isUsable( n[i], q ) ){
+ return false;
+ }
+ }
+ return true;
+ }else if( n.getKind()==INST_CONSTANT ){
+ return true;
+ }else{
+ std::map< Node, Node > coeffs;
+ if( isBooleanTermTrigger( n ) ){
+ return true;
+ }else if( options::purifyTriggers() ){
+ Node x = getInversionVariable( n );
+ if( !x.isNull() ){
+ return true;
+ }
+ }
+ }
+ return false;
+ }else{
+ return true;
+ }
+}
+
+Node Trigger::getIsUsableEq( Node q, Node n ) {
+ Assert( isRelationalTrigger( n ) );
+ for( unsigned i=0; i<2; i++) {
+ if( isUsableEqTerms( q, n[i], n[1-i] ) ){
+ if( i==1 && n.getKind()==EQUAL && !quantifiers::TermUtil::hasInstConstAttr(n[0]) ){
+ return NodeManager::currentNM()->mkNode( n.getKind(), n[1], n[0] );
+ }else{
+ return n;
+ }
+ }
+ }
+ return Node::null();
+}
+
+bool Trigger::isUsableEqTerms( Node q, Node n1, Node n2 ) {
+ if( n1.getKind()==INST_CONSTANT ){
+ if( options::relationalTriggers() ){
+ if( !quantifiers::TermUtil::hasInstConstAttr(n2) ){
+ return true;
+ }else if( n2.getKind()==INST_CONSTANT ){
+ return true;
+ }
+ }
+ }else if( isUsableAtomicTrigger( n1, q ) ){
+ if( options::relationalTriggers() && n2.getKind()==INST_CONSTANT && !quantifiers::TermUtil::containsTerm( n1, n2 ) ){
+ return true;
+ }else if( !quantifiers::TermUtil::hasInstConstAttr(n2) ){
+ return true;
+ }
+ }
+ return false;
+}
+
+Node Trigger::getIsUsableTrigger( Node n, Node q ) {
+ bool pol = true;
+ Trace("trigger-debug") << "Is " << n << " a usable trigger?" << std::endl;
+ if( n.getKind()==NOT ){
+ pol = !pol;
+ n = n[0];
+ }
+ if( n.getKind()==INST_CONSTANT ){
+ return pol ? n : NodeManager::currentNM()->mkNode( EQUAL, n, NodeManager::currentNM()->mkConst( true ) ).notNode();
+ }else if( isRelationalTrigger( n ) ){
+ Node rtr = getIsUsableEq( q, n );
+ if( rtr.isNull() && n[0].getType().isReal() ){
+ //try to solve relation
+ std::map< Node, Node > m;
+ if (ArithMSum::getMonomialSumLit(n, m))
+ {
+ for( std::map< Node, Node >::iterator it = m.begin(); it!=m.end(); ++it ){
+ bool trySolve = false;
+ if( !it->first.isNull() ){
+ if( it->first.getKind()==INST_CONSTANT ){
+ trySolve = options::relationalTriggers();
+ }else if( isUsableTrigger( it->first, q ) ){
+ trySolve = true;
+ }
+ }
+ if( trySolve ){
+ Trace("trigger-debug") << "Try to solve for " << it->first << std::endl;
+ Node veq;
+ if (ArithMSum::isolate(it->first, m, veq, n.getKind()) != 0)
+ {
+ rtr = getIsUsableEq( q, veq );
+ }
+ //either all solves will succeed or all solves will fail
+ break;
+ }
+ }
+ }
+ }
+ if( !rtr.isNull() ){
+ Trace("relational-trigger") << "Relational trigger : " << std::endl;
+ Trace("relational-trigger") << " " << rtr << " (from " << n << ")" << std::endl;
+ Trace("relational-trigger") << " in quantifier " << q << std::endl;
+ Node rtr2 = pol ? rtr : rtr.negate();
+ Trace("relational-trigger") << " return : " << rtr2 << std::endl;
+ return rtr2;
+ }
+ }else{
+ Trace("trigger-debug") << n << " usable : " << ( quantifiers::TermUtil::getInstConstAttr(n)==q ) << " " << isAtomicTrigger( n ) << " " << isUsable( n, q ) << std::endl;
+ if( isUsableAtomicTrigger( n, q ) ){
+ return pol ? n : NodeManager::currentNM()->mkNode( EQUAL, n, NodeManager::currentNM()->mkConst( true ) ).notNode();
+ }
+ }
+ return Node::null();
+}
+
+bool Trigger::isUsableAtomicTrigger( Node n, Node q ) {
+ return quantifiers::TermUtil::getInstConstAttr( n )==q && isAtomicTrigger( n ) && isUsable( n, q );
+}
+
+bool Trigger::isUsableTrigger( Node n, Node q ){
+ Node nu = getIsUsableTrigger( n, q );
+ return !nu.isNull();
+}
+
+bool Trigger::isAtomicTrigger( Node n ){
+ return isAtomicTriggerKind( n.getKind() );
+}
+
+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 || k == HO_APPLY;
+}
+
+bool Trigger::isRelationalTrigger( Node n ) {
+ return isRelationalTriggerKind( n.getKind() );
+}
+
+bool Trigger::isRelationalTriggerKind( Kind k ) {
+ return k==EQUAL || k==GEQ;
+}
+
+bool Trigger::isCbqiKind( Kind k ) {
+ if( quantifiers::TermUtil::isBoolConnective( k ) || k==PLUS || k==GEQ || k==EQUAL || k==MULT ){
+ return true;
+ }else{
+ //CBQI typically works for satisfaction-complete theories
+ TheoryId t = kindToTheoryId( k );
+ return t == THEORY_BV || t == THEORY_DATATYPES || t == THEORY_BOOL;
+ }
+}
+
+bool Trigger::isSimpleTrigger( Node n ){
+ Node t = n.getKind()==NOT ? n[0] : n;
+ if( t.getKind()==EQUAL ){
+ if( !quantifiers::TermUtil::hasInstConstAttr( t[1] ) ){
+ t = t[0];
+ }
+ }
+ if( isAtomicTrigger( t ) ){
+ for( unsigned i=0; i<t.getNumChildren(); i++ ){
+ if( t[i].getKind()!=INST_CONSTANT && quantifiers::TermUtil::hasInstConstAttr(t[i]) ){
+ return false;
+ }
+ }
+ 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;
+ }
+}
+
+//store triggers in reqPol, indicating their polarity (if any) they must appear to falsify the quantified formula
+void Trigger::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 ){
+ std::map< Node, std::vector< Node > >::iterator itv = visited.find( n );
+ if( itv==visited.end() ){
+ visited[ n ].clear();
+ Trace("auto-gen-trigger-debug2") << "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol << " " << hasEPol << std::endl;
+ if( n.getKind()!=FORALL && n.getKind()!=INST_CONSTANT ){
+ Node nu;
+ bool nu_single = false;
+ if( knowIsUsable ){
+ nu = n;
+ }else if( n.getKind()!=NOT && std::find( exclude.begin(), exclude.end(), n )==exclude.end() ){
+ nu = getIsUsableTrigger( n, q );
+ if( !nu.isNull() && nu!=n ){
+ collectPatTerms2( q, nu, visited, tinfo, tstrt, exclude, added, pol, hasPol, epol, hasEPol, true );
+ // copy to n
+ visited[n].insert( visited[n].end(), added.begin(), added.end() );
+ return;
+ }
+ }
+ if( !nu.isNull() ){
+ Assert( nu==n );
+ Assert( nu.getKind()!=NOT );
+ Trace("auto-gen-trigger-debug2") << "...found usable trigger : " << nu << std::endl;
+ Node reqEq;
+ if( nu.getKind()==EQUAL ){
+ if( isAtomicTrigger( nu[0] ) && !quantifiers::TermUtil::hasInstConstAttr(nu[1]) ){
+ if( hasPol ){
+ reqEq = nu[1];
+ }
+ nu = nu[0];
+ }
+ }
+ Assert( reqEq.isNull() || !quantifiers::TermUtil::hasInstConstAttr( reqEq ) );
+ Assert( isUsableTrigger( nu, q ) );
+ //tinfo.find( nu )==tinfo.end()
+ Trace("auto-gen-trigger-debug2") << "...add usable trigger : " << nu << std::endl;
+ tinfo[ nu ].init( q, nu, hasEPol ? ( epol ? 1 : -1 ) : 0, reqEq );
+ nu_single = tinfo[ nu ].d_fv.size()==q[0].getNumChildren();
+ }
+ Node nrec = nu.isNull() ? n : nu;
+ std::vector< Node > added2;
+ for( unsigned i=0; i<nrec.getNumChildren(); i++ ){
+ bool newHasPol, newPol;
+ bool newHasEPol, newEPol;
+ QuantPhaseReq::getPolarity( nrec, i, hasPol, pol, newHasPol, newPol );
+ QuantPhaseReq::getEntailPolarity( nrec, i, hasEPol, epol, newHasEPol, newEPol );
+ collectPatTerms2( q, nrec[i], visited, tinfo, tstrt, exclude, added2, newPol, newHasPol, newEPol, newHasEPol );
+ }
+ // if this is not a usable trigger, don't worry about caching the results, since triggers do not contain non-usable subterms
+ if( !nu.isNull() ){
+ bool rm_nu = false;
+ for( unsigned i=0; i<added2.size(); i++ ){
+ Trace("auto-gen-trigger-debug2") << "..." << nu << " added child " << i << " : " << added2[i] << std::endl;
+ Assert( added2[i]!=nu );
+ // if child was not already removed
+ if( tinfo.find( added2[i] )!=tinfo.end() ){
+ if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){
+ //discard all subterms
+ Trace("auto-gen-trigger-debug2") << "......remove it." << std::endl;
+ visited[ added2[i] ].clear();
+ tinfo.erase( added2[i] );
+ }else{
+ if( tinfo[ nu ].d_fv.size()==tinfo[ added2[i] ].d_fv.size() ){
+ if (tinfo[nu].d_weight >= tinfo[added2[i]].d_weight)
+ {
+ // discard if we added a subterm as a trigger with all
+ // variables that nu has
+ Trace("auto-gen-trigger-debug2")
+ << "......subsumes parent " << tinfo[nu].d_weight << " "
+ << tinfo[added2[i]].d_weight << "." << std::endl;
+ rm_nu = true;
+ }
+ }
+ if( std::find( added.begin(), added.end(), added2[i] )==added.end() ){
+ added.push_back( added2[i] );
+ }
+ }
+ }
+ }
+ if( rm_nu && ( tstrt==quantifiers::TRIGGER_SEL_MIN || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL && nu_single ) ) ){
+ tinfo.erase( nu );
+ }else{
+ if( std::find( added.begin(), added.end(), nu )==added.end() ){
+ added.push_back( nu );
+ }
+ }
+ visited[n].insert( visited[n].end(), added.begin(), added.end() );
+ }
+ }
+ }else{
+ for( unsigned i=0; i<itv->second.size(); ++i ){
+ Node t = itv->second[i];
+ if( std::find( added.begin(), added.end(), t )==added.end() ){
+ added.push_back( t );
+ }
+ }
+ }
+}
+
+bool Trigger::isBooleanTermTrigger( Node n ) {
+ if( n.getKind()==ITE ){
+ //check for boolean term converted to ITE
+ if( n[0].getKind()==INST_CONSTANT &&
+ n[1].getKind()==CONST_BITVECTOR &&
+ n[2].getKind()==CONST_BITVECTOR ){
+ if( ((BitVectorType)n[1].getType().toType()).getSize()==1 &&
+ n[1].getConst<BitVector>().toInteger()==1 &&
+ n[2].getConst<BitVector>().toInteger()==0 ){
+ return true;
+ }
+ }
+ }
+ return false;
+}
+
+bool Trigger::isPureTheoryTrigger( Node n ) {
+ if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){ //|| !quantifiers::TermUtil::hasInstConstAttr( n ) ){
+ return false;
+ }else{
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( !isPureTheoryTrigger( n[i] ) ){
+ return false;
+ }
+ }
+ return true;
+ }
+}
+
+int Trigger::getTriggerWeight( Node n ) {
+ if (n.getKind() == APPLY_UF)
+ {
+ return 0;
+ }
+ else if (isAtomicTrigger(n))
+ {
+ return 1;
+ }else{
+ if( options::relationalTriggers() ){
+ if( isRelationalTrigger( n ) ){
+ for( unsigned i=0; i<2; i++ ){
+ if( n[i].getKind()==INST_CONSTANT && !quantifiers::TermUtil::hasInstConstAttr( n[1-i] ) ){
+ return 0;
+ }
+ }
+ }
+ }
+ return 2;
+ }
+}
+
+bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< Node >& patTerms ) {
+ if( !n.getType().isBoolean() && n.getKind()==APPLY_UF ){
+ if( std::find( patTerms.begin(), patTerms.end(), n )==patTerms.end() ){
+ bool hasVar = false;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( n[i].getKind()==INST_CONSTANT ){
+ hasVar = true;
+ if( std::find( vars.begin(), vars.end(), n[i] )==vars.end() ){
+ vars.push_back( n[i] );
+ }else{
+ //do not allow duplicate variables
+ return false;
+ }
+ }else{
+ //do not allow nested function applications
+ return false;
+ }
+ }
+ if( hasVar ){
+ patTerms.push_back( n );
+ }
+ }
+ }else{
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( !isLocalTheoryExt( n[i], vars, patTerms ) ){
+ return false;
+ }
+ }
+ }
+ return true;
+}
+
+void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude,
+ std::map< Node, TriggerTermInfo >& tinfo, bool filterInst ){
+ std::map< Node, std::vector< Node > > visited;
+ if( filterInst ){
+ //immediately do not consider any term t for which another term is an instance of t
+ std::vector< Node > patTerms2;
+ std::map< Node, TriggerTermInfo > tinfo2;
+ collectPatTerms( q, n, patTerms2, quantifiers::TRIGGER_SEL_ALL, exclude, tinfo2, false );
+ std::vector< Node > temp;
+ temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() );
+ filterTriggerInstances(temp);
+ if (Trace.isOn("trigger-filter-instance"))
+ {
+ if (temp.size() != patTerms2.size())
+ {
+ Trace("trigger-filter-instance") << "Filtered an instance: "
+ << std::endl;
+ Trace("trigger-filter-instance") << "Old: ";
+ for (unsigned i = 0; i < patTerms2.size(); i++)
+ {
+ Trace("trigger-filter-instance") << patTerms2[i] << " ";
+ }
+ Trace("trigger-filter-instance") << std::endl << "New: ";
+ for (unsigned i = 0; i < temp.size(); i++)
+ {
+ Trace("trigger-filter-instance") << temp[i] << " ";
+ }
+ Trace("trigger-filter-instance") << std::endl;
+ }
+ }
+ if( tstrt==quantifiers::TRIGGER_SEL_ALL ){
+ for( unsigned i=0; i<temp.size(); i++ ){
+ //copy information
+ tinfo[temp[i]].d_fv.insert( tinfo[temp[i]].d_fv.end(), tinfo2[temp[i]].d_fv.begin(), tinfo2[temp[i]].d_fv.end() );
+ tinfo[temp[i]].d_reqPol = tinfo2[temp[i]].d_reqPol;
+ tinfo[temp[i]].d_reqPolEq = tinfo2[temp[i]].d_reqPolEq;
+ patTerms.push_back( temp[i] );
+ }
+ return;
+ }else{
+ //do not consider terms that have instances
+ for( unsigned i=0; i<patTerms2.size(); i++ ){
+ if( std::find( temp.begin(), temp.end(), patTerms2[i] )==temp.end() ){
+ visited[ patTerms2[i] ].clear();
+ }
+ }
+ }
+ }
+ std::vector< Node > added;
+ collectPatTerms2( q, n, visited, tinfo, tstrt, exclude, added, true, true, false, true );
+ for( std::map< Node, TriggerTermInfo >::iterator it = tinfo.begin(); it != tinfo.end(); ++it ){
+ patTerms.push_back( it->first );
+ }
+}
+
+int Trigger::isTriggerInstanceOf(Node n1,
+ Node n2,
+ std::vector<Node>& fv1,
+ std::vector<Node>& fv2)
+{
+ Assert(n1 != n2);
+ int status = 0;
+ std::unordered_set<TNode, TNodeHashFunction> subs_vars;
+ std::unordered_set<std::pair<TNode, TNode>,
+ PairHashFunction<TNode,
+ TNode,
+ TNodeHashFunction,
+ TNodeHashFunction> >
+ visited;
+ std::vector<std::pair<TNode, TNode> > visit;
+ std::pair<TNode, TNode> cur;
+ TNode cur1;
+ TNode cur2;
+ visit.push_back(std::pair<TNode, TNode>(n1, n2));
+ do
+ {
+ cur = visit.back();
+ visit.pop_back();
+ if (visited.find(cur) == visited.end())
+ {
+ visited.insert(cur);
+ cur1 = cur.first;
+ cur2 = cur.second;
+ Assert(cur1 != cur2);
+ // recurse if they have the same operator
+ if (cur1.hasOperator() && cur2.hasOperator()
+ && cur1.getNumChildren() == cur2.getNumChildren()
+ && cur1.getOperator() == cur2.getOperator()
+ && cur1.getOperator().getKind()!=INST_CONSTANT)
+ {
+ visit.push_back(std::pair<TNode, TNode>(cur1, cur2));
+ for (unsigned i = 0, size = cur1.getNumChildren(); i < size; i++)
+ {
+ if (cur1[i] != cur2[i])
+ {
+ visit.push_back(std::pair<TNode, TNode>(cur1[i], cur2[i]));
+ }
+ else if (cur1[i].getKind() == INST_CONSTANT)
+ {
+ if (subs_vars.find(cur1[i]) != subs_vars.end())
+ {
+ return 0;
+ }
+ // the variable must map to itself in the substitution
+ subs_vars.insert(cur1[i]);
+ }
+ }
+ }
+ else
+ {
+ bool success = false;
+ // check if we are in a unifiable instance case
+ // must be only this case
+ for (unsigned r = 0; r < 2; r++)
+ {
+ if (status == 0 || ((status == 1) == (r == 0)))
+ {
+ TNode curi = r == 0 ? cur1 : cur2;
+ if (curi.getKind() == INST_CONSTANT
+ && subs_vars.find(curi) == subs_vars.end())
+ {
+ TNode curj = r == 0 ? cur2 : cur1;
+ // RHS must be a simple trigger
+ if (getTriggerWeight(curj) == 0)
+ {
+ // must occur in the free variables in the other
+ std::vector<Node>& free_vars = r == 0 ? fv2 : fv1;
+ if (std::find(free_vars.begin(), free_vars.end(), curi)
+ != free_vars.end())
+ {
+ status = r == 0 ? 1 : -1;
+ subs_vars.insert(curi);
+ success = true;
+ break;
+ }
+ }
+ }
+ }
+ }
+ if (!success)
+ {
+ return 0;
+ }
+ }
+ }
+ } while (!visit.empty());
+ return status;
+}
+
+void Trigger::filterTriggerInstances(std::vector<Node>& nodes)
+{
+ std::map<unsigned, std::vector<Node> > fvs;
+ for (unsigned i = 0, size = nodes.size(); i < size; i++)
+ {
+ quantifiers::TermUtil::computeVarContains(nodes[i], fvs[i]);
+ }
+ std::vector<bool> active;
+ active.resize(nodes.size(), true);
+ for (unsigned i = 0, size = nodes.size(); i < size; i++)
+ {
+ std::vector<Node>& fvsi = fvs[i];
+ if (active[i])
+ {
+ for (unsigned j = i + 1, size2 = nodes.size(); j < size2; j++)
+ {
+ if (active[j])
+ {
+ int result = isTriggerInstanceOf(nodes[i], nodes[j], fvsi, fvs[j]);
+ if (result == 1)
+ {
+ Trace("filter-instances") << nodes[j] << " is an instance of "
+ << nodes[i] << std::endl;
+ active[i] = false;
+ break;
+ }
+ else if (result == -1)
+ {
+ Trace("filter-instances") << nodes[i] << " is an instance of "
+ << nodes[j] << std::endl;
+ active[j] = false;
+ }
+ }
+ }
+ }
+ }
+ std::vector<Node> temp;
+ for (unsigned i = 0; i < nodes.size(); i++)
+ {
+ if (active[i])
+ {
+ temp.push_back(nodes[i]);
+ }
+ }
+ nodes.clear();
+ nodes.insert(nodes.begin(), temp.begin(), temp.end());
+}
+
+Node Trigger::getInversionVariable( Node n ) {
+ if( n.getKind()==INST_CONSTANT ){
+ return n;
+ }else if( n.getKind()==PLUS || n.getKind()==MULT ){
+ Node ret;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( quantifiers::TermUtil::hasInstConstAttr(n[i]) ){
+ if( ret.isNull() ){
+ ret = getInversionVariable( n[i] );
+ if( ret.isNull() ){
+ Trace("var-trigger-debug") << "No : multiple variables " << n << std::endl;
+ return Node::null();
+ }
+ }else{
+ return Node::null();
+ }
+ }else if( n.getKind()==MULT ){
+ if( !n[i].isConst() ){
+ Trace("var-trigger-debug") << "No : non-linear coefficient " << n << std::endl;
+ return Node::null();
+ }
+ /*
+ else if( n.getType().isInteger() ){
+ Rational r = n[i].getConst<Rational>();
+ if( r!=Rational(-1) && r!=Rational(1) ){
+ Trace("var-trigger-debug") << "No : not integer coefficient " << n << std::endl;
+ return Node::null();
+ }
+ }
+ */
+ }
+ }
+ return ret;
+ }else{
+ Trace("var-trigger-debug") << "No : unsupported operator " << n << "." << std::endl;
+ }
+ return Node::null();
+}
+
+Node Trigger::getInversion( Node n, Node x ) {
+ if( n.getKind()==INST_CONSTANT ){
+ return x;
+ }else if( n.getKind()==PLUS || n.getKind()==MULT ){
+ int cindex = -1;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( !quantifiers::TermUtil::hasInstConstAttr(n[i]) ){
+ if( n.getKind()==PLUS ){
+ x = NodeManager::currentNM()->mkNode( MINUS, x, n[i] );
+ }else if( n.getKind()==MULT ){
+ Assert( n[i].isConst() );
+ if( x.getType().isInteger() ){
+ Node coeff = NodeManager::currentNM()->mkConst( n[i].getConst<Rational>().abs() );
+ if( !n[i].getConst<Rational>().abs().isOne() ){
+ x = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, x, coeff );
+ }
+ if( n[i].getConst<Rational>().sgn()<0 ){
+ x = NodeManager::currentNM()->mkNode( UMINUS, x );
+ }
+ }else{
+ Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / n[i].getConst<Rational>() );
+ x = NodeManager::currentNM()->mkNode( MULT, x, coeff );
+ }
+ }
+ x = Rewriter::rewrite( x );
+ }else{
+ Assert( cindex==-1 );
+ cindex = i;
+ }
+ }
+ Assert( cindex!=-1 );
+ return getInversion( n[cindex], x );
+ }
+ return Node::null();
+}
+
+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 n
+ std::vector< Node > exclude;
+ 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 );
+ }
+}
+
+int Trigger::getActiveScore() {
+ return d_mg->getActiveScore( d_quantEngine );
+}
+
+TriggerTrie::TriggerTrie()
+{}
+
+TriggerTrie::~TriggerTrie() {
+ for(std::map< TNode, TriggerTrie* >::iterator i = d_children.begin(), iend = d_children.end();
+ i != iend; ++i) {
+ TriggerTrie* current = (*i).second;
+ delete current;
+ }
+ d_children.clear();
+
+ for( unsigned i=0; i<d_tr.size(); i++ ){
+ delete d_tr[i];
+ }
+}
+
+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 */
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
new file mode 100644
index 000000000..e91a87e58
--- /dev/null
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -0,0 +1,476 @@
+/********************* */
+/*! \file trigger.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Tim King, Morgan Deters
+ ** 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 trigger class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__TRIGGER_H
+#define __CVC4__THEORY__QUANTIFIERS__TRIGGER_H
+
+#include <map>
+
+#include "expr/node.h"
+#include "theory/quantifiers/inst_match.h"
+#include "options/quantifiers_options.h"
+
+namespace CVC4 {
+namespace theory {
+
+class QuantifiersEngine;
+
+namespace inst {
+
+class IMGenerator;
+class InstMatchGenerator;
+
+/** 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), d_weight(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;
+ /** the weight of the trigger (see Trigger::getTriggerWeight). */
+ int d_weight;
+ /** 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 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/ematching/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() );
+* // add all instantiations based on E-matching with this trigger and the
+* // current context
+* t->addInstantiations();
+*
+* 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 {
+ friend class IMGenerator;
+
+ public:
+ virtual ~Trigger();
+ /** get the generator associated with this trigger */
+ IMGenerator* getGenerator() { return d_mg; }
+ /** Reset instantiation round.
+ *
+ * Called once at beginning of an instantiation round.
+ */
+ void resetInstantiationRound();
+ /** 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 );
+ /** 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/ematching/ho_trigger.h).
+ */
+ virtual int addInstantiations();
+ /** Return whether this is a multi-trigger. */
+ bool isMultiTrigger() { return d_nodes.size()>1; }
+ /** 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();
+ /* 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
+ };
+ 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 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 );
+ /** 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 );
+ /** 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);
+
+ protected:
+ /** trigger constructor, intentionally protected (use Trigger::mkTrigger). */
+ Trigger(QuantifiersEngine* ie, Node q, std::vector<Node>& nodes);
+ /** 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 );
+ /** 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 );
+
+ /** filter all nodes that have trigger instances
+ *
+ * This is used during collectModelInfo to filter certain trigger terms,
+ * stored in nodes. This updates nodes so that no pairs of distinct nodes
+ * (i,j) is such that i is a trigger instance of j or vice versa (see below).
+ */
+ static void filterTriggerInstances(std::vector<Node>& nodes);
+
+ /** is instance of
+ *
+ * We say a term t is an trigger instance of term s if
+ * (1) t = s * { x1 -> t1 ... xn -> tn }
+ * (2) { x1, ..., xn } are a subset of FV( t ).
+ * For example, f( g( h( x, x ) ) ) and f( g( x ) ) are instances of f( x ),
+ * but f( g( y ) ) and g( x ) are not instances of f( x ).
+ *
+ * When this method returns -1, n1 is an instance of n2,
+ * When this method returns 1, n1 is an instance of n2.
+ *
+ * The motivation for this method is to discard triggers s that are less
+ * restrictive (criteria (1)) and serve to bind the same variables (criteria
+ * (2)) as another trigger t. This often helps avoiding matching loops.
+ */
+ static int isTriggerInstanceOf(Node n1,
+ Node n2,
+ std::vector<Node>& fv1,
+ std::vector<Node>& fv2);
+
+ /** 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 associated with this trigger. */
+ QuantifiersEngine* d_quantEngine;
+ /** The quantified formula this trigger is for. */
+ Node d_quant;
+ /** 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.
+*
+* 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);
+
+ 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 */
+
+}/* CVC4::theory::inst namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__TRIGGER_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback