diff options
| author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2020-09-22 16:59:41 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-22 16:59:41 -0500 |
| commit | e4a29a6033ecc7ba5ec266f37e8f151f09ead020 (patch) | |
| tree | 26dff55bd5121dc311185dcd3071a6e8751f9f5e /src/CMakeLists.txt | |
| parent | 524c879720779abc3bc529459da8734f2eb3e3ad (diff) | |
Add skeleton for theory of bags (multisets) (#5100)
This PR adds initial headers and mostly empty source files for the theory of bags (multisets).
It acts as a basis for future commits.
It includes straightforward implementation for typing rules an enumerator for bags.
Diffstat (limited to 'src/CMakeLists.txt')
| -rw-r--r-- | src/CMakeLists.txt | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 2279c7097..1bc393053 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -402,6 +402,21 @@ libcvc4_add_sources( theory/assertion.h theory/atom_requests.cpp theory/atom_requests.h + theory/bags/inference_manager.cpp + theory/bags/inference_manager.h + theory/bags/normal_form.cpp + theory/bags/normal_form.h + theory/bags/solver_state.cpp + theory/bags/solver_state.h + theory/bags/term_registry.cpp + theory/bags/term_registry.h + theory/bags/theory_bags.cpp + theory/bags/theory_bags.h + theory/bags/theory_bags_rewriter.cpp + theory/bags/theory_bags_rewriter.h + theory/bags/theory_bags_type_enumerator.cpp + theory/bags/theory_bags_type_enumerator.h + theory/bags/theory_bags_type_rules.h theory/booleans/circuit_propagator.cpp theory/booleans/circuit_propagator.h theory/booleans/proof_checker.cpp @@ -908,6 +923,7 @@ set(KINDS_FILES ${PROJECT_SOURCE_DIR}/src/theory/datatypes/kinds ${PROJECT_SOURCE_DIR}/src/theory/sep/kinds ${PROJECT_SOURCE_DIR}/src/theory/sets/kinds + ${PROJECT_SOURCE_DIR}/src/theory/bags/kinds ${PROJECT_SOURCE_DIR}/src/theory/strings/kinds ${PROJECT_SOURCE_DIR}/src/theory/quantifiers/kinds) |