From 861dba0caea6c8bfa54bca58749323c4dbcfb282 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 14 Oct 2021 11:14:02 -0500
Subject: Fix quantifiers variable elimination for parametric datatypes (#7358)

Fixes #7353.
---
 src/theory/quantifiers/quantifiers_rewriter.cpp | 20 +++++++++++++++++---
 1 file changed, 17 insertions(+), 3 deletions(-)

(limited to 'src/theory/quantifiers')

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);
-- 
cgit v1.2.3


From 5c481b34eef5860d29ea1f2f62cea696fea01619 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 14 Oct 2021 14:15:29 -0500
Subject: Split entailment check from term database (#7342)

Towards addressing some bottlenecks on Facebook benchmarks.
---
 src/CMakeLists.txt                              |   2 +
 src/theory/quantifiers/conjecture_generator.cpp |   6 +-
 src/theory/quantifiers/ematching/ho_trigger.cpp |   4 +-
 src/theory/quantifiers/entailment_check.cpp     | 443 ++++++++++++++++++++++++
 src/theory/quantifiers/entailment_check.h       | 150 ++++++++
 src/theory/quantifiers/instantiate.cpp          |  10 +-
 src/theory/quantifiers/quant_conflict_find.cpp  |  30 +-
 src/theory/quantifiers/term_database.cpp        | 360 -------------------
 src/theory/quantifiers/term_database.h          |  90 -----
 src/theory/quantifiers/term_registry.cpp        |   7 +
 src/theory/quantifiers/term_registry.h          |   5 +
 11 files changed, 632 insertions(+), 475 deletions(-)
 create mode 100644 src/theory/quantifiers/entailment_check.cpp
 create mode 100644 src/theory/quantifiers/entailment_check.h

(limited to 'src/theory/quantifiers')

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 31dccdbc6..374c57726 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -805,6 +805,8 @@ libcvc5_add_sources(
   theory/quantifiers/ematching/trigger_trie.h
   theory/quantifiers/ematching/var_match_generator.cpp
   theory/quantifiers/ematching/var_match_generator.h
+  theory/quantifiers/entailment_check.cpp
+  theory/quantifiers/entailment_check.h
   theory/quantifiers/equality_query.cpp
   theory/quantifiers/equality_query.h
   theory/quantifiers/expr_miner.cpp
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 */
-- 
cgit v1.2.3


From 3e9e1c54ef54627e4f38094910effb32f6ad7cd2 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 20 Oct 2021 09:34:10 -0500
Subject: Do not make assumption about model for Boolean variables in FMF
 (#7407)

Fixes cases where models can be wrong for FMF with Boolean variables in the bodies of quantified formulas.

Fixes #6744, all benchmarks on that issue are fixed. This PR adds 2 of the regressions from that issue.
---
 src/theory/quantifiers/fmf/full_model_check.cpp         | 11 ++++++++---
 test/regress/CMakeLists.txt                             |  2 ++
 test/regress/regress1/fmf/issue6744-2-unc-bool-var.smt2 |  7 +++++++
 test/regress/regress1/fmf/issue6744-3-unc-bool-var.smt2 |  5 +++++
 4 files changed, 22 insertions(+), 3 deletions(-)
 create mode 100644 test/regress/regress1/fmf/issue6744-2-unc-bool-var.smt2
 create mode 100644 test/regress/regress1/fmf/issue6744-3-unc-bool-var.smt2

(limited to 'src/theory/quantifiers')

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/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index da6f4c3c9..d24150cf6 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1648,6 +1648,8 @@ set(regress_1_tests
   regress1/fmf/issue4225-univ-fun.smt2
   regress1/fmf/issue5738-dt-interp-finite.smt2
   regress1/fmf/issue6690-re-enum.smt2
+  regress1/fmf/issue6744-2-unc-bool-var.smt2
+  regress1/fmf/issue6744-3-unc-bool-var.smt2
   regress1/fmf/issue916-fmf-or.smt2
   regress1/fmf/jasmin-cdt-crash.smt2
   regress1/fmf/loopy_coda.smt2
diff --git a/test/regress/regress1/fmf/issue6744-2-unc-bool-var.smt2 b/test/regress/regress1/fmf/issue6744-2-unc-bool-var.smt2
new file mode 100644
index 000000000..024d5b6a3
--- /dev/null
+++ b/test/regress/regress1/fmf/issue6744-2-unc-bool-var.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL)
+(set-option :finite-model-find true)
+(set-info :status sat)
+(declare-fun v () Bool)
+(declare-fun v2 () Bool)
+(assert (exists ((q (Array Bool (Array Bool (Array Int Bool))))) (forall ((q3 (Array Bool (Array Bool (Array Int Bool))))) (xor v2 v2 v v2 (or v2 (not (= q3 q)))))))
+(check-sat)
diff --git a/test/regress/regress1/fmf/issue6744-3-unc-bool-var.smt2 b/test/regress/regress1/fmf/issue6744-3-unc-bool-var.smt2
new file mode 100644
index 000000000..eb0c35f68
--- /dev/null
+++ b/test/regress/regress1/fmf/issue6744-3-unc-bool-var.smt2
@@ -0,0 +1,5 @@
+(set-logic UFC)
+(set-info :status sat)
+(declare-fun v () Bool)
+(assert (and (forall ((q Bool)) (not (xor v (exists ((q Bool)) true) (and (not v) (not q)))))))
+(check-sat)
-- 
cgit v1.2.3


From b038b34584f37c40a6dc4a476e8f486cf6977b81 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 20 Oct 2021 11:14:50 -0500
Subject: Reimplement support for relational triggers (#7063)

This makes relational triggers its own kind of instantiation match generator. Future PRs will delete the code interleaved in the core InstMatchGenerator class for handling relational triggers.

This PR also fixes two issues related to how trigger techniques are combined:
(1) instantiation match generators that are generated as part of multi-triggers now are properly specialized (using getInstMatchGenerator),
(2) there was a bug with auto-generated triggers: when the first auto-generated trigger was generated that was already a user trigger, then we would ignore all other auto-generated triggers.

This is work towards finding a solution for the choice.move.hard Facebook benchmark, where relational-triggers appear to be a possible solution.
---
 src/CMakeLists.txt                                 |   2 +
 .../quantifiers/ematching/inst_match_generator.cpp |  14 ++-
 .../ematching/inst_strategy_e_matching.cpp         |  41 +++----
 .../ematching/relational_match_generator.cpp       | 125 +++++++++++++++++++++
 .../ematching/relational_match_generator.h         |  92 +++++++++++++++
 .../quantifiers/ematching/trigger_term_info.cpp    |  42 ++++++-
 .../quantifiers/ematching/trigger_term_info.h      |  16 ++-
 test/regress/CMakeLists.txt                        |   2 +
 test/regress/regress0/quantifiers/veqt-delta.smt2  |   8 ++
 .../quantifiers/choice-move-delta-relt.smt2        |   6 +
 10 files changed, 325 insertions(+), 23 deletions(-)
 create mode 100644 src/theory/quantifiers/ematching/relational_match_generator.cpp
 create mode 100644 src/theory/quantifiers/ematching/relational_match_generator.h
 create mode 100644 test/regress/regress0/quantifiers/veqt-delta.smt2
 create mode 100644 test/regress/regress1/quantifiers/choice-move-delta-relt.smt2

(limited to 'src/theory/quantifiers')

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index cde739454..a2b5966e1 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -795,6 +795,8 @@ libcvc5_add_sources(
   theory/quantifiers/ematching/instantiation_engine.h
   theory/quantifiers/ematching/pattern_term_selector.cpp
   theory/quantifiers/ematching/pattern_term_selector.h
+  theory/quantifiers/ematching/relational_match_generator.cpp
+  theory/quantifiers/ematching/relational_match_generator.h
   theory/quantifiers/ematching/trigger.cpp
   theory/quantifiers/ematching/trigger.h
   theory/quantifiers/ematching/trigger_database.cpp
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/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d24150cf6..6dafe6852 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -971,6 +971,7 @@ set(regress_0_tests
   regress0/quantifiers/simp-len.smt2
   regress0/quantifiers/simp-typ-test.smt2
   regress0/quantifiers/ufnia-fv-delta.smt2
+  regress0/quantifiers/veqt-delta.smt2
   regress0/rec-fun-const-parse-bug.smt2
   regress0/rels/addr_book_0.cvc.smt2
   regress0/rels/atom_univ2.cvc.smt2
@@ -1857,6 +1858,7 @@ set(regress_1_tests
   regress1/quantifiers/cee-npnt-dd.smt2
   regress1/quantifiers/cee-os-delta.smt2
   regress1/quantifiers/cdt-0208-to.smt2
+  regress1/quantifiers/choice-move-delta-relt.smt2
   regress1/quantifiers/const.cvc.smt2
   regress1/quantifiers/constfunc.cvc.smt2
   regress1/quantifiers/ddatv-delta2.smt2
diff --git a/test/regress/regress0/quantifiers/veqt-delta.smt2 b/test/regress/regress0/quantifiers/veqt-delta.smt2
new file mode 100644
index 000000000..dfac015c6
--- /dev/null
+++ b/test/regress/regress0/quantifiers/veqt-delta.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --relational-triggers
+; EXPECT: unsat
+(set-logic ALL)
+(declare-sort S 0)
+(declare-fun f () S)
+(assert (forall ((? S)) (= ? f)))
+(assert (exists ((? S) (v S)) (distinct ? v)))
+(check-sat)
diff --git a/test/regress/regress1/quantifiers/choice-move-delta-relt.smt2 b/test/regress/regress1/quantifiers/choice-move-delta-relt.smt2
new file mode 100644
index 000000000..a8fd0d498
--- /dev/null
+++ b/test/regress/regress1/quantifiers/choice-move-delta-relt.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --relational-triggers --user-pat=use
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun F (Int) Bool)
+(assert (forall ((v Int)) (! (= (F 0) (< v 0)) :qid |outputbpl.194:24| :pattern ((F 0)))))
+(check-sat)
-- 
cgit v1.2.3


From 51e438df97e12b7c893827fe36aca3832e3e1a07 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 20 Oct 2021 15:34:33 -0500
Subject: Do not construct instantiation for checking propagating
 instantiations spurious (#7390)

This makes the check for when an instantiation is "propagating" faster by not constructing the substitution + rewriting of the entire formula, and instead threading the substitution through the entailment check utility's evaluateTerm utility.

On a handful of challenge Facebook benchmarks, we go 35 seconds -> 18 seconds with this change.

This also eliminates the argument exp to the evaluateTerm method, which is no longer used, and eliminates hasSubs from several methods, which is redundant.
---
 src/theory/quantifiers/entailment_check.cpp    | 156 ++++++++++---------------
 src/theory/quantifiers/entailment_check.h      |  40 ++++---
 src/theory/quantifiers/quant_conflict_find.cpp |  43 +++----
 src/theory/quantifiers/quant_conflict_find.h   |   2 -
 4 files changed, 107 insertions(+), 134 deletions(-)

(limited to 'src/theory/quantifiers')

diff --git a/src/theory/quantifiers/entailment_check.cpp b/src/theory/quantifiers/entailment_check.cpp
index f27e14121..543414a4e 100644
--- a/src/theory/quantifiers/entailment_check.cpp
+++ b/src/theory/quantifiers/entailment_check.cpp
@@ -33,11 +33,12 @@ EntailmentCheck::EntailmentCheck(Env& env, QuantifiersState& qs, TermDb& tdb)
 }
 
 EntailmentCheck::~EntailmentCheck() {}
+
 Node EntailmentCheck::evaluateTerm2(TNode n,
                                     std::map<TNode, Node>& visited,
-                                    std::vector<Node>& exp,
+                                    std::map<TNode, TNode>& subs,
+                                    bool subsRep,
                                     bool useEntailmentTests,
-                                    bool computeExp,
                                     bool reqHasTerm)
 {
   std::map<TNode, Node>::iterator itv = visited.find(n);
@@ -45,36 +46,43 @@ Node EntailmentCheck::evaluateTerm2(TNode n,
   {
     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)
+  Kind k = n.getKind();
+  if (k == FORALL)
   {
     // do nothing
   }
-  else if (d_qstate.hasTerm(n))
+  else if (k == BOUND_VARIABLE)
   {
-    Trace("term-db-eval") << "...exists in ee, return rep" << std::endl;
-    ret = d_qstate.getRepresentative(n);
-    if (computeExp)
+    std::map<TNode, TNode>::iterator it = subs.find(n);
+    if (it != subs.end())
     {
-      if (n != ret)
+      if (!subsRep)
       {
-        exp.push_back(n.eqNode(ret));
+        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;
-    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);
+          n[i], visited, subs, subsRep, useEntailmentTests, reqHasTerm);
       if (c.isNull())
       {
         ret = Node::null();
@@ -95,32 +103,19 @@ Node EntailmentCheck::evaluateTerm2(TNode n,
         {
           ret = evaluateTerm2(n[c == d_true ? 1 : 2],
                               visited,
-                              tempExp,
+                              subs,
+                              subsRep,
                               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
+    if (!ret_set)
     {
       // get the (indexed) operator of n, if it exists
       TNode f = d_tdb.getMatchOperator(n);
@@ -133,29 +128,11 @@ Node EntailmentCheck::evaluateTerm2(TNode n,
                               << " 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)
@@ -188,10 +165,6 @@ Node EntailmentCheck::evaluateTerm2(TNode n,
               if (et.first)
               {
                 ret = j == 0 ? d_true : d_false;
-                if (computeExp)
-                {
-                  exp.push_back(et.second);
-                }
                 break;
               }
             }
@@ -203,9 +176,9 @@ Node EntailmentCheck::evaluateTerm2(TNode n,
   // 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)
+    Kind rk = ret.getKind();
+    if (rk != OR && rk != AND && rk != EQUAL && rk != ITE && rk != NOT
+        && rk != FORALL)
     {
       if (!d_qstate.hasTerm(ret))
       {
@@ -215,19 +188,13 @@ Node EntailmentCheck::evaluateTerm2(TNode n,
   }
   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)
+                                        bool subsRep)
 {
   Trace("term-db-entail") << "get entailed term : " << n << std::endl;
   if (d_qstate.hasTerm(n))
@@ -237,30 +204,27 @@ TNode EntailmentCheck::getEntailedTerm2(TNode n,
   }
   else if (n.getKind() == BOUND_VARIABLE)
   {
-    if (hasSubs)
+    std::map<TNode, TNode>::iterator it = subs.find(n);
+    if (it != subs.end())
     {
-      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)
       {
-        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);
+        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, hasSubs, i == 0))
+      if (isEntailed2(n[0], subs, subsRep, i == 0))
       {
-        return getEntailedTerm2(n[i == 0 ? 1 : 2], subs, subsRep, hasSubs);
+        return getEntailedTerm2(n[i == 0 ? 1 : 2], subs, subsRep);
       }
     }
   }
@@ -274,7 +238,7 @@ TNode EntailmentCheck::getEntailedTerm2(TNode n,
         std::vector<TNode> args;
         for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
         {
-          TNode c = getEntailedTerm2(n[i], subs, subsRep, hasSubs);
+          TNode c = getEntailedTerm2(n[i], subs, subsRep);
           if (c.isNull())
           {
             return TNode::null();
@@ -294,48 +258,52 @@ TNode EntailmentCheck::getEntailedTerm2(TNode n,
 }
 
 Node EntailmentCheck::evaluateTerm(TNode n,
+                                   std::map<TNode, TNode>& subs,
+                                   bool subsRep,
                                    bool useEntailmentTests,
                                    bool reqHasTerm)
 {
   std::map<TNode, Node> visited;
-  std::vector<Node> exp;
-  return evaluateTerm2(n, visited, exp, useEntailmentTests, false, reqHasTerm);
+  return evaluateTerm2(
+      n, visited, subs, subsRep, useEntailmentTests, 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);
+  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, true);
+  return getEntailedTerm2(n, subs, subsRep);
 }
 
 TNode EntailmentCheck::getEntailedTerm(TNode n)
 {
   std::map<TNode, TNode> subs;
-  return getEntailedTerm2(n, subs, false, false);
+  return getEntailedTerm2(n, subs, false);
 }
 
-bool EntailmentCheck::isEntailed2(
-    TNode n, std::map<TNode, TNode>& subs, bool subsRep, bool hasSubs, bool pol)
+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, hasSubs);
+    TNode n1 = getEntailedTerm2(n[0], subs, subsRep);
     if (!n1.isNull())
     {
-      TNode n2 = getEntailedTerm2(n[1], subs, subsRep, hasSubs);
+      TNode n2 = getEntailedTerm2(n[1], subs, subsRep);
       if (!n2.isNull())
       {
         if (n1 == n2)
@@ -360,14 +328,14 @@ bool EntailmentCheck::isEntailed2(
   }
   else if (n.getKind() == NOT)
   {
-    return isEntailed2(n[0], subs, subsRep, hasSubs, !pol);
+    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, hasSubs, pol))
+      if (isEntailed2(n[i], subs, subsRep, pol))
       {
         if (simPol)
         {
@@ -389,17 +357,17 @@ bool EntailmentCheck::isEntailed2(
   {
     for (size_t i = 0; i < 2; i++)
     {
-      if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0))
+      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, hasSubs, reqPol);
+        return isEntailed2(n[ch], subs, subsRep, reqPol);
       }
     }
   }
   else if (n.getKind() == APPLY_UF)
   {
-    TNode n1 = getEntailedTerm2(n, subs, subsRep, hasSubs);
+    TNode n1 = getEntailedTerm2(n, subs, subsRep);
     if (!n1.isNull())
     {
       Assert(d_qstate.hasTerm(n1));
@@ -419,7 +387,7 @@ bool EntailmentCheck::isEntailed2(
   }
   else if (n.getKind() == FORALL && !pol)
   {
-    return isEntailed2(n[1], subs, subsRep, hasSubs, pol);
+    return isEntailed2(n[1], subs, subsRep, pol);
   }
   return false;
 }
@@ -427,7 +395,7 @@ bool EntailmentCheck::isEntailed2(
 bool EntailmentCheck::isEntailed(TNode n, bool pol)
 {
   std::map<TNode, TNode> subs;
-  return isEntailed2(n, subs, false, false, pol);
+  return isEntailed2(n, subs, false, pol);
 }
 
 bool EntailmentCheck::isEntailed(TNode n,
@@ -435,7 +403,7 @@ bool EntailmentCheck::isEntailed(TNode n,
                                  bool subsRep,
                                  bool pol)
 {
-  return isEntailed2(n, subs, subsRep, true, pol);
+  return isEntailed2(n, subs, subsRep, pol);
 }
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/entailment_check.h b/src/theory/quantifiers/entailment_check.h
index 5f0af60a6..ecf74fe85 100644
--- a/src/theory/quantifiers/entailment_check.h
+++ b/src/theory/quantifiers/entailment_check.h
@@ -44,19 +44,18 @@ class EntailmentCheck : protected EnvObj
   ~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.
+   * 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.
    *
-   * 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
@@ -64,12 +63,23 @@ class EntailmentCheck : protected EnvObj
    * 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::vector<Node>& exp,
+                    std::map<TNode, TNode>& subs,
+                    bool subsRep,
                     bool useEntailmentTests = false,
                     bool reqHasTerm = false);
-  /** same as above, without exp */
+  /** Same as above, without a substitution */
   Node evaluateTerm(TNode n,
                     bool useEntailmentTests = false,
                     bool reqHasTerm = false);
@@ -119,20 +129,16 @@ class EntailmentCheck : protected EnvObj
   /** helper for evaluate term */
   Node evaluateTerm2(TNode n,
                      std::map<TNode, Node>& visited,
-                     std::vector<Node>& exp,
+                     std::map<TNode, TNode>& subs,
+                     bool subsRep,
                      bool useEntailmentTests,
-                     bool computeExp,
                      bool reqHasTerm);
   /** helper for get entailed term */
-  TNode getEntailedTerm2(TNode n,
-                         std::map<TNode, TNode>& subs,
-                         bool subsRep,
-                         bool hasSubs);
+  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 hasSubs,
                    bool pol);
   /** The quantifiers state object */
   QuantifiersState& d_qstate;
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index dc1043d28..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;
@@ -578,29 +572,32 @@ 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];
-      }
-      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 (!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 =
-          echeck->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>()))
       {
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;
-- 
cgit v1.2.3


From 628a13f0e5f95fb3372c0676e91a9e719fa05b8c Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 20 Oct 2021 15:47:06 -0500
Subject: Make SyGuS solver robust to non-closed enumerable sorts (#7417)

This makes the SyGuS solver robust to variables that are not closed enumerable, e.g. arrays of uninterpreted sorts.

It corrects an issue in array's mkGroundTerm issue which would allow constants to enter into constraints for SyGuS problems with arrays. This method does not cause further issues currently since quantifiers is guarded in several places to ensure array constants are not constructed via this method.

It also makes it so that we don't add explicit CEGIS refinement lemmas unless evaluation unfolding is enabled and the counterexamples are from closed enumerable types; there is no reason to add these unless we are combining with evaluation unfolding.

This addresses several of the issues raised in #6605.
---
 src/theory/arrays/theory_arrays_type_rules.cpp     | 20 +++++++++++++++-
 src/theory/quantifiers/sygus/cegis.cpp             | 28 +++++++++++++++-------
 src/theory/quantifiers/sygus/cegis.h               |  7 ++++++
 .../quantifiers/sygus/sygus_grammar_cons.cpp       |  3 +++
 test/regress/CMakeLists.txt                        |  1 +
 test/regress/regress1/sygus/array-uc.sy            | 14 +++++++++++
 6 files changed, 64 insertions(+), 9 deletions(-)
 create mode 100644 test/regress/regress1/sygus/array-uc.sy

(limited to 'src/theory/quantifiers')

diff --git a/src/theory/arrays/theory_arrays_type_rules.cpp b/src/theory/arrays/theory_arrays_type_rules.cpp
index e1b4813ec..433768e5d 100644
--- a/src/theory/arrays/theory_arrays_type_rules.cpp
+++ b/src/theory/arrays/theory_arrays_type_rules.cpp
@@ -18,6 +18,7 @@
 // for array-constant attributes
 #include "expr/array_store_all.h"
 #include "theory/arrays/theory_arrays_rewriter.h"
+#include "theory/builtin/theory_builtin_type_rules.h"
 #include "theory/type_enumerator.h"
 #include "util/cardinality.h"
 
@@ -249,7 +250,24 @@ bool ArraysProperties::isWellFounded(TypeNode type)
 
 Node ArraysProperties::mkGroundTerm(TypeNode type)
 {
-  return *TypeEnumerator(type);
+  Assert(type.getKind() == kind::ARRAY_TYPE);
+  TypeNode elemType = type.getArrayConstituentType();
+  Node elem = elemType.mkGroundTerm();
+  if (elem.isConst())
+  {
+    return NodeManager::currentNM()->mkConst(ArrayStoreAll(type, elem));
+  }
+  // Note the distinction between mkGroundTerm and mkGroundValue. While
+  // an arbitrary value can be obtained by calling the type enumerator here,
+  // that is wrong for types that are not closed enumerable since it may
+  // return a term containing values that should not appear in e.g. assertions.
+  // For example, arrays whose element type is an uninterpreted sort will
+  // incorrectly introduce uninterpreted sort values if this is done.
+  // It is currently infeasible to construct an ArrayStoreAll with the element
+  // type's mkGroundTerm as an argument when that term is not constant.
+  // Thus, we must simply return a fresh Skolem here, using the same utility
+  // as that of uninterpreted sorts.
+  return builtin::SortProperties::mkGroundTerm(type);
 }
 
 TypeNode ArrayPartialSelectTypeRule::computeType(NodeManager* nodeManager,
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/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 6dafe6852..0f7b19e47 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2314,6 +2314,7 @@ set(regress_1_tests
   regress1/sygus/abv.sy
   regress1/sygus/array-grammar-store.sy
   regress1/sygus/array_search_5-Q-easy.sy
+  regress1/sygus/array-uc.sy
   regress1/sygus/bvudiv-by-2.sy
   regress1/sygus/cegar1.sy
   regress1/sygus/cegis-unif-inv-eq-fair.sy
diff --git a/test/regress/regress1/sygus/array-uc.sy b/test/regress/regress1/sygus/array-uc.sy
new file mode 100644
index 000000000..b3d950436
--- /dev/null
+++ b/test/regress/regress1/sygus/array-uc.sy
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --sygus-out=status
+; EXPECT: unsat
+(set-logic ALL)
+(declare-sort U 0)
+(synth-fun f ((x (Array U Int)) (y U)) Bool)
+
+(declare-var x (Array U Int))
+(declare-var y U)
+
+(constraint (= (f (store x y 0) y) true))
+(constraint (= (f (store x y 1) y) false))
+
+; f can be (= (select x y) 0)
+(check-synth)
-- 
cgit v1.2.3