.TH "lfsc" "1" "1" "LFSC" "User Commands"
.SH "NAME"
lfsc \- a high-performance LFSC proof checker
.SH "SYNOPSIS"
.B lfsc
[\fIOPTIONS\fP] [\fIsig.plf\fP ...]
.SH "DESCRIPTION"
.PP
Checks an LFSC proof.  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.
.SH "OPTIONS"
.TP
\fB\-\-compile\-lib\fP
Undocumented.
.TP
\fB\-\-compile\-scc\fP
Write out all side conditions contained in signatures specified on the command
line to files \fIscccode.h\fP and \fIscccode.cpp\fP.
.TP
\fB\-\-compile\-scc\-debug\fP
Write side condition code to \fIscccode.h\fP and \fIscccode.cpp\fP that
contains print statements (for debugging running of side condition code).
.TP
\fB\-\-help\fP
Show usage information.
.TP
\fB\-\-no\-tail\-cails\fP
For debugging.
.TP
\fB\-\-run\-scc\fP
Run proof checking with compiled sie condition code.
.TP
\fB\-\-show\-runs\fP
Print debugging information for runs of side condition code.
.SH "Side condition code compilation"
.PP
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 \fIscccode.h\fP and
\fIscccode.cpp\fP.
.PP
An example for QF_IDL running with side condition code compilation:
.IP 1. 4
In the \fIsrc/\fP directory, run LFSC with the command line parameters:
.IP "" 4
\&./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
.IP "" 4
This will produce \fIscccode.h\fP and \fIscccode.cpp\fP in the working
directory where lfsc was run (here, \fIsrc/\fP).
.IP 2. 4
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++.
.IP 3. 4
To check a proof.plf with side condition code compilation, run LFSC with the
command line parameters:
.IP "" 4
\&./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
.IP "" 4
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.
.PP
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
.PP
svn co https://svn.divms.uiowa.edu/repos/clc/clsat/trunk clsat
.PP
should produce proofs compatible with the current version of sat.plf.