From: Andrew Reynolds Date: Tue, 3 Dec 2019 22:51:22 +0000 (-0600) Subject: Improve flexibility of lemma output in non-linear solver (#3518) X-Git-Tag: cvc5-1.0.0~3804 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=48ba9401dd647e737b79f1605dc68c44119e5baf;p=cvc5.git Improve flexibility of lemma output in non-linear solver (#3518) --- diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index d76089541..287acbc36 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -540,28 +540,46 @@ Node NonlinearExtension::mkMonomialRemFactor( return ret; } -int NonlinearExtension::flushLemma(Node lem) { +void NonlinearExtension::sendLemmas(const std::vector& out, + bool preprocess) +{ + for (const Node& lem : out) + { + Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << lem << std::endl; + d_containing.getOutputChannel().lemma(lem, false, preprocess); + // add to cache if not preprocess + if (!preprocess) + { + d_lemmas.insert(lem); + } + } +} + +unsigned NonlinearExtension::filterLemma(Node lem, std::vector& out) +{ Trace("nl-ext-lemma-debug") << "NonlinearExtension::Lemma pre-rewrite : " << lem << std::endl; lem = Rewriter::rewrite(lem); - if (Contains(d_lemmas, lem)) { + if (d_lemmas.find(lem) != d_lemmas.end() + || std::find(out.begin(), out.end(), lem) != out.end()) + { Trace("nl-ext-lemma-debug") << "NonlinearExtension::Lemma duplicate : " << lem << std::endl; - // should not generate duplicates - // Assert( false ); return 0; } - d_lemmas.insert(lem); - Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << lem << std::endl; - d_containing.getOutputChannel().lemma(lem); + out.push_back(lem); return 1; } -int NonlinearExtension::flushLemmas(std::vector& lemmas) { - if (options::nlExtEntailConflicts()) { +unsigned NonlinearExtension::filterLemmas(std::vector& lemmas, + std::vector& out) +{ + if (options::nlExtEntailConflicts()) + { // check if any are entailed to be false - for (unsigned i = 0; i < lemmas.size(); i++) { - Node ch_lemma = lemmas[i].negate(); + for (const Node& lem : lemmas) + { + Node ch_lemma = lem.negate(); ch_lemma = Rewriter::rewrite(ch_lemma); Trace("nl-ext-et-debug") << "Check entailment of " << ch_lemma << "..." << std::endl; @@ -569,11 +587,13 @@ int NonlinearExtension::flushLemmas(std::vector& lemmas) { THEORY_OF_TYPE_BASED, ch_lemma); Trace("nl-ext-et-debug") << "entailment test result : " << et.first << " " << et.second << std::endl; - if (et.first) { - Trace("nl-ext-et") << "*** Lemma entailed to be in conflict : " - << lemmas[i] << std::endl; + if (et.first) + { + Trace("nl-ext-et") << "*** Lemma entailed to be in conflict : " << lem + << std::endl; // return just this lemma - if (flushLemma(lemmas[i])) { + if (filterLemma(lem, out) > 0) + { lemmas.clear(); return 1; } @@ -581,9 +601,10 @@ int NonlinearExtension::flushLemmas(std::vector& lemmas) { } } - int sum = 0; - for (unsigned i = 0; i < lemmas.size(); i++) { - sum += flushLemma(lemmas[i]); + unsigned sum = 0; + for (const Node& lem : lemmas) + { + sum += filterLemma(lem, out); } lemmas.clear(); return sum; @@ -730,7 +751,9 @@ std::vector NonlinearExtension::checkModelEval( } bool NonlinearExtension::checkModel(const std::vector& assertions, - const std::vector& false_asserts) + const std::vector& false_asserts, + std::vector& lemmas, + std::vector& gs) { Trace("nl-ext-cm") << "--- check-model ---" << std::endl; @@ -791,23 +814,8 @@ bool NonlinearExtension::checkModel(const std::vector& assertions, } } } - std::vector lemmas; - std::vector gs; bool ret = d_model.checkModel( passertions, false_asserts, d_taylor_degree, lemmas, gs); - for (Node& mg : gs) - { - mg = Rewriter::rewrite(mg); - mg = d_containing.getValuation().ensureLiteral(mg); - d_containing.getOutputChannel().requirePhase(mg, true); - d_builtModel = true; - } - for (Node& lem : lemmas) - { - Trace("nl-ext-lemma-model") - << "Lemma from check model : " << lem << std::endl; - d_containing.getOutputChannel().lemma(lem); - } return ret; } @@ -856,7 +864,10 @@ class ArgTrie int NonlinearExtension::checkLastCall(const std::vector& assertions, const std::vector& false_asserts, - const std::vector& xts) + const std::vector& xts, + std::vector& lems, + std::vector& lemsPp, + std::vector& wlems) { d_ms_vars.clear(); d_ms_proc.clear(); @@ -869,9 +880,7 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, d_ci_max.clear(); d_f_map.clear(); d_tf_region.clear(); - d_waiting_lemmas.clear(); - int lemmas_proc = 0; std::vector lemmas; NodeManager* nm = NodeManager::currentNM(); @@ -989,10 +998,12 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, getCurrentPiBounds(lemmas); } - lemmas_proc = flushLemmas(lemmas); - if (lemmas_proc > 0) { - Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas during registration." << std::endl; - return lemmas_proc; + filterLemmas(lemmas, lems); + if (!lems.empty()) + { + Trace("nl-ext") << " ...finished with " << lems.size() + << " new lemmas during registration." << std::endl; + return lems.size(); } // process SINE phase shifting @@ -1035,15 +1046,14 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, // must do preprocess on this one Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem << std::endl; - d_containing.getOutputChannel().lemma(lem, false, true); - lemmas_proc++; + lemsPp.push_back(lem); } } - if (lemmas_proc > 0) + if (!lemsPp.empty()) { - Trace("nl-ext") << " ...finished with " << lemmas_proc + Trace("nl-ext") << " ...finished with " << lemsPp.size() << " new lemmas SINE phase shifting." << std::endl; - return lemmas_proc; + return lemsPp.size(); } Trace("nl-ext") << "We have " << d_ms.size() << " monomials." << std::endl; @@ -1088,35 +1098,43 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, if (options::nlExtSplitZero()) { Trace("nl-ext") << "Get zero split lemmas..." << std::endl; lemmas = checkSplitZero(); - lemmas_proc = flushLemmas(lemmas); - if (lemmas_proc > 0) { - Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." << std::endl; - return lemmas_proc; + filterLemmas(lemmas, lems); + if (!lems.empty()) + { + Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas." + << std::endl; + return lems.size(); } } //-----------------------------------initial lemmas for transcendental functions lemmas = checkTranscendentalInitialRefine(); - lemmas_proc = flushLemmas(lemmas); - if (lemmas_proc > 0) { - Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." << std::endl; - return lemmas_proc; + filterLemmas(lemmas, lems); + if (!lems.empty()) + { + Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas." + << std::endl; + return lems.size(); } - + //-----------------------------------lemmas based on sign (comparison to zero) lemmas = checkMonomialSign(); - lemmas_proc = flushLemmas(lemmas); - if (lemmas_proc > 0) { - Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." << std::endl; - return lemmas_proc; + filterLemmas(lemmas, lems); + if (!lems.empty()) + { + Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas." + << std::endl; + return lems.size(); } - + //-----------------------------------monotonicity of transdental functions lemmas = checkTranscendentalMonotonic(); - lemmas_proc = flushLemmas(lemmas); - if (lemmas_proc > 0) { - Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." << std::endl; - return lemmas_proc; + filterLemmas(lemmas, lems); + if (!lems.empty()) + { + Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas." + << std::endl; + return lems.size(); } //-----------------------------------lemmas based on magnitude of non-zero monomials @@ -1138,12 +1156,13 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, // c is effort level lemmas = checkMonomialMagnitude( c ); unsigned nlem = lemmas.size(); - lemmas_proc = flushLemmas(lemmas); - if (lemmas_proc > 0) { - Trace("nl-ext") << " ...finished with " << lemmas_proc + filterLemmas(lemmas, lems); + if (!lems.empty()) + { + Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas (out of possible " << nlem << ")." << std::endl; - return lemmas_proc; + return lems.size(); } } @@ -1162,36 +1181,40 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, // Trace("nl-ext") << "Bound lemmas : " << lemmas.size() << ", " << // nt_lemmas.size() << std::endl; prioritize lemmas that do not // introduce new monomials - lemmas_proc = flushLemmas(lemmas); + filterLemmas(lemmas, lems); if (options::nlExtTangentPlanes() && options::nlExtTangentPlanesInterleave()) { lemmas = checkTangentPlanes(); - lemmas_proc += flushLemmas(lemmas); + filterLemmas(lemmas, lems); } - if (lemmas_proc > 0) { - Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." + if (!lems.empty()) + { + Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas." << std::endl; - return lemmas_proc; + return lems.size(); } - + // from inferred bound inferences : now do ones that introduce new terms - lemmas_proc = flushLemmas(nt_lemmas); - if (lemmas_proc > 0) { - Trace("nl-ext") << " ...finished with " << lemmas_proc + filterLemmas(nt_lemmas, lems); + if (!lems.empty()) + { + Trace("nl-ext") << " ...finished with " << lems.size() << " new (monomial-introducing) lemmas." << std::endl; - return lemmas_proc; + return lems.size(); } - + //------------------------------------factoring lemmas // x*y + x*z >= t => exists k. k = y + z ^ x*k >= t if( options::nlExtFactor() ){ lemmas = checkFactoring(assertions, false_asserts); - lemmas_proc = flushLemmas(lemmas); - if (lemmas_proc > 0) { - Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." << std::endl; - return lemmas_proc; + filterLemmas(lemmas, lems); + if (!lems.empty()) + { + Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas." + << std::endl; + return lems.size(); } } @@ -1199,10 +1222,12 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, // e.g. ( y>=0 ^ s <= x*z ^ x*y <= t ) => y*s <= z*t if (options::nlExtResBound()) { lemmas = checkMonomialInferResBounds(); - lemmas_proc = flushLemmas(lemmas); - if (lemmas_proc > 0) { - Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." << std::endl; - return lemmas_proc; + filterLemmas(lemmas, lems); + if (!lems.empty()) + { + Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas." + << std::endl; + return lems.size(); } } @@ -1210,19 +1235,15 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, if (options::nlExtTangentPlanes() && !options::nlExtTangentPlanesInterleave()) { lemmas = checkTangentPlanes(); - d_waiting_lemmas.insert( - d_waiting_lemmas.end(), lemmas.begin(), lemmas.end()); - lemmas.clear(); + filterLemmas(lemmas, wlems); } if (options::nlExtTfTangentPlanes()) { lemmas = checkTranscendentalTangentPlanes(); - d_waiting_lemmas.insert( - d_waiting_lemmas.end(), lemmas.begin(), lemmas.end()); - lemmas.clear(); + filterLemmas(lemmas, wlems); } - Trace("nl-ext") << " ...finished with " << d_waiting_lemmas.size() - << " waiting lemmas." << std::endl; + Trace("nl-ext") << " ...finished with " << wlems.size() << " waiting lemmas." + << std::endl; return 0; } @@ -1255,9 +1276,13 @@ void NonlinearExtension::check(Theory::Effort e) { TheoryModel* tm = d_containing.getValuation().getModel(); if (!d_builtModel.get()) { - // run model-based refinement - if (modelBasedRefinement()) + // run a last call effort check + std::vector mlems; + std::vector mlemsPp; + if (modelBasedRefinement(mlems, mlemsPp)) { + sendLemmas(mlems); + sendLemmas(mlemsPp, true); return; } } @@ -1278,7 +1303,8 @@ void NonlinearExtension::check(Theory::Effort e) { } } -bool NonlinearExtension::modelBasedRefinement() +bool NonlinearExtension::modelBasedRefinement(std::vector& mlems, + std::vector& mlemsPp) { // reset the model object d_model.reset(d_containing.getValuation().getModel()); @@ -1359,14 +1385,15 @@ bool NonlinearExtension::modelBasedRefinement() // complete_status: // 1 : we may answer SAT, -1 : we may not answer SAT, 0 : unknown int complete_status = 1; - int num_added_lemmas = 0; - // we require a check either if an assertion is false or a shared term has + // 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; - num_added_lemmas = checkLastCall(assertions, false_asserts, xts); - if (num_added_lemmas > 0) + checkLastCall(assertions, false_asserts, xts, mlems, mlemsPp, wlems); + if (!mlems.empty() || !mlemsPp.empty()) { return true; } @@ -1382,20 +1409,34 @@ 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. - if (checkModel(assertions, false_asserts)) + std::vector lemmas; + std::vector gs; + if (checkModel(assertions, false_asserts, lemmas, gs)) { complete_status = 1; } + for (const Node& mg : gs) + { + Node mgr = Rewriter::rewrite(mg); + mgr = d_containing.getValuation().ensureLiteral(mgr); + d_containing.getOutputChannel().requirePhase(mgr, true); + d_builtModel = true; + } + filterLemmas(lemmas, mlems); + if (!mlems.empty()) + { + return true; + } } // if we have not concluded SAT if (complete_status != 1) { // flush the waiting lemmas - num_added_lemmas = flushLemmas(d_waiting_lemmas); - if (num_added_lemmas > 0) + if (!wlems.empty()) { - Trace("nl-ext") << "...added " << num_added_lemmas << " waiting lemmas." + mlems.insert(mlems.end(), wlems.begin(), wlems.end()); + Trace("nl-ext") << "...added " << wlems.size() << " waiting lemmas." << std::endl; return true; } @@ -1406,20 +1447,20 @@ bool NonlinearExtension::modelBasedRefinement() complete_status = -1; if (!shared_term_value_splits.empty()) { - std::vector shared_term_value_lemmas; + std::vector stvLemmas; for (const Node& eq : shared_term_value_splits) { Node req = Rewriter::rewrite(eq); Node literal = d_containing.getValuation().ensureLiteral(req); d_containing.getOutputChannel().requirePhase(literal, true); Trace("nl-ext-debug") << "Split on : " << literal << std::endl; - shared_term_value_lemmas.push_back( - literal.orNode(literal.negate())); + Node split = literal.orNode(literal.negate()); + filterLemma(split, stvLemmas); } - num_added_lemmas = flushLemmas(shared_term_value_lemmas); - if (num_added_lemmas > 0) + if (!stvLemmas.empty()) { - Trace("nl-ext") << "...added " << num_added_lemmas + mlems.insert(mlems.end(), stvLemmas.begin(), stvLemmas.end()); + Trace("nl-ext") << "...added " << stvLemmas.size() << " shared term value split lemmas." << std::endl; return true; } diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h index 1690c9334..20357b722 100644 --- a/src/theory/arith/nonlinear_extension.h +++ b/src/theory/arith/nonlinear_extension.h @@ -138,13 +138,13 @@ 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 sent out on the output - * channel of the theory of arithmetic. 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 true if a lemma was added to the vector lems/lemsPp. + * 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(); + bool modelBasedRefinement(std::vector& mlems, + std::vector& mlemsPp); /** returns true if the multiset containing the * factors of monomial a is a subset of the multiset * containing the factors of monomial b. @@ -181,12 +181,26 @@ class NonlinearExtension { * * xts : the list of (non-reduced) extended terms in the current context. * - * This method returns the number of lemmas added on the output channel of - * TheoryArith. + * This method adds lemmas to arguments lems, lemsPp, 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 + * 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. + * + * 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); + const std::vector& xts, + std::vector& lems, + std::vector& lemsPp, + std::vector& wlems); //---------------------------------------term utilities static bool isArithKind(Kind k); static Node mkLit(Node a, Node b, int status, bool isAbsolute = false); @@ -240,9 +254,15 @@ class NonlinearExtension { * * For details, see Section 3 of Cimatti et al CADE 2017 under the heading * "Detecting Satisfiable Formulas". + * + * The arguments lemmas and gs store the lemmas and guard literals to be sent + * out on the output channel of TheoryArith as lemmas and calls to + * ensureLiteral respectively. */ bool checkModel(const std::vector& assertions, - const std::vector& false_asserts); + const std::vector& false_asserts, + std::vector& lemmas, + std::vector& gs); //---------------------------end check model /** In the following functions, status states a relationship @@ -327,18 +347,19 @@ class NonlinearExtension { /** Is n entailed with polarity pol in the current context? */ bool isEntailed(Node n, bool pol); - /** flush lemmas - * - * Potentially sends lem on the output channel if lem has not been sent on the - * output channel in this context. Returns the number of lemmas sent on the - * output channel of TheoryArith. + /** + * Potentially adds lemmas to the set out and clears lemmas. Returns + * the number of lemmas added to out. We do not add lemmas that have already + * been sent on the output channel of TheoryArith. */ - int flushLemma(Node lem); + unsigned filterLemmas(std::vector& lemmas, std::vector& out); + /** singleton version of above */ + unsigned filterLemma(Node lem, std::vector& out); - /** Potentially sends lemmas to the output channel and clears lemmas. Returns - * the number of lemmas sent to the output channel. + /** + * Send lemmas in out on the output channel of theory of arithmetic. */ - int flushLemmas(std::vector& lemmas); + void sendLemmas(const std::vector& out, bool preprocess = false); // Returns the NodeMultiset for an existing monomial. const NodeMultiset& getMonomialExponentMap(Node monomial) const; @@ -439,8 +460,6 @@ class NonlinearExtension { /** Stores skolems in the range of the above map */ std::map d_tr_is_base; std::map< Node, bool > d_tf_initial_refine; - /** the list of lemmas we are waiting to flush until after check model */ - std::vector d_waiting_lemmas; void mkPi(); void getCurrentPiBounds( std::vector< Node >& lemmas );