diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/signatures/CMakeLists.txt | 30 | ||||
| -rw-r--r-- | proofs/signatures/signatures.cpp.in | 10 |
2 files changed, 40 insertions, 0 deletions
diff --git a/proofs/signatures/CMakeLists.txt b/proofs/signatures/CMakeLists.txt index e69de29bb..139a7c80e 100644 --- a/proofs/signatures/CMakeLists.txt +++ b/proofs/signatures/CMakeLists.txt @@ -0,0 +1,30 @@ +# These CORE_PLFs are combined to give a "master signature" against which +# proofs are checked internally when using --check-proofs. To add support for +# more theories, just list them here in the same order you would to the LFSC +# proof-checker binary. + +set(core_signature_files + sat.plf + smt.plf + th_base.plf + th_arrays.plf + th_bv.plf + th_bv_bitblast.plf + th_bv_rewrites.plf + th_real.plf + th_int.plf +) + +set(CORE_SIGNATURES "") + +foreach(f ${core_signature_files}) + file(READ ${f} tmp) + set(CORE_SIGNATURES "${CORE_SIGNATURES}\n${tmp}") +endforeach(f) + +string(REPLACE "\\" "\\\\" CORE_SIGNATURES "${CORE_SIGNATURES}") +string(REPLACE "\"" "\\\"" CORE_SIGNATURES "${CORE_SIGNATURES}") +string(REPLACE "\n" "\\n\\\n" CORE_SIGNATURES "${CORE_SIGNATURES}") +configure_file( + ${CMAKE_CURRENT_SOURCE_DIR}/signatures.cpp.in + ${CMAKE_CURRENT_BINARY_DIR}/signatures.cpp) diff --git a/proofs/signatures/signatures.cpp.in b/proofs/signatures/signatures.cpp.in new file mode 100644 index 000000000..0040eb0c6 --- /dev/null +++ b/proofs/signatures/signatures.cpp.in @@ -0,0 +1,10 @@ +namespace CVC4 { +namespace proof { + +extern const char *const plf_signatures; +const char *const plf_signatures = "\ +@CORE_SIGNATURES@ +"; + +} // namespace proof +} // namespace CVC4 |