Fix higher-order term indexing. (#1754)

8 files changed, 469 insertions, 167 deletions

diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index ec0a4039a..0252def60 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -1042,8 +1042,12 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
     TNode t = tat->getNodeData();
     Debug("simple-trigger") << "Actual term is " << t << std::endl;
     //convert to actual used terms
-    for( std::map< int, int >::iterator it = d_var_num.begin(); it != d_var_num.end(); ++it ){
+    for (std::map<unsigned, int>::iterator it = d_var_num.begin();
+         it != d_var_num.end();
+         ++it)
+    {
       if( it->second>=0 ){
+        Assert(it->first < t.getNumChildren());
         Debug("simple-trigger") << "...set " << it->second << " " << t[it->first] << std::endl;
         m.setValue( it->second, t[it->first] );
       }
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h
index cbd5702a0..2e7e3c90c 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator.h
@@ -644,8 +644,11 @@ class InstMatchGeneratorSimple : public IMGenerator {
   std::vector< TypeNode > d_match_pattern_arg_types;
   /** The match operator d_match_pattern (see TermDb::getMatchOperator). */
   Node d_op;
-  /** Map from child number to variable index. */
-  std::map< int, int > d_var_num;
+  /**
+   * Map from child number of d_match_pattern to variable index, or -1 if the
+   * child is not a variable.
+   */
+  std::map<unsigned, int> d_var_num;
   /** add instantiations, helper function.
    *
    * m is the current match we are building,
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 2013bff5d..54c19378a 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -222,49 +222,71 @@ Node TermDb::getMatchOperator( Node n ) {
   }
 }
 
-void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool withinInstClosure ){
+void TermDb::addTerm(Node n,
+                     std::set<Node>& added,
+                     bool withinQuant,
+                     bool withinInstClosure)
+{
   //don't add terms in quantifier bodies
   if( withinQuant && !options::registerQuantBodyTerms() ){
     return;
-  }else{
-    bool rec = false;
-    if( d_processed.find( n )==d_processed.end() ){
-      d_processed.insert(n);
-      if( !TermUtil::hasInstConstAttr(n) ){
-        Trace("term-db-debug") << "register term : " << n << std::endl;
-        d_type_map[ n.getType() ].push_back( n );
-        //if this is an atomic trigger, consider adding it
-        if( inst::Trigger::isAtomicTrigger( n ) ){
-          Trace("term-db") << "register term in db " << n << std::endl;
-
-          Node op = getMatchOperator( n );
-          Trace("term-db-debug") << "  match operator is : " << op << std::endl;
+  }
+  bool rec = false;
+  if (d_processed.find(n) == d_processed.end())
+  {
+    d_processed.insert(n);
+    if (!TermUtil::hasInstConstAttr(n))
+    {
+      Trace("term-db-debug") << "register term : " << n << std::endl;
+      d_type_map[n.getType()].push_back(n);
+      // if this is an atomic trigger, consider adding it
+      if (inst::Trigger::isAtomicTrigger(n))
+      {
+        Trace("term-db") << "register term in db " << n << std::endl;
+
+        Node op = getMatchOperator(n);
+        Trace("term-db-debug") << "  match operator is : " << op << std::endl;
+        if (d_op_map.find(op) == d_op_map.end())
+        {
           d_ops.push_back(op);
-          d_op_map[op].push_back( n );
-          added.insert( n );
         }
-      }else{
-        setTermInactive( n );
+        d_op_map[op].push_back(n);
+        added.insert(n);
+        // If we are higher-order, we may need to register more terms.
+        if (options::ufHo())
+        {
+          addTermHo(n, added, withinQuant, withinInstClosure);
+        }
       }
-      rec = true;
     }
-    if( withinInstClosure && d_iclosure_processed.find( n )==d_iclosure_processed.end() ){
-      d_iclosure_processed.insert( n );
-      rec = true;
+    else
+    {
+      setTermInactive(n);
     }
-    if( rec && n.getKind()!=FORALL ){
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        addTerm( n[i], added, withinQuant, withinInstClosure );
-      }
+    rec = true;
+  }
+  if (withinInstClosure
+      && d_iclosure_processed.find(n) == d_iclosure_processed.end())
+  {
+    d_iclosure_processed.insert(n);
+    rec = true;
+  }
+  if (rec && n.getKind() != FORALL)
+  {
+    for (const Node& nc : n)
+    {
+      addTerm(nc, added, withinQuant, withinInstClosure);
     }
   }
 }
 
 void TermDb::computeArgReps( TNode n ) {
-  if( d_arg_reps.find( n )==d_arg_reps.end() ){
+  if (d_arg_reps.find(n) == d_arg_reps.end())
+  {
     eq::EqualityEngine * ee = d_quantEngine->getActiveEqualityEngine();
-    for( unsigned j=0; j<n.getNumChildren(); j++ ){
-      TNode r = ee->hasTerm( n[j] ) ? ee->getRepresentative( n[j] ) : n[j];
+    for (const TNode& nc : n)
+    {
+      TNode r = ee->hasTerm(nc) ? ee->getRepresentative(nc) : nc;
       d_arg_reps[n].push_back( r );
     }
   }
@@ -272,141 +294,234 @@ 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 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] );
-          }
-        }
+  if (d_func_map_eqc_trie.find(f) != d_func_map_eqc_trie.end())
+  {
+    return;
+  }
+  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_slaves[f].begin(), d_ho_op_slaves[f].end());
+  }
+  eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
+  for (const Node& ff : ops)
+  {
+    for (const TNode& n : d_op_map[ff])
+    {
+      if (hasTermCurrent(n) && 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]);
       }
     }
   }
 }
 
 void TermDb::computeUfTerms( TNode f ) {
+  if (d_op_nonred_count.find(f) != d_op_nonred_count.end())
+  {
+    // already computed
+    return;
+  }
   Assert( f==getOperatorRepresentative( f ) );
-  if( d_op_nonred_count.find( f )==d_op_nonred_count.end() ){
-    d_op_nonred_count[ f ] = 0;
-    // 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() );
-    }
-    Trace("term-db-debug") << "computeUfTerms for " << f << std::endl;
-    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 " << ff << 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] );
-                }
+  d_op_nonred_count[f] = 0;
+  // 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_slaves[f].begin(), d_ho_op_slaves[f].end());
+  }
+  Trace("term-db-debug") << "computeUfTerms for " << f << std::endl;
+  unsigned congruentCount = 0;
+  unsigned nonCongruentCount = 0;
+  unsigned alreadyCongruentCount = 0;
+  unsigned relevantCount = 0;
+  eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
+  NodeManager* nm = NodeManager::currentNM();
+  for (const Node& ff : ops)
+  {
+    std::map<Node, std::vector<Node> >::iterator it = d_op_map.find(ff);
+    if (it == d_op_map.end())
+    {
+      // no terms for this operator
+      continue;
+    }
+    Trace("term-db-debug") << "Adding terms for operator " << ff << std::endl;
+    for (const Node& n : it->second)
+    {
+      // to be added to term index, term must be relevant, and exist in EE
+      if (!hasTermCurrent(n) || !ee->hasTerm(n))
+      {
+        Trace("term-db-debug") << n << " is not relevant." << std::endl;
+        continue;
+      }
+
+      relevantCount++;
+      if (!isTermActive(n))
+      {
+        Trace("term-db-debug") << n << " is already redundant." << std::endl;
+        alreadyCongruentCount++;
+        continue;
+      }
+
+      computeArgReps(n);
+      Trace("term-db-debug") << "Adding term " << n << " with arg reps : ";
+      for (unsigned i = 0, size = d_arg_reps[n].size(); i < 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;
+      Assert(ee->hasTerm(n));
+      Trace("term-db-debug") << "  and value : " << ee->getRepresentative(n)
+                             << std::endl;
+      Node at = d_func_map_trie[f].addOrGetTerm(n, d_arg_reps[n]);
+      Assert(ee->hasTerm(at));
+      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++;
+        continue;
+      }
+      if (ee->areDisequal(at, n, false))
+      {
+        std::vector<Node> lits;
+        lits.push_back(nm->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());
               }
-              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 );
-                        }
-                      }
-                    }
-                  }
-                  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;
-                  }
-                }
-                nonCongruentCount++;
-                d_op_nonred_count[ f ]++;
+              else
+              {
+                success = false;
+                Assert(false);
               }
-            }else{
-              Trace("term-db-debug") << n << " is already redundant." << std::endl;
-              alreadyCongruentCount++;
             }
-          }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 (success)
+        {
+          Assert(at.getNumChildren() == n.getNumChildren());
+          for (unsigned k = 0, size = at.getNumChildren(); k < size; k++)
+          {
+            if (at[k] != n[k])
+            {
+              lits.push_back(nm->mkNode(EQUAL, at[k], n[k]).negate());
+            }
+          }
+          Node lem = lits.size() == 1 ? lits[0] : nm->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;
         }
       }
+      nonCongruentCount++;
+      d_op_nonred_count[f]++;
+    }
+    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;
     }
   }
 }
 
+void TermDb::addTermHo(Node n,
+                       std::set<Node>& added,
+                       bool withinQuant,
+                       bool withinInstClosure)
+{
+  Assert(options::ufHo());
+  if (n.getType().isFunction())
+  {
+    // nothing special to do with functions
+    return;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  Node curr = n;
+  std::vector<Node> args;
+  while (curr.getKind() == HO_APPLY)
+  {
+    args.insert(args.begin(), curr[1]);
+    curr = curr[0];
+    if (!curr.isVar())
+    {
+      // purify the term
+      std::map<Node, Node>::iterator itp = d_ho_fun_op_purify.find(curr);
+      Node psk;
+      if (itp == d_ho_fun_op_purify.end())
+      {
+        psk = nm->mkSkolem("pfun",
+                           curr.getType(),
+                           "purify for function operator term indexing");
+        d_ho_fun_op_purify[curr] = psk;
+        // we do not add it to d_ops since it is an internal operator
+      }
+      else
+      {
+        psk = itp->second;
+      }
+      std::vector<Node> children;
+      children.push_back(psk);
+      children.insert(children.end(), args.begin(), args.end());
+      Node p_n = nm->mkNode(APPLY_UF, children);
+      Trace("term-db") << "register term in db (via purify) " << p_n
+                       << std::endl;
+      // also add this one internally
+      d_op_map[psk].push_back(p_n);
+      // maintain backwards mapping
+      d_ho_purify_to_term[p_n] = n;
+    }
+  }
+  if (!args.empty() && curr.isVar())
+  {
+    // also add standard application version
+    args.insert(args.begin(), curr);
+    Node uf_n = nm->mkNode(APPLY_UF, args);
+    addTerm(uf_n, added, withinQuant, withinInstClosure);
+  }
+}
 
 Node TermDb::getOperatorRepresentative( TNode op ) const {
   std::map< TNode, TNode >::const_iterator it = d_ho_op_rep.find( op );
@@ -799,6 +914,37 @@ bool TermDb::reset( Theory::Effort effort ){
   d_consistent_ee = true;
 
   eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
+
+  Assert(ee->consistent());
+  // if higher-order, add equalities for the purification terms now
+  if (options::ufHo())
+  {
+    Trace("quant-ho")
+        << "TermDb::reset : assert higher-order purify equalities..."
+        << std::endl;
+    for (std::pair<const Node, Node>& pp : d_ho_purify_to_term)
+    {
+      if (ee->hasTerm(pp.second)
+          && (!ee->hasTerm(pp.first) || !ee->areEqual(pp.second, pp.first)))
+      {
+        Node eq;
+        std::map<Node, Node>::iterator itpe = d_ho_purify_to_eq.find(pp.first);
+        if (itpe == d_ho_purify_to_eq.end())
+        {
+          eq = Rewriter::rewrite(pp.first.eqNode(pp.second));
+          d_ho_purify_to_eq[pp.first] = eq;
+        }
+        else
+        {
+          eq = itpe->second;
+        }
+        Trace("quant-ho") << "- assert purify equality : " << eq << std::endl;
+        ee->assertEquality(eq, true, eq);
+        Assert(ee->consistent());
+      }
+    }
+  }
+
   //compute has map
   if( options::termDbMode()==TERM_DB_RELEVANT || options::lteRestrictInstClosure() ){
     d_has_map.clear();
@@ -838,8 +984,8 @@ bool TermDb::reset( Theory::Effort effort ){
     }
   }
   //explicitly add inst closure terms to the equality engine to ensure only EE terms are indexed
-  for( std::unordered_set< Node, NodeHashFunction >::iterator it = d_iclosure_processed.begin(); it !=d_iclosure_processed.end(); ++it ){
-    Node n = *it;
+  for (const Node& n : d_iclosure_processed)
+  {
     if( !ee->hasTerm( n ) ){
       ee->addTerm( n );
     }
@@ -849,31 +995,45 @@ bool TermDb::reset( Theory::Effort effort ){
     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();
+    d_ho_op_slaves.clear();
     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
     while( !eqcs_i.isFinished() ){
       TNode r = (*eqcs_i);
       if( r.getType().isFunction() ){
+        Trace("quant-ho") << "  process function eqc " << r << std::endl;
         Node first;
         eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
         while( !eqc_i.isFinished() ){
           TNode n = (*eqc_i);
+          Node n_use;
           if (n.isVar())
           {
-            if (d_op_map.find(n) != d_op_map.end())
+            n_use = n;
+          }
+          else
+          {
+            // use its purified variable, if it exists
+            std::map<Node, Node>::iterator itp = d_ho_fun_op_purify.find(n);
+            if (itp != d_ho_fun_op_purify.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);
-              }
+              n_use = itp->second;
+            }
+          }
+          Trace("quant-ho") << "  - process " << n_use << ", from " << n
+                            << std::endl;
+          if (!n_use.isNull() && d_op_map.find(n_use) != d_op_map.end())
+          {
+            if (first.isNull())
+            {
+              first = n_use;
+              d_ho_op_rep[n_use] = n_use;
+            }
+            else
+            {
+              Trace("quant-ho") << "  have : " << n_use << " == " << first
+                                << ", type = " << n_use.getType() << std::endl;
+              d_ho_op_rep[n_use] = first;
+              d_ho_op_slaves[first].push_back(n_use);
             }
           }
           ++eqc_i;
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index e440e68e9..3268e79d6 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -385,10 +385,55 @@ class TermDb : public QuantifiersUtil {
   */
   void computeArgReps(TNode n);
   //------------------------------higher-order term indexing
+  /**
+   * Map from non-variable function terms to the operator used to purify it in
+   * this database. For details, see addTermHo.
+   */
+  std::map<Node, Node> d_ho_fun_op_purify;
+  /**
+   * Map from terms to the term that they purified. For details, see addTermHo.
+   */
+  std::map<Node, Node> d_ho_purify_to_term;
+  /**
+   * Map from terms in the domain of the above map to an equality between that
+   * term and its range in the above map.
+   */
+  std::map<Node, Node> d_ho_purify_to_eq;
   /** 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;
+  std::map<TNode, std::vector<TNode> > d_ho_op_slaves;
+  /** add term higher-order
+   *
+   * This registers additional terms corresponding to (possibly multiple)
+   * purifications of a higher-order term n.
+   *
+   * Consider the example:
+   *    g : Int -> Int, f : Int x Int -> Int
+   *    constraints: (@ f 0) = g, (f 0 1) = (@ (@ f 0) 1) = 3
+   *    pattern: (g x)
+   * where @ is HO_APPLY.
+   * We have that (g x){ x -> 1 } is an E-match for (@ (@ f 0) 1).
+   * With the standard registration in addTerm, we construct term indices for
+   *   f, g, @ : Int x Int -> Int, @ : Int -> Int.
+   * However, to match (g x) with (@ (@ f 0) 1), we require that
+   *   [1] -> (@ (@ f 0) 1)
+   * is an entry in the term index of g. To do this, we maintain a term
+   * index for a fresh variable pfun, the purification variable for
+   * (@ f 0). Thus, we register the term (psk 1) in the call to this function
+   * for (@ (@ f 0) 1). This ensures that, when processing the equality
+   * (@ f 0) = g, we merge the term indices of g and pfun. Hence, the entry
+   *   [1] -> (@ (@ f 0) 1)
+   * is added to the term index of g, assuming g is the representative of
+   * the equivalence class of g and pfun.
+   *
+   * Above, we set d_ho_fun_op_purify[(@ f 0)] = pfun, and
+   * d_ho_purify_to_term[(@ (@ f 0) 1)] = (psk 1).
+   */
+  void addTermHo(Node n,
+                 std::set<Node>& added,
+                 bool withinQuant,
+                 bool withinInstClosure);
   /** get operator representative */
   Node getOperatorRepresentative( TNode op ) const;
   //------------------------------end higher-order term indexing
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
index c45dd4833..fe9247ae8 100644
--- a/src/theory/uf/theory_uf_rewriter.h
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -148,7 +148,11 @@ public: //conversion between HO_APPLY AND APPLY_UF
     // cannot construct APPLY_UF if operator is partially applied or is not standard       
     return Node::null();
   }
-  // collects arguments into args, returns operator of a curried HO_APPLY node
+  /**
+   * Given a curried HO_APPLY term n, this method adds its arguments into args
+   * and returns its operator. If the argument opInArgs is true, then we add
+   * its operator to args.
+   */
   static Node decomposeHoApply(TNode n, std::vector<TNode>& args, bool opInArgs = false) {
     TNode curr = n;
     while( curr.getKind() == kind::HO_APPLY ){
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index c5b38dcd8..8f5b9bf4f 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1078,10 +1078,12 @@ REG1_TESTS = \
 	regress1/fmf/with-ind-104-core.smt2 \
 	regress1/gensys_brn001.smt2 \
 	regress1/ho/auth0068.smt2 \
+	regress1/ho/fta0210.smt2 \
 	regress1/ho/fta0409.smt2 \
 	regress1/ho/ho-exponential-model.smt2 \
 	regress1/ho/ho-matching-enum-2.smt2 \
 	regress1/ho/ho-std-fmf.smt2 \
+	regress1/ho/match-middle.smt2 \
 	regress1/hole6.cvc \
 	regress1/ite5.smt2 \
 	regress1/lemmas/clocksynchro_5clocks.main_invar.base.smt \
diff --git a/test/regress/regress1/ho/fta0210.smt2 b/test/regress/regress1/ho/fta0210.smt2
new file mode 100644
index 000000000..9f0a39f25
--- /dev/null
+++ b/test/regress/regress1/ho/fta0210.smt2
@@ -0,0 +1,64 @@
+; COMMAND-LINE: --uf-ho
+; EXPECT: unsat
+(set-logic ALL)
+(declare-sort A$ 0)
+(declare-sort Nat$ 0)
+(declare-sort A_poly$ 0)
+(declare-sort Nat_poly$ 0)
+(declare-sort A_poly_poly$ 0)
+(declare-fun p$ () A_poly$)
+(declare-fun uu$ (A_poly$ (-> A_poly$ A_poly$) A_poly$) A_poly$)
+(declare-fun one$ () Nat$)
+(declare-fun suc$ (Nat$) Nat$)
+(declare-fun uua$ (A_poly$) A_poly$)
+(declare-fun uub$ (A$ (-> A$ A$) A$) A$)
+(declare-fun uuc$ (A$) A$)
+(declare-fun uud$ (Nat$ (-> Nat$ Nat$) Nat$) Nat$)
+(declare-fun uue$ (Nat$) Nat$)
+(declare-fun one$a () Nat_poly$)
+(declare-fun one$b () A$)
+(declare-fun one$c () A_poly$)
+(declare-fun plus$ (A_poly$ A_poly$) A_poly$)
+(declare-fun poly$ (A_poly$ A$) A$)
+(declare-fun zero$ () A_poly$)
+(declare-fun pCons$ (A$ A_poly$) A_poly$)
+(declare-fun plus$a (Nat$ Nat$) Nat$)
+(declare-fun plus$b (A$ A$) A$)
+(declare-fun plus$c (Nat_poly$ Nat_poly$) Nat_poly$)
+(declare-fun poly$a (Nat_poly$ Nat$) Nat$)
+(declare-fun poly$b (A_poly_poly$ A_poly$) A_poly$)
+(declare-fun power$ (A$ Nat$) A$)
+(declare-fun psize$ (A_poly$) Nat$)
+(declare-fun times$ (A_poly$ A_poly$) A_poly$)
+(declare-fun zero$a () Nat$)
+(declare-fun zero$b () A$)
+(declare-fun zero$c () Nat_poly$)
+(declare-fun zero$d () A_poly_poly$)
+(declare-fun pCons$a (Nat$ Nat_poly$) Nat_poly$)
+(declare-fun pCons$b (A_poly$ A_poly_poly$) A_poly_poly$)
+(declare-fun power$a (A_poly$ Nat$) A_poly$)
+(declare-fun power$b (Nat_poly$ Nat$) Nat_poly$)
+(declare-fun power$c (Nat$ Nat$) Nat$)
+(declare-fun psize$a (A_poly_poly$) Nat$)
+(declare-fun times$a (Nat$ Nat$) Nat$)
+(declare-fun times$b (A$ A$) A$)
+(declare-fun times$c (Nat_poly$ Nat_poly$) Nat_poly$)
+(declare-fun times$d (A_poly_poly$ A_poly_poly$) A_poly_poly$)
+(declare-fun uminus$ (A_poly$) A_poly$)
+(declare-fun uminus$a (A$) A$)
+(declare-fun constant$ ((-> A$ A$)) Bool)
+(declare-fun pcompose$ (A_poly$ A_poly$) A_poly$)
+(declare-fun pcompose$a (Nat_poly$ Nat_poly$) Nat_poly$)
+(declare-fun pcompose$b (A_poly_poly$ A_poly_poly$) A_poly_poly$)
+(declare-fun poly_shift$ (Nat$ A_poly$) A_poly$)
+(declare-fun fold_coeffs$ ((-> A_poly$ (-> (-> A_poly$ A_poly$) (-> A_poly$ A_poly$))) A_poly_poly$ (-> A_poly$ A_poly$)) (-> A_poly$ A_poly$))
+(declare-fun poly_cutoff$ (Nat$ A_poly$) A_poly$)
+(declare-fun fold_coeffs$a ((-> A$ (-> (-> A$ A$) (-> A$ A$))) A_poly$ (-> A$ A$)) (-> A$ A$))
+(declare-fun fold_coeffs$b ((-> Nat$ (-> (-> Nat$ Nat$) (-> Nat$ Nat$))) Nat_poly$ (-> Nat$ Nat$)) (-> Nat$ Nat$))
+
+(assert (! (forall ((?v0 A$)) (= (poly$ zero$ ?v0) zero$b)) :named a14))
+(assert (! (forall ((?v0 (-> A$ A$))) (= (constant$ ?v0) (forall ((?v1 A$) (?v2 A$)) (= (?v0 ?v1) (?v0 ?v2))))) :named a69))
+(assert (! (not (constant$ (poly$ zero$))) :named a206))
+
+(check-sat)
+;(get-proof)
diff --git a/test/regress/regress1/ho/match-middle.smt2 b/test/regress/regress1/ho/match-middle.smt2
new file mode 100644
index 000000000..0485f9a6f
--- /dev/null
+++ b/test/regress/regress1/ho/match-middle.smt2
@@ -0,0 +1,20 @@
+; COMMAND-LINE: --uf-ho
+; EXPECT: unsat
+(set-logic UFLIA)
+(set-info :status unsat)
+(declare-fun f (Int Int Int) Int)
+(declare-fun h (Int Int Int) Int)
+(declare-fun g (Int Int) Int)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(declare-fun c () Int)
+(declare-fun d () Int)
+
+(assert (or (= (f a) g) (= (h a) g)))
+
+(assert (= (f a b d) c))
+(assert (= (h a b d) c))
+
+(assert (forall ((x Int) (y Int)) (not (= (g x y) c))))
+
+(check-sat)