diff options
Diffstat (limited to 'src/CMakeLists.txt')
| -rw-r--r-- | src/CMakeLists.txt | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 96de9afeb..1d57dfeb4 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -151,6 +151,8 @@ libcvc5_add_sources( printer/smt2/smt2_printer.h printer/tptp/tptp_printer.cpp printer/tptp/tptp_printer.h + proof/annotation_proof_generator.cpp + proof/annotation_proof_generator.h proof/assumption_proof_generator.cpp proof/assumption_proof_generator.h proof/buffered_proof_generator.cpp @@ -420,6 +422,8 @@ libcvc5_add_sources( theory/arith/nl/cad/proof_generator.h theory/arith/nl/cad/variable_ordering.cpp theory/arith/nl/cad/variable_ordering.h + theory/arith/nl/equality_substitution.cpp + theory/arith/nl/equality_substitution.h theory/arith/nl/ext/constraint.cpp theory/arith/nl/ext/constraint.h theory/arith/nl/ext/factoring_check.cpp @@ -681,6 +685,8 @@ libcvc5_add_sources( theory/incomplete_id.h theory/inference_id.cpp theory/inference_id.h + theory/inference_id_proof_annotator.cpp + theory/inference_id_proof_annotator.h theory/inference_manager_buffered.cpp theory/inference_manager_buffered.h theory/logic_info.cpp @@ -1013,6 +1019,8 @@ libcvc5_add_sources( theory/sort_inference.h theory/strings/array_solver.cpp theory/strings/array_solver.h + theory/strings/array_core_solver.cpp + theory/strings/array_core_solver.h theory/strings/arith_entail.cpp theory/strings/arith_entail.h theory/strings/base_solver.cpp |