diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-06-15 19:33:04 -0700 |
|---|---|---|
| committer | Mathias Preiner <mathias.preiner@gmail.com> | 2018-09-22 16:30:59 -0700 |
| commit | 07368b6c38112763ea727324403fe29269405d55 (patch) | |
| tree | ccb7fe0db51b5c3e39ac702296de7aad38881c3d /proofs/signatures | |
| parent | 61572fe01f0fcfe3c9c96811ec3572ad7e572189 (diff) | |
cmake: .cpp generation done, .h generation not yet complete
Diffstat (limited to 'proofs/signatures')
| -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 |