diff options
Diffstat (limited to 'src/theory/arith/nl/nonlinear_extension.cpp')
-rw-r--r-- | src/theory/arith/nl/nonlinear_extension.cpp | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index df3a304be..05442a566 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -47,6 +47,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, d_trSlv(d_im, d_model), d_nlSlv(containing, d_model), d_cadSlv(d_im, d_model), + d_icpSlv(d_im), d_iandSlv(containing, d_model), d_builtModel(containing.getSatContext(), false) { @@ -381,6 +382,21 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, } } + if (options::nlICP()) + { + d_icpSlv.reset(assertions); + d_icpSlv.check(); + + if (d_im.hasUsed()) + { + Trace("nl-ext") << " ...finished with " + << d_im.numPendingLemmas() + d_im.numSentLemmas() + << " new lemmas from ICP." << std::endl; + return d_im.numPendingLemmas() + d_im.numSentLemmas(); + } + Trace("nl-ext") << "Done with ICP" << std::endl; + } + if (options::nlExt()) { // initialize the non-linear solver @@ -758,7 +774,7 @@ bool NonlinearExtension::modelBasedRefinement(std::vector<NlLemma>& mlems) d_builtModel = true; } filterLemmas(lemmas, mlems); - if (!mlems.empty()) + if (!mlems.empty() || d_im.hasPendingLemma()) { return true; } |