diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-08-17 12:52:53 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-17 12:52:53 -0500 |
| commit | 0783307a81f3f27194d7c08e1e8f32123432b9b8 (patch) | |
| tree | 080b4b48b245aa2f055033708b6788a92610ce55 /src/theory/ext_theory.h | |
| parent | 1f9f73a863401da3bc06fc82bb06f0afe947cce9 (diff) | |
| parent | e8f18dd65c829c3c12158d57e1fc7d2c9dcdcfd4 (diff) | |
Merge branch 'master' into rmMaybermMaybe
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 */ |