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.

diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index 5c4b360431ee52c5d02bde3f061cdfa51b40267b..8ca099daeb19c51e7f0d8ef20bd4e3e32170fc92 100644 (file)
--- 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 06e39e7a9edb6965cf0d0cc753d47dbc09e3665e..e1d75d95764cd5546cca116a35074020bfcfaf31 100644 (file)
--- 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 6793e5e02cd2f14a2b707bfb936d5135acb75ef8..d894ca571ed7b54c4bf856f22ed76e9eb97ad858 100644 (file)
--- 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)