diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-15 14:57:53 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-15 21:57:53 +0000 |
commit | b7dcbee6f351c22ca3454d706d5773d01dd806fa (patch) | |
tree | eef642fd1c9818ac32dd4dff7e13edfff6ff352c /src/preprocessing | |
parent | 640a07690826d4bbd87398949091b94b32e35c7a (diff) |
preprocessing context: Add wrapper for model substitutions. (#6370)
Previously, preprocessing passes added model substitutions without
expanding definitions for substitutions, which can be a problem.
This adds a wrapper function to take care of it properly.
Fixes #5473.
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/bv_eager_atoms.cpp | 3 | ||||
-rw-r--r-- | src/preprocessing/passes/miplib_trick.cpp | 2 | ||||
-rw-r--r-- | src/preprocessing/passes/non_clausal_simp.cpp | 4 | ||||
-rw-r--r-- | src/preprocessing/preprocessing_pass_context.cpp | 9 | ||||
-rw-r--r-- | src/preprocessing/preprocessing_pass_context.h | 7 |
5 files changed, 19 insertions, 6 deletions
diff --git a/src/preprocessing/passes/bv_eager_atoms.cpp b/src/preprocessing/passes/bv_eager_atoms.cpp index 3ba2f8870..1466a945d 100644 --- a/src/preprocessing/passes/bv_eager_atoms.cpp +++ b/src/preprocessing/passes/bv_eager_atoms.cpp @@ -33,13 +33,12 @@ BvEagerAtoms::BvEagerAtoms(PreprocessingPassContext* preprocContext) PreprocessingPassResult BvEagerAtoms::applyInternal( AssertionPipeline* assertionsToPreprocess) { - theory::TheoryModel* tm = d_preprocContext->getTheoryEngine()->getModel(); NodeManager* nm = NodeManager::currentNM(); for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i) { TNode atom = (*assertionsToPreprocess)[i]; Node eager_atom = nm->mkNode(kind::BITVECTOR_EAGER_ATOM, atom); - tm->addSubstitution(eager_atom, atom); + d_preprocContext->addModelSubstitution(eager_atom, atom); assertionsToPreprocess->replace(i, eager_atom); } return PreprocessingPassResult::NO_CONFLICT; diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 142a66af8..52d6cce3c 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -550,7 +550,7 @@ PreprocessingPassResult MipLibTrick::applyInternal( << "unexpected solution from arith's ppAssert()"; Assert(nullMap.empty()) << "unexpected substitution from arith's ppAssert()"; - te->getModel()->addSubstitution(*ii, newVar.eqNode(one)); + d_preprocContext->addModelSubstitution(*ii, newVar.eqNode(one)); newVars.push_back(newVar); varRef = newVar; } diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index a253c7b15..05c53721f 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -325,8 +325,6 @@ PreprocessingPassResult NonClausalSimp::applyInternal( } // add substitutions to model, or as assertions if needed (when incremental) - TheoryModel* m = d_preprocContext->getTheoryEngine()->getModel(); - Assert(m != nullptr); NodeManager* nm = NodeManager::currentNM(); for (SubstitutionMap::iterator pos = nss.begin(); pos != nss.end(); ++pos) { @@ -341,7 +339,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( { Trace("non-clausal-simplify") << "substitute: " << lhs << " " << rhs << std::endl; - m->addSubstitution(lhs, rhs); + d_preprocContext->addModelSubstitution(lhs, rhs); } else { diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index 6e7d253f2..22cc15a97 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -16,6 +16,8 @@ #include "preprocessing/preprocessing_pass_context.h" #include "expr/node_algorithm.h" +#include "theory/theory_engine.h" +#include "theory/theory_model.h" namespace cvc5 { namespace preprocessing { @@ -54,6 +56,13 @@ void PreprocessingPassContext::recordSymbolsInAssertions( } } +void PreprocessingPassContext::addModelSubstitution(const Node& lhs, + const Node& rhs) +{ + getTheoryEngine()->getModel()->addSubstitution( + lhs, d_smt->expandDefinitions(rhs, false)); +} + ProofNodeManager* PreprocessingPassContext::getProofNodeManager() { return d_pnm; diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index cdeb37bbe..f1d92e864 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -80,6 +80,13 @@ class PreprocessingPassContext */ void recordSymbolsInAssertions(const std::vector<Node>& assertions); + /** + * Add substitution to theory model. + * @param lhs The node replaced by node 'rhs' + * @param rhs The node to substitute node 'lhs' + */ + void addModelSubstitution(const Node& lhs, const Node& rhs); + /** The the proof node manager associated with this context, if it exists */ ProofNodeManager* getProofNodeManager(); |