diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-03-11 23:48:11 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-11 22:48:11 +0000 |
| commit | a22deeb091673226a1edb5a89bc8a596a3d51fc7 (patch) | |
| tree | f51d6edc2fe374cb0001681c3f882e1a1e7f4a3a /src/theory/arith/nl/nonlinear_extension.cpp | |
| parent | 5998d7f5a9168b0dd1c26f3aa1b85e570fe72af8 (diff) | |
Make linear arithmetic use its inference manager (#5934)
This PR refactors the linear arithmetic solver to properly use its inference manager, instead of directly sending lemmas to the output channel. To do this, it introduces new InferenceIds for the various linear lemmas.
Diffstat (limited to 'src/theory/arith/nl/nonlinear_extension.cpp')
| -rw-r--r-- | src/theory/arith/nl/nonlinear_extension.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 3f32e7075..671c3f44a 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -244,6 +244,7 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions) void NonlinearExtension::check(Theory::Effort e) { + d_im.reset(); Trace("nl-ext") << std::endl; Trace("nl-ext") << "NonlinearExtension::check, effort = " << e << ", built model = " << d_builtModel.get() << std::endl; @@ -277,7 +278,6 @@ void NonlinearExtension::check(Theory::Effort e) d_im.doPendingFacts(); d_im.doPendingLemmas(); d_im.doPendingPhaseRequirements(); - d_im.reset(); return; } // Otherwise, we will answer SAT. The values that we approximated are |