diff options
Diffstat (limited to 'src/theory/quantifiers/ematching/trigger.h')
| -rw-r--r-- | src/theory/quantifiers/ematching/trigger.h | 476 |
1 files changed, 476 insertions, 0 deletions
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h new file mode 100644 index 000000000..e91a87e58 --- /dev/null +++ b/src/theory/quantifiers/ematching/trigger.h @@ -0,0 +1,476 @@ +/********************* */ +/*! \file trigger.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King, Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief trigger class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__TRIGGER_H +#define __CVC4__THEORY__QUANTIFIERS__TRIGGER_H + +#include <map> + +#include "expr/node.h" +#include "theory/quantifiers/inst_match.h" +#include "options/quantifiers_options.h" + +namespace CVC4 { +namespace theory { + +class QuantifiersEngine; + +namespace inst { + +class IMGenerator; +class InstMatchGenerator; + +/** Information about a node used in a trigger. +* +* This information includes: +* 1. the free variables of the node, and +* 2. information about which terms are useful for matching. +* +* As an example, consider the trigger +* { f( x ), g( y ), P( y, z ) } +* for quantified formula +* forall xy. ( f( x ) != b => ( P( x, g( y ) ) V P( y, z ) ) ) +* +* Notice that it is only useful to match f( x ) to f-applications not in the +* equivalence class of b, and P( y, z ) to P-applications not in the equivalence +* class of true, as such instances will always be entailed by the ground +* equalities and disequalities the current context. Entailed instances are +* typically not helpful, and are discarded in Instantiate::addInstantiation(...) +* unless the option --no-inst-no-entail is enabled. For more details, see page +* 10 of "Congruence Closure with Free Variables", Barbosa et al., TACAS 2017. +* +* This example is referenced for each of the functions below. +*/ +class TriggerTermInfo { + public: + TriggerTermInfo() : d_reqPol(0), d_weight(0) {} + ~TriggerTermInfo() {} + /** The free variables in the node + * + * In the trigger term info for f( x ) in the above example, d_fv = { x } + * In the trigger term info for g( y ) in the above example, d_fv = { y } + * In the trigger term info for P( y, z ) in the above example, d_fv = { y, z } + */ + std::vector<Node> d_fv; + /** Required polarity: 1 for equality, -1 for disequality, 0 for none + * + * In the trigger term info for f( x ) in the above example, d_reqPol = -1 + * In the trigger term info for g( y ) in the above example, d_reqPol = 0 + * In the trigger term info for P( y, z ) in the above example, d_reqPol = 1 + */ + int d_reqPol; + /** Required polarity equal term + * + * If d_reqPolEq is not null, + * if d_reqPol = 1, then this trigger term must be matched to terms in the + * equivalence class of d_reqPolEq, + * if d_reqPol = -1, then this trigger term must be matched to terms *not* in + * the equivalence class of d_reqPolEq. + * + * This information is typically chosen by analyzing the entailed equalities + * and disequalities of quantified formulas. + * In the trigger term info for f( x ) in the above example, d_reqPolEq = b + * In the trigger term info for g( y ) in the above example, + * d_reqPolEq = Node::null() + * In the trigger term info for P( y, z ) in the above example, + * d_reqPolEq = false + */ + Node d_reqPolEq; + /** the weight of the trigger (see Trigger::getTriggerWeight). */ + int d_weight; + /** Initialize this information class (can be called more than once). + * q is the quantified formula that n is a trigger term for + * n is the trigger term + * reqPol/reqPolEq are described above + */ + void init(Node q, Node n, int reqPol = 0, Node reqPolEq = Node::null()); +}; + +/** A collection of nodes representing a trigger. +* +* This class encapsulates all implementations of E-matching in CVC4. +* Its primary use is as a utility of the quantifiers module InstantiationEngine +* (see theory/quantifiers/ematching/instantiation_engine.h) which uses Trigger to make +* appropriate calls to Instantiate::addInstantiation(...) +* (see theory/instantiate.h) for the instantiate utility of the quantifiers +* engine (d_quantEngine) associated with this trigger. These calls +* queue instantiation lemmas to the output channel of TheoryQuantifiers during +* a full effort check. +* +* Concretely, a Trigger* t is used in the following way during a full effort +* check. Assume that t is associated with quantified formula q (see field d_f). +* We call : +* +* // setup initial information +* t->resetInstantiationRound(); +* // will produce instantiations based on matching with all terms +* t->reset( Node::null() ); +* // add all instantiations based on E-matching with this trigger and the +* // current context +* t->addInstantiations(); +* +* This will result in (a set of) calls to +* Instantiate::addInstantiation(q, m1)...Instantiate::addInstantiation(q, mn), +* where m1...mn are InstMatch objects. These calls add the corresponding +* instantiation lemma for (q,mi) on the output channel associated with +* d_quantEngine. +* +* The Trigger class is wrapper around an underlying IMGenerator class, which +* implements various forms of E-matching for its set of nodes (d_nodes), which +* is refered to in the literature as a "trigger". A trigger is a set of terms +* whose free variables are the bound variables of a quantified formula q, +* and that is used to guide instantiations for q (for example, see "Efficient +* E-Matching for SMT Solvers" by de Moura et al). +* +* For example of an instantiation lemma produced by E-matching : +* +* quantified formula : forall x. P( x ) +* trigger : P( x ) +* ground context : ~P( a ) +* +* Then E-matching matches P( x ) and P( a ), resulting in the match { x -> a } +* which is used to generate the instantiation lemma : +* (forall x. P( x )) => P( a ) +* +* Terms that are provided as input to a Trigger class via mkTrigger +* should be in "instantiation constant form", see TermUtil::getInstConstantNode. +* Say we have quantified formula q whose AST is the Node +* (FORALL +* (BOUND_VAR_LIST x) +* (NOT (P x)) +* (INST_PATTERN_LIST (INST_PATTERN (P x)))) +* then TermUtil::getInstConstantNode( q, (P x) ) = (P IC) where +* IC = TermUtil::getInstantiationConstant( q, i ). +* Trigger expects as input (P IC) to represent the Trigger (P x). This form +* ensures that references to bound variables are unique to quantified formulas, +* which is required to ensure the correctness of instantiation lemmas we +* generate. +* +*/ +class Trigger { + friend class IMGenerator; + + public: + virtual ~Trigger(); + /** get the generator associated with this trigger */ + IMGenerator* getGenerator() { return d_mg; } + /** Reset instantiation round. + * + * Called once at beginning of an instantiation round. + */ + void resetInstantiationRound(); + /** Reset the trigger. + * + * eqc is the equivalence class from which to match ground terms. If eqc is + * Node::null(), then we match ground terms from all equivalence classes. + */ + void reset( Node eqc ); + /** add all available instantiations, based on the current context + * + * This function makes the appropriate calls to d_qe->addInstantiation(...) + * based on the current ground terms and equalities in the current context, + * via queries to functions in d_qe. This calls the addInstantiations function + * of the underlying match generator. It can be extended to + * produce instantiations beyond what is produced by the match generator + * (for example, see theory/quantifiers/ematching/ho_trigger.h). + */ + virtual int addInstantiations(); + /** Return whether this is a multi-trigger. */ + bool isMultiTrigger() { return d_nodes.size()>1; } + /** Get instantiation pattern list associated with this trigger. + * + * An instantiation pattern list is the node representation of a trigger, in + * particular, it is the third argument of quantified formulas which have user + * (! ... :pattern) attributes. + */ + Node getInstPattern(); + /* A heuristic value indicating how active this generator is. + * + * This returns the number of ground terms for the match operators in terms + * from d_nodes. This score is only used with the experimental option + * --trigger-active-sel. + */ + int getActiveScore(); + /** print debug information for the trigger */ + void debugPrint(const char* c) + { + Trace(c) << "TRIGGER( "; + for (int i = 0; i < (int)d_nodes.size(); i++) + { + if (i > 0) + { + Trace(c) << ", "; + } + Trace(c) << d_nodes[i]; + } + Trace(c) << " )"; + } + /** mkTrigger method + * + * This makes an instance of a trigger object. + * qe : pointer to the quantifier engine; + * q : the quantified formula we are making a trigger for + * nodes : the nodes comprising the (multi-)trigger + * keepAll: don't remove unneeded patterns; + * trOption : policy for dealing with triggers that already exist + * (see below) + * use_n_vars : number of variables that should be bound by the trigger + * typically, the number of quantified variables in q. + */ + enum{ + TR_MAKE_NEW, //make new trigger even if it already may exist + TR_GET_OLD, //return a previous trigger if it had already been created + TR_RETURN_NULL //return null if a duplicate is found + }; + static Trigger* mkTrigger(QuantifiersEngine* qe, + Node q, + std::vector<Node>& nodes, + bool keepAll = true, + int trOption = TR_MAKE_NEW, + unsigned use_n_vars = 0); + /** single trigger version that calls the above function */ + static Trigger* mkTrigger(QuantifiersEngine* qe, + Node q, + Node n, + bool keepAll = true, + int trOption = TR_MAKE_NEW, + unsigned use_n_vars = 0); + /** make trigger terms + * + * This takes a set of eligible trigger terms and stores a subset of them in + * trNodes, such that : + * (1) the terms in trNodes contain at least n_vars of the quantified + * variables in quantified formula q, and + * (2) the set trNodes is minimal, i.e. removing one term from trNodes + * always violates (1). + */ + static bool mkTriggerTerms(Node q, + std::vector<Node>& nodes, + unsigned n_vars, + std::vector<Node>& trNodes); + /** collect pattern terms + * + * This collects all terms that are eligible for triggers for quantified + * formula q in term n and adds them to patTerms. + * tstrt : the selection strategy (see options/quantifiers_mode.h), + * exclude : a set of terms that *cannot* be selected as triggers, + * tinfo : stores the result of the collection, mapping terms to the + * information they are associated with, + * filterInst : flag that when true, we discard terms that have instances + * in the vector we are returning, e.g. we do not return f( x ) if we are + * also returning f( f( x ) ). TODO: revisit this (issue #1211) + */ + static void collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt, + std::vector< Node >& exclude, std::map< Node, TriggerTermInfo >& tinfo, + bool filterInst = false ); + + /** Is n a usable trigger in quantified formula q? + * + * A usable trigger is one that is matchable and contains free variables only + * from q. + */ + static bool isUsableTrigger( Node n, Node q ); + /** get is usable trigger + * + * Return the associated node of n that is a usable trigger in quantified + * formula q. This may be different than n in several cases : + * (1) Polarity information is explicitly converted to equalities, e.g. + * getIsUsableTrigger( (not (P x )), q ) may return (= (P x) false) + * (2) Relational triggers are put into solved form, e.g. + * getIsUsableTrigger( (= (+ x a) 5), q ) may return (= x (- 5 a)). + */ + static Node getIsUsableTrigger( Node n, Node q ); + /** Is n a usable atomic trigger? + * + * A usable atomic trigger is a term that is both a useable trigger and an + * atomic trigger. + */ + static bool isUsableAtomicTrigger( Node n, Node q ); + /** is n an atomic trigger? + * + * An atomic trigger is one whose kind is an atomic trigger kind. + */ + static bool isAtomicTrigger( Node n ); + /** Is k an atomic trigger kind? + * + * An atomic trigger kind is one for which term indexing/matching is possible. + */ + static bool isAtomicTriggerKind( Kind k ); + /** is n a relational trigger, e.g. like x >= a ? */ + static bool isRelationalTrigger( Node n ); + /** Is k a relational trigger kind? */ + static bool isRelationalTriggerKind( Kind k ); + /** Is k a kind for which counterexample-guided instantiation is possible? + * + * This typically corresponds to kinds that correspond to operators that + * have total interpretations and are a part of the signature of + * satisfaction complete theories (see Reynolds et al., CAV 2015). + */ + static bool isCbqiKind( Kind k ); + /** is n a simple trigger (see inst_match_generator.h)? */ + static bool isSimpleTrigger( Node n ); + /** is n a Boolean term trigger, e.g. ite( x, BV1, BV0 )? */ + static bool isBooleanTermTrigger( Node n ); + /** is n a pure theory trigger, e.g. head( x )? */ + static bool isPureTheoryTrigger( Node n ); + /** get trigger weight + * + * Returns 0 for triggers that are easy to process and 1 otherwise. + * A trigger is easy to process if it is an atomic trigger, or a relational + * trigger of the form x ~ g for ~ \in { =, >=, > }. + */ + static int getTriggerWeight( Node n ); + /** Returns whether n is a trigger term with a local theory extension + * property from Bansal et al., CAV 2015. + */ + static bool isLocalTheoryExt( Node n, std::vector< Node >& vars, + std::vector< Node >& patTerms ); + /** get the variable associated with an inversion for n + * + * A term n with an inversion variable x has the following property : + * There exists a closed function f such that for all terms t + * |= (n = t) <=> (x = f(t)) + * For example, getInversionVariable( x+1 ) returns x since for all terms t, + * |= x+1 = t <=> x = (\y. y-1)(t) + * We call f the inversion function for n. + */ + static Node getInversionVariable( Node n ); + /** Get the body of the inversion function for n whose argument is y. + * e.g. getInversion( x+1, y ) returns y-1 + */ + static Node getInversion(Node n, Node y); + /** get all variables that E-matching can instantiate from a subterm n. + * + * This returns the union of all free variables in usable triggers that are + * subterms of n. + */ + static void getTriggerVariables(Node n, Node f, std::vector<Node>& t_vars); + + protected: + /** trigger constructor, intentionally protected (use Trigger::mkTrigger). */ + Trigger(QuantifiersEngine* ie, Node q, std::vector<Node>& nodes); + /** is subterm of trigger usable (helper function for isUsableTrigger) */ + static bool isUsable( Node n, Node q ); + /** returns an equality that is equivalent to the equality eq and + * is a usable trigger for q if one exists, otherwise returns Node::null(). + */ + static Node getIsUsableEq( Node q, Node eq ); + /** returns whether n1 == n2 is a usable (relational) trigger for q. */ + static bool isUsableEqTerms( Node q, Node n1, Node n2 ); + /** recursive helper function for collectPatTerms + * + * This collects the usable trigger terms in the subterm n of the body of + * quantified formula q. + * visited : cache of the trigger terms collected for each visited node, + * tinfo : cache of trigger term info for each visited node, + * tstrat : the selection strategy (see options/quantifiers_mode.h) + * exclude : a set of terms that *cannot* be selected as triggers + * pol/hasPol : the polarity of node n in q + * (see QuantPhaseReq theory/quantifiers/quant_util.h) + * epol/hasEPol : the entailed polarity of node n in q + * (see QuantPhaseReq theory/quantifiers/quant_util.h) + * knowIsUsable : whether we know that n is a usable trigger. + * + * We add the triggers we collected recursively in n into added. + */ + static void collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Node > >& visited, std::map< Node, TriggerTermInfo >& tinfo, + quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added, + bool pol, bool hasPol, bool epol, bool hasEPol, bool knowIsUsable = false ); + + /** filter all nodes that have trigger instances + * + * This is used during collectModelInfo to filter certain trigger terms, + * stored in nodes. This updates nodes so that no pairs of distinct nodes + * (i,j) is such that i is a trigger instance of j or vice versa (see below). + */ + static void filterTriggerInstances(std::vector<Node>& nodes); + + /** is instance of + * + * We say a term t is an trigger instance of term s if + * (1) t = s * { x1 -> t1 ... xn -> tn } + * (2) { x1, ..., xn } are a subset of FV( t ). + * For example, f( g( h( x, x ) ) ) and f( g( x ) ) are instances of f( x ), + * but f( g( y ) ) and g( x ) are not instances of f( x ). + * + * When this method returns -1, n1 is an instance of n2, + * When this method returns 1, n1 is an instance of n2. + * + * The motivation for this method is to discard triggers s that are less + * restrictive (criteria (1)) and serve to bind the same variables (criteria + * (2)) as another trigger t. This often helps avoiding matching loops. + */ + static int isTriggerInstanceOf(Node n1, + Node n2, + std::vector<Node>& fv1, + std::vector<Node>& fv2); + + /** add an instantiation (called by InstMatchGenerator) + * + * This calls Instantiate::addInstantiation(...) for instantiations + * associated with m. Typically, m is associated with a single instantiation, + * but in some cases (e.g. higher-order) we may modify m before calling + * Instantiate::addInstantiation(...). + */ + virtual bool sendInstantiation(InstMatch& m); + /** The nodes comprising this trigger. */ + std::vector< Node > d_nodes; + /** The quantifiers engine associated with this trigger. */ + QuantifiersEngine* d_quantEngine; + /** The quantified formula this trigger is for. */ + Node d_quant; + /** match generator + * + * This is the back-end utility that implements the underlying matching + * algorithm associated with this trigger. + */ + IMGenerator* d_mg; +}; /* class Trigger */ + +/** A trie of triggers. +* +* This class is used to cache all Trigger objects that are generated in the +* current context. We index Triggers in this data structure based on the +* value of Trigger::d_nodes. When a Trigger is added to this data structure, +* this Trie assumes responsibility for deleting it. +*/ +class TriggerTrie { +public: + TriggerTrie(); + ~TriggerTrie(); + /** get trigger + * This returns a Trigger t that is indexed by nodes, + * or NULL otherwise. + */ + Trigger* getTrigger(std::vector<Node>& nodes); + /** add trigger + * This adds t to the trie, indexed by nodes. + * In typical use cases, nodes is t->d_nodes. + */ + void addTrigger(std::vector<Node>& nodes, Trigger* t); + + private: + /** The trigger at this node in the trie. */ + std::vector<Trigger*> d_tr; + /** The children of this node in the trie. */ + std::map< TNode, TriggerTrie* > d_children; +};/* class inst::Trigger::TriggerTrie */ + +}/* CVC4::theory::inst namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS__TRIGGER_H */ |