diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-27 21:24:16 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-27 21:24:16 -0500 |
| commit | a0a969d7d65a778f2230ee920339541fdf380234 (patch) | |
| tree | 2e8a3436a36a487f97b3bc75e473a68259fb145b /src/CMakeLists.txt | |
| parent | 31f2135ad14b12e2ee9a24f5ca0da06cf5ed7b92 (diff) | |
Add the buffered inference manager (#4954)
This class implements a highly common pattern of buffering facts and lemmas to send on the output channel. It is planned that the inference managers of strings, sets, datatypes, (non-linear) arithmetic, sep, quantifiers will inherit from this class.
This PR adds basic calls to add lemmas on the output channel from InferenceManager.
It introduces a Lemma virtual class which arith::nl::NlLemma and strings::InferInfo will inherit from.
This is required to begin refactoring a flexible configurable strategy for non-linear arithmetic, and will make it easier to further develop towards a configurable approach for theory combination.
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 e86f3e491..06bc9917f 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -510,6 +510,8 @@ libcvc4_add_sources( theory/fp/theory_fp_type_rules.h theory/fp/type_enumerator.h theory/interrupted.h + theory/inference_manager_buffered.cpp + theory/inference_manager_buffered.h theory/logic_info.cpp theory/logic_info.h theory/model_manager.cpp |