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