diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-09-03 16:27:56 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-03 16:27:56 +0200 |
| commit | 58733b382a4a956c051d06e7318afa1deed612da (patch) | |
| tree | e41944879de5e7f1a06b1994731c9957d65acd3d /src/theory/arith/nl/nonlinear_extension.h | |
| parent | 337f8b791943e9b6b9a234f4f5422cf173342dd9 (diff) | |
Basic integration of arith::InferenceManager (#4999)
This PR adds a first basic integration of the arith::InferenceManager into the arithmetic theory and the nonlinear extension in particular.
While the lemma collection mechanism (in the nonlinear extension) remains unchanged, the lemmas are ultimately not directly pushed to the output channel but instead added to the inference manager. Additionally, we no longer use the cache within the nonlinear extension but instead rely on the inference manager.
This PR is based on #4960.
Diffstat (limited to 'src/theory/arith/nl/nonlinear_extension.h')
| -rw-r--r-- | src/theory/arith/nl/nonlinear_extension.h | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index 41f24e769..b62b81e9c 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -26,6 +26,7 @@ #include "context/cdlist.h" #include "expr/kind.h" #include "expr/node.h" +#include "theory/arith/inference_manager.h" #include "theory/arith/nl/cad_solver.h" #include "theory/arith/nl/ext_theory_callback.h" #include "theory/arith/nl/iand_solver.h" @@ -237,10 +238,6 @@ class NonlinearExtension */ void sendLemmas(const std::vector<NlLemma>& out); - /** cache of all lemmas sent on the output channel (user-context-dependent) */ - NodeSet d_lemmas; - /** Same as above, for preprocessed lemmas */ - NodeSet d_lemmasPp; /** commonly used terms */ Node d_zero; Node d_one; @@ -248,6 +245,7 @@ class NonlinearExtension Node d_true; // The theory of arithmetic containing this extension. TheoryArith& d_containing; + InferenceManager& d_im; // pointer to used equality engine eq::EqualityEngine* d_ee; /** The statistics class */ |