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/theory.h | |
| 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/theory.h')
| -rw-r--r-- | src/theory/theory.h | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index 1c23d9041..3a90a8ace 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -458,13 +458,6 @@ class Theory { } /** - * Set the output channel associated to this theory. - */ - void setOutputChannel(OutputChannel& out) { - d_out = &out; - } - - /** * Get the output channel associated to this theory. */ OutputChannel& getOutputChannel() { |