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.

diff --git a/src/preprocessing/passes/bv_eager_atoms.cpp b/src/preprocessing/passes/bv_eager_atoms.cpp
index 3ba2f887005013a8f9d44254debd487a4bb883fe..1466a945d341dfcf7742d1786b96ac957cd6fbe0 100644 (file)
--- 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 142a66af8ba902ecf07843dc067f33cbf33aaf62..52d6cce3cf8188c4e5f0d93ffa70927fa675f043 100644 (file)
--- 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 a253c7b156b6b6cb127215bed946f26c3cbb8a23..05c53721f4e77965ae9eac515b308e2889993b86 100644 (file)
--- 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 6e7d253f216e70c189301c83aeb4d8c61f9a3c58..22cc15a973c6c67d876f4e84bbc8cbf491bec43f 100644 (file)
--- 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 cdeb37bbeda4fde89cffbc76132ff62c8e2d24d2..f1d92e864f01abeff73d0167aec93ae1f8de3dd0 100644 (file)
--- 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();
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a9b5174bb8aaa048be7890da16ef895ab396c4ee..12e0c568dee7f891384145f6bbab6de00fed5ba4 100644 (file)
--- 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 ea27672d51d0b149063d79259efbb36e6fb33d04..8816caa9ad545703d9bbc213261272ecd88e2121 100644 (file)
--- 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 (file)
index 0000000..bf24726
--- /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)