Split entailment check from term database (#7342)

Towards addressing some bottlenecks on Facebook benchmarks.

10 files changed, 630 insertions, 475 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/entailment_check.cpp b/src/theory/quantifiers/entailment_check.cpp
new file mode 100644
index 000000000..f27e14121
--- /dev/null
+++ b/src/theory/quantifiers/entailment_check.cpp
@@ -0,0 +1,443 @@
+/******************************************************************************
+ * 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::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 = 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())
+        {
+          if (computeExp)
+          {
+            Assert(nn.getNumChildren() == n.getNumChildren());
+            for (size_t 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 EntailmentCheck::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 (uint32_t 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 = 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, 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 = 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,
+                                   bool useEntailmentTests,
+                                   bool reqHasTerm)
+{
+  std::map<TNode, Node> visited;
+  std::vector<Node> exp;
+  return evaluateTerm2(n, visited, exp, useEntailmentTests, false, reqHasTerm);
+}
+
+Node EntailmentCheck::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 EntailmentCheck::getEntailedTerm(TNode n,
+                                       std::map<TNode, TNode>& subs,
+                                       bool subsRep)
+{
+  return getEntailedTerm2(n, subs, subsRep, true);
+}
+
+TNode EntailmentCheck::getEntailedTerm(TNode n)
+{
+  std::map<TNode, TNode> subs;
+  return getEntailedTerm2(n, subs, false, false);
+}
+
+bool EntailmentCheck::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 (size_t i = 0, nchild = n.getNumChildren(); i < nchild; 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 (size_t i = 0; i < 2; i++)
+    {
+      if (isEntailed2(n[0], subs, subsRep, hasSubs, 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, 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 EntailmentCheck::isEntailed(TNode n, bool pol)
+{
+  std::map<TNode, TNode> subs;
+  return isEntailed2(n, subs, false, false, pol);
+}
+
+bool EntailmentCheck::isEntailed(TNode n,
+                                 std::map<TNode, TNode>& subs,
+                                 bool subsRep,
+                                 bool pol)
+{
+  return isEntailed2(n, subs, subsRep, true, 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..5f0af60a6
--- /dev/null
+++ b/src/theory/quantifiers/entailment_check.h
@@ -0,0 +1,150 @@
+/******************************************************************************
+ * 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 = 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);
+
+ protected:
+  /** 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);
+  /** 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/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..dc1043d28 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -577,6 +577,7 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p,
 {
   if( options::qcfEagerTest() ){
     //check whether the instantiation evaluates as expected
+    EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck();
     if (p->atConflictEffort()) {
       Trace("qcf-instance-check") << "Possible conflict instance for " << d_q << " : " << std::endl;
       std::map< TNode, TNode > subs;
@@ -584,13 +585,12 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p,
         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;
@@ -599,8 +599,8 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p,
       Node inst =
           getInferenceManager().getInstantiate()->getInstantiation(d_q, terms);
       inst = Rewriter::rewrite(inst);
-      Node inst_eval = p->getTermDatabase()->evaluateTerm(
-          inst, options::qcfTConstraint(), true);
+      Node inst_eval =
+          echeck->evaluateTerm(inst, 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++ ){
@@ -1219,11 +1219,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 +1233,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 +1289,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 +2164,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/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 */