diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-16 09:17:24 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-16 09:17:24 -0500 |
| commit | 56f0e3c3455cc522bd18f41664591cae2c564be3 (patch) | |
| tree | 3849edbfa22185c6ff0dec0c1a3da6e57c6520df /src/CMakeLists.txt | |
| parent | 1a1aea5503132a0f55865cc21364bfee1d6a47c3 (diff) | |
Add inference enumeration to datatypes (#5275)
This adds an inference enumeration for datatypes, which is analogous to what is done in strings and non-linear arithmetic. Inferences are informal identifiers that serve the purpose of (1) debugging the code, (2) providing hints on how proofs can be reconstructed.
This PR also splits the InferenceManager file in datatypes into 2.
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 3896d3111..ec8aaf8dc 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -513,6 +513,8 @@ libcvc4_add_sources( theory/combination_engine.h theory/datatypes/datatypes_rewriter.cpp theory/datatypes/datatypes_rewriter.h + theory/datatypes/inference.cpp + theory/datatypes/inference.h theory/datatypes/inference_manager.cpp theory/datatypes/inference_manager.h theory/datatypes/sygus_datatype_utils.cpp |