1 files changed, 83 insertions, 0 deletions
diff --git a/proofs/lfsc_checker/README b/proofs/lfsc_checker/README
new file mode 100644
index 000000000..5073569bc
--- /dev/null
+++ b/proofs/lfsc_checker/README
@@ -0,0 +1,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.