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

1 files changed, 347 insertions, 80 deletions

diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index afab98cee..105878df1 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -23,7 +23,6 @@
 #include "theory/quantifiers/inst_match.h"
 #include "options/quantifiers_options.h"
 
-// Forward declarations for defining the Trigger and TriggerTrie.
 namespace CVC4 {
 namespace theory {
 
@@ -33,147 +32,415 @@ namespace inst {
 
 class IMGenerator;
 class InstMatchGenerator;
-}/* CVC4::theory::inst namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-
-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){}
   ~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<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 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<Node>& 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<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);
 
-  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<Trigger*> d_tr;
+  /** The children of this node in the trie. */
   std::map< TNode, TriggerTrie* > d_children;
 };/* class inst::Trigger::TriggerTrie */