From e969318f12d4e8ee01b12933e9e60fafafd96963 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 22 Sep 2020 17:49:46 +0200 Subject: ICP-based solver for nonlinear arithmetic (#5017) This PR adds a new icp-based solver to be integrated into the nonlinear extension. It is not meant to be used as a stand-alone ICP solver. It does not implement splits (only propagations) and implements a rather aggressive budget mechanism that aims to quickly stop propagation to allow other solvers to take over. Additionally, it enforces a maximum bit size to avoid divergence. --- src/theory/arith/nl/nonlinear_extension.cpp | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) (limited to 'src/theory/arith/nl/nonlinear_extension.cpp') 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& 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& mlems) d_builtModel = true; } filterLemmas(lemmas, mlems); - if (!mlems.empty()) + if (!mlems.empty() || d_im.hasPendingLemma()) { return true; } -- cgit v1.2.3