From 02e682821028bc704c57a762dadeb6f82bb70ebf Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 2 Sep 2020 15:48:12 +0200 Subject: Add ArithLemma and arith::InferenceManager (#4960) This PR adds a new ArithLemma that is essentiall NlLemma, but derived from the new theory::Lemma and meant to be used all across the arithmetic theory. Also, based on theory::InferenceManagerBuffered this PR adds arith::InferenceManager that shall become the sole interface between the arithmetic theory and the OutputChannel. --- src/theory/arith/nl/nonlinear_extension.h | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'src/theory/arith/nl/nonlinear_extension.h') diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index ee58a9e2e..d035b1056 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -172,6 +172,9 @@ class NonlinearExtension */ void presolve(); + /** Process side effect se */ + void processSideEffect(const NlLemma& se); + private: /** Model-based refinement * @@ -274,8 +277,6 @@ class NonlinearExtension * Send lemmas in out on the output channel of theory of arithmetic. */ void sendLemmas(const std::vector& out); - /** Process side effect se */ - void processSideEffect(const NlLemma& se); /** cache of all lemmas sent on the output channel (user-context-dependent) */ NodeSet d_lemmas; -- cgit v1.2.3