[lfsc] Initial import.
Jerry James
jjames at fedoraproject.org
Thu Apr 18 20:16:00 UTC 2013
commit e30a642dea1eddde0292ab7e1e5fb119a5639010
Author: Jerry James <loganjerry at gmail.com>
Date: Thu Apr 18 14:15:51 2013 -0600
Initial import.
.gitignore | 1 +
check.plf | 14 ++++++
lfsc-exit.patch | 10 +++++
lfsc.1 | 77 ++++++++++++++++++++++++++++++++++
lfsc.spec | 87 +++++++++++++++++++++++++++++++++++++++
license.txt | 15 +++++++
readme-lfsc.txt | 83 +++++++++++++++++++++++++++++++++++++
sat.plf | 122 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
sources | 1 +
9 files changed, 410 insertions(+), 0 deletions(-)
---
diff --git a/.gitignore b/.gitignore
index e69de29..b7fb87b 100644
--- a/.gitignore
+++ b/.gitignore
@@ -0,0 +1 @@
+/lfsc_src.zip
diff --git a/check.plf b/check.plf
new file mode 100644
index 0000000..cbbc5a3
--- /dev/null
+++ b/check.plf
@@ -0,0 +1,14 @@
+(check
+(% v1 var
+(% v2 var
+(% x0 (holds (clc (pos v1) (clc (pos v2) cln)))
+(% x1 (holds (clc (neg v1) (clc (pos v2) cln)))
+(% x2 (holds (clc (pos v1) (clc (neg v2) cln)))
+(% x3 (holds (clc (neg v1) (clc (neg v2) cln)))
+(: (holds cln)
+(satlem _ _ _ (R _ _ x0 x2 v2)
+(\ m0
+(satlem _ _ _ (R _ _ m0 (R _ _ x1 x3 v2) v1)
+(\ @done @done
+)))) ; closing the satlem applications
+))))))))
diff --git a/lfsc-exit.patch b/lfsc-exit.patch
new file mode 100644
index 0000000..ea5b01a
--- /dev/null
+++ b/lfsc-exit.patch
@@ -0,0 +1,10 @@
+--- check.cpp.orig 2010-10-26 16:20:58.000000000 -0600
++++ check.cpp 2012-12-04 09:09:16.366199168 -0700
+@@ -11,6 +11,7 @@
+ #include <stack>
+ #include <string.h>
+ #include <time.h>
++#include <unistd.h>
+ #include "scccode.h"
+ #include "print_smt2.h"
+
diff --git a/lfsc.1 b/lfsc.1
new file mode 100644
index 0000000..f8914e6
--- /dev/null
+++ b/lfsc.1
@@ -0,0 +1,77 @@
+.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.
diff --git a/lfsc.spec b/lfsc.spec
new file mode 100644
index 0000000..9ecc22e
--- /dev/null
+++ b/lfsc.spec
@@ -0,0 +1,87 @@
+# NOTE: upstream does not have a version numbering scheme (there has only been
+# one release so far), so I have chosen to use the date of release as the
+# version number.
+
+Name: lfsc
+Version: 0.20120321
+Release: 2%{?dist}
+Summary: SMT proof checker
+
+License: BSD
+URL: http://clc.cs.uiowa.edu/lfsc/
+Source0: http://clc.cs.uiowa.edu/%{name}/%{name}_src.zip
+Source1: http://clc.cs.uiowa.edu/%{name}/license.txt
+# Man page written by Jerry James from text available on the lfsc web site;
+# i.e., I wrote the formatting only, not the text, so this file is covered
+# under the same copyright and license as the source code.
+Source2: %{name}.1
+# Source text for the man page. Use this to validate the man page on update.
+Source3: http://clc.cs.uiowa.edu/lfsc/readme-lfsc.txt
+# Two proof files used to check the validity of a build.
+Source4: http://clc.cs.uiowa.edu/lfsc/sat.plf
+Source5: check.plf
+# Sent upstream 4 Dec 2012. Fix a build failure due to a missing prototype
+# for _exit().
+Patch0: %{name}-exit.patch
+
+BuildRequires: gmp-devel
+
+%description
+This package contains an SMT proof checker.
+
+%package devel
+Summary: Files needed to compile side conditions
+Requires: %{name}%{?_isa} = %{version}-%{release}
+Requires: gmp-devel%{?_isa}
+
+%description devel
+This package contains the files needed to compile a version of %{name} that
+can execute a side condition.
+
+%prep
+%setup -q -c
+%patch0
+cp -p %{SOURCE1} .
+
+# Use the correct compiler flags
+sed -ri 's/-(O4|w)//' Makefile
+
+%build
+make %{?_smp_mflags} CP_OPTS="%{optflags} -D_FILE_OFFSET_BITS=64"
+
+%install
+# Install the main binary
+mkdir -p %{buildroot}%{_bindir}
+install -m 0755 -p opt/%{name} %{buildroot}%{_bindir}
+
+# Install the man page
+mkdir -p %{buildroot}%{_mandir}/man1
+cp -p %{SOURCE2} %{buildroot}%{_mandir}/man1
+
+# Install the development source files
+mkdir -p %{buildroot}%{_libdir}/%{name}/opt
+install -m 0644 -p check.h chunking_memory_management.h code.cpp code.h \
+ expr.h trie.h Makefile %{buildroot}%{_libdir}/%{name}
+
+# Install the development binary files
+install -m 0644 -p opt/Makefile.d opt/*.o %{buildroot}%{_libdir}/%{name}/opt
+cp -a opt/deps %{buildroot}%{_libdir}/%{name}/opt
+
+%check
+opt/%{name} %{SOURCE4} %{SOURCE5}
+
+%files
+%doc license.txt
+%{_bindir}/%{name}
+%{_mandir}/man1/%{name}.1*
+
+%files devel
+%{_libdir}/%{name}/
+
+%changelog
+* Tue Apr 16 2013 Jerry James <loganjerry at gmail.com> - 0.20120321-2
+- Add source3 as a reminder to update source2
+- Add a check script, and source4 and source5 to feed it
+
+* Wed Jan 23 2013 Jerry James <loganjerry at gmail.com> - 0.20120321-1
+- Initial RPM
diff --git a/license.txt b/license.txt
new file mode 100644
index 0000000..395694e
--- /dev/null
+++ b/license.txt
@@ -0,0 +1,15 @@
+LFSC is copyright (C) 2012, 2013 The University of Iowa. All rights reserved.
+
+LFSC is open-source; distribution is under the terms of the modified BSD license.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS
+AS IS AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
\ No newline at end of file
diff --git a/readme-lfsc.txt b/readme-lfsc.txt
new file mode 100644
index 0000000..5073569
--- /dev/null
+++ b/readme-lfsc.txt
@@ -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.
diff --git a/sat.plf b/sat.plf
new file mode 100644
index 0000000..f463424
--- /dev/null
+++ b/sat.plf
@@ -0,0 +1,122 @@
+(declare bool type)
+(declare tt bool)
+(declare ff bool)
+
+(declare var type)
+
+(declare lit type)
+(declare pos (! x var lit))
+(declare neg (! x var lit))
+
+(declare clause type)
+(declare cln clause)
+(declare clc (! x lit (! c clause clause)))
+
+; constructs for general clauses for R, Q, satlem
+
+(declare concat (! c1 clause (! c2 clause clause)))
+(declare clr (! l lit (! c clause clause)))
+
+; code to check resolutions
+
+(program append ((c1 clause) (c2 clause)) clause
+ (match c1 (cln c2) ((clc l c1') (clc l (append c1' c2)))))
+
+; we use marks as follows:
+; -- mark 1 to record if we are supposed to remove a positive occurrence of the variable.
+; -- mark 2 to record if we are supposed to remove a negative occurrence of the variable.
+; -- mark 3 if we did indeed remove the variable positively
+; -- mark 4 if we did indeed remove the variable negatively
+(program simplify_clause ((c clause)) clause
+ (match c
+ (cln cln)
+ ((clc l c1)
+ (match l
+ ; Set mark 1 on v if it is not set, to indicate we should remove it.
+ ; After processing the rest of the clause, set mark 3 if we were already
+ ; supposed to remove v (so if mark 1 was set when we began). Clear mark3
+ ; if we were not supposed to be removing v when we began this call.
+ ((pos v)
+ (let m (ifmarked v tt (do (markvar v) ff))
+ (let c' (simplify_clause c1)
+ (match m
+ (tt (do (ifmarked3 v v (markvar3 v)) c'))
+ (ff (do (ifmarked3 v (markvar3 v) v) (markvar v) (clc l c')))))))
+ ; the same as the code for tt, but using different marks.
+ ((neg v)
+ (let m (ifmarked2 v tt (do (markvar2 v) ff))
+ (let c' (simplify_clause c1)
+ (match m
+ (tt (do (ifmarked4 v v (markvar4 v)) c'))
+ (ff (do (ifmarked4 v (markvar4 v) v) (markvar2 v) (clc l c')))))))))
+ ((concat c1 c2) (append (simplify_clause c1) (simplify_clause c2)))
+ ((clr l c1)
+ (match l
+ ; set mark 1 to indicate we should remove v, and fail if
+ ; mark 3 is not set after processing the rest of the clause
+ ; (we will set mark 3 if we remove a positive occurrence of v).
+ ((pos v)
+ (let m (ifmarked v tt (do (markvar v) ff))
+ (let m3 (ifmarked3 v (do (markvar3 v) tt) ff)
+ (let c' (simplify_clause c1)
+ (ifmarked3 v (do (match m3 (tt v) (ff (markvar3 v)))
+ (match m (tt v) (ff (markvar v))) c')
+ (fail clause))))))
+ ; same as the tt case, but with different marks.
+ ((neg v)
+ (let m2 (ifmarked2 v tt (do (markvar2 v) ff))
+ (let m4 (ifmarked4 v (do (markvar4 v) tt) ff)
+ (let c' (simplify_clause c1)
+ (ifmarked4 v (do (match m4 (tt v) (ff (markvar4 v)))
+ (match m2 (tt v) (ff (markvar2 v))) c')
+ (fail clause))))))
+ ))))
+
+
+; resolution proofs
+
+(declare holds (! c clause type))
+
+(define bottom (holds cln))
+
+(declare R (! c1 clause (! c2 clause
+ (! u1 (holds c1)
+ (! u2 (holds c2)
+ (! n var
+ (holds (concat (clr (pos n) c1)
+ (clr (neg n) c2)))))))))
+
+(declare Q (! c1 clause (! c2 clause
+ (! u1 (holds c1)
+ (! u2 (holds c2)
+ (! n var
+ (holds (concat (clr (neg n) c1)
+ (clr (pos n) c2)))))))))
+
+(declare satlem (! c1 clause
+ (! c2 clause
+ (! c3 clause
+ (! u1 (holds c1)
+ (! r (^ (simplify_clause c1) c2)
+ (! u2 (! x (holds c2) (holds c3))
+ (holds c3))))))))
+
+
+; A little example to demonstrate simplify_clause.
+; It can handle nested clr's of both polarities,
+; and correctly cleans up marks when it leaves a
+; clr or clc scope. Uncomment and run with
+; --show-runs to see it in action.
+;
+; (check
+; (% v1 var
+; (% u1 (holds (concat (clr (neg v1) (clr (pos v1) (clc (pos v1) (clr (pos v1) (clc (pos v1) (clc (neg v1) cln))))))
+; (clc (pos v1) (clc (pos v1) cln))))
+; (satlem _ _ _ u1 (\ x x))))))
+
+
+;(check
+; (% v1 var
+; (% u1 (holds (clr (neg v1) (concat (clc (neg v1) cln)
+; (clr (neg v1) (clc (neg v1) cln)))))
+; (satlem _ _ _ u1 (\ x x))))))
\ No newline at end of file
diff --git a/sources b/sources
index e69de29..6b49bac 100644
--- a/sources
+++ b/sources
@@ -0,0 +1 @@
+336278197465dd934ac5963b3bc581f2 lfsc_src.zip
More information about the scm-commits
mailing list