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.h | |
| 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.h')
| -rw-r--r-- | src/theory/theory.h | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index 1fdf96331..29a3a0998 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -43,6 +43,7 @@ #include "theory/logic_info.h" #include "theory/output_channel.h" #include "theory/theory_id.h" +#include "theory/theory_inference_manager.h" #include "theory/theory_rewriter.h" #include "theory/theory_state.h" #include "theory/trust_node.h" @@ -257,6 +258,12 @@ class Theory { */ TheoryState* d_theoryState; /** + * The theory inference manager. This is a wrapper around the equality + * engine and the output channel. It ensures that the output channel and + * the equality engine are used properly. + */ + TheoryInferenceManager* d_inferManager; + /** * Whether proofs are enabled * */ |