1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
|
[Note added by Matt K.: To process this directory using ``make'' from
the main ACL2 directory or its books/ subdirectory, you will need to
install minisat. See books/GNUmakefile. Feel free to contribute a
modification of books/GNUmakefile that permits other SAT solvers!]
A Tool for the Subclass of Unrollable List Formulas in ACL2 (SULFA)
by Erik Reeber and Warren A. Hunt, Jr.
For help on using the tool email Erik Reeber at
reeber@cs.utexas.edu
INSTALLATION
03/29/07
0) We assume you have a C compiler installed, as is presumably the case
on nearly all Unix-like systems (including Linux and MacOS). We also
assume that you have Perl installed, which again is very likely for
Unix-like systems, and can be confirmed by checking output from the
shell command "which perl".
1) In order to use our tool, you'll need a SAT solver. Download and
compile, if necessary, either zchaff version 2007.3.12, which can be found at:
http://www.princeton.edu/~chaff/zchaff.html
or
Minisat 1.4 or Minisat 2 (the first release), which can be found at:
http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/MiniSat.html
or in the ACL2 web space under:
http://www.cs.utexas.edu/users/moore/acl2/aux/
2) In the same directory as this README file, type:
"make ACL2_SYSTEM_BOOKS=<acl2-books> ACL2=<acl2-exec> PERL=<perl-int> CC=<c-comp> SAT_SOLVER=<sat-exec> SAT_SOLVER_TYPE=<sat-type>"
where <acl2-books> is the path to ACL2's system books (default "../../../books")
<acl2-exec> is your ACL2 executable (default "<acl2-books>/../saved_exec")
<perl-int> is your Perl interpreter (default "perl"),
<c-comp> is your C compiler (default "gcc"),
<sat-exec> is your SAT solver executable name
(default "../../../aux/minisat2/${HOSTTYPE}/minisat/core/minisat"), and
<sat-type> is either "minisat" or "zchaff" (default "minisat").
Note that the <perl-int>, <c-comp>, and <sat-exec> values should either be full
path names (e.g. "/var/local/minisat/core/minisat"), or names of executables
reachable from your PATH after starting a fresh shell (e.g. if you use c-shell
the PATH is set up in ~/.cshrc).
For example, if your PERL interpreter is in "/usr/bin/perl", you have "gcc" in
your PATH, and have installed minisat 2 in "/var/local/minisat/core/minisat",
then type:
"make PERL=/usr/bin/perl SAT_SOLVER=/var/local/minisat/core/minisat SAT_SOLVER_TYPE=minisat"
Alternatively, you can modify the defaults for the PERL, CC, SAT_SOLVER, and
SAT_SOLVER_TYPE variables in "Makefile".
Note: Minisat writes a bunch of output to stderr, so expect to see a bunch of
output during the compilation if you use minisat.
RUNNING THE TOOL(S)
3/29/07
Two tools are included in this distribution, a clause processor and
a bit-vector SMT solver.
1) To use the SULFA-SAT solver, first include the clause processor
into ACL2 by calling:
(include-book "clause-processors/SULFA/books/clause-processors/sat-clause-processor"
:dir :system :ttags (sat sat-cl))
You can then access the ACL2's "trusted clause-processor" interface. For
example,
(defthm prop-form-1
(or (and a b)
(and (not a) b)
(not b))
:hints (("Goal" :clause-processor (:function sat :hint nil)))
:rule-classes nil)
For more information on this clause processor, look at the tutorial in
"books/sat-tests/tutorial.lisp". You may also want to read ACL2's
documentation on clause processors.
2) A prototype bit-vector SMT solver, SULFA-SMT, is also included with
this distribution. SULFA-SMT can be executed as a perl script created in
"scripts/sulfa-smt" and accepts the standard bit-vector SMT format, described
at:
http://combination.cs.uiowa.edu/smtlib/
A number of bit-vector benchmark problems are also available from this
site, under the name "QF_UFBV32" (Quantifier-Free formulas with Uninterpreted
Functions and 32 bit, Bit Vectors). For convenience we've included a
few of these in the directory "smt-examples/smt-lib-crafted". Given such
a problem, such as "smt-examples/smt-lib-crafted/bb.smt", we can call the SMT solver as follows:
perl scripts/sulfa-smt < smt-examples/smt-lib-crafted/bb.smt
Which will then print either "sat" or "unsat". For a more verbose print
out, use the "-v 4" option:
perl scripts/sulfa-smt -v 4 < smt-examples/smt-lib-crafted/bb.smt
What's interesting about this SMT solver is that the bit-vector functions
are implemented as ACL2 functions (in the file
"books/bv-smt-solver/bv-lib-definitions.lisp"). Furthermore, it makes use of
the ACL2 theorem prover to perform simplification on these functions before
using the SULFA-SAT clause processor to solve them.
The basic methodology is that we use "books/bv-smt-solver/translation.lisp" to
translate the SMT-lib to ACL2, "books/bv-smt-solver/bv-lib-definitions.lisp" to
model the resulting bit-vector functions, and "smt-check" in
"books/bv-smt-solver/smt" to check the resulting formula. The "smt-check"
function first uses the ACL2 simplifier through the symbolic simulator defined
in "../../misc/expander.lisp", and the simplification rules
defined "books/bv-smt-solver/bv-lib-lemmas.lisp". After simplification,
"smt-check" solves the resulting problem by using the SAT-based SULFA solver
through the interface defined in "books/sat/sat".
A NOTE ON PARALLELISM
11/14/07
The SULFA tool currently does not support parallel execution. A
file is used to communicate with the SAT solver and this file always has the same
name. Thus, if two copies of ACL2 are operating in the same directory, they will
conflict with each other if they are both communicating with the SAT solver at the
same time.
GUIDE TO DOCUMENTATION
03/29/07
The directory "books/sat-tests" contains a number of examples that make
use of our SAT-based clause processor for SULFA formulas, including
the tutorial "books/sat-tests/tutorial.lisp".
The file "doc/sat-solver-interface.txt" explains the interface we use to
communicate with SAT solvers, so that you can put a new SAT solver
"under the hood."
The file "doc/tool-interface.txt" briefly explains each of the top-level
functions in "books/sat/sat.lisp" to better facilitate the creation of
new clause processors built on top of our underlying SAT-solving system.
RELEVANT PUBLICATION
03/29/07
Erik Reeber and Warren A. Hunt, Jr., A SAT-Based Decision
Publications Procedure for the Subclass of Unrollable List Functions in ACL2
(SULFA), The 3rd International Joint Conference on Automated
Reasoning (IJCAR 2006), pp 453-467, Springer.
|
