diff options
Diffstat (limited to 'src/theory/arith/nonlinear_extension.cpp')
-rw-r--r-- | src/theory/arith/nonlinear_extension.cpp | 91 |
1 files changed, 65 insertions, 26 deletions
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index 65daf8436..2d530d602 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -540,17 +540,38 @@ Node NonlinearExtension::mkMonomialRemFactor( } void NonlinearExtension::sendLemmas(const std::vector<Node>& out, - bool preprocess) + bool preprocess, + std::map<Node, NlLemmaSideEffect>& lemSE) { + std::map<Node, NlLemmaSideEffect>::iterator its; for (const Node& lem : out) { 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(its->second); + } // add to cache if not preprocess if (!preprocess) { d_lemmas.insert(lem); } + // also indicate this is a tautology + d_model.addTautology(lem); + } +} + +void NonlinearExtension::processSideEffect(const NlLemmaSideEffect& se) +{ + for (const std::tuple<Node, unsigned, Node>& sp : se.d_secantPoint) + { + Node tf = std::get<0>(sp); + unsigned d = std::get<1>(sp); + Node c = std::get<2>(sp); + d_secant_points[tf][d].push_back(c); } } @@ -890,7 +911,8 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, const std::vector<Node>& xts, std::vector<Node>& lems, std::vector<Node>& lemsPp, - std::vector<Node>& wlems) + std::vector<Node>& wlems, + std::map<Node, NlLemmaSideEffect>& lemSE) { d_ms_vars.clear(); d_ms_proc.clear(); @@ -1262,7 +1284,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, } if (options::nlExtTfTangentPlanes()) { - lemmas = checkTranscendentalTangentPlanes(); + lemmas = checkTranscendentalTangentPlanes(lemSE); filterLemmas(lemmas, wlems); } Trace("nl-ext") << " ...finished with " << wlems.size() << " waiting lemmas." @@ -1297,8 +1319,8 @@ void NonlinearExtension::check(Theory::Effort e) { // If we computed lemmas during collectModelInfo, send them now. if (!d_cmiLemmas.empty() || !d_cmiLemmasPp.empty()) { - sendLemmas(d_cmiLemmas); - sendLemmas(d_cmiLemmasPp, true); + sendLemmas(d_cmiLemmas, false, d_cmiLemmasSE); + sendLemmas(d_cmiLemmasPp, true, d_cmiLemmasSE); return; } // Otherwise, we will answer SAT. The values that we approximated are @@ -1318,8 +1340,10 @@ void NonlinearExtension::check(Theory::Effort e) { } } -bool NonlinearExtension::modelBasedRefinement(std::vector<Node>& mlems, - std::vector<Node>& mlemsPp) +bool NonlinearExtension::modelBasedRefinement( + std::vector<Node>& mlems, + std::vector<Node>& mlemsPp, + std::map<Node, NlLemmaSideEffect>& lemSE) { // get the assertions std::vector<Node> assertions; @@ -1405,7 +1429,8 @@ bool NonlinearExtension::modelBasedRefinement(std::vector<Node>& mlems, 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); + checkLastCall( + assertions, false_asserts, xts, mlems, mlemsPp, wlems, lemSE); if (!mlems.empty() || !mlemsPp.empty()) { return true; @@ -1522,10 +1547,11 @@ void NonlinearExtension::interceptModel(std::map<Node, Node>& 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); + modelBasedRefinement(d_cmiLemmas, d_cmiLemmasPp, d_cmiLemmasSE); } if (d_builtModel.get()) { @@ -3011,7 +3037,8 @@ std::vector<Node> NonlinearExtension::checkTranscendentalMonotonic() { return lemmas; } -std::vector<Node> NonlinearExtension::checkTranscendentalTangentPlanes() +std::vector<Node> NonlinearExtension::checkTranscendentalTangentPlanes( + std::map<Node, NlLemmaSideEffect>& lemSE) { std::vector<Node> lemmas; Trace("nl-ext") << "Get tangent plane lemmas for transcendental functions..." @@ -3051,7 +3078,7 @@ std::vector<Node> NonlinearExtension::checkTranscendentalTangentPlanes() { Trace("nl-ext-tftp") << "- run at degree " << d << "..." << std::endl; unsigned prev = lemmas.size(); - if (!checkTfTangentPlanesFun(tf, d, lemmas)) + if (!checkTfTangentPlanesFun(tf, d, lemmas, lemSE)) { Trace("nl-ext-tftp") << "...fail, #lemmas = " << (lemmas.size() - prev) << std::endl; @@ -3069,9 +3096,11 @@ std::vector<Node> NonlinearExtension::checkTranscendentalTangentPlanes() return lemmas; } -bool NonlinearExtension::checkTfTangentPlanesFun(Node tf, - unsigned d, - std::vector<Node>& lemmas) +bool NonlinearExtension::checkTfTangentPlanesFun( + Node tf, + unsigned d, + std::vector<Node>& lemmas, + std::map<Node, NlLemmaSideEffect>& lemSE) { Assert(d_model.isRefineableTfFun(tf)); @@ -3257,23 +3286,24 @@ bool NonlinearExtension::checkTfTangentPlanesFun(Node tf, Assert(std::find( d_secant_points[tf][d].begin(), d_secant_points[tf][d].end(), c) == d_secant_points[tf][d].end()); - // insert into the vector - d_secant_points[tf][d].push_back(c); + // Insert into the (temporary) vector. We do not update this vector + // until we are sure this secant plane lemma has been processed. We do + // this by mapping the lemma to a side effect below. + std::vector<Node> spoints = d_secant_points[tf][d]; + spoints.push_back(c); + // sort SortNlModel smv; smv.d_nlm = &d_model; smv.d_isConcrete = true; - std::sort( - d_secant_points[tf][d].begin(), d_secant_points[tf][d].end(), smv); + std::sort(spoints.begin(), spoints.end(), smv); // get the resulting index of c unsigned index = - std::find( - d_secant_points[tf][d].begin(), d_secant_points[tf][d].end(), c) - - d_secant_points[tf][d].begin(); + std::find(spoints.begin(), spoints.end(), c) - spoints.begin(); // bounds are the next closest upper/lower bound values if (index > 0) { - bounds[0] = d_secant_points[tf][d][index - 1]; + bounds[0] = spoints[index - 1]; } else { @@ -3289,9 +3319,9 @@ bool NonlinearExtension::checkTfTangentPlanesFun(Node tf, bounds[0] = Rewriter::rewrite(nm->mkNode(MINUS, c, d_one)); } } - if (index < d_secant_points[tf][d].size() - 1) + if (index < spoints.size() - 1) { - bounds[1] = d_secant_points[tf][d][index + 1]; + bounds[1] = spoints[index + 1]; } else { @@ -3310,6 +3340,8 @@ bool NonlinearExtension::checkTfTangentPlanesFun(Node tf, Trace("nl-ext-tftp-debug2") << "...secant bounds are : " << bounds[0] << " ... " << bounds[1] << std::endl; + // the secant plane may be conjunction of 1-2 guarded inequalities + std::vector<Node> lemmaConj; for (unsigned s = 0; s < 2; s++) { // compute secant plane @@ -3370,11 +3402,18 @@ bool NonlinearExtension::checkTfTangentPlanesFun(Node tf, lem = Rewriter::rewrite(lem); Trace("nl-ext-tftp-lemma") << "*** Secant plane lemma : " << lem << std::endl; - // Figure 3 : line 22 - lemmas.push_back(lem); + lemmaConj.push_back(lem); Assert(d_model.computeAbstractModelValue(lem) == d_false); } } + // Figure 3 : line 22 + Assert(!lemmaConj.empty()); + Node lem = + lemmaConj.size() == 1 ? lemmaConj[0] : nm->mkNode(AND, lemmaConj); + lemmas.push_back(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)); } return false; } |