blob: 698fa37fe69bd29a2e50159306c11d9fffcdc4f9 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
# 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
er.plf
smt.plf
th_base.plf
lrat.plf
drat.plf
th_arrays.plf
th_bv.plf
th_bv_bitblast.plf
th_bv_rewrites.plf
th_real.plf
th_int.plf
th_lira.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)
libcvc4_add_sources(GENERATED signatures.cpp)
install(FILES ${core_signature_files} DESTINATION share/cvc4)
|
