summaryrefslogtreecommitdiff
path: root/src/CMakeLists.txt
diff options
context:
space:
mode:
authorLachnitt <lachnitt@stanford.edu>2021-09-23 14:46:05 -0700
committerGitHub <noreply@github.com>2021-09-23 21:46:05 +0000
commit6c67ed5a2521012d523eb3f11ff344bf7062ee6e (patch)
treec698fe3125b452921deea9fe29d928ae2af00c82 /src/CMakeLists.txt
parent6d9f47e6e97b44991c8331ae8b5db087d9c9e5fe (diff)
[proofs] Alethe: Add Alethe Files to be Compiled (#7241)
Adds Alethe proof rule and option. Adds alethe_post_processor and alethe_proof_rule files to list of files to be compiled. During incorporating these changes errors occurred in the SCOPE rule that are also fixed in this PR.
Diffstat (limited to 'src/CMakeLists.txt')
-rw-r--r--src/CMakeLists.txt4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 3113f03ab..8f574dc82 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -221,6 +221,10 @@ libcvc5_add_sources(
proof/unsat_core.h
proof/alethe/alethe_node_converter.cpp
proof/alethe/alethe_node_converter.h
+ proof/alethe/alethe_post_processor.cpp
+ proof/alethe/alethe_post_processor.h
+ proof/alethe/alethe_proof_rule.cpp
+ proof/alethe/alethe_proof_rule.h
prop/bv_sat_solver_notify.h
prop/bvminisat/bvminisat.cpp
prop/bvminisat/bvminisat.h
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback