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/CMakeLists.txt | |
| 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/CMakeLists.txt')
| -rw-r--r-- | src/CMakeLists.txt | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c55c29ed4..df981db2d 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -823,6 +823,8 @@ libcvc4_add_sources( theory/theory_engine_proof_generator.h theory/theory_id.cpp theory/theory_id.h + theory/theory_inference_manager.cpp + theory/theory_inference_manager.h theory/theory_model.cpp theory/theory_model.h theory/theory_model_builder.cpp |