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.