Move higher-order matching predicate (#3280)

6 files changed, 34 insertions, 32 deletions

diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index 7598e6fdc..b01d5e1df 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -469,12 +469,12 @@ int HigherOrderTrigger::addHoTypeMatchPredicateLemmas()
   Trace("ho-quant-trigger") << "addHoTypeMatchPredicateLemmas..." << std::endl;
   unsigned numLemmas = 0;
   // this forces expansion of APPLY_UF terms to curried HO_APPLY chains
-  unsigned size = d_quantEngine->getTermDatabase()->getNumOperators();
-  quantifiers::TermUtil* tutil = d_quantEngine->getTermUtil();
+  quantifiers::TermDb* tdb = d_quantEngine->getTermDatabase();
+  unsigned size = tdb->getNumOperators();
   NodeManager* nm = NodeManager::currentNM();
   for (unsigned j = 0; j < size; j++)
   {
-    Node f = d_quantEngine->getTermDatabase()->getOperator(j);
+    Node f = tdb->getOperator(j);
     if (f.isVar())
     {
       TypeNode tn = f.getType();
@@ -497,7 +497,7 @@ int HigherOrderTrigger::addHoTypeMatchPredicateLemmas()
           // if a variable of this type occurs in this trigger
           if (d_ho_var_types.find(stn) != d_ho_var_types.end())
           {
-            Node u = tutil->getHoTypeMatchPredicate(tn);
+            Node u = tdb->getHoTypeMatchPredicate(tn);
             Node au = nm->mkNode(kind::APPLY_UF, u, f);
             if (d_quantEngine->addLemma(au))
             {
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 84147bf6b..9da9c95b6 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1229,6 +1229,20 @@ TNode TermDb::getCongruentTerm( Node f, std::vector< TNode >& args ) {
   return d_func_map_trie[f].existsTerm( args );
 }
 
+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())
+  {
+    return ithp->second;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  TypeNode ptn = nm->mkFunctionType(tn, nm->booleanType());
+  Node k = nm->mkSkolem("U", ptn, "predicate to force higher-order types");
+  d_ho_type_match_pred[tn] = k;
+  return k;
+}
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index f92bce8bd..7caf29d20 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -291,6 +291,14 @@ class TermDb : public QuantifiersUtil {
    * Bansal et al., CAV 2015.
    */
   bool isInstClosure(Node r);
+  /** 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.
+   */
+  Node getHoTypeMatchPredicate(TypeNode tn);
 
  private:
   /** reference to the quantifiers engine */
@@ -328,7 +336,12 @@ class TermDb : public QuantifiersUtil {
   /** has map */
   std::map< Node, bool > d_has_map;
   /** map from reps to a term in eqc in d_has_map */
-  std::map< Node, Node > d_term_elig_eqc;  
+  std::map<Node, Node> d_term_elig_eqc;
+  /**
+   * Dummy predicate that states terms should be considered first-class members
+   * of equality engine (for higher-order).
+   */
+  std::map<TypeNode, Node> d_ho_type_match_pred;
   /** set has term */
   void setHasTerm( Node n );
   /** helper for evaluate term */
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index 48dc88537..6ffc50c97 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -954,19 +954,6 @@ bool TermUtil::hasOffsetArg(Kind ik, int arg, int& offset, Kind& ok)
   return false;
 }
 
-Node TermUtil::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;  
-  }
-}
-
-
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index 99ea483d9..52965d2fa 100644
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -348,19 +348,6 @@ public:
    * minimum and maximum elements, for example tn is Bool or BitVector.
    */
   static Node mkTypeConst(TypeNode tn, bool pol);
-
-  // 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 );
 };/* class TermUtil */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp
index 4d5a879ad..88b2ba8d2 100644
--- a/src/theory/uf/ho_extension.cpp
+++ b/src/theory/uf/ho_extension.cpp
@@ -316,7 +316,8 @@ unsigned HoExtension::checkAppCompletion()
             // add to pending list
             apply_uf[rop].push_back(n);
           }
-          // arguments are also relevant operators  FIXME (github issue #1115)
+          // Arguments are also relevant operators.
+          // It might be possible include fewer terms here, see #1115.
           for (unsigned k = 0; k < n.getNumChildren(); k++)
           {
             if (n[k].getType().isFunction())