Merge branch 'master' into fix1649fix1649

22 files changed, 986 insertions, 533 deletions

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index b98088a71..d778a679e 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -245,6 +245,7 @@ Node ConjectureGenerator::getUniversalRepresentative(TNode n, bool add)
       // now, do instantiation-based merging for each of these terms
       Trace("thm-ee-debug") << "Merge equivalence classes based on instantiations of terms..." << std::endl;
       //merge all pending equalities
+      EntailmentCheck* echeck = d_treg.getEntailmentCheck();
       while( !d_upendingAdds.empty() ){
         Trace("sg-pending") << "Add " << d_upendingAdds.size() << " pending terms..." << std::endl;
         std::vector< Node > pending;
@@ -256,7 +257,7 @@ Node ConjectureGenerator::getUniversalRepresentative(TNode n, bool add)
           Trace("thm-ee-add") << "UEE : Add universal term " << t << std::endl;
           std::vector< Node > eq_terms;
           //if occurs modulo equality at ground level, it is equivalent to representative of ground equality engine
-          Node gt = getTermDatabase()->evaluateTerm(t);
+          Node gt = echeck->evaluateTerm(t);
           if( !gt.isNull() && gt!=t ){
             eq_terms.push_back( gt );
           }
@@ -1362,7 +1363,8 @@ bool ConjectureGenerator::notifySubstitution( TNode glhs, std::map< TNode, TNode
   }
   Trace("sg-cconj-debug") << "Evaluate RHS : : " << rhs << std::endl;
   //get the representative of rhs with substitution subs
-  TNode grhs = getTermDatabase()->getEntailedTerm( rhs, subs, true );
+  EntailmentCheck* echeck = d_treg.getEntailmentCheck();
+  TNode grhs = echeck->getEntailedTerm(rhs, subs, true);
   Trace("sg-cconj-debug") << "...done evaluating term, got : " << grhs << std::endl;
   if( !grhs.isNull() ){
     if( glhs!=grhs ){
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index a8ab760ce..d2b0b0542 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -238,6 +238,7 @@ bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
     d_lchildren.clear();
     d_arg_to_arg_rep.clear();
     d_arg_vector.clear();
+    EntailmentCheck* echeck = d_treg.getEntailmentCheck();
     for (std::pair<const TNode, std::vector<Node> >& ha : ho_var_apps_subs)
     {
       TNode var = ha.first;
@@ -291,8 +292,7 @@ bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
           {
             if (!d_qstate.areEqual(itf->second, args[k]))
             {
-              if (!d_treg.getTermDatabase()->isEntailed(
-                      itf->second.eqNode(args[k]), true))
+              if (!echeck->isEntailed(itf->second.eqNode(args[k]), true))
               {
                 fixed_vals[k] = Node::null();
               }
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index d8e3b7950..075299583 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -23,6 +23,7 @@
 #include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h"
 #include "theory/quantifiers/ematching/inst_match_generator_simple.h"
 #include "theory/quantifiers/ematching/pattern_term_selector.h"
+#include "theory/quantifiers/ematching/relational_match_generator.h"
 #include "theory/quantifiers/ematching/var_match_generator.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_state.h"
@@ -618,7 +619,7 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator(
     InstMatchGenerator* init;
     std::map< Node, InstMatchGenerator * >::iterator iti = pat_map_init.find( pats[pCounter] );
     if( iti==pat_map_init.end() ){
-      init = new InstMatchGenerator(tparent, pats[pCounter]);
+      init = getInstMatchGenerator(tparent, q, pats[pCounter]);
     }else{
       init = iti->second;
     }
@@ -645,6 +646,7 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Trigger* tparent,
                                                               Node q,
                                                               Node n)
 {
+  // maybe variable match generator
   if (n.getKind() != INST_CONSTANT)
   {
     Trace("var-trigger-debug")
@@ -672,6 +674,16 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Trigger* tparent,
       return vmg;
     }
   }
+  Trace("relational-trigger")
+      << "Is " << n << " a relational trigger?" << std::endl;
+  // relational triggers
+  bool hasPol, pol;
+  Node lit;
+  if (TriggerTermInfo::isUsableRelationTrigger(n, hasPol, pol, lit))
+  {
+    Trace("relational-trigger") << "...yes, for literal " << lit << std::endl;
+    return new RelationalMatchGenerator(tparent, lit, hasPol, pol);
+  }
   return new InstMatchGenerator(tparent, n);
 }
 
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 30be83ecc..fdb0d0db3 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -339,20 +339,18 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
                           TriggerDatabase::TR_GET_OLD,
                           d_num_trigger_vars[f]);
     }
-    if (tr == nullptr)
+    // if we generated a trigger above, add it
+    if (tr != nullptr)
     {
-      // did not generate a trigger
-      continue;
-    }
-    addTrigger(tr, f);
-    if (tr->isMultiTrigger())
-    {
-      // only add a single multi-trigger
-      continue;
+      addTrigger(tr, f);
+      if (tr->isMultiTrigger())
+      {
+        // only add a single multi-trigger
+        continue;
+      }
     }
     // if we are generating additional triggers...
-    size_t index = 0;
-    if (index < patTerms.size())
+    if (patTerms.size() > 1)
     {
       // check if similar patterns exist, and if so, add them additionally
       unsigned nqfs_curr = 0;
@@ -361,7 +359,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
         nqfs_curr =
             d_quant_rel->getNumQuantifiersForSymbol(patTerms[0].getOperator());
       }
-      index++;
+      size_t index = 1;
       bool success = true;
       while (success && index < patTerms.size()
              && d_is_single_trigger[patTerms[index]])
@@ -527,16 +525,22 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f)
     Trace("auto-gen-trigger-debug")
         << "...required polarity for " << pat << " is " << rpol
         << ", eq=" << rpoleq << std::endl;
+    // Currently, we have ad-hoc treatment for relational triggers that
+    // are not handled by RelationalMatchGen.
+    bool isAdHocRelationalTrigger =
+        TriggerTermInfo::isRelationalTrigger(pat)
+        && !TriggerTermInfo::isUsableRelationTrigger(pat);
     if (rpol != 0)
     {
       Assert(rpol == 1 || rpol == -1);
-      if (TriggerTermInfo::isRelationalTrigger(pat))
+      if (isAdHocRelationalTrigger)
       {
         pat = rpol == -1 ? pat.negate() : pat;
       }
       else
       {
-        Assert(TriggerTermInfo::isAtomicTrigger(pat));
+        Assert(TriggerTermInfo::isAtomicTrigger(pat)
+               || TriggerTermInfo::isUsableRelationTrigger(pat));
         if (pat.getType().isBoolean() && rpoleq.isNull())
         {
           if (options().quantifiers.literalMatchMode
@@ -575,13 +579,10 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f)
       }
       Trace("auto-gen-trigger-debug") << "...got : " << pat << std::endl;
     }
-    else
+    else if (isAdHocRelationalTrigger)
     {
-      if (TriggerTermInfo::isRelationalTrigger(pat))
-      {
-        // consider both polarities
-        addPatternToPool(f, pat.negate(), num_fv, mpat);
-      }
+      // consider both polarities
+      addPatternToPool(f, pat.negate(), num_fv, mpat);
     }
     addPatternToPool(f, pat, num_fv, mpat);
   }
diff --git a/src/theory/quantifiers/ematching/relational_match_generator.cpp b/src/theory/quantifiers/ematching/relational_match_generator.cpp
new file mode 100644
index 000000000..8981a7a2d
--- /dev/null
+++ b/src/theory/quantifiers/ematching/relational_match_generator.cpp
@@ -0,0 +1,125 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Relational match generator class.
+ */
+
+#include "theory/quantifiers/ematching/relational_match_generator.h"
+
+#include "theory/quantifiers/term_util.h"
+#include "util/rational.h"
+
+using namespace cvc5::kind;
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+namespace inst {
+
+RelationalMatchGenerator::RelationalMatchGenerator(Trigger* tparent,
+                                                   Node rtrigger,
+                                                   bool hasPol,
+                                                   bool pol)
+    : InstMatchGenerator(tparent, Node::null()),
+      d_vindex(-1),
+      d_hasPol(hasPol),
+      d_pol(pol),
+      d_counter(0)
+{
+  Assert((rtrigger.getKind() == EQUAL && rtrigger[0].getType().isReal())
+         || rtrigger.getKind() == GEQ);
+  Trace("relational-match-gen")
+      << "Relational trigger: " << rtrigger << ", hasPol/pol = " << hasPol
+      << "/" << pol << std::endl;
+  for (size_t i = 0; i < 2; i++)
+  {
+    if (rtrigger[i].getKind() == INST_CONSTANT)
+    {
+      d_var = rtrigger[i];
+      d_vindex = d_var.getAttribute(InstVarNumAttribute());
+      d_rhs = rtrigger[1 - i];
+      Assert(!quantifiers::TermUtil::hasInstConstAttr(d_rhs));
+      Kind k = rtrigger.getKind();
+      d_rel = (i == 0 ? k : (k == GEQ ? LEQ : k));
+      break;
+    }
+  }
+  Trace("relational-match-gen") << "...processed " << d_var << " (" << d_vindex
+                                << ") " << d_rel << " " << d_rhs << std::endl;
+  AlwaysAssert(!d_var.isNull())
+      << "Failed to initialize RelationalMatchGenerator";
+}
+
+bool RelationalMatchGenerator::reset(Node eqc)
+{
+  d_counter = 0;
+  return true;
+}
+
+int RelationalMatchGenerator::getNextMatch(Node q, InstMatch& m)
+{
+  Trace("relational-match-gen") << "getNextMatch, rel match gen" << std::endl;
+  // try (up to) two different terms
+  Node s;
+  Node rhs = d_rhs;
+  bool rmPrev = m.get(d_vindex).isNull();
+  while (d_counter < 2)
+  {
+    bool checkPol = false;
+    if (d_counter == 0)
+    {
+      checkPol = d_pol;
+    }
+    else
+    {
+      Assert(d_counter == 1);
+      if (d_hasPol)
+      {
+        break;
+      }
+      // try the opposite polarity
+      checkPol = !d_pol;
+    }
+    NodeManager* nm = NodeManager::currentNM();
+    // falsify ( d_var <d_rel> d_rhs ) = checkPol
+    s = rhs;
+    if (!checkPol)
+    {
+      s = nm->mkNode(PLUS, s, nm->mkConst(Rational(d_rel == GEQ ? -1 : 1)));
+    }
+    d_counter++;
+    Trace("relational-match-gen")
+        << "...try set " << s << " for " << checkPol << std::endl;
+    if (m.set(d_qstate, d_vindex, s))
+    {
+      Trace("relational-match-gen") << "...success" << std::endl;
+      int ret = continueNextMatch(q, m, InferenceId::UNKNOWN);
+      if (ret > 0)
+      {
+        Trace("relational-match-gen") << "...returned " << ret << std::endl;
+        return ret;
+      }
+      Trace("relational-match-gen") << "...failed to gen inst" << std::endl;
+      // failed
+      if (rmPrev)
+      {
+        m.d_vals[d_vindex] = Node::null();
+      }
+    }
+  }
+  return -1;
+}
+
+}  // namespace inst
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/ematching/relational_match_generator.h b/src/theory/quantifiers/ematching/relational_match_generator.h
new file mode 100644
index 000000000..eead2876a
--- /dev/null
+++ b/src/theory/quantifiers/ematching/relational_match_generator.h
@@ -0,0 +1,92 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Relational match generator class.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__QUANTIFIERS__RELATIONAL_MATCH_GENERATOR_H
+#define CVC5__THEORY__QUANTIFIERS__RELATIONAL_MATCH_GENERATOR_H
+
+#include "expr/node.h"
+#include "theory/quantifiers/ematching/inst_match_generator.h"
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+namespace inst {
+
+/**
+ * Match generator for relational triggers x ~ t where t is a ground term.
+ * This match generator tries a small fixed set of terms based on the kind of
+ * relation and the required polarity of the trigger in the quantified formula.
+ *
+ * For example, for quantified formula (forall ((x Int)) (=> (> x n) (P x))),
+ * we have that (> x n) is a relational trigger with required polarity "true".
+ * This generator will try the match `x -> n+1` only, where notice that n+1 is
+ * the canonical term chosen to satisfy x>n. Canonical terms for arithmetic
+ * relations (~ x n) are in set { n, n+1, n-1 }.
+ *
+ * If a relational trigger does not have a required polarity, then up to 2
+ * terms are tried, a term that satisfies the relation, and one that does not.
+ * If (>= x n) is a relational trigger with no polarity, then `x -> n` and
+ * `x -> n-1` will be generated.
+ *
+ * Currently this class handles only equality between real or integer valued
+ * terms, or inequalities (kind GEQ). It furthermore only considers ground terms
+ * t for the right hand side of relations.
+ */
+class RelationalMatchGenerator : public InstMatchGenerator
+{
+ public:
+  /**
+   * @param tparent The parent trigger that this match generator belongs to
+   * @param rtrigger The relational trigger
+   * @param hasPol Whether the trigger has an entailed polarity
+   * @param pol The entailed polarity of the relational trigger.
+   */
+  RelationalMatchGenerator(Trigger* tparent,
+                           Node rtrigger,
+                           bool hasPol,
+                           bool pol);
+
+  /** Reset */
+  bool reset(Node eqc) override;
+  /** Get the next match. */
+  int getNextMatch(Node q, InstMatch& m) override;
+
+ private:
+  /** the variable */
+  Node d_var;
+  /** The index of the variable */
+  int64_t d_vindex;
+  /** the relation kind */
+  Kind d_rel;
+  /** the right hand side */
+  Node d_rhs;
+  /** whether we have a required polarity */
+  bool d_hasPol;
+  /** the required polarity, if it exists */
+  bool d_pol;
+  /**
+   * The current number of terms we have generated since the last call to reset
+   */
+  size_t d_counter;
+};
+
+}  // namespace inst
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5
+
+#endif
diff --git a/src/theory/quantifiers/ematching/trigger_term_info.cpp b/src/theory/quantifiers/ematching/trigger_term_info.cpp
index 600797f4e..f31ec088a 100644
--- a/src/theory/quantifiers/ematching/trigger_term_info.cpp
+++ b/src/theory/quantifiers/ematching/trigger_term_info.cpp
@@ -70,6 +70,46 @@ bool TriggerTermInfo::isRelationalTriggerKind(Kind k)
   return k == EQUAL || k == GEQ;
 }
 
+bool TriggerTermInfo::isUsableRelationTrigger(Node n)
+{
+  bool hasPol, pol;
+  Node lit;
+  return isUsableRelationTrigger(n, hasPol, pol, lit);
+}
+bool TriggerTermInfo::isUsableRelationTrigger(Node n,
+                                              bool& hasPol,
+                                              bool& pol,
+                                              Node& lit)
+{
+  // relational triggers (not) (= (~ x t) true|false), where ~ in { =, >= }.
+  hasPol = false;
+  pol = n.getKind() != NOT;
+  lit = pol ? n : n[0];
+  if (lit.getKind() == EQUAL && lit[1].getType().isBoolean()
+      && lit[1].isConst())
+  {
+    hasPol = true;
+    pol = lit[1].getConst<bool>() ? pol : !pol;
+    lit = lit[0];
+  }
+  // is it a relational trigger?
+  if ((lit.getKind() == EQUAL && lit[0].getType().isReal())
+      || lit.getKind() == GEQ)
+  {
+    // if one side of the relation is a variable and the other side is a ground
+    // term, we can treat this using the relational match generator
+    for (size_t i = 0; i < 2; i++)
+    {
+      if (lit[i].getKind() == INST_CONSTANT
+          && !quantifiers::TermUtil::hasInstConstAttr(lit[1 - i]))
+      {
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
 bool TriggerTermInfo::isSimpleTrigger(Node n)
 {
   Node t = n.getKind() == NOT ? n[0] : n;
@@ -105,7 +145,7 @@ int32_t TriggerTermInfo::getTriggerWeight(Node n)
   {
     return 0;
   }
-  if (isAtomicTrigger(n))
+  if (isAtomicTrigger(n) || isUsableRelationTrigger(n))
   {
     return 1;
   }
diff --git a/src/theory/quantifiers/ematching/trigger_term_info.h b/src/theory/quantifiers/ematching/trigger_term_info.h
index 753d0850c..3816d0988 100644
--- a/src/theory/quantifiers/ematching/trigger_term_info.h
+++ b/src/theory/quantifiers/ematching/trigger_term_info.h
@@ -108,6 +108,19 @@ class TriggerTermInfo
   static bool isRelationalTrigger(Node n);
   /** Is k a relational trigger kind? */
   static bool isRelationalTriggerKind(Kind k);
+  /**
+   * Is n a usable relational trigger, which is true if RelationalMatchGenerator
+   * can process n.
+   */
+  static bool isUsableRelationTrigger(Node n);
+  /**
+   * Same as above, but lit / hasPol / pol are updated to the required
+   * constructor arguments for RelationalMatchGenerator.
+   */
+  static bool isUsableRelationTrigger(Node n,
+                                      bool& hasPol,
+                                      bool& pol,
+                                      Node& lit);
   /** is n a simple trigger (see inst_match_generator.h)? */
   static bool isSimpleTrigger(Node n);
   /** get trigger weight
@@ -116,7 +129,8 @@ class TriggerTermInfo
    * trigger term n, where the smaller the value, the easier.
    *
    * Returns 0 for triggers that are APPLY_UF terms.
-   * Returns 1 for other triggers whose kind is atomic.
+   * Returns 1 for other triggers whose kind is atomic, or are usable
+   * relational triggers.
    * Returns 2 otherwise.
    */
   static int32_t getTriggerWeight(Node n);
diff --git a/src/theory/quantifiers/entailment_check.cpp b/src/theory/quantifiers/entailment_check.cpp
new file mode 100644
index 000000000..543414a4e
--- /dev/null
+++ b/src/theory/quantifiers/entailment_check.cpp
@@ -0,0 +1,411 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Implementation of entailment check class.
+ */
+
+#include "theory/quantifiers/entailment_check.h"
+
+#include "theory/quantifiers/quantifiers_state.h"
+#include "theory/quantifiers/term_database.h"
+
+using namespace cvc5::kind;
+using namespace cvc5::context;
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+EntailmentCheck::EntailmentCheck(Env& env, QuantifiersState& qs, TermDb& tdb)
+    : EnvObj(env), d_qstate(qs), d_tdb(tdb)
+{
+  d_true = NodeManager::currentNM()->mkConst(true);
+  d_false = NodeManager::currentNM()->mkConst(false);
+}
+
+EntailmentCheck::~EntailmentCheck() {}
+
+Node EntailmentCheck::evaluateTerm2(TNode n,
+                                    std::map<TNode, Node>& visited,
+                                    std::map<TNode, TNode>& subs,
+                                    bool subsRep,
+                                    bool useEntailmentTests,
+                                    bool reqHasTerm)
+{
+  std::map<TNode, Node>::iterator itv = visited.find(n);
+  if (itv != visited.end())
+  {
+    return itv->second;
+  }
+  Trace("term-db-eval") << "evaluate term : " << n << std::endl;
+  Node ret = n;
+  Kind k = n.getKind();
+  if (k == FORALL)
+  {
+    // do nothing
+  }
+  else if (k == BOUND_VARIABLE)
+  {
+    std::map<TNode, TNode>::iterator it = subs.find(n);
+    if (it != subs.end())
+    {
+      if (!subsRep)
+      {
+        Assert(d_qstate.hasTerm(it->second));
+        ret = d_qstate.getRepresentative(it->second);
+      }
+      else
+      {
+        ret = it->second;
+      }
+    }
+  }
+  else if (d_qstate.hasTerm(n))
+  {
+    Trace("term-db-eval") << "...exists in ee, return rep" << std::endl;
+    ret = d_qstate.getRepresentative(n);
+    reqHasTerm = false;
+  }
+  else if (n.hasOperator())
+  {
+    std::vector<TNode> args;
+    bool ret_set = false;
+    for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++)
+    {
+      TNode c = evaluateTerm2(
+          n[i], visited, subs, subsRep, useEntailmentTests, reqHasTerm);
+      if (c.isNull())
+      {
+        ret = Node::null();
+        ret_set = true;
+        break;
+      }
+      else if (c == d_true || c == d_false)
+      {
+        // short-circuiting
+        if ((k == AND && c == d_false) || (k == OR && c == d_true))
+        {
+          ret = c;
+          ret_set = true;
+          reqHasTerm = false;
+          break;
+        }
+        else if (k == ITE && i == 0)
+        {
+          ret = evaluateTerm2(n[c == d_true ? 1 : 2],
+                              visited,
+                              subs,
+                              subsRep,
+                              useEntailmentTests,
+                              reqHasTerm);
+          ret_set = true;
+          reqHasTerm = false;
+          break;
+        }
+      }
+      Trace("term-db-eval") << "  child " << i << " : " << c << std::endl;
+      args.push_back(c);
+    }
+    if (!ret_set)
+    {
+      // get the (indexed) operator of n, if it exists
+      TNode f = d_tdb.getMatchOperator(n);
+      // if it is an indexed term, return the congruent term
+      if (!f.isNull())
+      {
+        // if f is congruent to a term indexed by this class
+        TNode nn = d_tdb.getCongruentTerm(f, args);
+        Trace("term-db-eval") << "  got congruent term " << nn
+                              << " from DB for " << n << std::endl;
+        if (!nn.isNull())
+        {
+          ret = d_qstate.getRepresentative(nn);
+          Trace("term-db-eval") << "return rep" << std::endl;
+          ret_set = true;
+          reqHasTerm = false;
+          Assert(!ret.isNull());
+        }
+      }
+      if (!ret_set)
+      {
+        Trace("term-db-eval") << "return rewrite" << std::endl;
+        // a theory symbol or a new UF term
+        if (n.getMetaKind() == metakind::PARAMETERIZED)
+        {
+          args.insert(args.begin(), n.getOperator());
+        }
+        ret = NodeManager::currentNM()->mkNode(n.getKind(), args);
+        ret = rewrite(ret);
+        if (ret.getKind() == EQUAL)
+        {
+          if (d_qstate.areDisequal(ret[0], ret[1]))
+          {
+            ret = d_false;
+          }
+        }
+        if (useEntailmentTests)
+        {
+          if (ret.getKind() == EQUAL || ret.getKind() == GEQ)
+          {
+            Valuation& val = d_qstate.getValuation();
+            for (unsigned j = 0; j < 2; j++)
+            {
+              std::pair<bool, Node> et = val.entailmentCheck(
+                  options::TheoryOfMode::THEORY_OF_TYPE_BASED,
+                  j == 0 ? ret : ret.negate());
+              if (et.first)
+              {
+                ret = j == 0 ? d_true : d_false;
+                break;
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+  // must have the term
+  if (reqHasTerm && !ret.isNull())
+  {
+    Kind rk = ret.getKind();
+    if (rk != OR && rk != AND && rk != EQUAL && rk != ITE && rk != NOT
+        && rk != FORALL)
+    {
+      if (!d_qstate.hasTerm(ret))
+      {
+        ret = Node::null();
+      }
+    }
+  }
+  Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret
+                        << ", reqHasTerm = " << reqHasTerm << std::endl;
+  visited[n] = ret;
+  return ret;
+}
+
+TNode EntailmentCheck::getEntailedTerm2(TNode n,
+                                        std::map<TNode, TNode>& subs,
+                                        bool subsRep)
+{
+  Trace("term-db-entail") << "get entailed term : " << n << std::endl;
+  if (d_qstate.hasTerm(n))
+  {
+    Trace("term-db-entail") << "...exists in ee, return rep " << std::endl;
+    return n;
+  }
+  else if (n.getKind() == BOUND_VARIABLE)
+  {
+    std::map<TNode, TNode>::iterator it = subs.find(n);
+    if (it != subs.end())
+    {
+      Trace("term-db-entail")
+          << "...substitution is : " << it->second << std::endl;
+      if (subsRep)
+      {
+        Assert(d_qstate.hasTerm(it->second));
+        Assert(d_qstate.getRepresentative(it->second) == it->second);
+        return it->second;
+      }
+      return getEntailedTerm2(it->second, subs, subsRep);
+    }
+  }
+  else if (n.getKind() == ITE)
+  {
+    for (uint32_t i = 0; i < 2; i++)
+    {
+      if (isEntailed2(n[0], subs, subsRep, i == 0))
+      {
+        return getEntailedTerm2(n[i == 0 ? 1 : 2], subs, subsRep);
+      }
+    }
+  }
+  else
+  {
+    if (n.hasOperator())
+    {
+      TNode f = d_tdb.getMatchOperator(n);
+      if (!f.isNull())
+      {
+        std::vector<TNode> args;
+        for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
+        {
+          TNode c = getEntailedTerm2(n[i], subs, subsRep);
+          if (c.isNull())
+          {
+            return TNode::null();
+          }
+          c = d_qstate.getRepresentative(c);
+          Trace("term-db-entail") << "  child " << i << " : " << c << std::endl;
+          args.push_back(c);
+        }
+        TNode nn = d_tdb.getCongruentTerm(f, args);
+        Trace("term-db-entail")
+            << "  got congruent term " << nn << " for " << n << std::endl;
+        return nn;
+      }
+    }
+  }
+  return TNode::null();
+}
+
+Node EntailmentCheck::evaluateTerm(TNode n,
+                                   std::map<TNode, TNode>& subs,
+                                   bool subsRep,
+                                   bool useEntailmentTests,
+                                   bool reqHasTerm)
+{
+  std::map<TNode, Node> visited;
+  return evaluateTerm2(
+      n, visited, subs, subsRep, useEntailmentTests, reqHasTerm);
+}
+
+Node EntailmentCheck::evaluateTerm(TNode n,
+                                   bool useEntailmentTests,
+                                   bool reqHasTerm)
+{
+  std::map<TNode, Node> visited;
+  std::map<TNode, TNode> subs;
+  return evaluateTerm2(n, visited, subs, false, useEntailmentTests, reqHasTerm);
+}
+
+TNode EntailmentCheck::getEntailedTerm(TNode n,
+                                       std::map<TNode, TNode>& subs,
+                                       bool subsRep)
+{
+  return getEntailedTerm2(n, subs, subsRep);
+}
+
+TNode EntailmentCheck::getEntailedTerm(TNode n)
+{
+  std::map<TNode, TNode> subs;
+  return getEntailedTerm2(n, subs, false);
+}
+
+bool EntailmentCheck::isEntailed2(TNode n,
+                                  std::map<TNode, TNode>& subs,
+                                  bool subsRep,
+                                  bool pol)
+{
+  Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol
+                          << std::endl;
+  Assert(n.getType().isBoolean());
+  if (n.getKind() == EQUAL && !n[0].getType().isBoolean())
+  {
+    TNode n1 = getEntailedTerm2(n[0], subs, subsRep);
+    if (!n1.isNull())
+    {
+      TNode n2 = getEntailedTerm2(n[1], subs, subsRep);
+      if (!n2.isNull())
+      {
+        if (n1 == n2)
+        {
+          return pol;
+        }
+        else
+        {
+          Assert(d_qstate.hasTerm(n1));
+          Assert(d_qstate.hasTerm(n2));
+          if (pol)
+          {
+            return d_qstate.areEqual(n1, n2);
+          }
+          else
+          {
+            return d_qstate.areDisequal(n1, n2);
+          }
+        }
+      }
+    }
+  }
+  else if (n.getKind() == NOT)
+  {
+    return isEntailed2(n[0], subs, subsRep, !pol);
+  }
+  else if (n.getKind() == OR || n.getKind() == AND)
+  {
+    bool simPol = (pol && n.getKind() == OR) || (!pol && n.getKind() == AND);
+    for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
+    {
+      if (isEntailed2(n[i], subs, subsRep, pol))
+      {
+        if (simPol)
+        {
+          return true;
+        }
+      }
+      else
+      {
+        if (!simPol)
+        {
+          return false;
+        }
+      }
+    }
+    return !simPol;
+    // Boolean equality here
+  }
+  else if (n.getKind() == EQUAL || n.getKind() == ITE)
+  {
+    for (size_t i = 0; i < 2; i++)
+    {
+      if (isEntailed2(n[0], subs, subsRep, i == 0))
+      {
+        size_t ch = (n.getKind() == EQUAL || i == 0) ? 1 : 2;
+        bool reqPol = (n.getKind() == ITE || i == 0) ? pol : !pol;
+        return isEntailed2(n[ch], subs, subsRep, reqPol);
+      }
+    }
+  }
+  else if (n.getKind() == APPLY_UF)
+  {
+    TNode n1 = getEntailedTerm2(n, subs, subsRep);
+    if (!n1.isNull())
+    {
+      Assert(d_qstate.hasTerm(n1));
+      if (n1 == d_true)
+      {
+        return pol;
+      }
+      else if (n1 == d_false)
+      {
+        return !pol;
+      }
+      else
+      {
+        return d_qstate.getRepresentative(n1) == (pol ? d_true : d_false);
+      }
+    }
+  }
+  else if (n.getKind() == FORALL && !pol)
+  {
+    return isEntailed2(n[1], subs, subsRep, pol);
+  }
+  return false;
+}
+
+bool EntailmentCheck::isEntailed(TNode n, bool pol)
+{
+  std::map<TNode, TNode> subs;
+  return isEntailed2(n, subs, false, pol);
+}
+
+bool EntailmentCheck::isEntailed(TNode n,
+                                 std::map<TNode, TNode>& subs,
+                                 bool subsRep,
+                                 bool pol)
+{
+  return isEntailed2(n, subs, subsRep, pol);
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/entailment_check.h b/src/theory/quantifiers/entailment_check.h
new file mode 100644
index 000000000..ecf74fe85
--- /dev/null
+++ b/src/theory/quantifiers/entailment_check.h
@@ -0,0 +1,156 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Entailment check class
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__QUANTIFIERS__ENTAILMENT_CHECK_H
+#define CVC5__THEORY__QUANTIFIERS__ENTAILMENT_CHECK_H
+
+#include <map>
+#include <vector>
+
+#include "expr/node.h"
+#include "smt/env_obj.h"
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+class QuantifiersState;
+class TermDb;
+
+/**
+ * Entailment check utility, which determines whether formulas are entailed
+ * in the current context. The main focus of this class is on UF formulas.
+ * It works by looking at the term argument trie data structures in term
+ * database. For details, see e.g. Section 4.1 of Reynolds et al TACAS 2018.
+ */
+class EntailmentCheck : protected EnvObj
+{
+ public:
+  EntailmentCheck(Env& env, QuantifiersState& qs, TermDb& tdb);
+  ~EntailmentCheck();
+  /** evaluate term
+   *
+   * Returns a term n' such that n * subs = n' is entailed based on the current
+   * set of equalities, where ( n * subs ) is term n under the substitution
+   * subs.
+   *
+   * This function may generate new terms. In particular, we typically rewrite
+   * subterms of n of maximal size (in terms of the AST) to terms that exist
+   * in the equality engine.
+   *
+   * useEntailmentTests is whether to call the theory engine's entailmentTest
+   * on literals n for which this call fails to find a term n' that is
+   * equivalent to n, for increased precision. This is not frequently used.
+   *
+   * If reqHasTerm, then we require that the returned term is a Boolean
+   * combination of terms that exist in the equality engine used by this call.
+   * If no such term is constructable, this call returns null. The motivation
+   * for setting this to true is to "fail fast" if we require the return value
+   * of this function to only involve existing terms. This is used e.g. in
+   * the "propagating instances" portion of conflict-based instantiation
+   * (quant_conflict_find.h).
+   *
+   * @param n The term under consideration
+   * @param subs The substitution under consideration
+   * @param subsRep Whether the range of subs are representatives in the current
+   * equality engine
+   * @param useEntailmentTests Whether to use entailment tests to show
+   * n * subs is equivalent to true/false.
+   * @param reqHasTerm Whether we require the returned term to be a Boolean
+   * combination of terms known to the current equality engine
+   * @return the term n * subs evaluates to
+   */
+  Node evaluateTerm(TNode n,
+                    std::map<TNode, TNode>& subs,
+                    bool subsRep,
+                    bool useEntailmentTests = false,
+                    bool reqHasTerm = false);
+  /** Same as above, without a substitution */
+  Node evaluateTerm(TNode n,
+                    bool useEntailmentTests = false,
+                    bool reqHasTerm = false);
+  /** get entailed term
+   *
+   * If possible, returns a term n' such that:
+   * (1) n' exists in the current equality engine (as specified by the state),
+   * (2) n = n' is entailed in the current context.
+   * It returns null if no such term can be found.
+   * Wrt evaluateTerm, this version does not construct new terms, and
+   * thus is less aggressive.
+   */
+  TNode getEntailedTerm(TNode n);
+  /** get entailed term
+   *
+   * If possible, returns a term n' such that:
+   * (1) n' exists in the current equality engine (as specified by the state),
+   * (2) n * subs = n' is entailed in the current context, where * denotes
+   * substitution application.
+   * It returns null if no such term can be found.
+   * subsRep is whether the substitution maps to terms that are representatives
+   * according to the quantifiers state.
+   * Wrt evaluateTerm, this version does not construct new terms, and
+   * thus is less aggressive.
+   */
+  TNode getEntailedTerm(TNode n, std::map<TNode, TNode>& subs, bool subsRep);
+  /** is entailed
+   * Checks whether the current context entails n with polarity pol, based on
+   * the equality information in the quantifiers state. Returns true if the
+   * entailment can be successfully shown.
+   */
+  bool isEntailed(TNode n, bool pol);
+  /** is entailed
+   *
+   * Checks whether the current context entails ( n * subs ) with polarity pol,
+   * based on the equality information in the quantifiers state,
+   * where * denotes substitution application.
+   * subsRep is whether the substitution maps to terms that are representatives
+   * according to in the quantifiers state.
+   */
+  bool isEntailed(TNode n,
+                  std::map<TNode, TNode>& subs,
+                  bool subsRep,
+                  bool pol);
+
+ protected:
+  /** helper for evaluate term */
+  Node evaluateTerm2(TNode n,
+                     std::map<TNode, Node>& visited,
+                     std::map<TNode, TNode>& subs,
+                     bool subsRep,
+                     bool useEntailmentTests,
+                     bool reqHasTerm);
+  /** helper for get entailed term */
+  TNode getEntailedTerm2(TNode n, std::map<TNode, TNode>& subs, bool subsRep);
+  /** helper for is entailed */
+  bool isEntailed2(TNode n,
+                   std::map<TNode, TNode>& subs,
+                   bool subsRep,
+                   bool pol);
+  /** The quantifiers state object */
+  QuantifiersState& d_qstate;
+  /** Reference to the term database */
+  TermDb& d_tdb;
+  /** boolean terms */
+  Node d_true;
+  Node d_false;
+}; /* class EntailmentCheck */
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5
+
+#endif /* CVC5__THEORY__QUANTIFIERS__ENTAILMENT_CHECK_H */
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 7c1d36ce8..94351274a 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -951,10 +951,15 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
     Node r = n;
     if( !n.isConst() ){
       TypeNode tn = n.getType();
-      if( !fm->hasTerm(n) && tn.isFirstClass() ){
-        r = getSomeDomainElement(fm, tn );
+      if (!fm->hasTerm(n) && tn.isFirstClass())
+      {
+        // if the term is unknown, we do not assume any value for it
+        r = Node::null();
+      }
+      else
+      {
+        r = fm->getRepresentative(r);
       }
-      r = fm->getRepresentative( r );
     }
     Trace("fmc-debug") << "Add constant entry..." << std::endl;
     d.addEntry(fm, mkCondDefault(fm, f), r);
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index f756fcfd1..be04f9404 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -25,6 +25,7 @@
 #include "smt/logic_exception.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
+#include "theory/quantifiers/entailment_check.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_preprocess.h"
@@ -183,7 +184,7 @@ bool Instantiate::addInstantiation(Node q,
 #endif
   }
 
-  TermDb* tdb = d_treg.getTermDatabase();
+  EntailmentCheck* ec = d_treg.getEntailmentCheck();
   // Note we check for entailment before checking for term vector duplication.
   // Although checking for term vector duplication is a faster check, it is
   // included automatically with recordInstantiationInternal, hence we prefer
@@ -206,7 +207,7 @@ bool Instantiate::addInstantiation(Node q,
     {
       subs[q[0][i]] = terms[i];
     }
-    if (tdb->isEntailed(q[1], subs, false, true))
+    if (ec->isEntailed(q[1], subs, false, true))
     {
       Trace("inst-add-debug") << " --> Currently entailed." << std::endl;
       ++(d_statistics.d_inst_duplicate_ent);
@@ -217,6 +218,7 @@ bool Instantiate::addInstantiation(Node q,
   // check based on instantiation level
   if (options::instMaxLevel() != -1)
   {
+    TermDb* tdb = d_treg.getTermDatabase();
     for (Node& t : terms)
     {
       if (!tdb->isTermEligibleForInstantiation(t, q))
@@ -409,7 +411,7 @@ bool Instantiate::addInstantiationExpFail(Node q,
     // will never succeed with 1 variable
     return false;
   }
-  TermDb* tdb = d_treg.getTermDatabase();
+  EntailmentCheck* echeck = d_treg.getEntailmentCheck();
   Trace("inst-exp-fail") << "Explain inst failure..." << terms << std::endl;
   // set up information for below
   std::vector<Node>& vars = d_qreg.d_vars[q];
@@ -445,7 +447,7 @@ bool Instantiate::addInstantiationExpFail(Node q,
     if (options::instNoEntail())
     {
       Trace("inst-exp-fail") << "  check entailment" << std::endl;
-      success = tdb->isEntailed(q[1], subs, false, true);
+      success = echeck->isEntailed(q[1], subs, false, true);
       Trace("inst-exp-fail") << "  entailed: " << success << std::endl;
     }
     // check whether the instantiation rewrites to the same thing
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 361adfd54..323398879 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -52,12 +52,6 @@ QuantInfo::~QuantInfo() {
   d_var_mg.clear();
 }
 
-QuantifiersInferenceManager& QuantInfo::getInferenceManager()
-{
-  Assert(d_parent != nullptr);
-  return d_parent->getInferenceManager();
-}
-
 void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) {
   d_parent = p;
   d_q = q;
@@ -577,30 +571,33 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p,
 {
   if( options::qcfEagerTest() ){
     //check whether the instantiation evaluates as expected
+    EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck();
+    std::map<TNode, TNode> subs;
+    for (size_t i = 0, tsize = terms.size(); i < tsize; i++)
+    {
+      Trace("qcf-instance-check") << "  " << terms[i] << std::endl;
+      subs[d_q[0][i]] = terms[i];
+    }
+    for (size_t i = 0, evsize = d_extra_var.size(); i < evsize; i++)
+    {
+      Node n = getCurrentExpValue(d_extra_var[i]);
+      Trace("qcf-instance-check")
+          << "  " << d_extra_var[i] << " -> " << n << std::endl;
+      subs[d_extra_var[i]] = n;
+    }
     if (p->atConflictEffort()) {
       Trace("qcf-instance-check") << "Possible conflict instance for " << d_q << " : " << std::endl;
-      std::map< TNode, TNode > subs;
-      for( unsigned i=0; i<terms.size(); i++ ){
-        Trace("qcf-instance-check") << "  " << terms[i] << std::endl;
-        subs[d_q[0][i]] = terms[i];
-      }
-      TermDb* tdb = p->getTermDatabase();
-      for( unsigned i=0; i<d_extra_var.size(); i++ ){
-        Node n = getCurrentExpValue( d_extra_var[i] );
-        Trace("qcf-instance-check") << "  " << d_extra_var[i] << " -> " << n << std::endl;
-        subs[d_extra_var[i]] = n;
-      }
-      if (!tdb->isEntailed(d_q[1], subs, false, false))
+      if (!echeck->isEntailed(d_q[1], subs, false, false))
       {
         Trace("qcf-instance-check") << "...not entailed to be false." << std::endl;
         return true;
       }
     }else{
-      Node inst =
-          getInferenceManager().getInstantiate()->getInstantiation(d_q, terms);
-      inst = Rewriter::rewrite(inst);
-      Node inst_eval = p->getTermDatabase()->evaluateTerm(
-          inst, options::qcfTConstraint(), true);
+      // see if the body of the quantified formula evaluates to a Boolean
+      // combination of known terms under the current substitution. We use
+      // the helper method evaluateTerm from the entailment check utility.
+      Node inst_eval = echeck->evaluateTerm(
+          d_q[1], subs, false, options::qcfTConstraint(), true);
       if( Trace.isOn("qcf-instance-check") ){
         Trace("qcf-instance-check") << "Possible propagating instance for " << d_q << " : " << std::endl;
         for( unsigned i=0; i<terms.size(); i++ ){
@@ -608,6 +605,10 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p,
         }
         Trace("qcf-instance-check") << "...evaluates to " << inst_eval << std::endl;
       }
+      // If it is the case that instantiation can be rewritten to a Boolean
+      // combination of terms that exist in the current context, then inst_eval
+      // is non-null. Moreover, we insist that inst_eval is not true, or else
+      // the instantiation is trivially entailed and hence is spurious.
       if (inst_eval.isNull()
           || (inst_eval.isConst() && inst_eval.getConst<bool>()))
       {
@@ -1219,11 +1220,11 @@ bool MatchGen::reset_round(QuantConflictFind* p)
     //  d_ground_eval[0] = p->d_false;
     //}
     // modified
-    TermDb* tdb = p->getTermDatabase();
+    EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck();
     QuantifiersState& qs = p->getState();
     for (unsigned i = 0; i < 2; i++)
     {
-      if (tdb->isEntailed(d_n, i == 0))
+      if (echeck->isEntailed(d_n, i == 0))
       {
         d_ground_eval[0] = i==0 ? p->d_true : p->d_false;
       }
@@ -1233,13 +1234,13 @@ bool MatchGen::reset_round(QuantConflictFind* p)
       }
     }
   }else if( d_type==typ_eq ){
-    TermDb* tdb = p->getTermDatabase();
+    EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck();
     QuantifiersState& qs = p->getState();
     for (unsigned i = 0, size = d_n.getNumChildren(); i < size; i++)
     {
       if (!expr::hasBoundVar(d_n[i]))
       {
-        TNode t = tdb->getEntailedTerm(d_n[i]);
+        TNode t = echeck->getEntailedTerm(d_n[i]);
         if (qs.isInConflict())
         {
           return false;
@@ -1289,13 +1290,9 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
     TNode n = qi->getCurrentValue( d_n );
     int vn = qi->getCurrentRepVar( qi->getVarNum( n ) );
     if( vn==-1 ){
-      //evaluate the value, see if it is compatible
-      //int e = p->evaluate( n );
-      //if( ( e==1 && d_tgt ) || ( e==0 && !d_tgt ) ){
-      //  d_child_counter = 0;
-      //}
-      //modified 
-      if( p->getTermDatabase()->isEntailed( n, d_tgt ) ){ 
+      EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck();
+      if (echeck->isEntailed(n, d_tgt))
+      {
         d_child_counter = 0;
       }
     }else{
@@ -2168,8 +2165,8 @@ void QuantConflictFind::checkQuantifiedFormula(Node q,
         Node inst = qinst->getInstantiation(q, terms);
         Debug("qcf-check-inst")
             << "Check instantiation " << inst << "..." << std::endl;
-        Assert(!getTermDatabase()->isEntailed(inst, true));
-        Assert(getTermDatabase()->isEntailed(inst, false)
+        Assert(!getTermRegistry().getEntailmentCheck()->isEntailed(inst, true));
+        Assert(getTermRegistry().getEntailmentCheck()->isEntailed(inst, false)
                || d_effort > EFFORT_CONFLICT);
       }
       // Process the lemma: either add an instantiation or specific lemmas
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 927a74ff2..d14e281fb 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -132,8 +132,6 @@ public:
 public:
   QuantInfo();
   ~QuantInfo();
-  /** Get quantifiers inference manager */
-  QuantifiersInferenceManager& getInferenceManager();
   std::vector< TNode > d_vars;
   std::vector< TypeNode > d_var_types;
   std::map< TNode, int > d_var_num;
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 7c7c7aade..52e90e26e 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/quantifiers/quantifiers_rewriter.h"
 
+#include "expr/ascription_type.h"
 #include "expr/bound_var_manager.h"
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
@@ -895,12 +896,25 @@ bool QuantifiersRewriter::getVarElimLit(Node body,
       const DType& dt = datatypes::utils::datatypeOf(tester);
       const DTypeConstructor& c = dt[index];
       std::vector<Node> newChildren;
-      newChildren.push_back(c.getConstructor());
+      Node cons = c.getConstructor();
+      TypeNode tspec;
+      // take into account if parametric
+      if (dt.isParametric())
+      {
+        tspec = c.getSpecializedConstructorType(lit[0].getType());
+        cons = nm->mkNode(
+            APPLY_TYPE_ASCRIPTION, nm->mkConst(AscriptionType(tspec)), cons);
+      }
+      else
+      {
+        tspec = cons.getType();
+      }
+      newChildren.push_back(cons);
       std::vector<Node> newVars;
       BoundVarManager* bvm = nm->getBoundVarManager();
-      for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++)
+      for (size_t j = 0, nargs = c.getNumArgs(); j < nargs; j++)
       {
-        TypeNode tn = c[j].getRangeType();
+        TypeNode tn = tspec[j];
         Node rn = nm->mkConst(Rational(j));
         Node cacheVal = BoundVarManager::getCacheValue(body, lit, rn);
         Node v = bvm->mkBoundVar<QRewDtExpandAttribute>(cacheVal, tn);
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index c8e14e4bd..fdc0b28e0 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -39,6 +39,7 @@ Cegis::Cegis(Env& env,
              SynthConjecture* p)
     : SygusModule(env, qs, qim, tds, p),
       d_eval_unfold(tds->getEvalUnfold()),
+      d_cexClosedEnum(false),
       d_cegis_sampler(env),
       d_usingSymCons(false)
 {
@@ -47,11 +48,18 @@ Cegis::Cegis(Env& env,
 bool Cegis::initialize(Node conj, Node n, const std::vector<Node>& candidates)
 {
   d_base_body = n;
+  d_cexClosedEnum = true;
   if (d_base_body.getKind() == NOT && d_base_body[0].getKind() == FORALL)
   {
     for (const Node& v : d_base_body[0][0])
     {
       d_base_vars.push_back(v);
+      if (!v.getType().isClosedEnumerable())
+      {
+        // not closed enumerable, refinement lemmas cannot be sent to the
+        // quantifier-free datatype solver
+        d_cexClosedEnum = false;
+      }
     }
     d_base_body = d_base_body[0][1];
   }
@@ -467,14 +475,18 @@ void Cegis::addRefinementLemmaConjunct(unsigned wcounter,
 void Cegis::registerRefinementLemma(const std::vector<Node>& vars, Node lem)
 {
   addRefinementLemma(lem);
-  // Make the refinement lemma and add it to lems.
-  // This lemma is guarded by the parent's guard, which has the semantics
-  // "this conjecture has a solution", hence this lemma states:
-  // if the parent conjecture has a solution, it satisfies the specification
-  // for the given concrete point.
-  Node rlem =
-      NodeManager::currentNM()->mkNode(OR, d_parent->getGuard().negate(), lem);
-  d_qim.addPendingLemma(rlem, InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE);
+  // must be closed enumerable
+  if (d_cexClosedEnum && options().quantifiers.sygusEvalUnfold)
+  {
+    // Make the refinement lemma and add it to lems.
+    // This lemma is guarded by the parent's guard, which has the semantics
+    // "this conjecture has a solution", hence this lemma states:
+    // if the parent conjecture has a solution, it satisfies the specification
+    // for the given concrete point.
+    Node rlem = NodeManager::currentNM()->mkNode(
+        OR, d_parent->getGuard().negate(), lem);
+    d_qim.addPendingLemma(rlem, InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE);
+  }
 }
 
 bool Cegis::usingRepairConst() { return true; }
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index 8e0fffdd1..8d1f0a1b2 100644
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -119,6 +119,13 @@ class Cegis : public SygusModule
   std::vector<Node> d_rl_vals;
   /** all variables appearing in refinement lemmas */
   std::unordered_set<Node> d_refinement_lemma_vars;
+  /**
+   * Are the counterexamples we are handling in this class of only closed
+   * enumerable types (see TypeNode::isClosedEnumerable). If this is false,
+   * then CEGIS refinement lemmas can contain terms that are unhandled by
+   * theory solvers, e.g. uninterpreted constants.
+   */
+  bool d_cexClosedEnum;
 
   /** adds lem as a refinement lemma */
   void addRefinementLemma(Node lem);
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 43c958ff9..9b4cfb9e1 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -20,6 +20,7 @@
 
 #include "expr/ascription_type.h"
 #include "expr/dtype_cons.h"
+#include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
@@ -420,6 +421,8 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type,
   {
     // generate constant array over the first element of the constituent type
     Node c = type.mkGroundTerm();
+    // note that c should never contain an uninterpreted constant
+    Assert(!expr::hasSubtermKind(UNINTERPRETED_CONSTANT, c));
     ops.push_back(c);
   }
   else if (type.isRoundingMode())
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index b1537a390..573cab7bf 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -451,366 +451,6 @@ bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) {
   }
 }
 
-Node TermDb::evaluateTerm2(TNode n,
-                           std::map<TNode, Node>& visited,
-                           std::vector<Node>& exp,
-                           bool useEntailmentTests,
-                           bool computeExp,
-                           bool reqHasTerm)
-{
-  std::map< TNode, Node >::iterator itv = visited.find( n );
-  if( itv != visited.end() ){
-    return itv->second;
-  }
-  size_t prevSize = exp.size();
-  Trace("term-db-eval") << "evaluate term : " << n << std::endl;
-  Node ret = n;
-  if( n.getKind()==FORALL || n.getKind()==BOUND_VARIABLE ){
-    //do nothing
-  }
-  else if (d_qstate.hasTerm(n))
-  {
-    Trace("term-db-eval") << "...exists in ee, return rep" << std::endl;
-    ret = d_qstate.getRepresentative(n);
-    if (computeExp)
-    {
-      if (n != ret)
-      {
-        exp.push_back(n.eqNode(ret));
-      }
-    }
-    reqHasTerm = false;
-  }
-  else if (n.hasOperator())
-  {
-    std::vector<TNode> args;
-    bool ret_set = false;
-    Kind k = n.getKind();
-    std::vector<Node> tempExp;
-    for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++)
-    {
-      TNode c = evaluateTerm2(n[i],
-                              visited,
-                              tempExp,
-                              useEntailmentTests,
-                              computeExp,
-                              reqHasTerm);
-      if (c.isNull())
-      {
-        ret = Node::null();
-        ret_set = true;
-        break;
-      }
-      else if (c == d_true || c == d_false)
-      {
-        // short-circuiting
-        if ((k == AND && c == d_false) || (k == OR && c == d_true))
-        {
-          ret = c;
-          ret_set = true;
-          reqHasTerm = false;
-          break;
-        }
-        else if (k == ITE && i == 0)
-        {
-          ret = evaluateTerm2(n[c == d_true ? 1 : 2],
-                              visited,
-                              tempExp,
-                              useEntailmentTests,
-                              computeExp,
-                              reqHasTerm);
-          ret_set = true;
-          reqHasTerm = false;
-          break;
-        }
-      }
-      if (computeExp)
-      {
-        exp.insert(exp.end(), tempExp.begin(), tempExp.end());
-      }
-      Trace("term-db-eval") << "  child " << i << " : " << c << std::endl;
-      args.push_back(c);
-    }
-    if (ret_set)
-    {
-      // if we short circuited
-      if (computeExp)
-      {
-        exp.clear();
-        exp.insert(exp.end(), tempExp.begin(), tempExp.end());
-      }
-    }
-    else
-    {
-      // get the (indexed) operator of n, if it exists
-      TNode f = getMatchOperator(n);
-      // if it is an indexed term, return the congruent term
-      if (!f.isNull())
-      {
-        // if f is congruent to a term indexed by this class
-        TNode nn = getCongruentTerm(f, args);
-        Trace("term-db-eval") << "  got congruent term " << nn
-                              << " from DB for " << n << std::endl;
-        if (!nn.isNull())
-        {
-          if (computeExp)
-          {
-            Assert(nn.getNumChildren() == n.getNumChildren());
-            for (unsigned i = 0, nchild = nn.getNumChildren(); i < nchild; i++)
-            {
-              if (nn[i] != n[i])
-              {
-                exp.push_back(nn[i].eqNode(n[i]));
-              }
-            }
-          }
-          ret = d_qstate.getRepresentative(nn);
-          Trace("term-db-eval") << "return rep" << std::endl;
-          ret_set = true;
-          reqHasTerm = false;
-          Assert(!ret.isNull());
-          if (computeExp)
-          {
-            if (n != ret)
-            {
-              exp.push_back(nn.eqNode(ret));
-            }
-          }
-        }
-      }
-      if( !ret_set ){
-        Trace("term-db-eval") << "return rewrite" << std::endl;
-        // a theory symbol or a new UF term
-        if (n.getMetaKind() == metakind::PARAMETERIZED)
-        {
-          args.insert(args.begin(), n.getOperator());
-        }
-        ret = NodeManager::currentNM()->mkNode(n.getKind(), args);
-        ret = rewrite(ret);
-        if (ret.getKind() == EQUAL)
-        {
-          if (d_qstate.areDisequal(ret[0], ret[1]))
-          {
-            ret = d_false;
-          }
-        }
-        if (useEntailmentTests)
-        {
-          if (ret.getKind() == EQUAL || ret.getKind() == GEQ)
-          {
-            Valuation& val = d_qstate.getValuation();
-            for (unsigned j = 0; j < 2; j++)
-            {
-              std::pair<bool, Node> et = val.entailmentCheck(
-                  options::TheoryOfMode::THEORY_OF_TYPE_BASED,
-                  j == 0 ? ret : ret.negate());
-              if (et.first)
-              {
-                ret = j == 0 ? d_true : d_false;
-                if (computeExp)
-                {
-                  exp.push_back(et.second);
-                }
-                break;
-              }
-            }
-          }
-        }
-      }
-    }
-  }
-  // must have the term
-  if (reqHasTerm && !ret.isNull())
-  {
-    Kind k = ret.getKind();
-    if (k != OR && k != AND && k != EQUAL && k != ITE && k != NOT
-        && k != FORALL)
-    {
-      if (!d_qstate.hasTerm(ret))
-      {
-        ret = Node::null();
-      }
-    }
-  }
-  Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret
-                        << ", reqHasTerm = " << reqHasTerm << std::endl;
-  // clear the explanation if failed
-  if (computeExp && ret.isNull())
-  {
-    exp.resize(prevSize);
-  }
-  visited[n] = ret;
-  return ret;
-}
-
-TNode TermDb::getEntailedTerm2(TNode n,
-                               std::map<TNode, TNode>& subs,
-                               bool subsRep,
-                               bool hasSubs)
-{
-  Trace("term-db-entail") << "get entailed term : " << n << std::endl;
-  if (d_qstate.hasTerm(n))
-  {
-    Trace("term-db-entail") << "...exists in ee, return rep " << std::endl;
-    return n;
-  }else if( n.getKind()==BOUND_VARIABLE ){
-    if( hasSubs ){
-      std::map< TNode, TNode >::iterator it = subs.find( n );
-      if( it!=subs.end() ){
-        Trace("term-db-entail") << "...substitution is : " << it->second << std::endl;
-        if( subsRep ){
-          Assert(d_qstate.hasTerm(it->second));
-          Assert(d_qstate.getRepresentative(it->second) == it->second);
-          return it->second;
-        }
-        return getEntailedTerm2(it->second, subs, subsRep, hasSubs);
-      }
-    }
-  }else if( n.getKind()==ITE ){
-    for( unsigned i=0; i<2; i++ ){
-      if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0))
-      {
-        return getEntailedTerm2(n[i == 0 ? 1 : 2], subs, subsRep, hasSubs);
-      }
-    }
-  }else{
-    if( n.hasOperator() ){
-      TNode f = getMatchOperator( n );
-      if( !f.isNull() ){
-        std::vector< TNode > args;
-        for( unsigned i=0; i<n.getNumChildren(); i++ ){
-          TNode c = getEntailedTerm2(n[i], subs, subsRep, hasSubs);
-          if( c.isNull() ){
-            return TNode::null();
-          }
-          c = d_qstate.getRepresentative(c);
-          Trace("term-db-entail") << "  child " << i << " : " << c << std::endl;
-          args.push_back( c );
-        }
-        TNode nn = getCongruentTerm(f, args);
-        Trace("term-db-entail") << "  got congruent term " << nn << " for " << n << std::endl;
-        return nn;
-      }
-    }
-  }
-  return TNode::null();
-}
-
-Node TermDb::evaluateTerm(TNode n,
-                          bool useEntailmentTests,
-                          bool reqHasTerm)
-{
-  std::map< TNode, Node > visited;
-  std::vector<Node> exp;
-  return evaluateTerm2(n, visited, exp, useEntailmentTests, false, reqHasTerm);
-}
-
-Node TermDb::evaluateTerm(TNode n,
-                          std::vector<Node>& exp,
-                          bool useEntailmentTests,
-                          bool reqHasTerm)
-{
-  std::map<TNode, Node> visited;
-  return evaluateTerm2(n, visited, exp, useEntailmentTests, true, reqHasTerm);
-}
-
-TNode TermDb::getEntailedTerm(TNode n,
-                              std::map<TNode, TNode>& subs,
-                              bool subsRep)
-{
-  return getEntailedTerm2(n, subs, subsRep, true);
-}
-
-TNode TermDb::getEntailedTerm(TNode n)
-{
-  std::map< TNode, TNode > subs;
-  return getEntailedTerm2(n, subs, false, false);
-}
-
-bool TermDb::isEntailed2(
-    TNode n, std::map<TNode, TNode>& subs, bool subsRep, bool hasSubs, bool pol)
-{
-  Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol << std::endl;
-  Assert(n.getType().isBoolean());
-  if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){
-    TNode n1 = getEntailedTerm2(n[0], subs, subsRep, hasSubs);
-    if( !n1.isNull() ){
-      TNode n2 = getEntailedTerm2(n[1], subs, subsRep, hasSubs);
-      if( !n2.isNull() ){
-        if( n1==n2 ){
-          return pol;
-        }else{
-          Assert(d_qstate.hasTerm(n1));
-          Assert(d_qstate.hasTerm(n2));
-          if( pol ){
-            return d_qstate.areEqual(n1, n2);
-          }else{
-            return d_qstate.areDisequal(n1, n2);
-          }
-        }
-      }
-    }
-  }else if( n.getKind()==NOT ){
-    return isEntailed2(n[0], subs, subsRep, hasSubs, !pol);
-  }else if( n.getKind()==OR || n.getKind()==AND ){
-    bool simPol = ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND );
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if (isEntailed2(n[i], subs, subsRep, hasSubs, pol))
-      {
-        if( simPol ){
-          return true;
-        }
-      }else{
-        if( !simPol ){
-          return false;
-        }
-      }
-    }
-    return !simPol;
-  //Boolean equality here
-  }else if( n.getKind()==EQUAL || n.getKind()==ITE ){
-    for( unsigned i=0; i<2; i++ ){
-      if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0))
-      {
-        unsigned ch = ( n.getKind()==EQUAL || i==0 ) ? 1 : 2;
-        bool reqPol = ( n.getKind()==ITE || i==0 ) ? pol : !pol;
-        return isEntailed2(n[ch], subs, subsRep, hasSubs, reqPol);
-      }
-    }
-  }else if( n.getKind()==APPLY_UF ){
-    TNode n1 = getEntailedTerm2(n, subs, subsRep, hasSubs);
-    if( !n1.isNull() ){
-      Assert(d_qstate.hasTerm(n1));
-      if( n1==d_true ){
-        return pol;
-      }else if( n1==d_false ){
-        return !pol;
-      }else{
-        return d_qstate.getRepresentative(n1) == (pol ? d_true : d_false);
-      }
-    }
-  }else if( n.getKind()==FORALL && !pol ){
-    return isEntailed2(n[1], subs, subsRep, hasSubs, pol);
-  }
-  return false;
-}
-
-bool TermDb::isEntailed(TNode n, bool pol)
-{
-  Assert(d_consistent_ee);
-  std::map< TNode, TNode > subs;
-  return isEntailed2(n, subs, false, false, pol);
-}
-
-bool TermDb::isEntailed(TNode n,
-                        std::map<TNode, TNode>& subs,
-                        bool subsRep,
-                        bool pol)
-{
-  Assert(d_consistent_ee);
-  return isEntailed2(n, subs, subsRep, true, pol);
-}
-
 bool TermDb::isTermActive( Node n ) {
   return d_inactive_map.find( n )==d_inactive_map.end(); 
   //return !n.getAttribute(NoMatchAttribute());
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index af0b87bd8..0e5c7bc01 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -176,78 +176,6 @@ class TermDb : public QuantifiersUtil {
   *     equivalence class of r.
   */
   bool inRelevantDomain(TNode f, unsigned i, TNode r);
-  /** evaluate term
-   *
-   * Returns a term n' such that n = n' is entailed based on the equality
-   * information ee.  This function may generate new terms. In particular,
-   * we typically rewrite subterms of n of maximal size to terms that exist in
-   * the equality engine specified by ee.
-   *
-   * useEntailmentTests is whether to call the theory engine's entailmentTest
-   * on literals n for which this call fails to find a term n' that is
-   * equivalent to n, for increased precision. This is not frequently used.
-   *
-   * The vector exp stores the explanation for why n evaluates to that term,
-   * that is, if this call returns a non-null node n', then:
-   *   exp => n = n'
-   *
-   * If reqHasTerm, then we require that the returned term is a Boolean
-   * combination of terms that exist in the equality engine used by this call.
-   * If no such term is constructable, this call returns null. The motivation
-   * for setting this to true is to "fail fast" if we require the return value
-   * of this function to only involve existing terms. This is used e.g. in
-   * the "propagating instances" portion of conflict-based instantiation
-   * (quant_conflict_find.h).
-   */
-  Node evaluateTerm(TNode n,
-                    std::vector<Node>& exp,
-                    bool useEntailmentTests = false,
-                    bool reqHasTerm = false);
-  /** same as above, without exp */
-  Node evaluateTerm(TNode n,
-                    bool useEntailmentTests = false,
-                    bool reqHasTerm = false);
-  /** get entailed term
-   *
-   * If possible, returns a term n' such that:
-   * (1) n' exists in the current equality engine (as specified by the state),
-   * (2) n = n' is entailed in the current context.
-   * It returns null if no such term can be found.
-   * Wrt evaluateTerm, this version does not construct new terms, and
-   * thus is less aggressive.
-   */
-  TNode getEntailedTerm(TNode n);
-  /** get entailed term
-   *
-   * If possible, returns a term n' such that:
-   * (1) n' exists in the current equality engine (as specified by the state),
-   * (2) n * subs = n' is entailed in the current context, where * denotes
-   * substitution application.
-   * It returns null if no such term can be found.
-   * subsRep is whether the substitution maps to terms that are representatives
-   * according to the quantifiers state.
-   * Wrt evaluateTerm, this version does not construct new terms, and
-   * thus is less aggressive.
-   */
-  TNode getEntailedTerm(TNode n, std::map<TNode, TNode>& subs, bool subsRep);
-  /** is entailed
-   * Checks whether the current context entails n with polarity pol, based on
-   * the equality information in the quantifiers state. Returns true if the
-   * entailment can be successfully shown.
-   */
-  bool isEntailed(TNode n, bool pol);
-  /** is entailed
-   *
-   * Checks whether the current context entails ( n * subs ) with polarity pol,
-   * based on the equality information in the quantifiers state,
-   * where * denotes substitution application.
-   * subsRep is whether the substitution maps to terms that are representatives
-   * according to in the quantifiers state.
-   */
-  bool isEntailed(TNode n,
-                  std::map<TNode, TNode>& subs,
-                  bool subsRep,
-                  bool pol);
   /** is the term n active in the current context?
    *
   * By default, all terms are active. A term is inactive if:
@@ -355,24 +283,6 @@ class TermDb : public QuantifiersUtil {
   //----------------------------- end implementation-specific
   /** set has term */
   void setHasTerm( Node n );
-  /** helper for evaluate term */
-  Node evaluateTerm2(TNode n,
-                     std::map<TNode, Node>& visited,
-                     std::vector<Node>& exp,
-                     bool useEntailmentTests,
-                     bool computeExp,
-                     bool reqHasTerm);
-  /** helper for get entailed term */
-  TNode getEntailedTerm2(TNode n,
-                         std::map<TNode, TNode>& subs,
-                         bool subsRep,
-                         bool hasSubs);
-  /** helper for is entailed */
-  bool isEntailed2(TNode n,
-                   std::map<TNode, TNode>& subs,
-                   bool subsRep,
-                   bool hasSubs,
-                   bool pol);
   /** compute uf eqc terms :
   * Ensure entries for f are in d_func_map_eqc_trie for all equivalence classes
   */
diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp
index ab999ad9b..d11fb0b8d 100644
--- a/src/theory/quantifiers/term_registry.cpp
+++ b/src/theory/quantifiers/term_registry.cpp
@@ -18,6 +18,7 @@
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
+#include "theory/quantifiers/entailment_check.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fmf/first_order_model_fmc.h"
 #include "theory/quantifiers/ho_term_database.h"
@@ -39,6 +40,7 @@ TermRegistry::TermRegistry(Env& env,
       d_termPools(new TermPools(env, qs)),
       d_termDb(logicInfo().isHigherOrder() ? new HoTermDb(env, qs, qr)
                                            : new TermDb(env, qs, qr)),
+      d_echeck(new EntailmentCheck(env, qs, *d_termDb.get())),
       d_sygusTdb(nullptr),
       d_qmodel(nullptr)
 {
@@ -132,6 +134,11 @@ TermDbSygus* TermRegistry::getTermDatabaseSygus() const
   return d_sygusTdb.get();
 }
 
+EntailmentCheck* TermRegistry::getEntailmentCheck() const
+{
+  return d_echeck.get();
+}
+
 TermEnumeration* TermRegistry::getTermEnumeration() const
 {
   return d_termEnum.get();
diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h
index 175d450df..60a87a91f 100644
--- a/src/theory/quantifiers/term_registry.h
+++ b/src/theory/quantifiers/term_registry.h
@@ -23,6 +23,7 @@
 
 #include "context/cdhashset.h"
 #include "smt/env_obj.h"
+#include "theory/quantifiers/entailment_check.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_enumeration.h"
@@ -83,6 +84,8 @@ class TermRegistry : protected EnvObj
   TermDb* getTermDatabase() const;
   /** get term database sygus */
   TermDbSygus* getTermDatabaseSygus() const;
+  /** get entailment check utility */
+  EntailmentCheck* getEntailmentCheck() const;
   /** get term enumeration utility */
   TermEnumeration* getTermEnumeration() const;
   /** get the term pools utility */
@@ -103,6 +106,8 @@ class TermRegistry : protected EnvObj
   std::unique_ptr<TermPools> d_termPools;
   /** term database */
   std::unique_ptr<TermDb> d_termDb;
+  /** entailment check */
+  std::unique_ptr<EntailmentCheck> d_echeck;
   /** sygus term database */
   std::unique_ptr<TermDbSygus> d_sygusTdb;
   /** extended model object */