From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 15 Apr 2021 21:57:53 +0000 (-0700)
Subject: preprocessing context: Add wrapper for model substitutions. (#6370)
X-Git-Tag: cvc5-1.0.0~1893
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b7dcbee6f351c22ca3454d706d5773d01dd806fa;p=cvc5.git

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 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();
 
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)