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.