diff options
| -rw-r--r-- | src/theory/arith/nl/nonlinear_extension.cpp | 33 | ||||
| -rw-r--r-- | src/theory/arith/nl/nonlinear_extension.h | 13 | ||||
| -rw-r--r-- | src/theory/arith/theory_arith.cpp | 3 |
3 files changed, 19 insertions, 30 deletions
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 25aebf6d4..781fb0c71 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -57,8 +57,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, d_tangentPlaneSlv(&d_extState), d_cadSlv(d_im, d_model, state.getUserContext(), pnm), d_icpSlv(d_im), - d_iandSlv(d_im, state, d_model), - d_builtModel(containing.getSatContext(), false) + d_iandSlv(d_im, state, d_model) { d_extTheory.addFunctionKind(kind::NONLINEAR_MULT); d_extTheory.addFunctionKind(kind::EXPONENTIAL); @@ -246,8 +245,7 @@ void NonlinearExtension::check(Theory::Effort e) { d_im.reset(); Trace("nl-ext") << std::endl; - Trace("nl-ext") << "NonlinearExtension::check, effort = " << e - << ", built model = " << d_builtModel.get() << std::endl; + Trace("nl-ext") << "NonlinearExtension::check, effort = " << e << std::endl; if (e == Theory::EFFORT_FULL) { d_extTheory.clearCache(); @@ -301,7 +299,7 @@ void NonlinearExtension::check(Theory::Effort e) } } -bool NonlinearExtension::modelBasedRefinement(const std::set<Node>& termSet) +Result::Sat NonlinearExtension::modelBasedRefinement(const std::set<Node>& termSet) { ++(d_stats.d_mbrRuns); d_checkCounter++; @@ -403,7 +401,7 @@ bool NonlinearExtension::modelBasedRefinement(const std::set<Node>& termSet) if (d_im.hasSentLemma() || d_im.hasPendingLemma()) { d_im.clearWaitingLemmas(); - return true; + return Result::Sat::UNSAT; } } Trace("nl-ext") << "Finished check with status : " << complete_status @@ -424,7 +422,7 @@ bool NonlinearExtension::modelBasedRefinement(const std::set<Node>& termSet) if (d_im.hasUsed()) { d_im.clearWaitingLemmas(); - return true; + return Result::Sat::UNSAT; } } @@ -438,7 +436,7 @@ bool NonlinearExtension::modelBasedRefinement(const std::set<Node>& termSet) d_im.flushWaitingLemmas(); Trace("nl-ext") << "...added " << count << " waiting lemmas." << std::endl; - return true; + return Result::Sat::UNSAT; } // resort to splitting on shared terms with their model value // if we did not add any lemmas @@ -464,7 +462,7 @@ bool NonlinearExtension::modelBasedRefinement(const std::set<Node>& termSet) d_im.flushWaitingLemmas(); Trace("nl-ext") << "...added " << d_im.numPendingLemmas() << " shared term value split lemmas." << std::endl; - return true; + return Result::Sat::UNSAT; } } else @@ -494,16 +492,11 @@ bool NonlinearExtension::modelBasedRefinement(const std::set<Node>& termSet) d_containing.getOutputChannel().setIncomplete(); } } - else - { - // we have built a model - d_builtModel = true; - } d_im.clearWaitingLemmas(); } while (needsRecheck); // did not add lemmas - return false; + return Result::Sat::SAT; } void NonlinearExtension::interceptModel(std::map<Node, Node>& arithModel, @@ -517,12 +510,9 @@ void NonlinearExtension::interceptModel(std::map<Node, Node>& arithModel, Trace("nl-ext") << "NonlinearExtension::interceptModel begin" << std::endl; d_model.reset(d_containing.getValuation().getModel(), arithModel); // run a last call effort check - if (!d_builtModel.get()) - { - Trace("nl-ext") << "interceptModel: do model-based refinement" << std::endl; - modelBasedRefinement(termSet); - } - if (d_builtModel.get()) + Trace("nl-ext") << "interceptModel: do model-based refinement" << std::endl; + Result::Sat res = modelBasedRefinement(termSet); + if (res == Result::Sat::SAT) { Trace("nl-ext") << "interceptModel: do model repair" << std::endl; d_approximations.clear(); @@ -535,7 +525,6 @@ void NonlinearExtension::interceptModel(std::map<Node, Node>& arithModel, void NonlinearExtension::presolve() { Trace("nl-ext") << "NonlinearExtension::presolve" << std::endl; - d_builtModel = false; } void NonlinearExtension::runStrategy(Theory::Effort effort, diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index 820c317c5..bc8f48c26 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -39,6 +39,7 @@ #include "theory/arith/nl/transcendental/transcendental_solver.h" #include "theory/ext_theory.h" #include "theory/theory.h" +#include "util/result.h" namespace CVC4 { namespace theory { @@ -154,12 +155,12 @@ class NonlinearExtension * described in Reynolds et al. FroCoS 2017 that are based on ruling out * the current candidate model. * - * This function returns true if a lemma was added to the inference manager. - * Otherwise, it returns false. In the latter case, the model object d_model - * may have information regarding how to construct a model, in the case that - * we determined the problem is satisfiable. + * This function returns whether we found a satisfying assignment + * (Result::Sat::SAT), or not (Result::Sat::UNSAT). Note that UNSAT does not + * necessarily means the whole query is UNSAT, but that the linear model was + * refuted by a lemma. */ - bool modelBasedRefinement(const std::set<Node>& termSet); + Result::Sat modelBasedRefinement(const std::set<Node>& termSet); /** get assertions * @@ -290,8 +291,6 @@ class NonlinearExtension * NlModel::getModelValueRepair. */ std::map<Node, Node> d_witnesses; - /** have we successfully built the model in this SAT context? */ - context::CDO<bool> d_builtModel; }; /* class NonlinearExtension */ } // namespace nl diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 36b2d3eb8..a179336af 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -270,7 +270,8 @@ bool TheoryArith::collectModelValues(TheoryModel* m, { Node eq = p.first.eqNode(p.second); Node lem = NodeManager::currentNM()->mkNode(kind::OR, eq, eq.negate()); - d_im.lemma(lem, InferenceId::ARITH_SPLIT_FOR_NL_MODEL); + bool added = d_im.lemma(lem, InferenceId::ARITH_SPLIT_FOR_NL_MODEL); + AlwaysAssert(added) << "The lemma was already in cache. Probably there is something wrong with theory combination..."; } return false; } |