From 79d0e47c14a9e8213d6c6e112835142cf2417943 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 6 Jun 2020 12:25:50 -0500 Subject: [PATCH] Use NlLemma utility for all lemmas in non-linear. (#4573) This makes it much easier to set custom properties of lemmas (e.g. preprocess) and also will allow proof tracking and debugging in the future. This also enables a fix on the IAND branch related to preprocessing lemmas. --- src/theory/arith/nl/nl_lemma_utils.cpp | 6 ++ src/theory/arith/nl/nl_lemma_utils.h | 24 +++-- src/theory/arith/nl/nl_model.cpp | 4 +- src/theory/arith/nl/nl_model.h | 5 +- src/theory/arith/nl/nl_solver.cpp | 47 +++++----- src/theory/arith/nl/nl_solver.h | 26 ++--- src/theory/arith/nl/nonlinear_extension.cpp | 94 +++++++++---------- src/theory/arith/nl/nonlinear_extension.h | 56 ++++------- src/theory/arith/nl/transcendental_solver.cpp | 39 ++++---- src/theory/arith/nl/transcendental_solver.h | 30 +++--- 10 files changed, 158 insertions(+), 173 deletions(-) diff --git a/src/theory/arith/nl/nl_lemma_utils.cpp b/src/theory/arith/nl/nl_lemma_utils.cpp index ca34d91a9..c1ec42497 100644 --- a/src/theory/arith/nl/nl_lemma_utils.cpp +++ b/src/theory/arith/nl/nl_lemma_utils.cpp @@ -21,6 +21,12 @@ namespace theory { namespace arith { namespace nl { +std::ostream& operator<<(std::ostream& out, NlLemma& n) +{ + out << n.d_lemma; + return out; +} + bool SortNlModel::operator()(Node i, Node j) { int cv = d_nlm->compare(i, j, d_isConcrete, d_isAbsolute); diff --git a/src/theory/arith/nl/nl_lemma_utils.h b/src/theory/arith/nl/nl_lemma_utils.h index 64a4deb17..a0fce378f 100644 --- a/src/theory/arith/nl/nl_lemma_utils.h +++ b/src/theory/arith/nl/nl_lemma_utils.h @@ -27,16 +27,24 @@ namespace nl { class NlModel; /** - * A side effect of adding a lemma in the non-linear solver. This is used - * to specify how the state of the non-linear solver should update. This - * includes: + * The data structure for a single lemma to process by the non-linear solver, + * including the lemma itself and whether it should be preprocessed (see + * OutputChannel::lemma). + * + * This also includes data structures that encapsulate the side effect of adding + * this lemma in the non-linear solver. This is used to specify how the state of + * the non-linear solver should update. This includes: * - A set of secant points to record (for transcendental secant plane * inferences). */ -struct NlLemmaSideEffect +struct NlLemma { - NlLemmaSideEffect() {} - ~NlLemmaSideEffect() {} + NlLemma(Node lem) : d_lemma(lem), d_preprocess(false) {} + ~NlLemma() {} + /** The lemma */ + Node d_lemma; + /** Whether to preprocess the lemma */ + bool d_preprocess; /** secant points to add * * A member (tf, d, c) in this vector indicates that point c should be added @@ -48,6 +56,10 @@ struct NlLemmaSideEffect */ std::vector > d_secantPoint; }; +/** + * Writes a non-linear lemma to a stream. + */ +std::ostream& operator<<(std::ostream& out, NlLemma& n); struct SortNlModel { diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index d5df96bd8..2ed901f1f 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -213,7 +213,7 @@ int NlModel::compareValue(Node i, Node j, bool isAbsolute) const bool NlModel::checkModel(const std::vector& assertions, const std::vector& false_asserts, unsigned d, - std::vector& lemmas, + std::vector& lemmas, std::vector& gs) { Trace("nl-ext-cm-debug") << " solve for equalities..." << std::endl; @@ -478,7 +478,7 @@ void NlModel::addTautology(Node n) bool NlModel::solveEqualitySimple(Node eq, unsigned d, - std::vector& lemmas) + std::vector& lemmas) { Node seq = eq; if (!d_check_model_vars.empty()) diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h index 61193fc12..7a40e3926 100644 --- a/src/theory/arith/nl/nl_model.h +++ b/src/theory/arith/nl/nl_model.h @@ -23,6 +23,7 @@ #include "context/context.h" #include "expr/kind.h" #include "expr/node.h" +#include "theory/arith/nl/nl_lemma_utils.h" #include "theory/theory_model.h" namespace CVC4 { @@ -152,7 +153,7 @@ class NlModel bool checkModel(const std::vector& assertions, const std::vector& false_asserts, unsigned d, - std::vector& lemmas, + std::vector& lemmas, std::vector& gs); /** * Set that we have used an approximation during this check. This flag is @@ -233,7 +234,7 @@ class NlModel * For instance, if eq reduces to a univariate quadratic equation with no * root, we send a conflict clause of the form a*x^2 + b*x + c != 0. */ - bool solveEqualitySimple(Node eq, unsigned d, std::vector& lemmas); + bool solveEqualitySimple(Node eq, unsigned d, std::vector& lemmas); /** simple check model for transcendental functions for literal * diff --git a/src/theory/arith/nl/nl_solver.cpp b/src/theory/arith/nl/nl_solver.cpp index 12cb02c70..c24ea41c8 100644 --- a/src/theory/arith/nl/nl_solver.cpp +++ b/src/theory/arith/nl/nl_solver.cpp @@ -165,9 +165,9 @@ void NlSolver::setMonomialFactor(Node a, Node b, const NodeMultiset& common) } } -std::vector NlSolver::checkSplitZero() +std::vector NlSolver::checkSplitZero() { - std::vector lemmas; + std::vector lemmas; for (unsigned i = 0; i < d_ms_vars.size(); i++) { Node v = d_ms_vars[i]; @@ -260,7 +260,7 @@ int NlSolver::compareSign(Node oa, unsigned a_index, int status, std::vector& exp, - std::vector& lem) + std::vector& lem) { Trace("nl-ext-debug") << "Process " << a << " at index " << a_index << ", status is " << status << std::endl; @@ -311,7 +311,7 @@ bool NlSolver::compareMonomial( Node b, NodeMultiset& b_exp_proc, std::vector& exp, - std::vector& lem, + std::vector& lem, std::map > >& cmp_infers) { Trace("nl-ext-comp-debug") @@ -415,7 +415,7 @@ bool NlSolver::compareMonomial( NodeMultiset& b_exp_proc, int status, std::vector& exp, - std::vector& lem, + std::vector& lem, std::map > >& cmp_infers) { Trace("nl-ext-comp-debug") @@ -628,9 +628,9 @@ bool NlSolver::compareMonomial( return false; } -std::vector NlSolver::checkMonomialSign() +std::vector NlSolver::checkMonomialSign() { - std::vector lemmas; + std::vector lemmas; std::map signs; Trace("nl-ext") << "Get monomial sign lemmas..." << std::endl; for (unsigned j = 0; j < d_ms.size(); j++) @@ -667,7 +667,7 @@ std::vector NlSolver::checkMonomialSign() return lemmas; } -std::vector NlSolver::checkMonomialMagnitude(unsigned c) +std::vector NlSolver::checkMonomialMagnitude(unsigned c) { // ensure information is setup if (c == 0) @@ -681,7 +681,7 @@ std::vector NlSolver::checkMonomialMagnitude(unsigned c) } unsigned r = 1; - std::vector lemmas; + std::vector lemmas; // if (x,y,L) in cmp_infers, then x > y inferred as conclusion of L // in lemmas std::map > > cmp_infers; @@ -803,7 +803,7 @@ std::vector NlSolver::checkMonomialMagnitude(unsigned c) Trace("nl-ext-comp") << "Compute redundancies for " << lemmas.size() << " lemmas." << std::endl; // naive - std::vector r_lemmas; + std::unordered_set r_lemmas; for (std::map > >::iterator itb = cmp_infers.begin(); itb != cmp_infers.end(); @@ -828,7 +828,7 @@ std::vector NlSolver::checkMonomialMagnitude(unsigned c) std::vector exp; if (cmp_holds(itc3->first, itc2->first, itb->second, exp, visited)) { - r_lemmas.push_back(itc2->second); + r_lemmas.insert(itc2->second); Trace("nl-ext-comp") << "...inference of " << itc->first << " > " << itc2->first << " was redundant." << std::endl; @@ -839,11 +839,10 @@ std::vector NlSolver::checkMonomialMagnitude(unsigned c) } } } - std::vector nr_lemmas; + std::vector nr_lemmas; for (unsigned i = 0; i < lemmas.size(); i++) { - if (std::find(r_lemmas.begin(), r_lemmas.end(), lemmas[i]) - == r_lemmas.end()) + if (r_lemmas.find(lemmas[i].d_lemma) == r_lemmas.end()) { nr_lemmas.push_back(lemmas[i]); } @@ -855,9 +854,9 @@ std::vector NlSolver::checkMonomialMagnitude(unsigned c) return nr_lemmas; } -std::vector NlSolver::checkTangentPlanes() +std::vector NlSolver::checkTangentPlanes() { - std::vector lemmas; + std::vector lemmas; Trace("nl-ext") << "Get monomial tangent plane lemmas..." << std::endl; NodeManager* nm = NodeManager::currentNM(); const std::map >& ccMap = @@ -1013,8 +1012,8 @@ std::vector NlSolver::checkTangentPlanes() return lemmas; } -std::vector NlSolver::checkMonomialInferBounds( - std::vector& nt_lemmas, +std::vector NlSolver::checkMonomialInferBounds( + std::vector& nt_lemmas, const std::vector& asserts, const std::vector& false_asserts) { @@ -1028,7 +1027,7 @@ std::vector NlSolver::checkMonomialInferBounds( const std::map >& cim = d_cdb.getConstraints(); - std::vector lemmas; + std::vector lemmas; NodeManager* nm = NodeManager::currentNM(); // register constraints Trace("nl-ext-debug") << "Register bound constraints..." << std::endl; @@ -1271,10 +1270,10 @@ std::vector NlSolver::checkMonomialInferBounds( return lemmas; } -std::vector NlSolver::checkFactoring( +std::vector NlSolver::checkFactoring( const std::vector& asserts, const std::vector& false_asserts) { - std::vector lemmas; + std::vector lemmas; NodeManager* nm = NodeManager::currentNM(); Trace("nl-ext") << "Get factoring lemmas..." << std::endl; for (const Node& lit : asserts) @@ -1401,7 +1400,7 @@ std::vector NlSolver::checkFactoring( return lemmas; } -Node NlSolver::getFactorSkolem(Node n, std::vector& lemmas) +Node NlSolver::getFactorSkolem(Node n, std::vector& lemmas) { std::map::iterator itf = d_factor_skolem.find(n); if (itf == d_factor_skolem.end()) @@ -1416,9 +1415,9 @@ Node NlSolver::getFactorSkolem(Node n, std::vector& lemmas) return itf->second; } -std::vector NlSolver::checkMonomialInferResBounds() +std::vector NlSolver::checkMonomialInferResBounds() { - std::vector lemmas; + std::vector lemmas; NodeManager* nm = NodeManager::currentNM(); Trace("nl-ext") << "Get monomial resolution inferred bound lemmas..." << std::endl; diff --git a/src/theory/arith/nl/nl_solver.h b/src/theory/arith/nl/nl_solver.h index 35c51569b..a2f514b9d 100644 --- a/src/theory/arith/nl/nl_solver.h +++ b/src/theory/arith/nl/nl_solver.h @@ -79,7 +79,7 @@ class NlSolver * t = 0 V t != 0 * where t is a term that exists in the current context. */ - std::vector checkSplitZero(); + std::vector checkSplitZero(); /** check monomial sign * @@ -96,7 +96,7 @@ class NlSolver * x < 0 => x*y*y < 0 * x = 0 => x*y*z = 0 */ - std::vector checkMonomialSign(); + std::vector checkMonomialSign(); /** check monomial magnitude * @@ -118,7 +118,7 @@ class NlSolver * against 1, 1 : compare non-linear monomials against variables, 2 : compare * non-linear monomials against other non-linear monomials. */ - std::vector checkMonomialMagnitude(unsigned c); + std::vector checkMonomialMagnitude(unsigned c); /** check monomial inferred bounds * @@ -137,8 +137,8 @@ class NlSolver * ...where (y > z + w) and x*y are a constraint and term * that occur in the current context. */ - std::vector checkMonomialInferBounds( - std::vector& nt_lemmas, + std::vector checkMonomialInferBounds( + std::vector& nt_lemmas, const std::vector& asserts, const std::vector& false_asserts); @@ -154,8 +154,8 @@ class NlSolver * ...where k is fresh and x*z + y*z > t is a * constraint that occurs in the current context. */ - std::vector checkFactoring(const std::vector& asserts, - const std::vector& false_asserts); + std::vector checkFactoring(const std::vector& asserts, + const std::vector& false_asserts); /** check monomial infer resolution bounds * @@ -171,7 +171,7 @@ class NlSolver * ...where s <= x*z and x*y <= t are constraints * that occur in the current context. */ - std::vector checkMonomialInferResBounds(); + std::vector checkMonomialInferResBounds(); /** check tangent planes * @@ -197,7 +197,7 @@ class NlSolver * ( ( x>2 ^ y>5) ^ (x<2 ^ y<5) ) => x*y > 5*x + 2*y - 10 * ( ( x>2 ^ y<5) ^ (x<2 ^ y>5) ) => x*y < 5*x + 2*y - 10 */ - std::vector checkTangentPlanes(); + std::vector checkTangentPlanes(); //-------------------------------------------- end lemma schemas private: @@ -295,7 +295,7 @@ class NlSolver unsigned a_index, int status, std::vector& exp, - std::vector& lem); + std::vector& lem); /** compare monomials a and b * * Initially, a call to this function is such that : @@ -338,7 +338,7 @@ class NlSolver Node b, NodeMultiset& b_exp_proc, std::vector& exp, - std::vector& lem, + std::vector& lem, std::map > >& cmp_infers); /** helper function for above * @@ -356,10 +356,10 @@ class NlSolver NodeMultiset& b_exp_proc, int status, std::vector& exp, - std::vector& lem, + std::vector& lem, std::map > >& cmp_infers); /** Get factor skolem for n, add resulting lemmas to lemmas */ - Node getFactorSkolem(Node n, std::vector& lemmas); + Node getFactorSkolem(Node n, std::vector& lemmas); }; /* class NlSolver */ } // namespace nl diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 4b2d2fd37..bf3e7fdda 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -33,6 +33,7 @@ namespace nl { NonlinearExtension::NonlinearExtension(TheoryArith& containing, eq::EqualityEngine* ee) : d_lemmas(containing.getUserContext()), + d_lemmasPp(containing.getUserContext()), d_containing(containing), d_ee(ee), d_needsLastCall(false), @@ -143,23 +144,22 @@ std::pair NonlinearExtension::isExtfReduced( return std::make_pair(true, Node::null()); } -void NonlinearExtension::sendLemmas(const std::vector& out, - bool preprocess, - std::map& lemSE) +void NonlinearExtension::sendLemmas(const std::vector& out) { - std::map::iterator its; - for (const Node& lem : out) + for (const NlLemma& nlem : out) { + Node lem = nlem.d_lemma; + bool preprocess = nlem.d_preprocess; Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << lem << std::endl; d_containing.getOutputChannel().lemma(lem, false, preprocess); // process the side effect - its = lemSE.find(lem); - if (its != lemSE.end()) + processSideEffect(nlem); + // add to cache if not preprocess + if (preprocess) { - processSideEffect(its->second); + d_lemmasPp.insert(lem); } - // add to cache if not preprocess - if (!preprocess) + else { d_lemmas.insert(lem); } @@ -168,36 +168,37 @@ void NonlinearExtension::sendLemmas(const std::vector& out, } } -void NonlinearExtension::processSideEffect(const NlLemmaSideEffect& se) +void NonlinearExtension::processSideEffect(const NlLemma& se) { d_trSlv.processSideEffect(se); } -unsigned NonlinearExtension::filterLemma(Node lem, std::vector& out) +unsigned NonlinearExtension::filterLemma(NlLemma lem, std::vector& out) { Trace("nl-ext-lemma-debug") - << "NonlinearExtension::Lemma pre-rewrite : " << lem << std::endl; - lem = Rewriter::rewrite(lem); - if (d_lemmas.find(lem) != d_lemmas.end() - || std::find(out.begin(), out.end(), lem) != out.end()) + << "NonlinearExtension::Lemma pre-rewrite : " << lem.d_lemma << std::endl; + lem.d_lemma = Rewriter::rewrite(lem.d_lemma); + // get the proper cache + NodeSet& lcache = lem.d_preprocess ? d_lemmasPp : d_lemmas; + if (lcache.find(lem.d_lemma) != lcache.end()) { Trace("nl-ext-lemma-debug") - << "NonlinearExtension::Lemma duplicate : " << lem << std::endl; + << "NonlinearExtension::Lemma duplicate : " << lem.d_lemma << std::endl; return 0; } out.push_back(lem); return 1; } -unsigned NonlinearExtension::filterLemmas(std::vector& lemmas, - std::vector& out) +unsigned NonlinearExtension::filterLemmas(std::vector& lemmas, + std::vector& out) { if (options::nlExtEntailConflicts()) { // check if any are entailed to be false - for (const Node& lem : lemmas) + for (const NlLemma& lem : lemmas) { - Node ch_lemma = lem.negate(); + Node ch_lemma = lem.d_lemma.negate(); ch_lemma = Rewriter::rewrite(ch_lemma); Trace("nl-ext-et-debug") << "Check entailment of " << ch_lemma << "..." << std::endl; @@ -207,8 +208,8 @@ unsigned NonlinearExtension::filterLemmas(std::vector& lemmas, << et.second << std::endl; if (et.first) { - Trace("nl-ext-et") << "*** Lemma entailed to be in conflict : " << lem - << std::endl; + Trace("nl-ext-et") << "*** Lemma entailed to be in conflict : " + << lem.d_lemma << std::endl; // return just this lemma if (filterLemma(lem, out) > 0) { @@ -220,7 +221,7 @@ unsigned NonlinearExtension::filterLemmas(std::vector& lemmas, } unsigned sum = 0; - for (const Node& lem : lemmas) + for (const NlLemma& lem : lemmas) { sum += filterLemma(lem, out); } @@ -371,7 +372,7 @@ std::vector NonlinearExtension::checkModelEval( bool NonlinearExtension::checkModel(const std::vector& assertions, const std::vector& false_asserts, - std::vector& lemmas, + std::vector& lemmas, std::vector& gs) { Trace("nl-ext-cm") << "--- check-model ---" << std::endl; @@ -396,24 +397,22 @@ bool NonlinearExtension::checkModel(const std::vector& assertions, int NonlinearExtension::checkLastCall(const std::vector& assertions, const std::vector& false_asserts, const std::vector& xts, - std::vector& lems, - std::vector& lemsPp, - std::vector& wlems, - std::map& lemSE) + std::vector& lems, + std::vector& wlems) { // initialize the non-linear solver d_nlSlv.initLastCall(assertions, false_asserts, xts); // initialize the trancendental function solver - std::vector lemmas; - d_trSlv.initLastCall(assertions, false_asserts, xts, lemmas, lemsPp); + std::vector lemmas; + d_trSlv.initLastCall(assertions, false_asserts, xts, lemmas); // process lemmas that may have been generated by the transcendental solver filterLemmas(lemmas, lems); - if (!lems.empty() || !lemsPp.empty()) + if (!lems.empty()) { Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas during registration." << std::endl; - return lems.size() + lemsPp.size(); + return lems.size(); } //----------------------------------- possibly split on zero @@ -480,7 +479,7 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, //-----------------------------------inferred bounds lemmas // e.g. x >= t => y*x >= y*t - std::vector nt_lemmas; + std::vector nt_lemmas; lemmas = d_nlSlv.checkMonomialInferBounds(nt_lemmas, assertions, false_asserts); // Trace("nl-ext") << "Bound lemmas : " << lemmas.size() << ", " << @@ -546,7 +545,7 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, } if (options::nlExtTfTangentPlanes()) { - lemmas = d_trSlv.checkTranscendentalTangentPlanes(lemSE); + lemmas = d_trSlv.checkTranscendentalTangentPlanes(); filterLemmas(lemmas, wlems); } Trace("nl-ext") << " ...finished with " << wlems.size() << " waiting lemmas." @@ -585,10 +584,9 @@ void NonlinearExtension::check(Theory::Effort e) else { // If we computed lemmas during collectModelInfo, send them now. - if (!d_cmiLemmas.empty() || !d_cmiLemmasPp.empty()) + if (!d_cmiLemmas.empty()) { - sendLemmas(d_cmiLemmas, false, d_cmiLemmasSE); - sendLemmas(d_cmiLemmasPp, true, d_cmiLemmasSE); + sendLemmas(d_cmiLemmas); return; } // Otherwise, we will answer SAT. The values that we approximated are @@ -608,10 +606,7 @@ void NonlinearExtension::check(Theory::Effort e) } } -bool NonlinearExtension::modelBasedRefinement( - std::vector& mlems, - std::vector& mlemsPp, - std::map& lemSE) +bool NonlinearExtension::modelBasedRefinement(std::vector& mlems) { // get the assertions std::vector assertions; @@ -691,15 +686,14 @@ bool NonlinearExtension::modelBasedRefinement( // 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; + 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, mlemsPp, wlems, lemSE); - if (!mlems.empty() || !mlemsPp.empty()) + checkLastCall(assertions, false_asserts, xts, mlems, wlems); + if (!mlems.empty()) { return true; } @@ -715,7 +709,7 @@ bool NonlinearExtension::modelBasedRefinement( << 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 lemmas; std::vector gs; if (checkModel(assertions, false_asserts, lemmas, gs)) { @@ -753,7 +747,7 @@ bool NonlinearExtension::modelBasedRefinement( complete_status = -1; if (!shared_term_value_splits.empty()) { - std::vector stvLemmas; + std::vector stvLemmas; for (const Node& eq : shared_term_value_splits) { Node req = Rewriter::rewrite(eq); @@ -814,12 +808,10 @@ void NonlinearExtension::interceptModel(std::map& arithModel) d_model.reset(d_containing.getValuation().getModel(), arithModel); // run a last call effort check d_cmiLemmas.clear(); - d_cmiLemmasPp.clear(); - d_cmiLemmasSE.clear(); if (!d_builtModel.get()) { Trace("nl-ext") << "interceptModel: do model-based refinement" << std::endl; - modelBasedRefinement(d_cmiLemmas, d_cmiLemmasPp, d_cmiLemmasSE); + modelBasedRefinement(d_cmiLemmas); } if (d_builtModel.get()) { diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index 855310daa..5cf2eb84b 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -147,8 +147,8 @@ class NonlinearExtension * 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 vectors d_cmiLemmas - * and d_cmiLemmasPp, which are then sent out (if necessary) when a last call + * 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); @@ -173,17 +173,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/lemsPp. + * This function returns true if a lemma was added to the vector lems. * 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. - * - * The argument lemSE is the "side effect" of the lemmas in mlems and mlemsPp - * (for details, see checkLastCall). */ - bool modelBasedRefinement(std::vector& mlems, - std::vector& mlemsPp, - std::map& lemSE); + bool modelBasedRefinement(std::vector& mlems); /** check last call * @@ -192,32 +187,24 @@ class NonlinearExtension * * xts : the list of (non-reduced) extended terms in the current context. * - * This method adds lemmas to arguments lems, lemsPp, and wlems, each of + * 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. * - * If the set lems or lemsPp is non-empty, then no further processing is + * 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 set lemsPp is distinguished from lems since - * the preprocess flag on the lemma(...) call should be set to true. + * 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. - * - * The argument lemSE is the "side effect" of the lemmas from the previous - * three calls. If a lemma is mapping to a side effect, it should be - * processed via a call to processSideEffect(...) immediately after the - * lemma is sent (if it is indeed sent on this call to check). */ int checkLastCall(const std::vector& assertions, const std::vector& false_asserts, const std::vector& xts, - std::vector& lems, - std::vector& lemsPp, - std::vector& wlems, - std::map& lemSE); + std::vector& lems, + std::vector& wlems); /** get assertions * @@ -259,7 +246,7 @@ class NonlinearExtension */ bool checkModel(const std::vector& assertions, const std::vector& false_asserts, - std::vector& lemmas, + std::vector& lemmas, std::vector& gs); //---------------------------end check model @@ -271,21 +258,22 @@ class NonlinearExtension * the number of lemmas added to out. We do not add lemmas that have already * been sent on the output channel of TheoryArith. */ - unsigned filterLemmas(std::vector& lemmas, std::vector& out); + unsigned filterLemmas(std::vector& lemmas, + std::vector& out); /** singleton version of above */ - unsigned filterLemma(Node lem, std::vector& out); + unsigned filterLemma(NlLemma lem, std::vector& out); /** * Send lemmas in out on the output channel of theory of arithmetic. */ - void sendLemmas(const std::vector& out, - bool preprocess, - std::map& lemSE); + void sendLemmas(const std::vector& out); /** Process side effect se */ - void processSideEffect(const NlLemmaSideEffect& se); + void processSideEffect(const NlLemma& se); /** cache of all lemmas sent on the output channel (user-context-dependent) */ NodeSet d_lemmas; + /** Same as above, for preprocessed lemmas */ + NodeSet d_lemmasPp; /** commonly used terms */ Node d_zero; Node d_one; @@ -316,14 +304,10 @@ class NonlinearExtension */ NlSolver d_nlSlv; /** - * The lemmas we computed during collectModelInfo. We store two vectors of - * lemmas to be sent out on the output channel of TheoryArith. The first - * is not preprocessed, the second is. + * The lemmas we computed during collectModelInfo, to be sent out on the + * output channel of TheoryArith. */ - std::vector d_cmiLemmas; - std::vector d_cmiLemmasPp; - /** the side effects of the above lemmas */ - std::map d_cmiLemmasSE; + std::vector d_cmiLemmas; /** * The approximations computed during collectModelInfo. For details, see * NlModel::getModelValueRepair. diff --git a/src/theory/arith/nl/transcendental_solver.cpp b/src/theory/arith/nl/transcendental_solver.cpp index 3e10f6397..3b5bdb17f 100644 --- a/src/theory/arith/nl/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental_solver.cpp @@ -50,8 +50,7 @@ TranscendentalSolver::~TranscendentalSolver() {} void TranscendentalSolver::initLastCall(const std::vector& assertions, const std::vector& false_asserts, const std::vector& xts, - std::vector& lems, - std::vector& lemsPp) + std::vector& lems) { d_funcCongClass.clear(); d_funcMap.clear(); @@ -213,7 +212,9 @@ void TranscendentalSolver::initLastCall(const std::vector& assertions, // note we must do preprocess on this lemma Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem << std::endl; - lemsPp.push_back(lem); + NlLemma nlem(lem); + nlem.d_preprocess = true; + lems.push_back(nlem); } if (Trace.isOn("nl-ext-mv")) @@ -333,7 +334,7 @@ unsigned TranscendentalSolver::getTaylorDegree() const return d_taylor_degree; } -void TranscendentalSolver::processSideEffect(const NlLemmaSideEffect& se) +void TranscendentalSolver::processSideEffect(const NlLemma& se) { for (const std::tuple& sp : se.d_secantPoint) { @@ -362,7 +363,7 @@ void TranscendentalSolver::mkPi() } } -void TranscendentalSolver::getCurrentPiBounds(std::vector& lemmas) +void TranscendentalSolver::getCurrentPiBounds(std::vector& lemmas) { NodeManager* nm = NodeManager::currentNM(); Node pi_lem = nm->mkNode(AND, @@ -371,10 +372,10 @@ void TranscendentalSolver::getCurrentPiBounds(std::vector& lemmas) lemmas.push_back(pi_lem); } -std::vector TranscendentalSolver::checkTranscendentalInitialRefine() +std::vector TranscendentalSolver::checkTranscendentalInitialRefine() { NodeManager* nm = NodeManager::currentNM(); - std::vector lemmas; + std::vector lemmas; Trace("nl-ext") << "Get initial refinement lemmas for transcendental functions..." << std::endl; @@ -462,9 +463,9 @@ std::vector TranscendentalSolver::checkTranscendentalInitialRefine() return lemmas; } -std::vector TranscendentalSolver::checkTranscendentalMonotonic() +std::vector TranscendentalSolver::checkTranscendentalMonotonic() { - std::vector lemmas; + std::vector lemmas; Trace("nl-ext") << "Get monotonicity lemmas for transcendental functions..." << std::endl; @@ -644,10 +645,9 @@ std::vector TranscendentalSolver::checkTranscendentalMonotonic() return lemmas; } -std::vector TranscendentalSolver::checkTranscendentalTangentPlanes( - std::map& lemSE) +std::vector TranscendentalSolver::checkTranscendentalTangentPlanes() { - std::vector lemmas; + std::vector lemmas; Trace("nl-ext") << "Get tangent plane lemmas for transcendental functions..." << std::endl; // this implements Figure 3 of "Satisfiaility Modulo Transcendental Functions @@ -683,7 +683,7 @@ std::vector TranscendentalSolver::checkTranscendentalTangentPlanes( { Trace("nl-ext-tftp") << "- run at degree " << d << "..." << std::endl; unsigned prev = lemmas.size(); - if (checkTfTangentPlanesFun(tf, d, lemmas, lemSE)) + if (checkTfTangentPlanesFun(tf, d, lemmas)) { Trace("nl-ext-tftp") << "...fail, #lemmas = " << (lemmas.size() - prev) << std::endl; @@ -700,11 +700,9 @@ std::vector TranscendentalSolver::checkTranscendentalTangentPlanes( return lemmas; } -bool TranscendentalSolver::checkTfTangentPlanesFun( - Node tf, - unsigned d, - std::vector& lemmas, - std::map& lemSE) +bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, + unsigned d, + std::vector& lemmas) { NodeManager* nm = NodeManager::currentNM(); Kind k = tf.getKind(); @@ -1020,10 +1018,11 @@ bool TranscendentalSolver::checkTfTangentPlanesFun( Assert(!lemmaConj.empty()); Node lem = lemmaConj.size() == 1 ? lemmaConj[0] : nm->mkNode(AND, lemmaConj); - lemmas.push_back(lem); + NlLemma nlem(lem); // The side effect says that if lem is added, then we should add the // secant point c for (tf,d). - lemSE[lem].d_secantPoint.push_back(std::make_tuple(tf, d, c)); + nlem.d_secantPoint.push_back(std::make_tuple(tf, d, c)); + lemmas.push_back(nlem); } return true; } diff --git a/src/theory/arith/nl/transcendental_solver.h b/src/theory/arith/nl/transcendental_solver.h index 5cd57d8fa..0285b49e3 100644 --- a/src/theory/arith/nl/transcendental_solver.h +++ b/src/theory/arith/nl/transcendental_solver.h @@ -55,14 +55,13 @@ class TranscendentalSolver * model, and xts is the set of extended function terms that are active in * the current context. * - * This call may add lemmas to lems/lemsPp based on registering term + * This call may add lemmas to lems based on registering term * information (for example, purification of sine terms). */ void initLastCall(const std::vector& assertions, const std::vector& false_asserts, const std::vector& xts, - std::vector& lems, - std::vector& lemsPp); + std::vector& lems); /** increment taylor degree */ void incrementTaylorDegree(); /** get taylor degree */ @@ -76,8 +75,8 @@ class TranscendentalSolver * was conflicting. */ bool preprocessAssertionsCheckModel(std::vector& assertions); - /** Process side effect se */ - void processSideEffect(const NlLemmaSideEffect& se); + /** Process side effects in lemma se */ + void processSideEffect(const NlLemma& se); //-------------------------------------------- lemma schemas /** check transcendental initial refine * @@ -95,7 +94,7 @@ class TranscendentalSolver * exp( x )>0 * x<0 => exp( x )<1 */ - std::vector checkTranscendentalInitialRefine(); + std::vector checkTranscendentalInitialRefine(); /** check transcendental monotonic * @@ -109,7 +108,7 @@ class TranscendentalSolver * PI/2 > x > y > 0 => sin( x ) > sin( y ) * PI > x > y > PI/2 => sin( x ) < sin( y ) */ - std::vector checkTranscendentalMonotonic(); + std::vector checkTranscendentalMonotonic(); /** check transcendental tangent planes * @@ -168,12 +167,8 @@ class TranscendentalSolver * ( 1 < y < PI/2 ) => (sin y) >= c1*(y+c2) * where c1, c2 are rationals (for brevity, omitted here) * such that c1 ~= .277 and c2 ~= 2.032. - * - * The argument lemSE is the "side effect" of the lemmas in the return - * value of this function (for details, see checkLastCall). */ - std::vector checkTranscendentalTangentPlanes( - std::map& lemSE); + std::vector checkTranscendentalTangentPlanes(); /** check transcendental function refinement for tf * * This method is called by the above method for each "master" @@ -185,16 +180,13 @@ class TranscendentalSolver * * This runs Figure 3 of Cimatti et al., CADE 2017 for transcendental * function application tf for Taylor degree d. It may add a secant or - * tangent plane lemma to lems and its side effect (if one exists) - * to lemSE. + * tangent plane lemma to lems, which includes the side effect of the lemma + * (if one exists). * * It returns false if the bounds are not precise enough to add a * secant or tangent plane lemma. */ - bool checkTfTangentPlanesFun(Node tf, - unsigned d, - std::vector& lems, - std::map& lemSE); + bool checkTfTangentPlanesFun(Node tf, unsigned d, std::vector& lems); //-------------------------------------------- end lemma schemas private: /** polynomial approximation bounds @@ -276,7 +268,7 @@ class TranscendentalSolver Node getDerivative(Node n, Node x); void mkPi(); - void getCurrentPiBounds(std::vector& lemmas); + void getCurrentPiBounds(std::vector& lemmas); /** Make the node -pi <= a <= pi */ static Node mkValidPhase(Node a, Node pi); -- 2.30.2