diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-08-03 11:50:51 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-03 16:50:51 +0000 |
| commit | 2c2981d419bdf5a7bbf424f62266883724e85168 (patch) | |
| tree | f813f04236439c5c7bc245c3a71784fb9f211bdd /src/theory/output_channel.h | |
| parent | 6b55bf59675fcdaab4c8dbf70a8a74ebb1f990e9 (diff) | |
Refactor shared solver to use theory builtin inference manager (#6960)
This ensures that e.g. COMBINATION_SPLIT shows up under theory::builtin::inferencesLemmas, and -t im. It also removes outdated interfaces from OutputChannel, and makes the feature TheoryEngine::ensureLemmaAtoms more modular, which was required for making these interfaces more consistent.
It also ensures that TheoryBuiltin has an inference manager, which will simplify special casing in #6956.
Diffstat (limited to 'src/theory/output_channel.h')
| -rw-r--r-- | src/theory/output_channel.h | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index b681dad17..80115d438 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -122,16 +122,6 @@ class OutputChannel { virtual void lemma(TNode n, LemmaProperty p = LemmaProperty::NONE) = 0; /** - * Request a split on a new theory atom. This is equivalent to - * calling lemma({OR n (NOT n)}). - * - * @param n - a theory atom; must be of Boolean type - */ - void split(TNode n); - - virtual void splitLemma(TNode n, bool removable = false) = 0; - - /** * If a decision is made on n, it must be in the phase specified. * Note that this is enforced *globally*, i.e., it is completely * context-INdependent. If you ever requirePhase() on a literal, |