summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-08-26 22:50:06 -0500
committerGitHub <noreply@github.com>2020-08-26 22:50:06 -0500
commit34953e8f4d9928cd8a92177f104b87e56479b437 (patch)
tree2792084fca0eb1b56dd1e2088076b9f15e492255 /src/theory/theory_engine.h
parent00c9ae6e2796c45d821ea9dd45ff7c33a5770922 (diff)
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.
Diffstat (limited to 'src/theory/theory_engine.h')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback