diff options
Diffstat (limited to 'src/theory/arith/nl/nonlinear_extension.cpp')
-rw-r--r-- | src/theory/arith/nl/nonlinear_extension.cpp | 25 |
1 files changed, 22 insertions, 3 deletions
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 5ded7d3d0..bd48a726a 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -40,6 +40,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, d_model(containing.getSatContext()), d_trSlv(d_model), d_nlSlv(containing, d_model), + d_iandSlv(containing, d_model), d_builtModel(containing.getSatContext(), false) { d_true = NodeManager::currentNM()->mkConst(true); @@ -96,8 +97,9 @@ std::pair<bool, Node> NonlinearExtension::isExtfReduced( if (n != d_zero) { Kind k = n.getKind(); - return std::make_pair(k != NONLINEAR_MULT && !isTranscendentalKind(k), - Node::null()); + return std::make_pair( + k != NONLINEAR_MULT && !isTranscendentalKind(k) && k != IAND, + Node::null()); } Assert(n == d_zero); if (on.getKind() == NONLINEAR_MULT) @@ -402,6 +404,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, std::vector<NlLemma>& wlems) { std::vector<NlLemma> lemmas; + if (options::nlExt()) { // initialize the non-linear solver @@ -411,6 +414,10 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, // process lemmas that may have been generated by the transcendental solver filterLemmas(lemmas, lems); } + + // init last call with IAND + d_iandSlv.initLastCall(assertions, false_asserts, xts); + if (!lems.empty()) { Trace("nl-ext") << " ...finished with " << lems.size() @@ -445,7 +452,16 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, return lems.size(); } } - + //-----------------------------------initial lemmas for iand + lemmas = d_iandSlv.checkInitialRefine(); + filterLemmas(lemmas, lems); + if (!lems.empty()) + { + Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas." + << std::endl; + return lems.size(); + } + // main calls to nlExt if (options::nlExt()) { @@ -559,6 +575,9 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, filterLemmas(lemmas, wlems); } } + // run the full refinement in the IAND solver + lemmas = d_iandSlv.checkFullRefine(); + filterLemmas(lemmas, wlems); Trace("nl-ext") << " ...finished with " << wlems.size() << " waiting lemmas." << std::endl; |