diff options
Diffstat (limited to 'proofs/lfsc_checker/README')
-rw-r--r-- | proofs/lfsc_checker/README | 83 |
1 files changed, 0 insertions, 83 deletions
diff --git a/proofs/lfsc_checker/README b/proofs/lfsc_checker/README deleted file mode 100644 index 5073569bc..000000000 --- a/proofs/lfsc_checker/README +++ /dev/null @@ -1,83 +0,0 @@ -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. |