From: Andrew Reynolds Date: Thu, 22 Apr 2021 22:36:02 +0000 (-0500) Subject: Minor improvements to substitutions (#6380) X-Git-Tag: cvc5-1.0.0~1848 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cd7432f10ca15585df81e3ef2d49fcddbfa9c3c8;p=cvc5.git 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 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 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)