Minor improvements to substitutions (#6380)

In preparation for using this class as part of our proof checker.

This removes an option that was previously used as a hack to try to make check-models work for quantifiers. It also makes supplying a context optional.

1 files changed, 9 insertions, 8 deletions

diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index 5c4b36043..8ca099dae 100644
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -22,6 +22,15 @@ using namespace std;
 namespace cvc5 {
 namespace theory {
 
+SubstitutionMap::SubstitutionMap(context::Context* context)
+    : d_context(),
+      d_substitutions(context ? context : &d_context),
+      d_substitutionCache(),
+      d_cacheInvalidated(false),
+      d_cacheInvalidator(context ? context : &d_context, d_cacheInvalidated)
+{
+}
+
 struct substitution_stack_element {
   TNode d_node;
   bool d_children_added;
@@ -57,14 +66,6 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) {
       continue;
     }
 
-    if (!d_substituteUnderQuantifiers && current.isClosure())
-    {
-      Debug("substitution::internal") << "--not substituting under quantifier" << endl;
-      cache[current] = current;
-      toVisit.pop_back();
-      continue;
-    }
-
     NodeMap::iterator find2 = d_substitutions.find(current);
     if (find2 != d_substitutions.end()) {
       Node rhs = (*find2).second;