This separates the utilities for selecting pattern terms from the Trigger class itself. This includes a PatternTermSelector, which implements the techniques for selecting the pool of pattern terms, and TriggerTermInfo which contains basic information about pattern terms.
It makes minor refactoring to make the PatternTermSelector class more than just static methods, e.g. it is now a configurable object that selects pattern terms. This makes some of the methods take fewer arguments.
More refactoring is possible, to be addressed on future PRs.
theory/quantifiers/ematching/inst_strategy_e_matching_user.h
theory/quantifiers/ematching/instantiation_engine.cpp
theory/quantifiers/ematching/instantiation_engine.h
+ theory/quantifiers/ematching/pattern_term_selector.cpp
+ theory/quantifiers/ematching/pattern_term_selector.h
theory/quantifiers/ematching/trigger.cpp
theory/quantifiers/ematching/trigger.h
+ theory/quantifiers/ematching/trigger_term_info.cpp
+ theory/quantifiers/ematching/trigger_term_info.h
theory/quantifiers/ematching/trigger_trie.cpp
theory/quantifiers/ematching/trigger_trie.h
theory/quantifiers/ematching/var_match_generator.cpp
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "theory/arith/arith_msum.h"
-#include "theory/quantifiers/ematching/trigger.h"
+#include "theory/quantifiers/ematching/pattern_term_selector.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
return pol && n.getKind()==EQUAL;
}
-bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) {
+bool QuantifierMacros::isGroundUfTerm(Node q, Node n)
+{
Node icn = d_preprocContext->getTheoryEngine()
->getQuantifiersEngine()
->getTermUtil()
- ->substituteBoundVariablesToInstConstants(n, f);
+ ->substituteBoundVariablesToInstConstants(n, q);
Trace("macros-debug2") << "Get free variables in " << icn << std::endl;
std::vector< Node > var;
- quantifiers::TermUtil::computeInstConstContainsForQuant(f, icn, var);
+ quantifiers::TermUtil::computeInstConstContainsForQuant(q, icn, var);
Trace("macros-debug2") << "Get trigger variables for " << icn << std::endl;
std::vector< Node > trigger_var;
- inst::Trigger::getTriggerVariables( icn, f, trigger_var );
+ inst::PatternTermSelector::getTriggerVariables(icn, q, trigger_var);
Trace("macros-debug2") << "Done." << std::endl;
//only if all variables are also trigger variables
return trigger_var.size()>=var.size();
#include "theory/quantifiers/conjecture_generator.h"
#include "expr/term_canonize.h"
#include "options/quantifiers_options.h"
-#include "theory/quantifiers/ematching/trigger.h"
+#include "theory/quantifiers/ematching/trigger_term_info.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/skolemize.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_enumeration.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
-#include "theory/theory_engine.h"
#include "util/random.h"
using namespace CVC4;
}
bool ConjectureGenerator::isHandledTerm( TNode n ){
- return d_quantEngine->getTermDatabase()->isTermActive( n ) && inst::Trigger::isAtomicTrigger( n ) && ( n.getKind()!=APPLY_UF || n.getOperator().getKind()!=SKOLEM );
+ return d_quantEngine->getTermDatabase()->isTermActive(n)
+ && inst::TriggerTermInfo::isAtomicTrigger(n)
+ && (n.getKind() != APPLY_UF || n.getOperator().getKind() != SKOLEM);
}
Node ConjectureGenerator::getGroundEqc( TNode r ) {
#include "theory/quantifiers/ematching/inst_match_generator_multi.h"
#include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h"
#include "theory/quantifiers/ematching/inst_match_generator_simple.h"
+#include "theory/quantifiers/ematching/pattern_term_selector.h"
#include "theory/quantifiers/ematching/trigger.h"
#include "theory/quantifiers/ematching/var_match_generator.h"
#include "theory/quantifiers/instantiate.h"
int InstMatchGenerator::getActiveScore( QuantifiersEngine * qe ) {
if( d_match_pattern.isNull() ){
return -1;
- }else if( Trigger::isAtomicTrigger( d_match_pattern ) ){
+ }
+ else if (TriggerTermInfo::isAtomicTrigger(d_match_pattern))
+ {
Node f = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
unsigned ngt = qe->getTermDatabase()->getNumGroundTerms( f );
Trace("trigger-active-sel-debug") << "Number of ground terms for " << f << " is " << ngt << std::endl;
// applied selectors
d_cg = new inst::CandidateGeneratorSelector(qe, d_match_pattern);
}
- else if (Trigger::isAtomicTriggerKind(mpk))
+ else if (TriggerTermInfo::isAtomicTriggerKind(mpk))
{
if (mpk == APPLY_CONSTRUCTOR)
{
Node x;
if (options::purifyTriggers())
{
- Node xi = Trigger::getInversionVariable(n);
+ Node xi = PatternTermSelector::getInversionVariable(n);
if (!xi.isNull())
{
Node qa = quantifiers::TermUtil::getInstConstAttr(xi);
}
if (!x.isNull())
{
- Node s = Trigger::getInversion(n, x);
+ Node s = PatternTermSelector::getInversion(n, x);
VarMatchGeneratorTermSubs* vmg = new VarMatchGeneratorTermSubs(x, s);
Trace("var-trigger") << "Term substitution trigger : " << n
<< ", var = " << x << ", subs = " << s << std::endl;
**/
#include "theory/quantifiers/ematching/inst_match_generator_simple.h"
+#include "theory/quantifiers/ematching/trigger_term_info.h"
#include "theory/quantifiers_engine.h"
using namespace CVC4::kind;
d_match_pattern = d_match_pattern[0];
Assert(!quantifiers::TermUtil::hasInstConstAttr(d_eqc));
}
- Assert(Trigger::isSimpleTrigger(d_match_pattern));
+ Assert(TriggerTermInfo::isSimpleTrigger(d_match_pattern));
for (size_t i = 0, nchild = d_match_pattern.getNumChildren(); i < nchild; i++)
{
if (d_match_pattern[i].getKind() == INST_CONSTANT)
#include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
+#include "theory/quantifiers/ematching/pattern_term_selector.h"
#include "theory/quantifiers/quant_relevance.h"
#include "theory/quantifiers_engine.h"
#include "util/random.h"
struct sortTriggers {
bool operator() (Node i, Node j) {
- int wi = Trigger::getTriggerWeight( i );
- int wj = Trigger::getTriggerWeight( j );
+ int32_t wi = TriggerTermInfo::getTriggerWeight(i);
+ int32_t wj = TriggerTermInfo::getTriggerWeight(j);
if( wi==wj ){
return i<j;
}
if (patTermsF.empty())
{
Node bd = tu->getInstConstantBody(f);
- Trigger::collectPatTerms(
- f, bd, patTermsF, d_tr_strategy, d_user_no_gen[f], tinfo, true);
+ PatternTermSelector pts(f, d_tr_strategy, d_user_no_gen[f], true);
+ pts.collect(bd, patTermsF, tinfo);
if (ntrivTriggers)
{
sortTriggers st;
// considered
std::map<Node, bool> vcMap;
std::map<Node, bool> rmPatTermsF;
- int last_weight = -1;
+ int32_t last_weight = -1;
for (const Node& p : patTermsF)
{
Assert(p.getKind() != NOT);
newVar = true;
}
}
- int curr_w = Trigger::getTriggerWeight(p);
+ int32_t curr_w = TriggerTermInfo::getTriggerWeight(p);
// triggers whose value is maximum (2) are considered expendable.
if (ntrivTriggers && !newVar && last_weight != -1 && curr_w > last_weight
&& curr_w >= 2)
if (rpol != 0)
{
Assert(rpol == 1 || rpol == -1);
- if (Trigger::isRelationalTrigger(pat))
+ if (TriggerTermInfo::isRelationalTrigger(pat))
{
pat = rpol == -1 ? pat.negate() : pat;
}
else
{
- Assert(Trigger::isAtomicTrigger(pat));
+ Assert(TriggerTermInfo::isAtomicTrigger(pat));
if (pat.getType().isBoolean() && rpoleq.isNull())
{
if (options::literalMatchMode() == options::LiteralMatchMode::USE)
}
else
{
- if (Trigger::isRelationalTrigger(pat))
+ if (TriggerTermInfo::isRelationalTrigger(pat))
{
// consider both polarities
addPatternToPool(f, pat.negate(), num_fv, mpat);
#include "theory/quantifiers/ematching/inst_strategy_e_matching_user.h"
+#include "theory/quantifiers/ematching/pattern_term_selector.h"
#include "theory/quantifiers_engine.h"
using namespace CVC4::kind;
std::vector<Node> nodes;
for (const Node& p : pat)
{
- Node pat_use = Trigger::getIsUsableTrigger(p, q);
+ Node pat_use = PatternTermSelector::getIsUsableTrigger(p, q);
if (pat_use.isNull())
{
Trace("trigger-warn") << "User-provided trigger is not usable : " << pat
--- /dev/null
+/********************* */
+/*! \file pattern_term_selector.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Morgan Deters, Mathias Preiner
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 pattern term selector class
+ **/
+
+#include "theory/quantifiers/ematching/pattern_term_selector.h"
+
+#include "expr/node_algorithm.h"
+#include "theory/arith/arith_msum.h"
+#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/term_util.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace inst {
+
+PatternTermSelector::PatternTermSelector(Node q,
+ options::TriggerSelMode tstrt,
+ const std::vector<Node>& exc,
+ bool filterInst)
+ : d_quant(q), d_tstrt(tstrt), d_excluded(exc), d_filterInst(filterInst)
+{
+}
+
+PatternTermSelector::~PatternTermSelector() {}
+
+bool PatternTermSelector::isUsable(Node n, Node q)
+{
+ if (quantifiers::TermUtil::getInstConstAttr(n) != q)
+ {
+ return true;
+ }
+ if (TriggerTermInfo::isAtomicTrigger(n))
+ {
+ for (const Node& nc : n)
+ {
+ if (!isUsable(nc, q))
+ {
+ return false;
+ }
+ }
+ return true;
+ }
+ else if (n.getKind() == INST_CONSTANT)
+ {
+ return true;
+ }
+ std::map<Node, Node> coeffs;
+ if (options::purifyTriggers())
+ {
+ Node x = getInversionVariable(n);
+ if (!x.isNull())
+ {
+ return true;
+ }
+ }
+ return false;
+}
+
+Node PatternTermSelector::getIsUsableEq(Node q, Node n)
+{
+ Assert(TriggerTermInfo::isRelationalTrigger(n));
+ for (size_t i = 0; i < 2; i++)
+ {
+ if (isUsableEqTerms(q, n[i], n[1 - i]))
+ {
+ if (i == 1 && n.getKind() == EQUAL
+ && !quantifiers::TermUtil::hasInstConstAttr(n[0]))
+ {
+ return NodeManager::currentNM()->mkNode(n.getKind(), n[1], n[0]);
+ }
+ else
+ {
+ return n;
+ }
+ }
+ }
+ return Node::null();
+}
+
+bool PatternTermSelector::isUsableEqTerms(Node q, Node n1, Node n2)
+{
+ if (n1.getKind() == INST_CONSTANT)
+ {
+ if (options::relationalTriggers())
+ {
+ Node q1 = quantifiers::TermUtil::getInstConstAttr(n1);
+ if (q1 != q)
+ {
+ // x is a variable from another quantified formula, fail
+ return false;
+ }
+ Node q2 = quantifiers::TermUtil::getInstConstAttr(n2);
+ if (q2.isNull())
+ {
+ // x = c
+ return true;
+ }
+ if (n2.getKind() == INST_CONSTANT && q2 == q)
+ {
+ // x = y
+ return true;
+ }
+ // we dont check x = f(y), which is handled symmetrically below
+ // when n1 and n2 are swapped
+ }
+ }
+ else if (isUsableAtomicTrigger(n1, q))
+ {
+ if (options::relationalTriggers() && n2.getKind() == INST_CONSTANT
+ && quantifiers::TermUtil::getInstConstAttr(n2) == q
+ && !expr::hasSubterm(n1, n2))
+ {
+ // f(x) = y
+ return true;
+ }
+ else if (!quantifiers::TermUtil::hasInstConstAttr(n2))
+ {
+ // f(x) = c
+ return true;
+ }
+ }
+ return false;
+}
+
+Node PatternTermSelector::getIsUsableTrigger(Node n, Node q)
+{
+ bool pol = true;
+ Trace("trigger-debug") << "Is " << n << " a usable trigger?" << std::endl;
+ if (n.getKind() == NOT)
+ {
+ pol = !pol;
+ n = n[0];
+ }
+ NodeManager* nm = NodeManager::currentNM();
+ if (n.getKind() == INST_CONSTANT)
+ {
+ return pol ? n : nm->mkNode(EQUAL, n, nm->mkConst(true)).notNode();
+ }
+ else if (TriggerTermInfo::isRelationalTrigger(n))
+ {
+ Node rtr = getIsUsableEq(q, n);
+ if (rtr.isNull() && n[0].getType().isReal())
+ {
+ // try to solve relation
+ std::map<Node, Node> m;
+ if (ArithMSum::getMonomialSumLit(n, m))
+ {
+ for (std::map<Node, Node>::iterator it = m.begin(); it != m.end(); ++it)
+ {
+ bool trySolve = false;
+ if (!it->first.isNull())
+ {
+ if (it->first.getKind() == INST_CONSTANT)
+ {
+ trySolve = options::relationalTriggers();
+ }
+ else if (isUsableTrigger(it->first, q))
+ {
+ trySolve = true;
+ }
+ }
+ if (trySolve)
+ {
+ Trace("trigger-debug")
+ << "Try to solve for " << it->first << std::endl;
+ Node veq;
+ if (ArithMSum::isolate(it->first, m, veq, n.getKind()) != 0)
+ {
+ rtr = getIsUsableEq(q, veq);
+ }
+ // either all solves will succeed or all solves will fail
+ break;
+ }
+ }
+ }
+ }
+ if (!rtr.isNull())
+ {
+ Trace("relational-trigger") << "Relational trigger : " << std::endl;
+ Trace("relational-trigger")
+ << " " << rtr << " (from " << n << ")" << std::endl;
+ Trace("relational-trigger") << " in quantifier " << q << std::endl;
+ Node rtr2 = pol ? rtr : rtr.negate();
+ Trace("relational-trigger") << " return : " << rtr2 << std::endl;
+ return rtr2;
+ }
+ return Node::null();
+ }
+ Trace("trigger-debug") << n << " usable : "
+ << (quantifiers::TermUtil::getInstConstAttr(n) == q)
+ << " " << TriggerTermInfo::isAtomicTrigger(n) << " "
+ << isUsable(n, q) << std::endl;
+ if (isUsableAtomicTrigger(n, q))
+ {
+ return pol ? n : nm->mkNode(EQUAL, n, nm->mkConst(true)).notNode();
+ }
+ return Node::null();
+}
+
+bool PatternTermSelector::isUsableAtomicTrigger(Node n, Node q)
+{
+ return quantifiers::TermUtil::getInstConstAttr(n) == q
+ && TriggerTermInfo::isAtomicTrigger(n) && isUsable(n, q);
+}
+
+bool PatternTermSelector::isUsableTrigger(Node n, Node q)
+{
+ Node nu = getIsUsableTrigger(n, q);
+ return !nu.isNull();
+}
+
+// store triggers in reqPol, indicating their polarity (if any) they must appear
+// to falsify the quantified formula
+void PatternTermSelector::collectTermsInternal(
+ Node n,
+ std::map<Node, std::vector<Node> >& visited,
+ std::map<Node, TriggerTermInfo>& tinfo,
+ options::TriggerSelMode tstrt,
+ std::vector<Node>& added,
+ bool pol,
+ bool hasPol,
+ bool epol,
+ bool hasEPol,
+ bool knowIsUsable)
+{
+ std::map<Node, std::vector<Node> >::iterator itv = visited.find(n);
+ if (itv != visited.end())
+ {
+ // already visited
+ for (const Node& t : itv->second)
+ {
+ if (std::find(added.begin(), added.end(), t) == added.end())
+ {
+ added.push_back(t);
+ }
+ }
+ return;
+ }
+ visited[n].clear();
+ Trace("auto-gen-trigger-debug2")
+ << "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol
+ << " " << hasEPol << std::endl;
+ Kind nk = n.getKind();
+ if (nk == FORALL || nk == INST_CONSTANT)
+ {
+ // do not traverse beneath quantified formulas
+ return;
+ }
+ Node nu;
+ bool nu_single = false;
+ if (knowIsUsable)
+ {
+ nu = n;
+ }
+ else if (nk != NOT
+ && std::find(d_excluded.begin(), d_excluded.end(), n)
+ == d_excluded.end())
+ {
+ nu = getIsUsableTrigger(n, d_quant);
+ if (!nu.isNull() && nu != n)
+ {
+ collectTermsInternal(
+ nu, visited, tinfo, tstrt, added, pol, hasPol, epol, hasEPol, true);
+ // copy to n
+ visited[n].insert(visited[n].end(), added.begin(), added.end());
+ return;
+ }
+ }
+ if (!nu.isNull())
+ {
+ Assert(nu == n);
+ Assert(nu.getKind() != NOT);
+ Trace("auto-gen-trigger-debug2")
+ << "...found usable trigger : " << nu << std::endl;
+ Node reqEq;
+ if (nu.getKind() == EQUAL)
+ {
+ if (TriggerTermInfo::isAtomicTrigger(nu[0])
+ && !quantifiers::TermUtil::hasInstConstAttr(nu[1]))
+ {
+ if (hasPol)
+ {
+ reqEq = nu[1];
+ }
+ nu = nu[0];
+ }
+ }
+ Assert(reqEq.isNull() || !quantifiers::TermUtil::hasInstConstAttr(reqEq));
+ Assert(isUsableTrigger(nu, d_quant));
+ Trace("auto-gen-trigger-debug2")
+ << "...add usable trigger : " << nu << std::endl;
+ tinfo[nu].init(d_quant, nu, hasEPol ? (epol ? 1 : -1) : 0, reqEq);
+ nu_single = tinfo[nu].d_fv.size() == d_quant[0].getNumChildren();
+ }
+ Node nrec = nu.isNull() ? n : nu;
+ std::vector<Node> added2;
+ for (size_t i = 0, nrecc = nrec.getNumChildren(); i < nrecc; i++)
+ {
+ bool newHasPol, newPol;
+ bool newHasEPol, newEPol;
+ QuantPhaseReq::getPolarity(nrec, i, hasPol, pol, newHasPol, newPol);
+ QuantPhaseReq::getEntailPolarity(
+ nrec, i, hasEPol, epol, newHasEPol, newEPol);
+ collectTermsInternal(nrec[i],
+ visited,
+ tinfo,
+ tstrt,
+ added2,
+ newPol,
+ newHasPol,
+ newEPol,
+ newHasEPol);
+ }
+ // if this is not a usable trigger, don't worry about caching the results,
+ // since triggers do not contain non-usable subterms
+ if (nu.isNull())
+ {
+ return;
+ }
+ bool rm_nu = false;
+ for (size_t i = 0, asize = added2.size(); i < asize; i++)
+ {
+ Trace("auto-gen-trigger-debug2") << "..." << nu << " added child " << i
+ << " : " << added2[i] << std::endl;
+ Assert(added2[i] != nu);
+ // if child was not already removed
+ if (tinfo.find(added2[i]) != tinfo.end())
+ {
+ if (tstrt == options::TriggerSelMode::MAX
+ || (tstrt == options::TriggerSelMode::MIN_SINGLE_MAX && !nu_single))
+ {
+ // discard all subterms
+ // do not remove if it has smaller weight
+ if (tinfo[nu].d_weight <= tinfo[added2[i]].d_weight)
+ {
+ Trace("auto-gen-trigger-debug2") << "......remove it." << std::endl;
+ visited[added2[i]].clear();
+ tinfo.erase(added2[i]);
+ }
+ }
+ else
+ {
+ if (tinfo[nu].d_fv.size() == tinfo[added2[i]].d_fv.size())
+ {
+ if (tinfo[nu].d_weight >= tinfo[added2[i]].d_weight)
+ {
+ // discard if we added a subterm as a trigger with all
+ // variables that nu has
+ Trace("auto-gen-trigger-debug2")
+ << "......subsumes parent " << tinfo[nu].d_weight << " "
+ << tinfo[added2[i]].d_weight << "." << std::endl;
+ rm_nu = true;
+ }
+ }
+ if (std::find(added.begin(), added.end(), added2[i]) == added.end())
+ {
+ added.push_back(added2[i]);
+ }
+ }
+ }
+ }
+ if (rm_nu
+ && (tstrt == options::TriggerSelMode::MIN
+ || (tstrt == options::TriggerSelMode::MIN_SINGLE_ALL && nu_single)))
+ {
+ tinfo.erase(nu);
+ }
+ else
+ {
+ if (std::find(added.begin(), added.end(), nu) == added.end())
+ {
+ added.push_back(nu);
+ }
+ }
+ visited[n].insert(visited[n].end(), added.begin(), added.end());
+}
+
+void PatternTermSelector::collect(Node n,
+ std::vector<Node>& patTerms,
+ std::map<Node, TriggerTermInfo>& tinfo)
+{
+ collectInternal(n, patTerms, tinfo, d_tstrt, d_filterInst);
+}
+
+void PatternTermSelector::collectInternal(
+ Node n,
+ std::vector<Node>& patTerms,
+ std::map<Node, TriggerTermInfo>& tinfo,
+ options::TriggerSelMode tstrt,
+ bool filterInst)
+{
+ std::map<Node, std::vector<Node> > visited;
+ if (filterInst)
+ {
+ // immediately do not consider any term t for which another term is an
+ // instance of t
+ std::vector<Node> patTerms2;
+ std::map<Node, TriggerTermInfo> tinfo2;
+ collectInternal(n, patTerms2, tinfo2, options::TriggerSelMode::ALL, false);
+ std::vector<Node> temp;
+ temp.insert(temp.begin(), patTerms2.begin(), patTerms2.end());
+ filterInstances(temp);
+ if (Trace.isOn("trigger-filter-instance"))
+ {
+ if (temp.size() != patTerms2.size())
+ {
+ Trace("trigger-filter-instance")
+ << "Filtered an instance: " << std::endl;
+ Trace("trigger-filter-instance") << "Old: ";
+ for (unsigned i = 0; i < patTerms2.size(); i++)
+ {
+ Trace("trigger-filter-instance") << patTerms2[i] << " ";
+ }
+ Trace("trigger-filter-instance") << std::endl << "New: ";
+ for (unsigned i = 0; i < temp.size(); i++)
+ {
+ Trace("trigger-filter-instance") << temp[i] << " ";
+ }
+ Trace("trigger-filter-instance") << std::endl;
+ }
+ }
+ if (tstrt == options::TriggerSelMode::ALL)
+ {
+ for (const Node& t : temp)
+ {
+ // copy information
+ tinfo[t].d_fv.insert(
+ tinfo[t].d_fv.end(), tinfo2[t].d_fv.begin(), tinfo2[t].d_fv.end());
+ tinfo[t].d_reqPol = tinfo2[t].d_reqPol;
+ tinfo[t].d_reqPolEq = tinfo2[t].d_reqPolEq;
+ patTerms.push_back(t);
+ }
+ return;
+ }
+ // do not consider terms that have instances
+ for (const Node& t : patTerms2)
+ {
+ if (std::find(temp.begin(), temp.end(), t) == temp.end())
+ {
+ visited[t].clear();
+ }
+ }
+ }
+ std::vector<Node> added;
+ collectTermsInternal(
+ n, visited, tinfo, tstrt, added, true, true, false, true);
+ for (const std::pair<const Node, TriggerTermInfo>& t : tinfo)
+ {
+ patTerms.push_back(t.first);
+ }
+}
+
+int PatternTermSelector::isInstanceOf(Node n1,
+ Node n2,
+ const std::vector<Node>& fv1,
+ const std::vector<Node>& fv2)
+{
+ Assert(n1 != n2);
+ int status = 0;
+ std::unordered_set<TNode, TNodeHashFunction> subs_vars;
+ std::unordered_set<
+ std::pair<TNode, TNode>,
+ PairHashFunction<TNode, TNode, TNodeHashFunction, TNodeHashFunction> >
+ visited;
+ std::vector<std::pair<TNode, TNode> > visit;
+ std::pair<TNode, TNode> cur;
+ TNode cur1;
+ TNode cur2;
+ visit.push_back(std::pair<TNode, TNode>(n1, n2));
+ do
+ {
+ cur = visit.back();
+ visit.pop_back();
+ if (visited.find(cur) != visited.end())
+ {
+ continue;
+ }
+ visited.insert(cur);
+ cur1 = cur.first;
+ cur2 = cur.second;
+ Assert(cur1 != cur2);
+ // recurse if they have the same operator
+ if (cur1.hasOperator() && cur2.hasOperator()
+ && cur1.getNumChildren() == cur2.getNumChildren()
+ && cur1.getOperator() == cur2.getOperator()
+ && cur1.getOperator().getKind() != INST_CONSTANT)
+ {
+ visit.push_back(std::pair<TNode, TNode>(cur1, cur2));
+ for (size_t i = 0, size = cur1.getNumChildren(); i < size; i++)
+ {
+ if (cur1[i] != cur2[i])
+ {
+ visit.push_back(std::pair<TNode, TNode>(cur1[i], cur2[i]));
+ }
+ else if (cur1[i].getKind() == INST_CONSTANT)
+ {
+ if (subs_vars.find(cur1[i]) != subs_vars.end())
+ {
+ return 0;
+ }
+ // the variable must map to itself in the substitution
+ subs_vars.insert(cur1[i]);
+ }
+ }
+ continue;
+ }
+ bool success = false;
+ // check if we are in a unifiable instance case
+ // must be only this case
+ for (unsigned r = 0; r < 2; r++)
+ {
+ if (status == 0 || ((status == 1) == (r == 0)))
+ {
+ TNode curi = r == 0 ? cur1 : cur2;
+ if (curi.getKind() == INST_CONSTANT
+ && subs_vars.find(curi) == subs_vars.end())
+ {
+ TNode curj = r == 0 ? cur2 : cur1;
+ // RHS must be a simple trigger
+ if (TriggerTermInfo::getTriggerWeight(curj) == 0)
+ {
+ // must occur in the free variables in the other
+ const std::vector<Node>& free_vars = r == 0 ? fv2 : fv1;
+ if (std::find(free_vars.begin(), free_vars.end(), curi)
+ != free_vars.end())
+ {
+ status = r == 0 ? 1 : -1;
+ subs_vars.insert(curi);
+ success = true;
+ break;
+ }
+ }
+ }
+ }
+ }
+ if (!success)
+ {
+ return 0;
+ }
+ } while (!visit.empty());
+ return status;
+}
+
+void PatternTermSelector::filterInstances(std::vector<Node>& nodes)
+{
+ std::map<unsigned, std::vector<Node> > fvs;
+ for (size_t i = 0, size = nodes.size(); i < size; i++)
+ {
+ quantifiers::TermUtil::computeInstConstContains(nodes[i], fvs[i]);
+ }
+ std::vector<bool> active;
+ active.resize(nodes.size(), true);
+ for (size_t i = 0, size = nodes.size(); i < size; i++)
+ {
+ std::vector<Node>& fvsi = fvs[i];
+ if (!active[i])
+ {
+ continue;
+ }
+ for (size_t j = i + 1, size2 = nodes.size(); j < size2; j++)
+ {
+ if (!active[j])
+ {
+ continue;
+ }
+ int result = isInstanceOf(nodes[i], nodes[j], fvsi, fvs[j]);
+ if (result == 1)
+ {
+ Trace("filter-instances")
+ << nodes[j] << " is an instance of " << nodes[i] << std::endl;
+ active[i] = false;
+ break;
+ }
+ else if (result == -1)
+ {
+ Trace("filter-instances")
+ << nodes[i] << " is an instance of " << nodes[j] << std::endl;
+ active[j] = false;
+ }
+ }
+ }
+ std::vector<Node> temp;
+ for (size_t i = 0, nsize = nodes.size(); i < nsize; i++)
+ {
+ if (active[i])
+ {
+ temp.push_back(nodes[i]);
+ }
+ }
+ nodes.clear();
+ nodes.insert(nodes.begin(), temp.begin(), temp.end());
+}
+
+Node PatternTermSelector::getInversionVariable(Node n)
+{
+ Kind nk = n.getKind();
+ if (nk == INST_CONSTANT)
+ {
+ return n;
+ }
+ else if (nk == PLUS || nk == MULT)
+ {
+ Node ret;
+ for (const Node& nc : n)
+ {
+ if (quantifiers::TermUtil::hasInstConstAttr(nc))
+ {
+ if (ret.isNull())
+ {
+ ret = getInversionVariable(nc);
+ if (ret.isNull())
+ {
+ Trace("var-trigger-debug")
+ << "No : multiple variables " << n << std::endl;
+ return Node::null();
+ }
+ }
+ else
+ {
+ return Node::null();
+ }
+ }
+ else if (nk == MULT)
+ {
+ if (!nc.isConst())
+ {
+ Trace("var-trigger-debug")
+ << "No : non-linear coefficient " << n << std::endl;
+ return Node::null();
+ }
+ }
+ }
+ return ret;
+ }
+ Trace("var-trigger-debug")
+ << "No : unsupported operator " << n << "." << std::endl;
+ return Node::null();
+}
+
+Node PatternTermSelector::getInversion(Node n, Node x)
+{
+ Kind nk = n.getKind();
+ if (nk == INST_CONSTANT)
+ {
+ return x;
+ }
+ else if (nk == PLUS || nk == MULT)
+ {
+ NodeManager* nm = NodeManager::currentNM();
+ int cindex = -1;
+ bool cindexSet = false;
+ for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
+ {
+ Node nc = n[i];
+ if (!quantifiers::TermUtil::hasInstConstAttr(nc))
+ {
+ if (nk == PLUS)
+ {
+ x = nm->mkNode(MINUS, x, nc);
+ }
+ else if (nk == MULT)
+ {
+ Assert(nc.isConst());
+ if (x.getType().isInteger())
+ {
+ Node coeff = nm->mkConst(nc.getConst<Rational>().abs());
+ if (!nc.getConst<Rational>().abs().isOne())
+ {
+ x = nm->mkNode(INTS_DIVISION_TOTAL, x, coeff);
+ }
+ if (nc.getConst<Rational>().sgn() < 0)
+ {
+ x = nm->mkNode(UMINUS, x);
+ }
+ }
+ else
+ {
+ Node coeff = nm->mkConst(Rational(1) / nc.getConst<Rational>());
+ x = nm->mkNode(MULT, x, coeff);
+ }
+ }
+ x = Rewriter::rewrite(x);
+ }
+ else
+ {
+ Assert(!cindexSet);
+ cindex = i;
+ cindexSet = true;
+ }
+ }
+ if (cindexSet)
+ {
+ return getInversion(n[cindex], x);
+ }
+ }
+ return Node::null();
+}
+
+void PatternTermSelector::getTriggerVariables(Node n,
+ Node q,
+ std::vector<Node>& tvars)
+{
+ PatternTermSelector pts(q, options::TriggerSelMode::ALL);
+ std::vector<Node> patTerms;
+ std::map<Node, TriggerTermInfo> tinfo;
+ // collect all patterns from n
+ pts.collect(n, patTerms, tinfo);
+ // collect all variables from all patterns in patTerms, add to tvars
+ for (const Node& pat : patTerms)
+ {
+ quantifiers::TermUtil::computeInstConstContainsForQuant(q, pat, tvars);
+ }
+}
+
+} // namespace inst
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file pattern_term_selector.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Mathias Preiner, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 pattern term selector class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__PATTERN_TERM_SELECTOR_H
+#define CVC4__THEORY__QUANTIFIERS__PATTERN_TERM_SELECTOR_H
+
+#include <map>
+
+#include "expr/node.h"
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/ematching/trigger_term_info.h"
+
+namespace CVC4 {
+namespace theory {
+namespace inst {
+
+/**
+ * Pattern term selector, which is responsible for constructing a pool of terms,
+ * generally based on the body of a quantified formula, which is then used for
+ * selecting triggers.
+ */
+class PatternTermSelector
+{
+ public:
+ /**
+ * @param q The quantified formula we are selecting pattern terms for
+ * @param tstrt the selection strategy (see options/quantifiers_mode.h),
+ * @param exc The set of terms we are excluding as pattern terms.
+ * @param filterInst when true, we discard terms that have instances
+ * in the pattern terms we are return, e.g. we do not return f(x) if we are
+ * also returning f(f(x)). This is default true since it helps in practice
+ * to filter trigger instances.
+ */
+ PatternTermSelector(Node q,
+ options::TriggerSelMode tstrt,
+ const std::vector<Node>& exc = {},
+ bool filterInst = true);
+ ~PatternTermSelector();
+ /** collect pattern terms
+ *
+ * This collects all terms that are eligible for triggers for the quantified
+ * formula of this class in term n and adds them to patTerms.
+ *
+ * @param n The node to collect pattern terms from
+ * @param patTerm The vector to add pattern terms to
+ * @param tinfo stores the result of the collection, mapping terms to the
+ * information they are associated with.
+ */
+ void collect(Node n,
+ std::vector<Node>& patTerms,
+ std::map<Node, TriggerTermInfo>& tinfo);
+ /** 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);
+ /** get the variable associated with an inversion for n
+ *
+ * A term n with an inversion variable x has the following property :
+ * There exists a closed function f such that for all terms t
+ * |= (n = t) <=> (x = f(t))
+ * For example, getInversionVariable( x+1 ) returns x since for all terms t,
+ * |= x+1 = t <=> x = (\y. y-1)(t)
+ * We call f the inversion function for n.
+ */
+ static Node getInversionVariable(Node n);
+ /** Get the body of the inversion function for n whose argument is y.
+ * e.g. getInversion( x+1, y ) returns y-1
+ */
+ static Node getInversion(Node n, Node y);
+
+ /**
+ * get all variables that E-matching can instantiate from a subterm n in
+ * quantified formula q.
+ *
+ * This returns the union of all free variables in usable triggers that are
+ * subterms of n.
+ */
+ static void getTriggerVariables(Node n, Node q, std::vector<Node>& tvars);
+
+ protected:
+ /** 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);
+ /** 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 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);
+ /** Helper for collect, with a fixed strategy for selection and filtering */
+ void collectInternal(Node n,
+ std::vector<Node>& patTerms,
+ std::map<Node, TriggerTermInfo>& tinfo,
+ options::TriggerSelMode tstrt,
+ bool filterInst);
+ /** recursive helper function for collectPatTerms
+ *
+ * This collects the usable trigger terms in the subterm n of the body of
+ * quantified formula of this class.
+ * @param visited cache of the trigger terms collected for each visited node,
+ * @param tinfo cache of trigger term info for each visited node,
+ * @param tstrat the selection strategy (see options/quantifiers_mode.h)
+ * @param pol/hasPol the polarity of node n in q (see QuantPhaseReq
+ * theory/quantifiers/quant_util.h)
+ * @param epol/hasEPol the entailed polarity of node n in q (see
+ * QuantPhaseReq theory/quantifiers/quant_util.h)
+ * @param knowIsUsable whether we know that n is a usable trigger.
+ *
+ * We add the triggers we collected recursively in n into added.
+ */
+ void collectTermsInternal(Node n,
+ std::map<Node, std::vector<Node> >& visited,
+ std::map<Node, TriggerTermInfo>& tinfo,
+ options::TriggerSelMode tstrt,
+ std::vector<Node>& added,
+ bool pol,
+ bool hasPol,
+ bool epol,
+ bool hasEPol,
+ bool knowIsUsable = false);
+
+ /** filter all nodes that have instances
+ *
+ * This is used during collectModelInfo to filter certain trigger terms,
+ * stored in nodes. This updates nodes so that no pairs of distinct nodes
+ * (i,j) is such that i is a trigger instance of j or vice versa (see below).
+ */
+ static void filterInstances(std::vector<Node>& nodes);
+
+ /** is instance of
+ *
+ * We say a term t is an trigger instance of term s if
+ * (1) t = s * { x1 -> t1 ... xn -> tn }
+ * (2) { x1, ..., xn } are a subset of FV( t ).
+ * For example, f( g( h( x, x ) ) ) and f( g( x ) ) are instances of f( x ),
+ * but f( g( y ) ) and g( x ) are not instances of f( x ).
+ *
+ * When this method returns -1, n1 is an instance of n2,
+ * When this method returns 1, n1 is an instance of n2.
+ *
+ * The motivation for this method is to discard triggers s that are less
+ * restrictive (criteria (1)) and serve to bind the same variables (criteria
+ * (2)) as another trigger t. This often helps avoiding matching loops.
+ *
+ * Notice that n1 and n2 are in instantiation constant form.
+ */
+ static int isInstanceOf(Node n1,
+ Node n2,
+ const std::vector<Node>& fv1,
+ const std::vector<Node>& fv2);
+ /** The quantified formula this trigger is for. */
+ Node d_quant;
+ /** The trigger selection strategy */
+ options::TriggerSelMode d_tstrt;
+ /** The set of terms to exclude */
+ std::vector<Node> d_excluded;
+ /** Whether we are filtering instances */
+ bool d_filterInst;
+};
+
+} // namespace inst
+} // namespace theory
+} // namespace CVC4
+
+#endif
#include "theory/quantifiers/ematching/trigger.h"
-#include "expr/node_algorithm.h"
#include "expr/skolem_manager.h"
-#include "theory/arith/arith_msum.h"
#include "theory/quantifiers/ematching/candidate_generator.h"
#include "theory/quantifiers/ematching/ho_trigger.h"
#include "theory/quantifiers/ematching/inst_match_generator.h"
#include "theory/quantifiers/ematching/inst_match_generator_multi.h"
#include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h"
#include "theory/quantifiers/ematching/inst_match_generator_simple.h"
+#include "theory/quantifiers/ematching/pattern_term_selector.h"
#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
-#include "theory/theory_engine.h"
-#include "theory/uf/equality_engine.h"
-#include "util/hash.h"
-using namespace std;
using namespace CVC4::kind;
-using namespace CVC4::context;
namespace CVC4 {
namespace theory {
namespace inst {
-void TriggerTermInfo::init( Node q, Node n, int reqPol, Node reqPolEq ){
- if( d_fv.empty() ){
- quantifiers::TermUtil::computeInstConstContainsForQuant(q, n, d_fv);
- }
- if( d_reqPol==0 ){
- d_reqPol = reqPol;
- d_reqPolEq = reqPolEq;
- }else{
- //determined a ground (dis)equality must hold or else q is a tautology?
- }
- d_weight = Trigger::getTriggerWeight(n);
-}
-
/** trigger class constructor */
Trigger::Trigger(QuantifiersEngine* qe, Node q, std::vector<Node>& nodes)
: d_quantEngine(qe), d_quant(q)
}
}
if( d_nodes.size()==1 ){
- if( isSimpleTrigger( d_nodes[0] ) ){
+ if (TriggerTermInfo::isSimpleTrigger(d_nodes[0]))
+ {
d_mg = new InstMatchGeneratorSimple(q, d_nodes[0], qe);
++(qe->d_statistics.d_triggers);
}else{
return mkTrigger(qe, f, nodes, keepAll, trOption, useNVars);
}
-bool Trigger::isUsable( Node n, Node q ){
- if (quantifiers::TermUtil::getInstConstAttr(n) != q)
- {
- return true;
- }
- if (isAtomicTrigger(n))
- {
- for (const Node& nc : n)
- {
- if (!isUsable(nc, q))
- {
- return false;
- }
- }
- return true;
- }
- else if (n.getKind() == INST_CONSTANT)
- {
- return true;
- }
- std::map<Node, Node> coeffs;
- if (options::purifyTriggers())
- {
- Node x = getInversionVariable(n);
- if (!x.isNull())
- {
- return true;
- }
- }
- return false;
-}
-
-Node Trigger::getIsUsableEq( Node q, Node n ) {
- Assert(isRelationalTrigger(n));
- for (size_t i = 0; i < 2; i++)
- {
- if( isUsableEqTerms( q, n[i], n[1-i] ) ){
- if( i==1 && n.getKind()==EQUAL && !quantifiers::TermUtil::hasInstConstAttr(n[0]) ){
- return NodeManager::currentNM()->mkNode( n.getKind(), n[1], n[0] );
- }else{
- return n;
- }
- }
- }
- return Node::null();
-}
-
-bool Trigger::isUsableEqTerms( Node q, Node n1, Node n2 ) {
- if( n1.getKind()==INST_CONSTANT ){
- if( options::relationalTriggers() ){
- Node q1 = quantifiers::TermUtil::getInstConstAttr(n1);
- if (q1 != q)
- {
- // x is a variable from another quantified formula, fail
- return false;
- }
- Node q2 = quantifiers::TermUtil::getInstConstAttr(n2);
- if (q2.isNull())
- {
- // x = c
- return true;
- }
- if (n2.getKind() == INST_CONSTANT && q2 == q)
- {
- // x = y
- return true;
- }
- // we dont check x = f(y), which is handled symmetrically below
- // when n1 and n2 are swapped
- }
- }else if( isUsableAtomicTrigger( n1, q ) ){
- if (options::relationalTriggers() && n2.getKind() == INST_CONSTANT
- && quantifiers::TermUtil::getInstConstAttr(n2) == q
- && !expr::hasSubterm(n1, n2))
- {
- // f(x) = y
- return true;
- }
- else if (!quantifiers::TermUtil::hasInstConstAttr(n2))
- {
- // f(x) = c
- return true;
- }
- }
- return false;
-}
-
-Node Trigger::getIsUsableTrigger( Node n, Node q ) {
- bool pol = true;
- Trace("trigger-debug") << "Is " << n << " a usable trigger?" << std::endl;
- if( n.getKind()==NOT ){
- pol = !pol;
- n = n[0];
- }
- NodeManager* nm = NodeManager::currentNM();
- if( n.getKind()==INST_CONSTANT ){
- return pol ? n : nm->mkNode(EQUAL, n, nm->mkConst(true)).notNode();
- }else if( isRelationalTrigger( n ) ){
- Node rtr = getIsUsableEq( q, n );
- if( rtr.isNull() && n[0].getType().isReal() ){
- //try to solve relation
- std::map< Node, Node > m;
- if (ArithMSum::getMonomialSumLit(n, m))
- {
- for( std::map< Node, Node >::iterator it = m.begin(); it!=m.end(); ++it ){
- bool trySolve = false;
- if( !it->first.isNull() ){
- if( it->first.getKind()==INST_CONSTANT ){
- trySolve = options::relationalTriggers();
- }else if( isUsableTrigger( it->first, q ) ){
- trySolve = true;
- }
- }
- if( trySolve ){
- Trace("trigger-debug") << "Try to solve for " << it->first << std::endl;
- Node veq;
- if (ArithMSum::isolate(it->first, m, veq, n.getKind()) != 0)
- {
- rtr = getIsUsableEq( q, veq );
- }
- //either all solves will succeed or all solves will fail
- break;
- }
- }
- }
- }
- if( !rtr.isNull() ){
- Trace("relational-trigger") << "Relational trigger : " << std::endl;
- Trace("relational-trigger") << " " << rtr << " (from " << n << ")" << std::endl;
- Trace("relational-trigger") << " in quantifier " << q << std::endl;
- Node rtr2 = pol ? rtr : rtr.negate();
- Trace("relational-trigger") << " return : " << rtr2 << std::endl;
- return rtr2;
- }
- return Node::null();
- }
- Trace("trigger-debug") << n << " usable : "
- << (quantifiers::TermUtil::getInstConstAttr(n) == q)
- << " " << isAtomicTrigger(n) << " " << isUsable(n, q)
- << std::endl;
- if (isUsableAtomicTrigger(n, q))
- {
- return pol ? n : nm->mkNode(EQUAL, n, nm->mkConst(true)).notNode();
- }
- return Node::null();
-}
-
-bool Trigger::isUsableAtomicTrigger( Node n, Node q ) {
- return quantifiers::TermUtil::getInstConstAttr( n )==q && isAtomicTrigger( n ) && isUsable( n, q );
-}
-
-bool Trigger::isUsableTrigger( Node n, Node q ){
- Node nu = getIsUsableTrigger( n, q );
- return !nu.isNull();
-}
-
-bool Trigger::isAtomicTrigger( Node n ){
- return isAtomicTriggerKind( n.getKind() );
-}
-
-bool Trigger::isAtomicTriggerKind( Kind k ) {
- // we use both APPLY_SELECTOR and APPLY_SELECTOR_TOTAL since this
- // method is used both for trigger selection and for ground term registration,
- // where these two things require those kinds respectively.
- return k == APPLY_UF || k == SELECT || k == STORE || k == APPLY_CONSTRUCTOR
- || k == APPLY_SELECTOR || 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
- || k == STRING_LENGTH || k == SEQ_NTH;
-}
-
-bool Trigger::isRelationalTrigger( Node n ) {
- return isRelationalTriggerKind( n.getKind() );
-}
-
-bool Trigger::isRelationalTriggerKind( Kind k ) {
- return k==EQUAL || k==GEQ;
-}
-
-bool Trigger::isSimpleTrigger( Node n ){
- Node t = n.getKind()==NOT ? n[0] : n;
- if( t.getKind()==EQUAL ){
- if( !quantifiers::TermUtil::hasInstConstAttr( t[1] ) ){
- t = t[0];
- }
- }
- if (!isAtomicTrigger(t))
- {
- return false;
- }
- for (const Node& tc : t)
- {
- if (tc.getKind() != INST_CONSTANT
- && quantifiers::TermUtil::hasInstConstAttr(tc))
- {
- return false;
- }
- }
- if (t.getKind() == HO_APPLY && t[0].getKind() == INST_CONSTANT)
- {
- return false;
- }
- return true;
-}
-
-//store triggers in reqPol, indicating their polarity (if any) they must appear to falsify the quantified formula
-void Trigger::collectPatTerms2(Node q,
- Node n,
- std::map<Node, std::vector<Node> >& visited,
- std::map<Node, TriggerTermInfo>& tinfo,
- options::TriggerSelMode tstrt,
- std::vector<Node>& exclude,
- std::vector<Node>& added,
- bool pol,
- bool hasPol,
- bool epol,
- bool hasEPol,
- bool knowIsUsable)
-{
- std::map< Node, std::vector< Node > >::iterator itv = visited.find( n );
- if (itv != visited.end())
- {
- // already visited
- for (const Node& t : itv->second)
- {
- if (std::find(added.begin(), added.end(), t) == added.end())
- {
- added.push_back(t);
- }
- }
- return;
- }
- visited[n].clear();
- Trace("auto-gen-trigger-debug2")
- << "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol
- << " " << hasEPol << std::endl;
- Kind nk = n.getKind();
- if (nk == FORALL || nk == INST_CONSTANT)
- {
- // do not traverse beneath quantified formulas
- return;
- }
- Node nu;
- bool nu_single = false;
- if (knowIsUsable)
- {
- nu = n;
- }
- else if (nk != NOT
- && std::find(exclude.begin(), exclude.end(), n) == exclude.end())
- {
- nu = getIsUsableTrigger(n, q);
- if (!nu.isNull() && nu != n)
- {
- collectPatTerms2(q,
- nu,
- visited,
- tinfo,
- tstrt,
- exclude,
- added,
- pol,
- hasPol,
- epol,
- hasEPol,
- true);
- // copy to n
- visited[n].insert(visited[n].end(), added.begin(), added.end());
- return;
- }
- }
- if (!nu.isNull())
- {
- Assert(nu == n);
- Assert(nu.getKind() != NOT);
- Trace("auto-gen-trigger-debug2")
- << "...found usable trigger : " << nu << std::endl;
- Node reqEq;
- if (nu.getKind() == EQUAL)
- {
- if (isAtomicTrigger(nu[0])
- && !quantifiers::TermUtil::hasInstConstAttr(nu[1]))
- {
- if (hasPol)
- {
- reqEq = nu[1];
- }
- nu = nu[0];
- }
- }
- Assert(reqEq.isNull() || !quantifiers::TermUtil::hasInstConstAttr(reqEq));
- Assert(isUsableTrigger(nu, q));
- // tinfo.find( nu )==tinfo.end()
- Trace("auto-gen-trigger-debug2")
- << "...add usable trigger : " << nu << std::endl;
- tinfo[nu].init(q, nu, hasEPol ? (epol ? 1 : -1) : 0, reqEq);
- nu_single = tinfo[nu].d_fv.size() == q[0].getNumChildren();
- }
- Node nrec = nu.isNull() ? n : nu;
- std::vector<Node> added2;
- for (size_t i = 0, nrecc = nrec.getNumChildren(); i < nrecc; i++)
- {
- bool newHasPol, newPol;
- bool newHasEPol, newEPol;
- QuantPhaseReq::getPolarity(nrec, i, hasPol, pol, newHasPol, newPol);
- QuantPhaseReq::getEntailPolarity(
- nrec, i, hasEPol, epol, newHasEPol, newEPol);
- collectPatTerms2(q,
- nrec[i],
- visited,
- tinfo,
- tstrt,
- exclude,
- added2,
- newPol,
- newHasPol,
- newEPol,
- newHasEPol);
- }
- // if this is not a usable trigger, don't worry about caching the results,
- // since triggers do not contain non-usable subterms
- if (nu.isNull())
- {
- return;
- }
- bool rm_nu = false;
- for (size_t i = 0, asize = added2.size(); i < asize; i++)
- {
- Trace("auto-gen-trigger-debug2") << "..." << nu << " added child " << i
- << " : " << added2[i] << std::endl;
- Assert(added2[i] != nu);
- // if child was not already removed
- if (tinfo.find(added2[i]) != tinfo.end())
- {
- if (tstrt == options::TriggerSelMode::MAX
- || (tstrt == options::TriggerSelMode::MIN_SINGLE_MAX && !nu_single))
- {
- // discard all subterms
- // do not remove if it has smaller weight
- if (tinfo[nu].d_weight <= tinfo[added2[i]].d_weight)
- {
- Trace("auto-gen-trigger-debug2") << "......remove it." << std::endl;
- visited[added2[i]].clear();
- tinfo.erase(added2[i]);
- }
- }
- else
- {
- if (tinfo[nu].d_fv.size() == tinfo[added2[i]].d_fv.size())
- {
- if (tinfo[nu].d_weight >= tinfo[added2[i]].d_weight)
- {
- // discard if we added a subterm as a trigger with all
- // variables that nu has
- Trace("auto-gen-trigger-debug2")
- << "......subsumes parent " << tinfo[nu].d_weight << " "
- << tinfo[added2[i]].d_weight << "." << std::endl;
- rm_nu = true;
- }
- }
- if (std::find(added.begin(), added.end(), added2[i]) == added.end())
- {
- added.push_back(added2[i]);
- }
- }
- }
- }
- if (rm_nu
- && (tstrt == options::TriggerSelMode::MIN
- || (tstrt == options::TriggerSelMode::MIN_SINGLE_ALL && nu_single)))
- {
- tinfo.erase(nu);
- }
- else
- {
- if (std::find(added.begin(), added.end(), nu) == added.end())
- {
- added.push_back(nu);
- }
- }
- visited[n].insert(visited[n].end(), added.begin(), added.end());
-}
-
-int Trigger::getTriggerWeight( Node n ) {
- if (n.getKind() == APPLY_UF)
- {
- return 0;
- }
- if (isAtomicTrigger(n))
- {
- return 1;
- }
- return 2;
-}
-
-void Trigger::collectPatTerms(Node q,
- Node n,
- std::vector<Node>& patTerms,
- options::TriggerSelMode tstrt,
- std::vector<Node>& exclude,
- std::map<Node, TriggerTermInfo>& tinfo,
- bool filterInst)
-{
- std::map< Node, std::vector< Node > > visited;
- if( filterInst ){
- //immediately do not consider any term t for which another term is an instance of t
- std::vector< Node > patTerms2;
- std::map< Node, TriggerTermInfo > tinfo2;
- collectPatTerms(
- q, n, patTerms2, options::TriggerSelMode::ALL, exclude, tinfo2, false);
- std::vector< Node > temp;
- temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() );
- filterTriggerInstances(temp);
- if (Trace.isOn("trigger-filter-instance"))
- {
- if (temp.size() != patTerms2.size())
- {
- Trace("trigger-filter-instance") << "Filtered an instance: "
- << std::endl;
- Trace("trigger-filter-instance") << "Old: ";
- for (unsigned i = 0; i < patTerms2.size(); i++)
- {
- Trace("trigger-filter-instance") << patTerms2[i] << " ";
- }
- Trace("trigger-filter-instance") << std::endl << "New: ";
- for (unsigned i = 0; i < temp.size(); i++)
- {
- Trace("trigger-filter-instance") << temp[i] << " ";
- }
- Trace("trigger-filter-instance") << std::endl;
- }
- }
- if (tstrt == options::TriggerSelMode::ALL)
- {
- for( unsigned i=0; i<temp.size(); i++ ){
- //copy information
- tinfo[temp[i]].d_fv.insert( tinfo[temp[i]].d_fv.end(), tinfo2[temp[i]].d_fv.begin(), tinfo2[temp[i]].d_fv.end() );
- tinfo[temp[i]].d_reqPol = tinfo2[temp[i]].d_reqPol;
- tinfo[temp[i]].d_reqPolEq = tinfo2[temp[i]].d_reqPolEq;
- patTerms.push_back( temp[i] );
- }
- return;
- }
- else
- {
- //do not consider terms that have instances
- for( unsigned i=0; i<patTerms2.size(); i++ ){
- if( std::find( temp.begin(), temp.end(), patTerms2[i] )==temp.end() ){
- visited[ patTerms2[i] ].clear();
- }
- }
- }
- }
- std::vector< Node > added;
- collectPatTerms2( q, n, visited, tinfo, tstrt, exclude, added, true, true, false, true );
- for (const std::pair<const Node, TriggerTermInfo>& t : tinfo)
- {
- patTerms.push_back(t.first);
- }
-}
-
-int Trigger::isTriggerInstanceOf(Node n1,
- Node n2,
- const std::vector<Node>& fv1,
- const std::vector<Node>& fv2)
-{
- Assert(n1 != n2);
- int status = 0;
- std::unordered_set<TNode, TNodeHashFunction> subs_vars;
- std::unordered_set<std::pair<TNode, TNode>,
- PairHashFunction<TNode,
- TNode,
- TNodeHashFunction,
- TNodeHashFunction> >
- visited;
- std::vector<std::pair<TNode, TNode> > visit;
- std::pair<TNode, TNode> cur;
- TNode cur1;
- TNode cur2;
- visit.push_back(std::pair<TNode, TNode>(n1, n2));
- do
- {
- cur = visit.back();
- visit.pop_back();
- if (visited.find(cur) != visited.end())
- {
- continue;
- }
- visited.insert(cur);
- cur1 = cur.first;
- cur2 = cur.second;
- Assert(cur1 != cur2);
- // recurse if they have the same operator
- if (cur1.hasOperator() && cur2.hasOperator()
- && cur1.getNumChildren() == cur2.getNumChildren()
- && cur1.getOperator() == cur2.getOperator()
- && cur1.getOperator().getKind() != INST_CONSTANT)
- {
- visit.push_back(std::pair<TNode, TNode>(cur1, cur2));
- for (size_t i = 0, size = cur1.getNumChildren(); i < size; i++)
- {
- if (cur1[i] != cur2[i])
- {
- visit.push_back(std::pair<TNode, TNode>(cur1[i], cur2[i]));
- }
- else if (cur1[i].getKind() == INST_CONSTANT)
- {
- if (subs_vars.find(cur1[i]) != subs_vars.end())
- {
- return 0;
- }
- // the variable must map to itself in the substitution
- subs_vars.insert(cur1[i]);
- }
- }
- continue;
- }
- bool success = false;
- // check if we are in a unifiable instance case
- // must be only this case
- for (unsigned r = 0; r < 2; r++)
- {
- if (status == 0 || ((status == 1) == (r == 0)))
- {
- TNode curi = r == 0 ? cur1 : cur2;
- if (curi.getKind() == INST_CONSTANT
- && subs_vars.find(curi) == subs_vars.end())
- {
- TNode curj = r == 0 ? cur2 : cur1;
- // RHS must be a simple trigger
- if (getTriggerWeight(curj) == 0)
- {
- // must occur in the free variables in the other
- const std::vector<Node>& free_vars = r == 0 ? fv2 : fv1;
- if (std::find(free_vars.begin(), free_vars.end(), curi)
- != free_vars.end())
- {
- status = r == 0 ? 1 : -1;
- subs_vars.insert(curi);
- success = true;
- break;
- }
- }
- }
- }
- }
- if (!success)
- {
- return 0;
- }
- } while (!visit.empty());
- return status;
-}
-
-void Trigger::filterTriggerInstances(std::vector<Node>& nodes)
-{
- std::map<unsigned, std::vector<Node> > fvs;
- for (size_t i = 0, size = nodes.size(); i < size; i++)
- {
- quantifiers::TermUtil::computeInstConstContains(nodes[i], fvs[i]);
- }
- std::vector<bool> active;
- active.resize(nodes.size(), true);
- for (size_t i = 0, size = nodes.size(); i < size; i++)
- {
- std::vector<Node>& fvsi = fvs[i];
- if (!active[i])
- {
- continue;
- }
- for (size_t j = i + 1, size2 = nodes.size(); j < size2; j++)
- {
- if (!active[j])
- {
- continue;
- }
- int result = isTriggerInstanceOf(nodes[i], nodes[j], fvsi, fvs[j]);
- if (result == 1)
- {
- Trace("filter-instances")
- << nodes[j] << " is an instance of " << nodes[i] << std::endl;
- active[i] = false;
- break;
- }
- else if (result == -1)
- {
- Trace("filter-instances")
- << nodes[i] << " is an instance of " << nodes[j] << std::endl;
- active[j] = false;
- }
- }
- }
- std::vector<Node> temp;
- for (size_t i = 0, nsize = nodes.size(); i < nsize; i++)
- {
- if (active[i])
- {
- temp.push_back(nodes[i]);
- }
- }
- nodes.clear();
- nodes.insert(nodes.begin(), temp.begin(), temp.end());
-}
-
-Node Trigger::getInversionVariable( Node n ) {
- Kind nk = n.getKind();
- if (nk == INST_CONSTANT)
- {
- return n;
- }
- else if (nk == PLUS || nk == MULT)
- {
- Node ret;
- for (const Node& nc : n)
- {
- if (quantifiers::TermUtil::hasInstConstAttr(nc))
- {
- if( ret.isNull() ){
- ret = getInversionVariable(nc);
- if( ret.isNull() ){
- Trace("var-trigger-debug") << "No : multiple variables " << n << std::endl;
- return Node::null();
- }
- }else{
- return Node::null();
- }
- }
- else if (nk == MULT)
- {
- if (!nc.isConst())
- {
- Trace("var-trigger-debug") << "No : non-linear coefficient " << n << std::endl;
- return Node::null();
- }
- }
- }
- return ret;
- }
- Trace("var-trigger-debug")
- << "No : unsupported operator " << n << "." << std::endl;
- return Node::null();
-}
-
-Node Trigger::getInversion( Node n, Node x ) {
- Kind nk = n.getKind();
- if (nk == INST_CONSTANT)
- {
- return x;
- }
- else if (nk == PLUS || nk == MULT)
- {
- NodeManager* nm = NodeManager::currentNM();
- int cindex = -1;
- bool cindexSet = false;
- for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
- {
- Node nc = n[i];
- if (!quantifiers::TermUtil::hasInstConstAttr(nc))
- {
- if (nk == PLUS)
- {
- x = nm->mkNode(MINUS, x, nc);
- }
- else if (nk == MULT)
- {
- Assert(nc.isConst());
- if( x.getType().isInteger() ){
- Node coeff = nm->mkConst(nc.getConst<Rational>().abs());
- if (!nc.getConst<Rational>().abs().isOne())
- {
- x = nm->mkNode(INTS_DIVISION_TOTAL, x, coeff);
- }
- if (nc.getConst<Rational>().sgn() < 0)
- {
- x = nm->mkNode(UMINUS, x);
- }
- }else{
- Node coeff = nm->mkConst(Rational(1) / nc.getConst<Rational>());
- x = nm->mkNode(MULT, x, coeff);
- }
- }
- x = Rewriter::rewrite( x );
- }else{
- Assert(!cindexSet);
- cindex = i;
- cindexSet = true;
- }
- }
- if (cindexSet)
- {
- return getInversion(n[cindex], x);
- }
- }
- return Node::null();
-}
-
-void Trigger::getTriggerVariables(Node n, Node q, std::vector<Node>& t_vars)
-{
- std::vector< Node > patTerms;
- std::map< Node, TriggerTermInfo > tinfo;
- // collect all patterns from n
- std::vector< Node > exclude;
- collectPatTerms(q, n, patTerms, options::TriggerSelMode::ALL, exclude, tinfo);
- //collect all variables from all patterns in patTerms, add to t_vars
- for (const Node& pat : patTerms)
- {
- quantifiers::TermUtil::computeInstConstContainsForQuant(q, pat, t_vars);
- }
-}
-
int Trigger::getActiveScore() {
return d_mg->getActiveScore( d_quantEngine );
}
class IMGenerator;
class InstMatchGenerator;
-/** Information about a node used in a trigger.
-*
-* This information includes:
-* 1. the free variables of the node, and
-* 2. information about which terms are useful for matching.
-*
-* As an example, consider the trigger
-* { f( x ), g( y ), P( y, z ) }
-* for quantified formula
-* forall xy. ( f( x ) != b => ( P( x, g( y ) ) V P( y, z ) ) )
-*
-* Notice that it is only useful to match f( x ) to f-applications not in the
-* equivalence class of b, and P( y, z ) to P-applications not in the equivalence
-* class of true, as such instances will always be entailed by the ground
-* equalities and disequalities the current context. Entailed instances are
-* typically not helpful, and are discarded in Instantiate::addInstantiation(...)
-* unless the option --no-inst-no-entail is enabled. For more details, see page
-* 10 of "Congruence Closure with Free Variables", Barbosa et al., TACAS 2017.
-*
-* This example is referenced for each of the functions below.
-*/
-class TriggerTermInfo {
- public:
- TriggerTermInfo() : d_reqPol(0), d_weight(0) {}
- ~TriggerTermInfo() {}
- /** The free variables in the node
- *
- * In the trigger term info for f( x ) in the above example, d_fv = { x }
- * In the trigger term info for g( y ) in the above example, d_fv = { y }
- * In the trigger term info for P( y, z ) in the above example, d_fv = { y, z }
- */
- std::vector<Node> d_fv;
- /** Required polarity: 1 for equality, -1 for disequality, 0 for none
- *
- * In the trigger term info for f( x ) in the above example, d_reqPol = -1
- * In the trigger term info for g( y ) in the above example, d_reqPol = 0
- * In the trigger term info for P( y, z ) in the above example, d_reqPol = 1
- */
- int d_reqPol;
- /** Required polarity equal term
- *
- * If d_reqPolEq is not null,
- * if d_reqPol = 1, then this trigger term must be matched to terms in the
- * equivalence class of d_reqPolEq,
- * if d_reqPol = -1, then this trigger term must be matched to terms *not* in
- * the equivalence class of d_reqPolEq.
- *
- * This information is typically chosen by analyzing the entailed equalities
- * and disequalities of quantified formulas.
- * In the trigger term info for f( x ) in the above example, d_reqPolEq = b
- * In the trigger term info for g( y ) in the above example,
- * d_reqPolEq = Node::null()
- * In the trigger term info for P( y, z ) in the above example,
- * d_reqPolEq = false
- */
- Node d_reqPolEq;
- /** the weight of the trigger (see Trigger::getTriggerWeight). */
- int d_weight;
- /** Initialize this information class (can be called more than once).
- * q is the quantified formula that n is a trigger term for
- * n is the trigger term
- * reqPol/reqPolEq are described above
- */
- void init(Node q, Node n, int reqPol = 0, Node reqPolEq = Node::null());
-};
-
/** A collection of nodes representing a trigger.
*
* This class encapsulates all implementations of E-matching in CVC4.
std::vector<Node>& nodes,
size_t nvars,
std::vector<Node>& trNodes);
- /** collect pattern terms
- *
- * This collects all terms that are eligible for triggers for quantified
- * formula q in term n and adds them to patTerms.
- * tstrt : the selection strategy (see options/quantifiers_mode.h),
- * exclude : a set of terms that *cannot* be selected as triggers,
- * tinfo : stores the result of the collection, mapping terms to the
- * information they are associated with,
- * filterInst : flag that when true, we discard terms that have instances
- * in the vector we are returning, e.g. we do not return f( x ) if we are
- * also returning f( f( x ) ). TODO: revisit this (issue #1211)
- */
- static void collectPatTerms(Node q,
- Node n,
- std::vector<Node>& patTerms,
- options::TriggerSelMode tstrt,
- std::vector<Node>& exclude,
- std::map<Node, TriggerTermInfo>& tinfo,
- bool filterInst = false);
-
- /** Is n a usable trigger in quantified formula q?
- *
- * A usable trigger is one that is matchable and contains free variables only
- * from q.
- */
- static bool isUsableTrigger( Node n, Node q );
- /** get is usable trigger
- *
- * Return the associated node of n that is a usable trigger in quantified
- * formula q. This may be different than n in several cases :
- * (1) Polarity information is explicitly converted to equalities, e.g.
- * getIsUsableTrigger( (not (P x )), q ) may return (= (P x) false)
- * (2) Relational triggers are put into solved form, e.g.
- * getIsUsableTrigger( (= (+ x a) 5), q ) may return (= x (- 5 a)).
- */
- static Node getIsUsableTrigger( Node n, Node q );
- /** Is n a usable atomic trigger?
- *
- * A usable atomic trigger is a term that is both a useable trigger and an
- * atomic trigger.
- */
- static bool isUsableAtomicTrigger( Node n, Node q );
- /** is n an atomic trigger?
- *
- * An atomic trigger is one whose kind is an atomic trigger kind.
- */
- static bool isAtomicTrigger( Node n );
- /** Is k an atomic trigger kind?
- *
- * An atomic trigger kind is one for which term indexing/matching is possible.
- */
- static bool isAtomicTriggerKind( Kind k );
- /** is n a relational trigger, e.g. like x >= a ? */
- static bool isRelationalTrigger( Node n );
- /** Is k a relational trigger kind? */
- static bool isRelationalTriggerKind( Kind k );
- /** is n a simple trigger (see inst_match_generator.h)? */
- static bool isSimpleTrigger( Node n );
- /** get trigger weight
- *
- * Intutively, this function classifies how difficult it is to handle the
- * trigger term n, where the smaller the value, the easier.
- *
- * Returns 0 for triggers that are APPLY_UF terms.
- * Returns 1 for other triggers whose kind is atomic.
- * Returns 2 otherwise.
- */
- static int getTriggerWeight( 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 );
- /** Get the body of the inversion function for n whose argument is y.
- * e.g. getInversion( x+1, y ) returns y-1
- */
- static Node getInversion(Node n, Node y);
- /** get all variables that E-matching can instantiate from a subterm n.
- *
- * This returns the union of all free variables in usable triggers that are
- * subterms of n.
- */
- static void getTriggerVariables(Node n, Node f, std::vector<Node>& t_vars);
protected:
/** trigger constructor, intentionally protected (use Trigger::mkTrigger). */
Trigger(QuantifiersEngine* ie, Node q, std::vector<Node>& nodes);
- /** is subterm of trigger usable (helper function for isUsableTrigger) */
- static bool isUsable( Node n, Node q );
- /** returns an equality that is equivalent to the equality eq and
- * is a usable trigger for q if one exists, otherwise returns Node::null().
- */
- static Node getIsUsableEq( Node q, Node eq );
- /** returns whether n1 == n2 is a usable (relational) trigger for q. */
- static bool isUsableEqTerms( Node q, Node n1, Node n2 );
- /** recursive helper function for collectPatTerms
- *
- * This collects the usable trigger terms in the subterm n of the body of
- * quantified formula q.
- * visited : cache of the trigger terms collected for each visited node,
- * tinfo : cache of trigger term info for each visited node,
- * tstrat : the selection strategy (see options/quantifiers_mode.h)
- * exclude : a set of terms that *cannot* be selected as triggers
- * pol/hasPol : the polarity of node n in q
- * (see QuantPhaseReq theory/quantifiers/quant_util.h)
- * epol/hasEPol : the entailed polarity of node n in q
- * (see QuantPhaseReq theory/quantifiers/quant_util.h)
- * knowIsUsable : whether we know that n is a usable trigger.
- *
- * We add the triggers we collected recursively in n into added.
- */
- static void collectPatTerms2(Node q,
- Node n,
- std::map<Node, std::vector<Node> >& visited,
- std::map<Node, TriggerTermInfo>& tinfo,
- options::TriggerSelMode tstrt,
- std::vector<Node>& exclude,
- std::vector<Node>& added,
- bool pol,
- bool hasPol,
- bool epol,
- bool hasEPol,
- bool knowIsUsable = false);
-
- /** filter all nodes that have trigger instances
- *
- * This is used during collectModelInfo to filter certain trigger terms,
- * stored in nodes. This updates nodes so that no pairs of distinct nodes
- * (i,j) is such that i is a trigger instance of j or vice versa (see below).
- */
- static void filterTriggerInstances(std::vector<Node>& nodes);
-
- /** is instance of
- *
- * We say a term t is an trigger instance of term s if
- * (1) t = s * { x1 -> t1 ... xn -> tn }
- * (2) { x1, ..., xn } are a subset of FV( t ).
- * For example, f( g( h( x, x ) ) ) and f( g( x ) ) are instances of f( x ),
- * but f( g( y ) ) and g( x ) are not instances of f( x ).
- *
- * When this method returns -1, n1 is an instance of n2,
- * When this method returns 1, n1 is an instance of n2.
- *
- * The motivation for this method is to discard triggers s that are less
- * restrictive (criteria (1)) and serve to bind the same variables (criteria
- * (2)) as another trigger t. This often helps avoiding matching loops.
- */
- static int isTriggerInstanceOf(Node n1,
- Node n2,
- const std::vector<Node>& fv1,
- const std::vector<Node>& fv2);
-
/** add an instantiation (called by InstMatchGenerator)
*
* This calls Instantiate::addInstantiation(...) for instantiations
--- /dev/null
+/********************* */
+/*! \file trigger_term_info.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Morgan Deters, Mathias Preiner
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of trigger term info class
+ **/
+
+#include "theory/quantifiers/ematching/trigger_term_info.h"
+
+#include "theory/quantifiers/term_util.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace inst {
+
+void TriggerTermInfo::init(Node q, Node n, int reqPol, Node reqPolEq)
+{
+ if (d_fv.empty())
+ {
+ quantifiers::TermUtil::computeInstConstContainsForQuant(q, n, d_fv);
+ }
+ if (d_reqPol == 0)
+ {
+ d_reqPol = reqPol;
+ d_reqPolEq = reqPolEq;
+ }
+ else
+ {
+ // determined a ground (dis)equality must hold or else q is a tautology?
+ }
+ d_weight = getTriggerWeight(n);
+}
+
+bool TriggerTermInfo::isAtomicTrigger(Node n)
+{
+ return isAtomicTriggerKind(n.getKind());
+}
+
+bool TriggerTermInfo::isAtomicTriggerKind(Kind k)
+{
+ // we use both APPLY_SELECTOR and APPLY_SELECTOR_TOTAL since this
+ // method is used both for trigger selection and for ground term registration,
+ // where these two things require those kinds respectively.
+ return k == APPLY_UF || k == SELECT || k == STORE || k == APPLY_CONSTRUCTOR
+ || k == APPLY_SELECTOR || 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
+ || k == STRING_LENGTH || k == SEQ_NTH;
+}
+
+bool TriggerTermInfo::isRelationalTrigger(Node n)
+{
+ return isRelationalTriggerKind(n.getKind());
+}
+
+bool TriggerTermInfo::isRelationalTriggerKind(Kind k)
+{
+ return k == EQUAL || k == GEQ;
+}
+
+bool TriggerTermInfo::isSimpleTrigger(Node n)
+{
+ Node t = n.getKind() == NOT ? n[0] : n;
+ if (t.getKind() == EQUAL)
+ {
+ if (!quantifiers::TermUtil::hasInstConstAttr(t[1]))
+ {
+ t = t[0];
+ }
+ }
+ if (!isAtomicTrigger(t))
+ {
+ return false;
+ }
+ for (const Node& tc : t)
+ {
+ if (tc.getKind() != INST_CONSTANT
+ && quantifiers::TermUtil::hasInstConstAttr(tc))
+ {
+ return false;
+ }
+ }
+ if (t.getKind() == HO_APPLY && t[0].getKind() == INST_CONSTANT)
+ {
+ return false;
+ }
+ return true;
+}
+
+int32_t TriggerTermInfo::getTriggerWeight(Node n)
+{
+ if (n.getKind() == APPLY_UF)
+ {
+ return 0;
+ }
+ if (isAtomicTrigger(n))
+ {
+ return 1;
+ }
+ return 2;
+}
+
+} // namespace inst
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file trigger_term_info.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Mathias Preiner, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief trigger term info class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_TERM_INFO_H
+#define CVC4__THEORY__QUANTIFIERS__TRIGGER_TERM_INFO_H
+
+#include <map>
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace inst {
+
+/** Information about a node used in a trigger.
+ *
+ * This information includes:
+ * 1. the free variables of the node, and
+ * 2. information about which terms are useful for matching.
+ *
+ * As an example, consider the trigger
+ * { f( x ), g( y ), P( y, z ) }
+ * for quantified formula
+ * forall xy. ( f( x ) != b => ( P( x, g( y ) ) V P( y, z ) ) )
+ *
+ * Notice that it is only useful to match f( x ) to f-applications not in the
+ * equivalence class of b, and P( y, z ) to P-applications not in the
+ * equivalence class of true, as such instances will always be entailed by the
+ * ground equalities and disequalities the current context. Entailed instances
+ * are typically not helpful, and are discarded in
+ * Instantiate::addInstantiation(...) unless the option --no-inst-no-entail is
+ * enabled. For more details, see page 10 of "Congruence Closure with Free
+ * Variables", Barbosa et al., TACAS 2017.
+ *
+ * This example is referenced for each of the functions below.
+ */
+class TriggerTermInfo
+{
+ public:
+ TriggerTermInfo() : d_reqPol(0), d_weight(0) {}
+ ~TriggerTermInfo() {}
+ /** The free variables in the node
+ *
+ * In the trigger term info for f( x ) in the above example, d_fv = { x }
+ * In the trigger term info for g( y ) in the above example, d_fv = { y }
+ * In the trigger term info for P( y, z ) in the above example, d_fv = { y, z
+ * }
+ */
+ std::vector<Node> d_fv;
+ /** Required polarity: 1 for equality, -1 for disequality, 0 for none
+ *
+ * In the trigger term info for f( x ) in the above example, d_reqPol = -1
+ * In the trigger term info for g( y ) in the above example, d_reqPol = 0
+ * In the trigger term info for P( y, z ) in the above example, d_reqPol = 1
+ */
+ int d_reqPol;
+ /** Required polarity equal term
+ *
+ * If d_reqPolEq is not null,
+ * if d_reqPol = 1, then this trigger term must be matched to terms in the
+ * equivalence class of d_reqPolEq,
+ * if d_reqPol = -1, then this trigger term must be matched to terms *not*
+ * in the equivalence class of d_reqPolEq.
+ *
+ * This information is typically chosen by analyzing the entailed equalities
+ * and disequalities of quantified formulas.
+ * In the trigger term info for f( x ) in the above example, d_reqPolEq = b
+ * In the trigger term info for g( y ) in the above example,
+ * d_reqPolEq = Node::null()
+ * In the trigger term info for P( y, z ) in the above example,
+ * d_reqPolEq = false
+ */
+ Node d_reqPolEq;
+ /** the weight of the trigger (see getTriggerWeight). */
+ int32_t d_weight;
+ /** Initialize this information class (can be called more than once).
+ * q is the quantified formula that n is a trigger term for
+ * n is the trigger term
+ * reqPol/reqPolEq are described above
+ */
+ void init(Node q, Node n, int reqPol = 0, Node reqPolEq = Node::null());
+ /** 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 n a simple trigger (see inst_match_generator.h)? */
+ static bool isSimpleTrigger(Node n);
+ /** get trigger weight
+ *
+ * Intutively, this function classifies how difficult it is to handle the
+ * trigger term n, where the smaller the value, the easier.
+ *
+ * Returns 0 for triggers that are APPLY_UF terms.
+ * Returns 1 for other triggers whose kind is atomic.
+ * Returns 2 otherwise.
+ */
+ static int32_t getTriggerWeight(Node n);
+};
+
+} // namespace inst
+} // namespace theory
+} // namespace CVC4
+
+#endif
#include "options/quantifiers_options.h"
#include "options/theory_options.h"
#include "smt/smt_statistics_registry.h"
-#include "theory/quantifiers/ematching/trigger.h"
+#include "theory/quantifiers/ematching/trigger_term_info.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quant_util.h"
// n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER;
//TODO : treat APPLY_TESTER as a T-constraint instead of matching (currently leads to overabundance of instantiations)
//return inst::Trigger::isAtomicTriggerKind( n.getKind() ) && ( !options::qcfTConstraint() || n.getKind()!=APPLY_TESTER );
- return inst::Trigger::isAtomicTriggerKind( n.getKind() );
+ return inst::TriggerTermInfo::isAtomicTriggerKind(n.getKind());
}
Node MatchGen::getMatchOperator( QuantConflictFind * p, Node n ) {
#include "options/quantifiers_options.h"
#include "options/theory_options.h"
#include "options/uf_options.h"
-#include "theory/quantifiers/ematching/trigger.h"
+#include "theory/quantifiers/ematching/trigger_term_info.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
Trace("par-op") << "Parametric operator : " << k << ", " << n.getOperator() << ", " << tn << " : " << n << std::endl;
d_par_op_map[op][tn] = n;
return n;
- }else if( inst::Trigger::isAtomicTriggerKind( k ) ){
+ }
+ else if (inst::TriggerTermInfo::isAtomicTriggerKind(k))
+ {
return n.getOperator();
}else{
return Node::null();
Trace("term-db-debug") << "register term : " << n << std::endl;
d_type_map[n.getType()].push_back(n);
// if this is an atomic trigger, consider adding it
- if (inst::Trigger::isAtomicTrigger(n))
+ if (inst::TriggerTermInfo::isAtomicTrigger(n))
{
Trace("term-db") << "register term in db " << n << std::endl;
void TermDb::setHasTerm( Node n ) {
Trace("term-db-debug2") << "hasTerm : " << n << std::endl;
- //if( inst::Trigger::isAtomicTrigger( n ) ){
if( d_has_map.find( n )==d_has_map.end() ){
d_has_map[n] = true;
for( unsigned i=0; i<n.getNumChildren(); i++ ){
projects / cvc5.git / commitdiff