Add the theory inference manager (#4948)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 27 Aug 2020 03:50:06 +0000 (22:50 -0500)
committerGitHub <noreply@github.com>
Thu, 27 Aug 2020 03:50:06 +0000 (22:50 -0500)
commit34953e8f4d9928cd8a92177f104b87e56479b437
tree2792084fca0eb1b56dd1e2088076b9f15e492255
parent00c9ae6e2796c45d821ea9dd45ff7c33a5770922
Add the theory inference manager (#4948)

This class is a wrapper around OutputChannel and EqualityEngine. It is preferred that the Theory use this interface when asserting "internal facts" to the equality engine, and for sending lemmas, conflicts and propagations on the output channel.

This class will be useful when trying new methods for theory combination, where all theories behavior can be modified in a standard way based on modifications to the base inference manager class.
src/CMakeLists.txt
src/theory/theory.cpp
src/theory/theory.h
src/theory/theory_inference_manager.cpp [new file with mode: 0644]
src/theory/theory_inference_manager.h [new file with mode: 0644]