Do not eliminate variables that are equal to unevaluatable terms (#4267)

When we eliminate a variable x -> v during simplification, it may be the case that v contains "unevaluated" operators like forall, choice, etc. Thus, we do not produce correct models for such inputs unless simplification is disabled.

This PR ensures we only eliminate variables when v contains only evaluated operators.

Additionally, the kinds registered as unevaluated were slightly modified so that when we are in a logic like QF_LIA, there are no registered unevaluated operators, hence the check above is unnecessary. This is to minimize the performance impact of this change.

Fixes #4500.

18 files changed, 182 insertions, 86 deletions

diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index 0c572f615..44430f072 100644
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -155,6 +155,34 @@ bool hasSubtermKind(Kind k, Node n)
   return false;
 }
 
+bool hasSubtermKinds(const std::unordered_set<Kind, kind::KindHashFunction>& ks,
+                     Node n)
+{
+  if (ks.empty())
+  {
+    return false;
+  }
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    if (visited.find(cur) == visited.end())
+    {
+      if (ks.find(cur.getKind()) != ks.end())
+      {
+        return true;
+      }
+      visited.insert(cur);
+      visit.insert(visit.end(), cur.begin(), cur.end());
+    }
+  } while (!visit.empty());
+  return false;
+}
+
 bool hasSubterm(TNode n, const std::vector<Node>& t, bool strict)
 {
   if (t.empty())
diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h
index 5e042d591..894dce7c6 100644
--- a/src/expr/node_algorithm.h
+++ b/src/expr/node_algorithm.h
@@ -52,6 +52,14 @@ bool hasSubtermMulti(TNode n, TNode t);
 bool hasSubtermKind(Kind k, Node n);
 
 /**
+ * @param ks The kinds of node to check
+ * @param n The node to search in.
+ * @return true iff there is a term in n that has any kind ks
+ */
+bool hasSubtermKinds(const std::unordered_set<Kind, kind::KindHashFunction>& ks,
+                     Node n);
+
+/**
  * Check if the node n has a subterm that occurs in t.
  * @param n The node to search in
  * @param t The set of subterms to search for
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index cdb6c77f3..e65369f96 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -63,6 +63,18 @@ void TheoryArith::preRegisterTerm(TNode n){
   d_internal->preRegisterTerm(n);
 }
 
+void TheoryArith::finishInit()
+{
+  TheoryModel* tm = d_valuation.getModel();
+  Assert(tm != nullptr);
+  if (getLogicInfo().isTheoryEnabled(THEORY_ARITH)
+      && getLogicInfo().areTranscendentalsUsed())
+  {
+    // witness is used to eliminate square root
+    tm->setUnevaluatedKind(kind::WITNESS);
+  }
+}
+
 Node TheoryArith::expandDefinition(Node node)
 {
   return d_internal->expandDefinition(node);
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index f15db32a1..8672f7145 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -58,6 +58,8 @@ public:
    */
   void preRegisterTerm(TNode n) override;
 
+  void finishInit() override;
+
   Node expandDefinition(Node node) override;
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 0f2f4bbf4..7fdab2034 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -1337,7 +1337,8 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert(TNode in, SubstitutionMap& o
     if (m.getVarList().singleton()){
       VarList vl = m.getVarList();
       Node var = vl.getNode();
-      if (var.getKind() == kind::VARIABLE){
+      if (var.isVar())
+      {
         // if vl.isIntegral then m.getConstant().isOne()
         if(!vl.isIntegral() || m.getConstant().isOne()){
           minVar = var;
@@ -1362,15 +1363,8 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert(TNode in, SubstitutionMap& o
             << minVar << ":" << elim << endl;
         Debug("simplify") << right.size() << endl;
       }
-      else if (expr::hasSubterm(elim, minVar))
-      {
-        Debug("simplify") << "TheoryArithPrivate::solve(): can't substitute "
-                             "due to recursive pattern with sharing: "
-                          << minVar << ":" << elim << endl;
-      }
-      else if (!minVar.getType().isInteger() || right.isIntegral())
+      else if (d_containing.isLegalElimination(minVar, elim))
       {
-        Assert(!expr::hasSubterm(elim, minVar));
         // cannot eliminate integers here unless we know the resulting
         // substitution is integral
         Debug("simplify") << "TheoryArithPrivate::solve(): substitution "
@@ -1382,7 +1376,6 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert(TNode in, SubstitutionMap& o
       else
       {
         Debug("simplify") << "TheoryArithPrivate::solve(): can't substitute "
-                             "b/c it's integer: "
                           << minVar << ":" << minVar.getType() << " |-> "
                           << elim << ":" << elim.getType() << endl;
       }
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index e4b1e1c4c..5085c00ec 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -355,14 +355,12 @@ Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubs
     {
       d_ppFacts.push_back(in);
       d_ppEqualityEngine.assertEquality(in, true, in);
-      if (in[0].isVar() && !expr::hasSubterm(in[1], in[0])
-          && (in[1].getType()).isSubtypeOf(in[0].getType()))
+      if (in[0].isVar() && isLegalElimination(in[0], in[1]))
       {
         outSubstitutions.addSubstitution(in[0], in[1]);
         return PP_ASSERT_STATUS_SOLVED;
       }
-      if (in[1].isVar() && !expr::hasSubterm(in[0], in[1])
-          && (in[0].getType()).isSubtypeOf(in[1].getType()))
+      if (in[1].isVar() && isLegalElimination(in[1], in[0]))
       {
         outSubstitutions.addSubstitution(in[1], in[0]);
         return PP_ASSERT_STATUS_SOLVED;
diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index 1667e5505..a49903f13 100644
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -43,10 +43,13 @@ std::string TheoryBuiltin::identify() const
 
 void TheoryBuiltin::finishInit()
 {
-  // choice nodes are not evaluated in getModelValue
-  TheoryModel* theoryModel = d_valuation.getModel();
-  Assert(theoryModel != nullptr);
-  theoryModel->setUnevaluatedKind(kind::WITNESS);
+  // Notice that choice is an unevaluated kind belonging to this theory.
+  // However, it should be set as an unevaluated kind where it is used, e.g.
+  // in the quantifiers theory. This ensures that a logic like QF_LIA, which
+  // includes the builtin theory, does not mark any kinds as unevaluated and
+  // hence it is easy to check for illegal eliminations via TheoryModel
+  // (see TheoryModel::isLegalElimination) since there are no unevaluated kinds
+  // present.
 }
 
 }  // namespace builtin
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 32791415e..fd8459641 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -634,13 +634,13 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in,
   {
     case kind::EQUAL:
     {
-      if (in[0].isVar() && !expr::hasSubterm(in[1], in[0]))
+      if (in[0].isVar() && isLegalElimination(in[0], in[1]))
       {
         ++(d_statistics.d_solveSubstitutions);
         outSubstitutions.addSubstitution(in[0], in[1]);
         return PP_ASSERT_STATUS_SOLVED;
       }
-      if (in[1].isVar() && !expr::hasSubterm(in[0], in[1]))
+      if (in[1].isVar() && isLegalElimination(in[1], in[0]))
       {
         ++(d_statistics.d_solveSubstitutions);
         outSubstitutions.addSubstitution(in[1], in[0]);
@@ -652,7 +652,7 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in,
               && node[0].isConst()))
       {
         Node extract = node[0].isConst() ? node[1] : node[0];
-        if (extract[0].getKind() == kind::VARIABLE)
+        if (extract[0].isVar())
         {
           Node c = node[0].isConst() ? node[0] : node[1];
 
@@ -688,8 +688,11 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in,
           }
           Node concat = utils::mkConcat(children);
           Assert(utils::getSize(concat) == utils::getSize(extract[0]));
-          outSubstitutions.addSubstitution(extract[0], concat);
-          return PP_ASSERT_STATUS_SOLVED;
+          if (isLegalElimination(extract[0], concat))
+          {
+            outSubstitutions.addSubstitution(extract[0], concat);
+            return PP_ASSERT_STATUS_SOLVED;
+          }
         }
       }
     }
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 6407e0d6d..9242bec7c 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -58,6 +58,8 @@ void TheoryQuantifiers::finishInit()
   Assert(tm != nullptr);
   tm->setUnevaluatedKind(EXISTS);
   tm->setUnevaluatedKind(FORALL);
+  // witness is used in several instantiation strategies
+  tm->setUnevaluatedKind(WITNESS);
 }
 
 void TheoryQuantifiers::preRegisterTerm(TNode n) {
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 8430987f2..b5c2590d5 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -56,6 +56,8 @@ void TheorySets::finishInit()
   TheoryModel* tm = d_valuation.getModel();
   Assert(tm != nullptr);
   tm->setUnevaluatedKind(COMPREHENSION);
+  // choice is used to eliminate witness
+  tm->setUnevaluatedKind(WITNESS);
 }
 
 void TheorySets::addSharedTerm(TNode n) {
@@ -123,7 +125,41 @@ Node TheorySets::expandDefinition(Node n)
 }
 
 Theory::PPAssertStatus TheorySets::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
-  return d_internal->ppAssert( in, outSubstitutions );
+  Debug("sets-proc") << "ppAssert : " << in << std::endl;
+  Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED;
+
+  // this is based off of Theory::ppAssert
+  if (in.getKind() == kind::EQUAL)
+  {
+    if (in[0].isVar() && isLegalElimination(in[0], in[1]))
+    {
+      // We cannot solve for sets if setsExt is enabled, since universe set
+      // may appear when this option is enabled, and solving for such a set
+      // impacts the semantics of universe set, see
+      // regress0/sets/pre-proc-univ.smt2
+      if (!in[0].getType().isSet() || !options::setsExt())
+      {
+        outSubstitutions.addSubstitution(in[0], in[1]);
+        status = Theory::PP_ASSERT_STATUS_SOLVED;
+      }
+    }
+    else if (in[1].isVar() && isLegalElimination(in[1], in[0]))
+    {
+      if (!in[0].getType().isSet() || !options::setsExt())
+      {
+        outSubstitutions.addSubstitution(in[1], in[0]);
+        status = Theory::PP_ASSERT_STATUS_SOLVED;
+      }
+    }
+    else if (in[0].isConst() && in[1].isConst())
+    {
+      if (in[0] != in[1])
+      {
+        status = Theory::PP_ASSERT_STATUS_CONFLICT;
+      }
+    }
+  }
+  return status;
 }
 
 void TheorySets::presolve() {
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index fbf1e6fcf..78f6fa8b5 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1536,46 +1536,6 @@ Node TheorySetsPrivate::getChooseFunction(const TypeNode& setType)
   return chooseSkolem;
 }
 
-Theory::PPAssertStatus TheorySetsPrivate::ppAssert(
-    TNode in, SubstitutionMap& outSubstitutions)
-{
-  Debug("sets-proc") << "ppAssert : " << in << std::endl;
-  Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED;
-
-  // TODO: allow variable elimination for sets when setsExt = true
-
-  // this is based off of Theory::ppAssert
-  if (in.getKind() == kind::EQUAL)
-  {
-    if (in[0].isVar() && !expr::hasSubterm(in[1], in[0])
-        && (in[1].getType()).isSubtypeOf(in[0].getType()))
-    {
-      if (!in[0].getType().isSet() || !options::setsExt())
-      {
-        outSubstitutions.addSubstitution(in[0], in[1]);
-        status = Theory::PP_ASSERT_STATUS_SOLVED;
-      }
-    }
-    else if (in[1].isVar() && !expr::hasSubterm(in[0], in[1])
-             && (in[0].getType()).isSubtypeOf(in[1].getType()))
-    {
-      if (!in[1].getType().isSet() || !options::setsExt())
-      {
-        outSubstitutions.addSubstitution(in[1], in[0]);
-        status = Theory::PP_ASSERT_STATUS_SOLVED;
-      }
-    }
-    else if (in[0].isConst() && in[1].isConst())
-    {
-      if (in[0] != in[1])
-      {
-        status = Theory::PP_ASSERT_STATUS_CONFLICT;
-      }
-    }
-  }
-  return status;
-}
-
 void TheorySetsPrivate::presolve() { d_state.reset(); }
 
 /**************************** eq::NotifyClass *****************************/
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index a7e6f69ee..da42ad1fe 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -210,8 +210,6 @@ class TheorySetsPrivate {
    * so that it makes theory-specific calls to evaluate interpreted symbols.
    */
   Node expandDefinition(Node n);
-
-  Theory::PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
   
   void presolve();
 
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index b98bd1dea..6f3b4c0cb 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -135,6 +135,13 @@ TheoryStrings::~TheoryStrings() {
 
 }
 
+void TheoryStrings::finishInit()
+{
+  TheoryModel* tm = d_valuation.getModel();
+  // witness is used to eliminate str.from_code
+  tm->setUnevaluatedKind(WITNESS);
+}
+
 bool TheoryStrings::areCareDisequal( TNode x, TNode y ) {
   Assert(d_equalityEngine.hasTerm(x));
   Assert(d_equalityEngine.hasTerm(y));
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 2e78198e3..7c99b6968 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -108,6 +108,9 @@ class TheoryStrings : public Theory {
                 const LogicInfo& logicInfo);
   ~TheoryStrings();
 
+  /** finish initialization */
+  void finishInit() override;
+
   TheoryRewriter* getTheoryRewriter() override { return &d_rewriter; }
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 635a3216a..3069461fa 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -268,6 +268,28 @@ void Theory::debugPrintFacts() const{
   printFacts(DebugChannel.getStream());
 }
 
+bool Theory::isLegalElimination(TNode x, TNode val)
+{
+  Assert(x.isVar());
+  if (expr::hasSubterm(val, x))
+  {
+    return false;
+  }
+  if (!val.getType().isSubtypeOf(x.getType()))
+  {
+    return false;
+  }
+  if (!options::produceModels())
+  {
+    // don't care about the model, we are fine
+    return true;
+  }
+  // if there is a model object
+  TheoryModel* tm = d_valuation.getModel();
+  Assert(tm != nullptr);
+  return tm->isLegalElimination(x, val);
+}
+
 std::unordered_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{
   std::unordered_set<TNode, TNodeHashFunction> currentlyShared;
   for (shared_terms_iterator i = shared_terms_begin(),
@@ -337,15 +359,13 @@ Theory::PPAssertStatus Theory::ppAssert(TNode in,
     // 1) x is a variable
     // 2) x is not in the term t
     // 3) x : T and t : S, then S <: T
-    if (in[0].isVar() && !expr::hasSubterm(in[1], in[0])
-        && (in[1].getType()).isSubtypeOf(in[0].getType())
+    if (in[0].isVar() && isLegalElimination(in[0], in[1])
         && in[0].getKind() != kind::BOOLEAN_TERM_VARIABLE)
     {
       outSubstitutions.addSubstitution(in[0], in[1]);
       return PP_ASSERT_STATUS_SOLVED;
     }
-    if (in[1].isVar() && !expr::hasSubterm(in[0], in[1])
-        && (in[0].getType()).isSubtypeOf(in[1].getType())
+    if (in[1].isVar() && isLegalElimination(in[1], in[0])
         && in[1].getKind() != kind::BOOLEAN_TERM_VARIABLE)
     {
       outSubstitutions.addSubstitution(in[1], in[0]);
diff --git a/src/theory/theory.h b/src/theory/theory.h
index c777f164f..366a943ef 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -248,8 +248,24 @@ class Theory {
   void printFacts(std::ostream& os) const;
   void debugPrintFacts() const;
 
-public:
+  /** is legal elimination
+   *
+   * Returns true if x -> val is a legal elimination of variable x. This is
+   * useful for ppAssert, when x = val is an entailed equality. This function
+   * determines whether indeed x can be eliminated from the problem via the
+   * substituion x -> val.
+   *
+   * The following criteria imply that x -> val is *not* a legal elimination:
+   * (1) If x is contained in val,
+   * (2) If the type of val is not a subtype of the type of x,
+   * (3) If val contains an operator that cannot be evaluated, and produceModels
+   * is true. For example, x -> sqrt(2) is not a legal elimination if we
+   * are producing models. This is because we care about the value of x, and
+   * its value must be computed (approximated) by the non-linear solver.
+   */
+  bool isLegalElimination(TNode x, TNode val);
 
+ public:
   /**
    * Return the ID of the theory responsible for the given type.
    */
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index f24e4fc66..567b5c4e4 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -13,6 +13,7 @@
  **/
 #include "theory/theory_model.h"
 
+#include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
 #include "options/uf_options.h"
@@ -56,7 +57,6 @@ TheoryModel::TheoryModel(context::Context* c,
   {
     setSemiEvaluatedKind(kind::APPLY_UF);
   }
-  setUnevaluatedKind(kind::BOUND_VARIABLE);
 }
 
 TheoryModel::~TheoryModel()
@@ -203,19 +203,20 @@ Node TheoryModel::getModelValue(TNode n) const
   }
   Debug("model-getvalue-debug") << "Get model value " << n << " ... ";
   Debug("model-getvalue-debug") << d_equalityEngine->hasTerm(n) << std::endl;
-  if (n.isConst())
+  Kind nk = n.getKind();
+  if (n.isConst() || nk == BOUND_VARIABLE)
   {
     d_modelCache[n] = n;
     return n;
   }
 
   Node ret = n;
-  Kind nk = n.getKind();
   NodeManager* nm = NodeManager::currentNM();
 
   // if it is an evaluated kind, compute model values for children and evaluate
   if (n.getNumChildren() > 0
-      && d_not_evaluated_kinds.find(nk) == d_not_evaluated_kinds.end())
+      && d_unevaluated_kinds.find(nk) == d_unevaluated_kinds.end()
+      && d_semi_evaluated_kinds.find(nk) == d_semi_evaluated_kinds.end())
   {
     Debug("model-getvalue-debug")
         << "Get model value children " << n << std::endl;
@@ -308,10 +309,8 @@ Node TheoryModel::getModelValue(TNode n) const
   }
 
   // if we are a evaluated or semi-evaluated kind, return an arbitrary value
-  // if we are not in the d_not_evaluated_kinds map, we are evaluated
-  // if we are in the d_semi_evaluated_kinds, we are semi-evaluated
-  if (d_not_evaluated_kinds.find(nk) == d_not_evaluated_kinds.end()
-      || d_semi_evaluated_kinds.find(nk) != d_semi_evaluated_kinds.end())
+  // if we are not in the d_unevaluated_kinds map, we are evaluated
+  if (d_unevaluated_kinds.find(nk) == d_unevaluated_kinds.end())
   {
     if (t.isFunction() || t.isPredicate())
     {
@@ -617,17 +616,18 @@ void TheoryModel::recordModelCoreSymbol(Expr sym)
   d_model_core.insert(Node::fromExpr(sym));
 }
 
-void TheoryModel::setUnevaluatedKind(Kind k)
-{
-  d_not_evaluated_kinds.insert(k);
-}
+void TheoryModel::setUnevaluatedKind(Kind k) { d_unevaluated_kinds.insert(k); }
 
 void TheoryModel::setSemiEvaluatedKind(Kind k)
 {
-  d_not_evaluated_kinds.insert(k);
   d_semi_evaluated_kinds.insert(k);
 }
 
+bool TheoryModel::isLegalElimination(TNode x, TNode val)
+{
+  return !expr::hasSubtermKinds(d_unevaluated_kinds, val);
+}
+
 bool TheoryModel::hasTerm(TNode a)
 {
   return d_equalityEngine->hasTerm( a );
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index d984fbc6b..1deec82d9 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -266,6 +266,13 @@ public:
    */
   void setUnevaluatedKind(Kind k);
   void setSemiEvaluatedKind(Kind k);
+  /** is legal elimination
+   *
+   * Returns true if x -> val is a legal elimination of variable x.
+   * In particular, this ensures that val does not have any subterms that
+   * are of unevaluated kinds.
+   */
+  bool isLegalElimination(TNode x, TNode val);
   //---------------------------- end building the model
 
   // ------------------- general equality queries
@@ -356,8 +363,8 @@ public:
   std::map<Node, Node> d_approximations;
   /** list of all approximations */
   std::vector<std::pair<Node, Node> > d_approx_list;
-  /** a set of kinds that are not evaluated */
-  std::unordered_set<Kind, kind::KindHashFunction> d_not_evaluated_kinds;
+  /** a set of kinds that are unevaluated */
+  std::unordered_set<Kind, kind::KindHashFunction> d_unevaluated_kinds;
   /** a set of kinds that are semi-evaluated */
   std::unordered_set<Kind, kind::KindHashFunction> d_semi_evaluated_kinds;
   /**