Ho quant util (#1119)

Quantifiers utilities for higher-order.

This makes the term indexing mechanisms in Term Database take into account equalities between functions, in which case the term indices for the two functions merges.

Also adds required options and a minor utility for implementing app completion.

4 files changed, 219 insertions, 77 deletions

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 44fbc4ee7..2e765ce6b 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -368,6 +368,16 @@ option quantAntiSkolem --quant-anti-skolem bool :read-write :default false
 option quantEqualityEngine --quant-ee bool :default false
   maintain congrunce closure over universal equalities
  
+### higher-order options
+
+option hoMatching --ho-matching bool :default true
+  do higher-order matching algorithm for triggers with variable operators
+option hoMatchingVarArgPriority --ho-matching-var-priority bool :default true
+  give priority to variable arguments over constant arguments
+
+option hoMergeTermDb --ho-merge-term-db bool :default true
+  merge term indices modulo equality
+
 ### proof options
 
 option trackInstLemmas --track-inst-lemmas bool :read-write :default false
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 18ba08ae2..79fdf8791 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -18,6 +18,7 @@
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "options/datatypes_options.h"
+#include "options/uf_options.h"
 #include "theory/quantifiers/ce_guided_instantiation.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fun_def_engine.h"
@@ -135,7 +136,7 @@ Node TermDb::getMatchOperator( Node n ) {
   Kind k = n.getKind();
   //datatype operators may be parametric, always assume they are
   if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || 
-      k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER || k==SEP_PTO ){
+      k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER || k==SEP_PTO || k==HO_APPLY ){
     //since it is parametric, use a particular one as op
     TypeNode tn = n[0].getType();
     Node op = n.getOperator();
@@ -146,6 +147,7 @@ Node TermDb::getMatchOperator( Node n ) {
         return it->second;
       }
     }
+    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 ) ){
@@ -210,16 +212,27 @@ void TermDb::computeArgReps( TNode n ) {
 }
 
 void TermDb::computeUfEqcTerms( TNode f ) {
+  Assert( f==getOperatorRepresentative( f ) );
   if( d_func_map_eqc_trie.find( f )==d_func_map_eqc_trie.end() ){
     d_func_map_eqc_trie[f].clear();
+    // get the matchable operators in the equivalence class of f
+    std::vector< TNode > ops;
+    ops.push_back( f );
+    if( options::ufHo() ){
+      ops.insert( ops.end(), d_ho_op_rep_slaves[f].begin(), d_ho_op_rep_slaves[f].end() );
+    }
     eq::EqualityEngine * ee = d_quantEngine->getActiveEqualityEngine();
-    for( unsigned i=0; i<d_op_map[f].size(); i++ ){
-      TNode n = d_op_map[f][i];
-      if( hasTermCurrent( n ) ){
-        if( isTermActive( n ) ){
-          computeArgReps( n );
-          TNode r = ee->hasTerm( n ) ? ee->getRepresentative( n ) : n;
-          d_func_map_eqc_trie[f].d_data[r].addTerm( n, d_arg_reps[n] );
+    for( unsigned j=0; j<ops.size(); j++ ){
+      Node ff = ops[j];
+      //Assert( !options::ufHo() || ee->areEqual( ff, f ) );
+      for( unsigned i=0; i<d_op_map[ff].size(); i++ ){
+        TNode n = d_op_map[ff][i];
+        if( hasTermCurrent( n ) ){
+          if( isTermActive( n ) ){
+            computeArgReps( n );
+            TNode r = ee->hasTerm( n ) ? ee->getRepresentative( n ) : n;
+            d_func_map_eqc_trie[f].d_data[r].addTerm( n, d_arg_reps[n] );
+          }
         }
       }
     }
@@ -227,84 +240,126 @@ void TermDb::computeUfEqcTerms( TNode f ) {
 }
 
 void TermDb::computeUfTerms( TNode f ) {
+  Assert( f==getOperatorRepresentative( f ) );
   if( d_op_nonred_count.find( f )==d_op_nonred_count.end() ){
     d_op_nonred_count[ f ] = 0;
-    std::map< Node, std::vector< Node > >::iterator it = d_op_map.find( f );
-    if( it!=d_op_map.end() ){
-      eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
-      Trace("term-db-debug") << "Adding terms for operator " << f << std::endl;
-      unsigned congruentCount = 0;
-      unsigned nonCongruentCount = 0;
-      unsigned alreadyCongruentCount = 0;
-      unsigned relevantCount = 0;
-      for( unsigned i=0; i<it->second.size(); i++ ){
-        Node n = it->second[i];
-        //to be added to term index, term must be relevant, and exist in EE
-        if( hasTermCurrent( n ) && ee->hasTerm( n ) ){
-          relevantCount++;
-          if( isTermActive( n ) ){
-            computeArgReps( n );
-
-            Trace("term-db-debug") << "Adding term " << n << " with arg reps : ";
-            for( unsigned i=0; i<d_arg_reps[n].size(); i++ ){
-              Trace("term-db-debug") << d_arg_reps[n][i] << " ";
-              if( std::find( d_func_map_rel_dom[f][i].begin(), 
-                             d_func_map_rel_dom[f][i].end(), d_arg_reps[n][i] ) == d_func_map_rel_dom[f][i].end() ){
-                d_func_map_rel_dom[f][i].push_back( d_arg_reps[n][i] );
+    // get the matchable operators in the equivalence class of f
+    std::vector< TNode > ops;
+    ops.push_back( f );
+    if( options::ufHo() ){
+      ops.insert( ops.end(), d_ho_op_rep_slaves[f].begin(), d_ho_op_rep_slaves[f].end() );
+    }
+    unsigned congruentCount = 0;
+    unsigned nonCongruentCount = 0;
+    unsigned alreadyCongruentCount = 0;
+    unsigned relevantCount = 0;
+    eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
+    for( unsigned j=0; j<ops.size(); j++ ){
+      Node ff = ops[j];
+      //Assert( !options::ufHo() || ee->areEqual( ff, f ) );
+      std::map< Node, std::vector< Node > >::iterator it = d_op_map.find( ff );
+      if( it!=d_op_map.end() ){
+        Trace("term-db-debug") << "Adding terms for operator " << f << std::endl;
+        for( unsigned i=0; i<it->second.size(); i++ ){
+          Node n = it->second[i];
+          //to be added to term index, term must be relevant, and exist in EE
+          if( hasTermCurrent( n ) && ee->hasTerm( n ) ){
+            relevantCount++;
+            if( isTermActive( n ) ){
+              computeArgReps( n );
+
+              Trace("term-db-debug") << "Adding term " << n << " with arg reps : ";
+              for( unsigned i=0; i<d_arg_reps[n].size(); i++ ){
+                Trace("term-db-debug") << d_arg_reps[n][i] << " ";
+                if( std::find( d_func_map_rel_dom[f][i].begin(), 
+                               d_func_map_rel_dom[f][i].end(), d_arg_reps[n][i] ) == d_func_map_rel_dom[f][i].end() ){
+                  d_func_map_rel_dom[f][i].push_back( d_arg_reps[n][i] );
+                }
               }
-            }
-            Trace("term-db-debug") << std::endl;
-            Trace("term-db-debug") << "  and value : " << ee->getRepresentative( n ) << std::endl;
-            Node at = d_func_map_trie[ f ].addOrGetTerm( n, d_arg_reps[n] );
-            Trace("term-db-debug2") << "...add term returned " << at << std::endl;
-            if( at!=n && ee->areEqual( at, n ) ){
-              setTermInactive( n );
-              Trace("term-db-debug") << n << " is redundant." << std::endl;
-              congruentCount++;
-            }else{
-              if( at!=n && ee->areDisequal( at, n, false ) ){
-                std::vector< Node > lits;
-                lits.push_back( NodeManager::currentNM()->mkNode( EQUAL, at, n ) );
-                for( unsigned i=0; i<at.getNumChildren(); i++ ){
-                  if( at[i]!=n[i] ){
-                    lits.push_back( NodeManager::currentNM()->mkNode( EQUAL, at[i], n[i] ).negate() );
+              Trace("term-db-debug") << std::endl;
+              Trace("term-db-debug") << "  and value : " << ee->getRepresentative( n ) << std::endl;
+              Node at = d_func_map_trie[ f ].addOrGetTerm( n, d_arg_reps[n] );
+              Trace("term-db-debug2") << "...add term returned " << at << std::endl;
+              if( at!=n && ee->areEqual( at, n ) ){
+                setTermInactive( n );
+                Trace("term-db-debug") << n << " is redundant." << std::endl;
+                congruentCount++;
+              }else{
+                if( at!=n && ee->areDisequal( at, n, false ) ){
+                  std::vector< Node > lits;
+                  lits.push_back( NodeManager::currentNM()->mkNode( EQUAL, at, n ) );
+                  bool success = true;
+                  if( options::ufHo() ){
+                    //operators might be disequal
+                    if( ops.size()>1 ){
+                      Node atf = getMatchOperator( at );
+                      Node nf = getMatchOperator( n );
+                      if( atf!=nf ){
+                        if( at.getKind()==APPLY_UF && n.getKind()==APPLY_UF ){
+                          lits.push_back( atf.eqNode( nf ).negate() );
+                        }else{
+                          success = false;
+                          Assert( false );
+                        }
+                      }
+                    }
                   }
-                }
-                Node lem = lits.size()==1 ? lits[0] : NodeManager::currentNM()->mkNode( OR, lits );
-                if( Trace.isOn("term-db-lemma") ){
-                  Trace("term-db-lemma") << "Disequal congruent terms : " << at << " " << n << "!!!!" << std::endl;
-                  if( !d_quantEngine->getTheoryEngine()->needCheck() ){
-                    Trace("term-db-lemma") << "  all theories passed with no lemmas." << std::endl;
-                    // we should be a full effort check, prior to theory combination
+                  if( success ){
+                    for( unsigned k=0; k<at.getNumChildren(); k++ ){
+                      if( at[k]!=n[k] ){
+                        lits.push_back( NodeManager::currentNM()->mkNode( EQUAL, at[k], n[k] ).negate() );
+                      }
+                    }
+                    Node lem = lits.size()==1 ? lits[0] : NodeManager::currentNM()->mkNode( OR, lits );
+                    if( Trace.isOn("term-db-lemma") ){
+                      Trace("term-db-lemma") << "Disequal congruent terms : " << at << " " << n << "!!!!" << std::endl;
+                      if( !d_quantEngine->getTheoryEngine()->needCheck() ){
+                        Trace("term-db-lemma") << "  all theories passed with no lemmas." << std::endl;
+                        // we should be a full effort check, prior to theory combination
+                      }
+                      Trace("term-db-lemma") << "  add lemma : " << lem << std::endl;
+                    }
+                    d_quantEngine->addLemma( lem );
+                    d_quantEngine->setConflict();
+                    d_consistent_ee = false;
+                    return;
                   }
-                  Trace("term-db-lemma") << "  add lemma : " << lem << std::endl;
                 }
-                d_quantEngine->addLemma( lem );
-                d_quantEngine->setConflict();
-                d_consistent_ee = false;
-                return;
+                nonCongruentCount++;
+                d_op_nonred_count[ f ]++;
               }
-              nonCongruentCount++;
-              d_op_nonred_count[ f ]++;
+            }else{
+              Trace("term-db-debug") << n << " is already redundant." << std::endl;
+              alreadyCongruentCount++;
             }
           }else{
-            Trace("term-db-debug") << n << " is already redundant." << std::endl;
-            alreadyCongruentCount++;
+            Trace("term-db-debug") << n << " is not relevant." << std::endl;
           }
-        }else{
-          Trace("term-db-debug") << n << " is not relevant." << std::endl;
         }
-      }
-      if( Trace.isOn("tdb") ){
-        Trace("tdb") << "Term db size [" << f << "] : " << nonCongruentCount << " / ";
-        Trace("tdb") << ( nonCongruentCount + congruentCount ) << " / " << ( nonCongruentCount + congruentCount + alreadyCongruentCount ) << " / ";
-        Trace("tdb") << relevantCount << " / " << it->second.size() << std::endl;
+        if( Trace.isOn("tdb") ){
+          Trace("tdb") << "Term db size [" << f << "] : " << nonCongruentCount << " / ";
+          Trace("tdb") << ( nonCongruentCount + congruentCount ) << " / " << ( nonCongruentCount + congruentCount + alreadyCongruentCount ) << " / ";
+          Trace("tdb") << relevantCount << " / " << it->second.size() << std::endl;
+        }
       }
     }
   }
 }
 
+
+Node TermDb::getOperatorRepresentative( TNode op ) const {
+  std::map< TNode, TNode >::const_iterator it = d_ho_op_rep.find( op );
+  if( it!=d_ho_op_rep.end() ){
+    return it->second;
+  }else{
+    return op;
+  }
+}
+
 bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) {
+  if( options::ufHo() ){
+    f = getOperatorRepresentative( f );
+  }
   computeUfTerms( f );
   Assert( !d_quantEngine->getActiveEqualityEngine()->hasTerm( r ) || 
           d_quantEngine->getActiveEqualityEngine()->getRepresentative( r )==r );
@@ -727,6 +782,37 @@ bool TermDb::reset( Theory::Effort effort ){
     }
   }
 
+  if( options::ufHo() && options::hoMergeTermDb() ){
+    Trace("quant-ho") << "TermDb::reset : compute equal functions..." << std::endl;
+    // build operator representative map
+    d_ho_op_rep.clear();
+    d_ho_op_rep_slaves.clear();
+    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
+    while( !eqcs_i.isFinished() ){
+      TNode r = (*eqcs_i);
+      if( r.getType().isFunction() ){
+        Node first;
+        eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
+        while( !eqc_i.isFinished() ){
+          TNode n = (*eqc_i);
+          if( d_op_map.find( n )!=d_op_map.end() ){
+            if( first.isNull() ){
+              first = n;
+              d_ho_op_rep[n] = n;
+            }else{
+              Trace("quant-ho") << "  have : " << n << " == " << first << ", type = " << n.getType() << std::endl;
+              d_ho_op_rep[n] = first;
+              d_ho_op_rep_slaves[first].push_back( n );
+            }
+          }
+          ++eqc_i;
+        }
+      }
+      ++eqcs_i;
+    }
+    Trace("quant-ho") << "...finished compute equal functions." << std::endl;
+  }
+
 /*
   //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms
   for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
@@ -740,6 +826,9 @@ bool TermDb::reset( Theory::Effort effort ){
 }
 
 TermArgTrie * TermDb::getTermArgTrie( Node f ) {
+  if( options::ufHo() ){
+    f = getOperatorRepresentative( f );
+  }
   computeUfTerms( f );
   std::map< Node, TermArgTrie >::iterator itut = d_func_map_trie.find( f );
   if( itut!=d_func_map_trie.end() ){
@@ -750,6 +839,9 @@ TermArgTrie * TermDb::getTermArgTrie( Node f ) {
 }
 
 TermArgTrie * TermDb::getTermArgTrie( Node eqc, Node f ) {
+  if( options::ufHo() ){
+    f = getOperatorRepresentative( f );
+  }
   computeUfEqcTerms( f );
   std::map< Node, TermArgTrie >::iterator itut = d_func_map_eqc_trie.find( f );
   if( itut==d_func_map_eqc_trie.end() ){
@@ -769,6 +861,9 @@ TermArgTrie * TermDb::getTermArgTrie( Node eqc, Node f ) {
 }
 
 TNode TermDb::getCongruentTerm( Node f, Node n ) {
+  if( options::ufHo() ){
+    f = getOperatorRepresentative( f );
+  }
   computeUfTerms( f );
   std::map< Node, TermArgTrie >::iterator itut = d_func_map_trie.find( f );
   if( itut!=d_func_map_trie.end() ){
@@ -780,6 +875,9 @@ TNode TermDb::getCongruentTerm( Node f, Node n ) {
 }
 
 TNode TermDb::getCongruentTerm( Node f, std::vector< TNode >& args ) {
+  if( options::ufHo() ){
+    f = getOperatorRepresentative( f );
+  }
   computeUfTerms( f );
   return d_func_map_trie[f].existsTerm( args );
 }
@@ -1272,7 +1370,7 @@ bool TermDb::isClosedEnumerableType( TypeNode tn ) {
   if( it==d_typ_closed_enum.end() ){
     d_typ_closed_enum[tn] = true;
     bool ret = true;
-    if( tn.isArray() || tn.isSort() || tn.isCodatatype() ){
+    if( tn.isArray() || tn.isSort() || tn.isCodatatype() || tn.isFunction() ){
       ret = false;
     }else if( tn.isSet() ){
       ret = isClosedEnumerableType( tn.getSetElementType() );
@@ -1290,9 +1388,8 @@ bool TermDb::isClosedEnumerableType( TypeNode tn ) {
           break;
         }
       }
-    }else{
-      //TODO: all subfields must be closed enumerable
     }
+    //TODO: other parametric sorts go here
     d_typ_closed_enum[tn] = ret;
     return ret;
   }else{
@@ -1985,6 +2082,18 @@ void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){
   }
 }
 
+Node TermDb::getHoTypeMatchPredicate( TypeNode tn ) {
+  std::map< TypeNode, Node >::iterator ithp = d_ho_type_match_pred.find( tn );
+  if( ithp==d_ho_type_match_pred.end() ){
+    TypeNode ptn = NodeManager::currentNM()->mkFunctionType( tn, NodeManager::currentNM()->booleanType() );
+    Node k = NodeManager::currentNM()->mkSkolem( "U", ptn, "predicate to force higher-order types" );
+    d_ho_type_match_pred[tn] = k;
+    return k;
+  }else{
+    return ithp->second;  
+  }
+}
+
 bool TermDb::isInductionTerm( Node n ) {
   TypeNode tn = n.getType();
   if( options::dtStcInduction() && tn.isDatatype() ){
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 9df9da957..852d94fde 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -132,6 +132,7 @@ class QuantifiersEngine;
 
 namespace inst{
   class Trigger;
+  class HigherOrderTrigger;
 }
 
 namespace quantifiers {
@@ -188,6 +189,7 @@ class TermDb : public QuantifiersUtil {
   friend class ::CVC4::theory::QuantifiersEngine;
   //TODO: eliminate most of these
   friend class ::CVC4::theory::inst::Trigger;
+  friend class ::CVC4::theory::inst::HigherOrderTrigger;
   friend class ::CVC4::theory::quantifiers::fmcheck::FullModelChecker;
   friend class ::CVC4::theory::quantifiers::QuantConflictFind;
   friend class ::CVC4::theory::quantifiers::RelevantDomain;
@@ -251,6 +253,17 @@ private:
   Node evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy, bool useEntailmentTests );
   TNode getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy );
   bool isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy );
+  /** compute uf eqc terms */
+  void computeUfEqcTerms( TNode f );
+  /** compute uf terms */
+  void computeUfTerms( TNode f );
+private: // for higher-order term indexing
+  /** a map from matchable operators to their representative */
+  std::map< TNode, TNode > d_ho_op_rep;
+  /** for each representative matchable operator, the list of other matchable operators in their equivalence class */
+  std::map< TNode, std::vector< TNode > > d_ho_op_rep_slaves;
+  /** get operator representative */
+  Node getOperatorRepresentative( TNode op ) const;
 public:
   /** ground terms for operator */
   unsigned getNumGroundTerms( Node f );
@@ -272,10 +285,6 @@ public:
   TNode getCongruentTerm( Node f, std::vector< TNode >& args );
   /** compute arg reps */
   void computeArgReps( TNode n );
-  /** compute uf eqc terms */
-  void computeUfEqcTerms( TNode f );
-  /** compute uf terms */
-  void computeUfTerms( TNode f );
   /** in relevant domain */
   bool inRelevantDomain( TNode f, unsigned i, TNode r );
   /** evaluate a term under a substitution.  Return representative in EE if possible.
@@ -520,6 +529,19 @@ public:
   /** is bool connective term */
   static bool isBoolConnectiveTerm( TNode n );
 
+//for higher-order
+private:
+  /** dummy predicate that states terms should be considered first-class members of equality engine */
+  std::map< TypeNode, Node > d_ho_type_match_pred;
+public:
+  /** get higher-order type match predicate
+   * This predicate is used to force certain functions f of type tn to appear as first-class representatives in the
+   * quantifier-free UF solver. For a typical use case, we call getHoTypeMatchPredicate which returns a fresh 
+   * predicate P of type (tn -> Bool). Then, we add P( f ) as a lemma.  
+   * TODO: we may eliminate this depending on how github issue #1115 is resolved.
+   */
+  Node getHoTypeMatchPredicate( TypeNode tn );
+
 //for sygus
 private:
   TermDbSygus * d_sygus_tdb;
diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h
index f3e68b9f9..2ea7e9b72 100644
--- a/src/theory/quantifiers/theory_quantifiers_type_rules.h
+++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h
@@ -86,7 +86,8 @@ struct QuantifierInstPatternTypeRule {
     Assert(n.getKind() == kind::INST_PATTERN );
     if( check ){
       TypeNode tn = n[0].getType(check);
-      if( tn.isFunction() ){
+      // this check catches the common mistake writing :pattern (f x) instead of :pattern ((f x))
+      if( n[0].isVar() && n[0].getKind()!=kind::BOUND_VARIABLE && tn.isFunction() ){
         throw TypeCheckingExceptionPrivate(n[0], "Pattern must be a list of fully-applied terms.");
       }
     }