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.

1 files changed, 181 insertions, 72 deletions

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() ){