diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-22 17:36:02 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-22 22:36:02 +0000 |
commit | cd7432f10ca15585df81e3ef2d49fcddbfa9c3c8 (patch) | |
tree | 0bdb3f081a7c878f4b3c0a9440551f7eb1e95b8d | |
parent | 0e79ea91e254a716b94bc74dc9e5aef13d4a8cba (diff) |
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.
-rw-r--r-- | src/theory/substitutions.cpp | 17 | ||||
-rw-r--r-- | src/theory/substitutions.h | 17 | ||||
-rw-r--r-- | 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) |