diff options
author | Gereon Kremer <nafur42@gmail.com> | 2021-05-17 17:18:57 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-17 15:18:57 +0000 |
commit | 63281fbfe093b1d5e375a378bb59761f77256d08 (patch) | |
tree | ea4e7dc183ddfb23709c92f74b4d35f581ad8d32 /src/theory | |
parent | f1a65bef2675495f09603901a7166f20221b0449 (diff) |
Improve integration of CAD with nl-Ext (#6542)
This PR improves the integration of the CAD solver with the nl-ext solver in a simple way: we simply use a few of the simple linearization lemmas in combination with CAD by default, significantly improving the performance on QF_NRA.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/nl/nonlinear_extension.cpp | 6 | ||||
-rw-r--r-- | src/theory/arith/nl/strategy.cpp | 17 |
2 files changed, 16 insertions, 7 deletions
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 8221e18d5..7f97c4122 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -218,7 +218,7 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions) // relevance here, since we may have discarded literals that are relevant // that are entailed based on the techniques in getAssertions. std::vector<Node> passertions = assertions; - if (options::nlExt()) + if (options::nlExt() == options::NlExtMode::FULL) { // preprocess the assertions with the trancendental solver if (!d_trSlv.preprocessAssertionsCheckModel(passertions)) @@ -474,8 +474,8 @@ Result::Sat NonlinearExtension::modelBasedRefinement(const std::set<Node>& termS } // we are incomplete - if (options::nlExt() && options::nlExtIncPrecision() - && d_model.usedApproximate()) + if (options::nlExt() == options::NlExtMode::FULL + && options::nlExtIncPrecision() && d_model.usedApproximate()) { d_trSlv.incrementTaylorDegree(); needsRecheck = true; diff --git a/src/theory/arith/nl/strategy.cpp b/src/theory/arith/nl/strategy.cpp index 01e319d37..ffe925830 100644 --- a/src/theory/arith/nl/strategy.cpp +++ b/src/theory/arith/nl/strategy.cpp @@ -109,9 +109,14 @@ void Strategy::initializeStrategy() { one << InferStep::ICP << InferStep::BREAK; } - if (options::nlExt()) + if (options::nlExt() == options::NlExtMode::FULL + || options::nlExt() == options::NlExtMode::LIGHT) { - one << InferStep::NL_INIT << InferStep::TRANS_INIT << InferStep::BREAK; + one << InferStep::NL_INIT << InferStep::BREAK; + } + if (options::nlExt() == options::NlExtMode::FULL) + { + one << InferStep::TRANS_INIT << InferStep::BREAK; if (options::nlExtSplitZero()) { one << InferStep::NL_SPLIT_ZERO << InferStep::BREAK; @@ -120,11 +125,15 @@ void Strategy::initializeStrategy() } one << InferStep::IAND_INIT; one << InferStep::IAND_INITIAL << InferStep::BREAK; - if (options::nlExt()) + if (options::nlExt() == options::NlExtMode::FULL + || options::nlExt() == options::NlExtMode::LIGHT) { one << InferStep::NL_MONOMIAL_SIGN << InferStep::BREAK; - one << InferStep::TRANS_MONOTONIC << InferStep::BREAK; one << InferStep::NL_MONOMIAL_MAGNITUDE0 << InferStep::BREAK; + } + if (options::nlExt() == options::NlExtMode::FULL) + { + one << InferStep::TRANS_MONOTONIC << InferStep::BREAK; one << InferStep::NL_MONOMIAL_MAGNITUDE1 << InferStep::BREAK; one << InferStep::NL_MONOMIAL_MAGNITUDE2 << InferStep::BREAK; one << InferStep::NL_MONOMIAL_INFER_BOUNDS; |