diff options
Diffstat (limited to 'src/theory/quantifiers/ematching')
-rw-r--r-- | src/theory/quantifiers/ematching/ho_trigger.cpp | 475 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/ho_trigger.h | 278 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/inst_match_generator.cpp | 1138 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/inst_match_generator.h | 694 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp | 613 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/inst_strategy_e_matching.h | 119 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/instantiation_engine.cpp | 209 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/instantiation_engine.h | 98 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/trigger.cpp | 969 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/trigger.h | 476 |
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 */ |