blob: 5073569bc843f9f9b9bfc2fe652a94ce1ad35306 (
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
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
|
lfsc: a high-performance LFSC proof checker.
Andy Reynolds and Aaron Stump
----------------------------------------------------------------------
Command line parameters for LFSC:
lfsc [sig_1 .... sig_n] [opts_1...opts_n]
[sig_1 .... sig_n] are signature files, and options [opts_1...opts_n]
are any of the following:
--compile-scc : Write out all side conditions contained in signatures
specified on the command line to files scccode.h, scccode.cpp (see
below for example)
--run-scc : Run proof checking with compiled side condition code (see
below).
--compile-scc-debug : Write side condition code to scccode.h,
scccode.cpp that contains print statements (for debugging running of
side condition code).
Typical usage:
./src/opt/lfsc [sig_1 .... sig_n] [proof] [opts_1...opts_n]
A proof is typically specified at the end of the list of input files
in file [proof]. This will tell LFSC to type check the proof term in
the file [proof]. The extension (*.plf) is commonly used for both
user signature files and proof files.
Side condition code compilation:
LFSC may be used with side condition code compilation. This will take
all side conditions ("program" constructs) in the user signature and
produce equivalent C++ code in the output files scccode.h,
scccode.cpp.
An example for QF_IDL running with side condition code compilation:
(1) In the src/ directory, run LFSC with the command line parameters:
./opt/lfsc ../sat-tests/sat.plf ../sat-tests/smt.plf \
../sat-tests/cnf_conv.plf ../sat-tests/th_base.plf \
../sat-tests/th_idl.plf --compile-scc
This will produce scccode.h and scccode.cpp in the working directory
where lfsc was run (here, src/).
(2) Recompile the code base for lfsc. This will produce a copy of the
LFSC executable that is capable of calling side conditions directly as
compiled C++.
(3) To check a proof.plf* with side condition code compilation, run
LFSC with the command line parameters:
./opt/lfsc ../sat-tests/sat.plf ../sat-tests/smt.plf \
../sat-tests/cnf_conv.plf ../sat-tests/th_base.plf \
../sat-tests/th_idl.plf --run-scc proof.plf
*Note that this proof must be compatible with the proof checking
signature. The proof generator is responsible for producing a proof
in the proper format that can be checked by the proof signature
specified when running LFSC.
For example, in the case of CLSAT in the QF_IDL logic, older proofs
(proofs produced before Feb 2009) may be incompatible with the newest
version of the resolution checking signature (sat.plf). The newest
version of CLSAT -- which can be checked out from the Iowa repository
with
svn co https://svn.divms.uiowa.edu/repos/clc/clsat/trunk clsat
should produce proofs compatible with the current version of sat.plf.
|