diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-03 12:23:27 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-03 12:23:27 -0600 |
commit | dd67f7c0250a0725f2afc9fa38d3fca219eb2088 (patch) | |
tree | c0f4175dd15fa9089aeb6fe9ac634e4f54a26253 /src | |
parent | 5b010143cce0cace27e2556e26221f69ae43f688 (diff) |
Split on model values when repaired model from non-linear is inconsisent (#3668)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arith/nonlinear_extension.cpp | 3 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 10 |
2 files changed, 13 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; } } |