From b7dcbee6f351c22ca3454d706d5773d01dd806fa Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 15 Apr 2021 14:57:53 -0700 Subject: [PATCH] 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. --- src/preprocessing/passes/bv_eager_atoms.cpp | 3 +-- src/preprocessing/passes/miplib_trick.cpp | 2 +- src/preprocessing/passes/non_clausal_simp.cpp | 4 +--- src/preprocessing/preprocessing_pass_context.cpp | 9 +++++++++ src/preprocessing/preprocessing_pass_context.h | 7 +++++++ test/regress/CMakeLists.txt | 1 + test/regress/regress0/datatypes/v3l60006.cvc | 1 + test/regress/regress0/issue5473.smt2 | 11 +++++++++++ 8 files changed, 32 insertions(+), 6 deletions(-) create mode 100644 test/regress/regress0/issue5473.smt2 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& 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(); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a9b5174bb..12e0c568d 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -638,6 +638,7 @@ set(regress_0_tests regress0/issue5187-div-justification.smt2 regress0/issue5370.smt2 regress0/issue5462.smt2 + regress0/issue5473.smt2 regress0/issue5540-2-dump-model.smt2 regress0/issue5540-model-decls.smt2 regress0/issue5550-num-children.smt2 diff --git a/test/regress/regress0/datatypes/v3l60006.cvc b/test/regress/regress0/datatypes/v3l60006.cvc index ea27672d5..8816caa9a 100644 --- a/test/regress/regress0/datatypes/v3l60006.cvc +++ b/test/regress/regress0/datatypes/v3l60006.cvc @@ -1,3 +1,4 @@ +% COMMAND-LINE: -q % EXPECT: not_entailed DATATYPE nat = succ(pred : nat) | zero, diff --git a/test/regress/regress0/issue5473.smt2 b/test/regress/regress0/issue5473.smt2 new file mode 100644 index 000000000..bf24726f9 --- /dev/null +++ b/test/regress/regress0/issue5473.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: -q +; EXPECT: sat +; EXPECT: ((baz true)) +(set-logic QF_NIRA) +(set-option :produce-models true) +(declare-fun a () Int) +(declare-fun b () Int) +(assert (! (or (= a (div 0 b))) :named baz)) +(assert (and (< b 5))) +(check-sat) +(get-assignment) -- 2.30.2