diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-09-04 16:59:49 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-04 09:59:49 -0500 |
| commit | 0d0c1cdbce4fb46ad5c7d4bc620b712ea014722e (patch) | |
| tree | 5fa7c5d06cbf0a67541c5bdbc82bf692f5d1dd48 /src/theory/arith/nl/nonlinear_extension.cpp | |
| parent | bfb744af4f932f095640d97be8f0bfa9ff60e981 (diff) | |
Use arith::InferenceManager for CAD lemmas (#5015)
This makes the CAD solver use the new arith::InferenceManager instead of the previously used lemma collection scheme.
Diffstat (limited to 'src/theory/arith/nl/nonlinear_extension.cpp')
| -rw-r--r-- | src/theory/arith/nl/nonlinear_extension.cpp | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 537dd604c..3bf547ceb 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -46,7 +46,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, d_model(containing.getSatContext()), d_trSlv(d_model), d_nlSlv(containing, d_model), - d_cadSlv(containing, d_model), + d_cadSlv(d_im, d_model), d_iandSlv(containing, d_model), d_builtModel(containing.getSatContext(), false) { @@ -557,12 +557,16 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, } if (options::nlCad()) { - lemmas = d_cadSlv.checkFull(); - if (lemmas.empty()) + d_cadSlv.checkFull(); + if (!d_im.hasUsed()) { Trace("nl-cad") << "nl-cad found SAT!" << std::endl; } - filterLemmas(lemmas, wlems); + else + { + // checkFull() only adds a single conflict + return 1; + } } // run the full refinement in the IAND solver lemmas = d_iandSlv.checkFullRefine(); |