diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-26 22:50:06 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-26 22:50:06 -0500 |
commit | 34953e8f4d9928cd8a92177f104b87e56479b437 (patch) | |
tree | 2792084fca0eb1b56dd1e2088076b9f15e492255 /src/theory/theory.cpp | |
parent | 00c9ae6e2796c45d821ea9dd45ff7c33a5770922 (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.cpp')
-rw-r--r-- | src/theory/theory.cpp | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 50a5c4493..66541a63e 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -81,6 +81,7 @@ Theory::Theory(TheoryId id, d_equalityEngine(nullptr), d_allocEqualityEngine(nullptr), d_theoryState(nullptr), + d_inferManager(nullptr), d_proofsEnabled(false) { smtStatisticsRegistry()->registerStat(&d_checkTime); @@ -106,6 +107,10 @@ void Theory::setEqualityEngine(eq::EqualityEngine* ee) { d_theoryState->setEqualityEngine(ee); } + if (d_inferManager != nullptr) + { + d_inferManager->setEqualityEngine(ee); + } } void Theory::setQuantifiersEngine(QuantifiersEngine* qe) |