From cd7432f10ca15585df81e3ef2d49fcddbfa9c3c8 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 22 Apr 2021 17:36:02 -0500
Subject: [PATCH] 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.
---
 src/theory/substitutions.cpp | 17 +++++++++--------
 src/theory/substitutions.h   | 17 ++++-------------
 src/theory/theory_model.cpp  |  2 +-
 3 files changed, 14 insertions(+), 22 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;
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index 06e39e7a9..e1d75d957 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -52,6 +52,8 @@ public:
 private:
 
   typedef std::unordered_map<Node, Node, NodeHashFunction> NodeCache;
+  /** A dummy context used by this class if none is provided */
+  context::Context d_context;
 
   /** The variables, in order of addition */
   NodeMap d_substitutions;
@@ -59,9 +61,6 @@ private:
   /** Cache of the already performed substitutions */
   NodeCache d_substitutionCache;
 
-  /** Whether or not to substitute under quantifiers */
-  bool d_substituteUnderQuantifiers;
-
   /** Has the cache been invalidated? */
   bool d_cacheInvalidated;
 
@@ -88,16 +87,8 @@ private:
    */
   CacheInvalidator d_cacheInvalidator;
 
-public:
- SubstitutionMap(context::Context* context,
-                 bool substituteUnderQuantifiers = true)
-     : d_substitutions(context),
-       d_substitutionCache(),
-       d_substituteUnderQuantifiers(substituteUnderQuantifiers),
-       d_cacheInvalidated(false),
-       d_cacheInvalidator(context, d_cacheInvalidated)
- {
-  }
+ public:
+  SubstitutionMap(context::Context* context = nullptr);
 
   /**
    * Adds a substitution from x to t.
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 6793e5e02..d894ca571 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -33,7 +33,7 @@ TheoryModel::TheoryModel(context::Context* c,
                          std::string name,
                          bool enableFuncModels)
     : d_name(name),
-      d_substitutions(c, false),
+      d_substitutions(c),
       d_equalityEngine(nullptr),
       d_using_model_core(false),
       d_enableFuncModels(enableFuncModels)
-- 
2.30.2