diff options
Diffstat (limited to 'src/theory/ext_theory.h')
| -rw-r--r-- | src/theory/ext_theory.h | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/theory/ext_theory.h b/src/theory/ext_theory.h index f5e08e2f5..01b191e0a 100644 --- a/src/theory/ext_theory.h +++ b/src/theory/ext_theory.h @@ -41,6 +41,7 @@ #include "context/cdo.h" #include "context/context.h" #include "expr/node.h" +#include "theory/theory_inference_manager.h" namespace cvc5 { namespace theory { @@ -176,7 +177,7 @@ class ExtTheory ExtTheory(ExtTheoryCallback& p, context::Context* c, context::UserContext* u, - OutputChannel& out); + TheoryInferenceManager& im); virtual ~ExtTheory() {} /** Tells this class to treat terms with Kind k as extended functions */ void addFunctionKind(Kind k) { d_extf_kind[k] = true; } @@ -291,11 +292,11 @@ class ExtTheory bool batch, bool isRed); /** send lemma on the output channel */ - bool sendLemma(Node lem, bool preprocess = false); + bool sendLemma(Node lem, InferenceId id, bool preprocess = false); /** reference to the callback */ ExtTheoryCallback& d_parent; - /** Reference to the output channel we are using */ - OutputChannel& d_out; + /** inference manager used to send lemmas */ + TheoryInferenceManager& d_im; /** the true node */ Node d_true; /** extended function terms, map to whether they are active */ |