Refactor shared solver to use theory builtin inference manager (#6960)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 3 Aug 2021 16:50:51 +0000 (11:50 -0500)
committerGitHub <noreply@github.com>
Tue, 3 Aug 2021 16:50:51 +0000 (16:50 +0000)
commit2c2981d419bdf5a7bbf424f62266883724e85168
treef813f04236439c5c7bc245c3a71784fb9f211bdd
parent6b55bf59675fcdaab4c8dbf70a8a74ebb1f990e9
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.
13 files changed:
src/theory/builtin/theory_builtin.cpp
src/theory/builtin/theory_builtin.h
src/theory/ee_manager_central.cpp
src/theory/engine_output_channel.cpp
src/theory/engine_output_channel.h
src/theory/output_channel.cpp
src/theory/output_channel.h
src/theory/shared_solver.cpp
src/theory/shared_solver.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
test/unit/test_smt.h
test/unit/theory/theory_white.cpp