diff options
| -rw-r--r-- | src/theory/arith/nonlinear_extension.cpp | 3 | ||||
| -rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 10 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/nl/issue3617.smt2 | 11 |
4 files changed, 25 insertions, 0 deletions
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) |