From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 3 Feb 2020 18:23:27 +0000 (-0600)
Subject: Split on model values when repaired model from non-linear is inconsisent (#3668)
X-Git-Tag: cvc5-1.0.0~3692
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dd67f7c0250a0725f2afc9fa38d3fca219eb2088;p=cvc5.git

Split on model values when repaired model from non-linear is inconsisent (#3668)
---

diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index 46be960c7..1c8b9611f 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -1485,16 +1485,19 @@ void NonlinearExtension::interceptModel(std::map<Node, Node>& arithModel)
     // no non-linear constraints, we are done
     return;
   }
+  Trace("nl-ext") << "NonlinearExtension::interceptModel begin" << std::endl;
   d_model.reset(d_containing.getValuation().getModel(), arithModel);
   // run a last call effort check
   d_cmiLemmas.clear();
   d_cmiLemmasPp.clear();
   if (!d_builtModel.get())
   {
+    Trace("nl-ext") << "interceptModel: do model-based refinement" << std::endl;
     modelBasedRefinement(d_cmiLemmas, d_cmiLemmasPp);
   }
   if (d_builtModel.get())
   {
+    Trace("nl-ext") << "interceptModel: do model repair" << std::endl;
     d_approximations.clear();
     // modify the model values
     d_model.getModelValueRepair(arithModel, d_approximations);
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index b8bdd04e1..2b8ce922d 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -4376,6 +4376,16 @@ bool TheoryArithPrivate::collectModelInfo(TheoryModel* m)
     {
       if (!m->assertEquality(p.first, p.second, true))
       {
+        // If we failed to assert an equality, it is likely due to theory
+        // combination, namely the repaired model for non-linear changed
+        // an equality status that was agreed upon by both (linear) arithmetic
+        // and another theory. In this case, we must add a lemma, or otherwise
+        // we would terminate with an invalid model. Thus, we add a splitting
+        // lemma of the form ( x = v V x != v ) where v is the model value
+        // assigned by the non-linear solver to x.
+        Node eq = p.first.eqNode(p.second);
+        Node lem = NodeManager::currentNM()->mkNode(kind::OR, eq, eq.negate());
+        d_containing.d_out->lemma(lem);
         return false;
       }
     }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index cea7b60ad..aeca8e720 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1288,6 +1288,7 @@ set(regress_1_tests
   regress1/nl/exp_monotone.smt2
   regress1/nl/factor_agg_s.smt2
   regress1/nl/issue3441.smt2
+  regress1/nl/issue3617.smt2
   regress1/nl/issue3656.smt2
   regress1/nl/metitarski-1025.smt2
   regress1/nl/metitarski-3-4.smt2
diff --git a/test/regress/regress1/nl/issue3617.smt2 b/test/regress/regress1/nl/issue3617.smt2
new file mode 100644
index 000000000..cd96d536a
--- /dev/null
+++ b/test/regress/regress1/nl/issue3617.smt2
@@ -0,0 +1,11 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () Real)
+(declare-fun b () Real)
+(declare-fun dbz (Real) Real)
+(assert
+(let ((_let_0 (dbz 0.0))) (let ((_let_1 (= b 0.0))) (let ((_let_2 (/ 1.0 a))) (let ((_let_3 (dbz 1.0))) (let ((_let_4 (= a 0.0))) (let ((_let_5 (ite _let_4 _let_3 _let_2))) (let ((_let_6 (/ _let_5 b))) (let ((_let_7 (dbz _let_5))) (let ((_let_8 (dbz (dbz (ite _let_1 _let_7 _let_6))))) (or (>= (* (- 1.0) (ite (= _let_8 0.0) _let_0 (/ 0.0 _let_8))) 0.0) (>= _let_0 0.0)))))))))))
+)
+(assert (> a 0))
+(check-sat)
+(get-model)