From b2137af7e9dd3993b4206274c59d0e3eeb2725cc Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 29 Sep 2020 14:05:46 +0200 Subject: [PATCH] Clean up nonlinear extension (#5149) This PR performs some cleanups in the nonlinear extension, in particular it removes the old lemma collection scheme. It is no longer needed, as all subsolvers use the inference manager. --- src/theory/arith/nl/nonlinear_extension.cpp | 95 +++++++++------------ src/theory/arith/nl/nonlinear_extension.h | 32 ++----- 2 files changed, 47 insertions(+), 80 deletions(-) diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 251294d37..a166a5609 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -334,7 +334,6 @@ std::vector NonlinearExtension::checkModelEval( } bool NonlinearExtension::checkModel(const std::vector& assertions, - std::vector& lemmas, std::vector& gs) { Trace("nl-ext-cm") << "--- check-model ---" << std::endl; @@ -361,19 +360,19 @@ bool NonlinearExtension::checkModel(const std::vector& assertions, Trace("nl-ext-cm") << "-----" << std::endl; unsigned tdegree = d_trSlv.getTaylorDegree(); - bool ret = - d_model.checkModel(passertions, tdegree, lemmas, gs); + std::vector lemmas; + bool ret = d_model.checkModel(passertions, tdegree, lemmas, gs); + for (const auto& al: lemmas) + { + d_im.addPendingArithLemma(al); + } return ret; } -int NonlinearExtension::checkLastCall(const std::vector& assertions, - const std::vector& false_asserts, - const std::vector& xts, - std::vector& lems, - std::vector& wlems) +void NonlinearExtension::checkLastCall(const std::vector& assertions, + const std::vector& false_asserts, + const std::vector& xts) { - std::vector lemmas; - ++(d_stats.d_checkRuns); if (Trace.isOn("nl-ext")) @@ -394,7 +393,7 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() + d_im.numSentLemmas() << " new lemmas from ICP." << std::endl; - return d_im.numPendingLemmas() + d_im.numSentLemmas(); + return; } Trace("nl-ext") << "Done with ICP" << std::endl; } @@ -406,20 +405,16 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, // initialize the trancendental function solver d_trSlv.initLastCall(assertions, false_asserts, xts); } - if (options::nlCad()) - { - d_cadSlv.initLastCall(assertions); - } // init last call with IAND d_iandSlv.initLastCall(assertions, false_asserts, xts); - if (d_im.hasUsed() || !lems.empty()) + if (d_im.hasUsed()) { - unsigned count = lems.size() + d_im.numPendingLemmas() + d_im.numSentLemmas(); + std::size_t count = d_im.numPendingLemmas() + d_im.numSentLemmas(); Trace("nl-ext") << " ...finished with " << count << " new lemmas during registration." << std::endl; - return count; + return; } //----------------------------------- possibly split on zero @@ -431,7 +426,7 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, { Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() << " new lemmas." << std::endl; - return d_im.numPendingLemmas(); + return; } } @@ -442,10 +437,10 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, d_trSlv.checkTranscendentalInitialRefine(); if (d_im.hasUsed()) { - unsigned count = lems.size() + d_im.numPendingLemmas() + d_im.numSentLemmas(); + std::size_t count = d_im.numPendingLemmas() + d_im.numSentLemmas(); Trace("nl-ext") << " ...finished with " << count << " new lemmas." << std::endl; - return count; + return; } } //-----------------------------------initial lemmas for iand @@ -454,7 +449,7 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, { Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() << " new lemmas." << std::endl; - return d_im.numPendingLemmas(); + return; } // main calls to nlExt @@ -466,17 +461,17 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, { Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() << " new lemmas." << std::endl; - return d_im.numPendingLemmas(); + return; } //-----------------------------------monotonicity of transdental functions d_trSlv.checkTranscendentalMonotonic(); if (d_im.hasUsed()) { - unsigned count = lems.size() + d_im.numPendingLemmas() + d_im.numSentLemmas(); + std::size_t count = d_im.numPendingLemmas() + d_im.numSentLemmas(); Trace("nl-ext") << " ...finished with " << count << " new lemmas." << std::endl; - return count; + return; } //------------------------lemmas based on magnitude of non-zero monomials @@ -488,7 +483,7 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, { Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() << " new lemmas." << std::endl; - return d_im.numPendingLemmas(); + return; } } @@ -497,7 +492,6 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, d_nlSlv.checkMonomialInferBounds(assertions, false_asserts); Trace("nl-ext") << "Bound lemmas : " << d_im.numPendingLemmas() << ", " << d_im.numWaitingLemmas() << std::endl; // prioritize lemmas that do not introduce new monomials - if (options::nlExtTangentPlanes() && options::nlExtTangentPlanesInterleave()) { @@ -508,7 +502,7 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, { Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() << " new lemmas." << std::endl; - return d_im.numPendingLemmas(); + return; } // from inferred bound inferences : now do ones that introduce new terms @@ -517,7 +511,7 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, { Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() << " new (monomial-introducing) lemmas." << std::endl; - return d_im.numPendingLemmas(); + return; } //------------------------------------factoring lemmas @@ -529,7 +523,7 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, { Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() << " new lemmas." << std::endl; - return d_im.numPendingLemmas(); + return; } } @@ -542,7 +536,7 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, { Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() << " new lemmas." << std::endl; - return d_im.numPendingLemmas(); + return; } } @@ -559,6 +553,7 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, } if (options::nlCad()) { + d_cadSlv.initLastCall(assertions); d_cadSlv.checkFull(); if (!d_im.hasUsed()) { @@ -567,7 +562,7 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, else { // checkFull() only adds a single conflict - return 1; + return; } } // run the full refinement in the IAND solver @@ -577,7 +572,7 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, << std::endl; Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() << " lemmas." << std::endl; - return 0; + return; } void NonlinearExtension::check(Theory::Effort e) @@ -610,9 +605,8 @@ void NonlinearExtension::check(Theory::Effort e) else { // If we computed lemmas during collectModelInfo, send them now. - if (!d_cmiLemmas.empty() || d_im.hasPendingLemma()) + if (d_im.hasPendingLemma()) { - sendLemmas(d_cmiLemmas); d_im.doPendingFacts(); d_im.doPendingLemmas(); d_im.doPendingPhaseRequirements(); @@ -640,7 +634,7 @@ void NonlinearExtension::check(Theory::Effort e) } } -bool NonlinearExtension::modelBasedRefinement(std::vector& mlems) +bool NonlinearExtension::modelBasedRefinement() { ++(d_stats.d_mbrRuns); d_checkCounter++; @@ -723,15 +717,13 @@ bool NonlinearExtension::modelBasedRefinement(std::vector& mlems) // complete_status: // 1 : we may answer SAT, -1 : we may not answer SAT, 0 : unknown int complete_status = 1; - // lemmas that should be sent later - std::vector wlems; // We require a check either if an assertion is false or a shared term has // a wrong value if (!false_asserts.empty() || num_shared_wrong_value > 0) { complete_status = num_shared_wrong_value > 0 ? -1 : 0; - checkLastCall(assertions, false_asserts, xts, mlems, wlems); - if (!mlems.empty() || d_im.hasSentLemma() || d_im.hasPendingLemma()) + checkLastCall(assertions, false_asserts, xts); + if (d_im.hasSentLemma() || d_im.hasPendingLemma()) { d_im.clearWaitingLemmas(); return true; @@ -748,9 +740,8 @@ bool NonlinearExtension::modelBasedRefinement(std::vector& mlems) << std::endl; // check the model based on simple solving of equalities and using // error bounds on the Taylor approximation of transcendental functions. - std::vector lemmas; std::vector gs; - if (checkModel(assertions, lemmas, gs)) + if (checkModel(assertions, gs)) { complete_status = 1; } @@ -761,8 +752,7 @@ bool NonlinearExtension::modelBasedRefinement(std::vector& mlems) d_containing.getOutputChannel().requirePhase(mgr, true); d_builtModel = true; } - filterLemmas(lemmas, mlems); - if (!mlems.empty() || d_im.hasPendingLemma()) + if (d_im.hasUsed()) { d_im.clearWaitingLemmas(); return true; @@ -773,10 +763,9 @@ bool NonlinearExtension::modelBasedRefinement(std::vector& mlems) if (complete_status != 1) { // flush the waiting lemmas - if (!wlems.empty() || d_im.hasWaitingLemma()) + if (d_im.hasWaitingLemma()) { - std::size_t count = wlems.size() + d_im.numWaitingLemmas(); - mlems.insert(mlems.end(), wlems.begin(), wlems.end()); + std::size_t count = d_im.numWaitingLemmas(); d_im.flushWaitingLemmas(); Trace("nl-ext") << "...added " << count << " waiting lemmas." << std::endl; @@ -789,7 +778,6 @@ bool NonlinearExtension::modelBasedRefinement(std::vector& mlems) complete_status = -1; if (!shared_term_value_splits.empty()) { - std::vector stvLemmas; for (const Node& eq : shared_term_value_splits) { Node req = Rewriter::rewrite(eq); @@ -798,12 +786,12 @@ bool NonlinearExtension::modelBasedRefinement(std::vector& mlems) Trace("nl-ext-debug") << "Split on : " << literal << std::endl; Node split = literal.orNode(literal.negate()); NlLemma nsplit(split, InferenceId::NL_SHARED_TERM_VALUE_SPLIT); - filterLemma(nsplit, stvLemmas); + d_im.addPendingArithLemma(nsplit, true); } - if (!stvLemmas.empty()) + if (d_im.hasWaitingLemma()) { - mlems.insert(mlems.end(), stvLemmas.begin(), stvLemmas.end()); - Trace("nl-ext") << "...added " << stvLemmas.size() + d_im.flushWaitingLemmas(); + Trace("nl-ext") << "...added " << d_im.numPendingLemmas() << " shared term value split lemmas." << std::endl; return true; } @@ -852,11 +840,10 @@ void NonlinearExtension::interceptModel(std::map& arithModel) 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(); if (!d_builtModel.get()) { Trace("nl-ext") << "interceptModel: do model-based refinement" << std::endl; - modelBasedRefinement(d_cmiLemmas); + modelBasedRefinement(); } if (d_builtModel.get()) { diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index d09d92c9f..f0e61435f 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -115,11 +115,6 @@ class NonlinearExtension * constraints are satisfiable, it may "repair" the values in the argument * arithModel so that it satisfies certain nonlinear constraints. This may * involve e.g. solving for variables in nonlinear equations. - * - * Notice that in the former case, the lemmas it constructs are not sent out - * immediately. Instead, they are put in temporary vector d_cmiLemmas, which - * are then sent out (if necessary) when a last call - * effort check is issued to this class. */ void interceptModel(std::map& arithModel); /** Does this class need a call to check(...) at last call effort? */ @@ -146,12 +141,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 vector lems. + * 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. */ - bool modelBasedRefinement(std::vector& mlems); + bool modelBasedRefinement(); /** check last call * @@ -160,24 +155,15 @@ class NonlinearExtension * * xts : the list of (non-reduced) extended terms in the current context. * - * This method adds lemmas to arguments lems and wlems, each of - * which are intended to be sent out on the output channel of TheoryArith - * under certain conditions. + * This method adds lemmas to d_im directly. * * If the set lems is non-empty, then no further processing is * necessary. The last call effort check should terminate and these * lemmas should be sent. - * - * The "waiting" lemmas wlems contain lemmas that should be sent on the - * output channel as a last resort. In other words, only if we are not - * able to establish SAT via a call to checkModel(...) should wlems be - * considered. This set typically contains tangent plane lemmas. */ - int checkLastCall(const std::vector& assertions, - const std::vector& false_asserts, - const std::vector& xts, - std::vector& lems, - std::vector& wlems); + void checkLastCall(const std::vector& assertions, + const std::vector& false_asserts, + const std::vector& xts); /** get assertions * @@ -218,7 +204,6 @@ class NonlinearExtension * ensureLiteral respectively. */ bool checkModel(const std::vector& assertions, - std::vector& lemmas, std::vector& gs); //---------------------------end check model /** compute relevant assertions */ @@ -290,11 +275,6 @@ class NonlinearExtension * constraints involving integer and. */ IAndSolver d_iandSlv; - /** - * The lemmas we computed during collectModelInfo, to be sent out on the - * output channel of TheoryArith. - */ - std::vector d_cmiLemmas; /** * The approximations computed during collectModelInfo. For details, see * NlModel::getModelValueRepair. -- 2.30.2