6 Interface to external SAT solvers, and (simple) built-in SAT solvers. |
6 Interface to external SAT solvers, and (simple) built-in SAT solvers. |
7 *) |
7 *) |
8 |
8 |
9 signature SAT_SOLVER = |
9 signature SAT_SOLVER = |
10 sig |
10 sig |
11 exception NOT_CONFIGURED |
11 exception NOT_CONFIGURED |
12 |
12 |
13 type assignment = int -> bool option |
13 type assignment = int -> bool option |
14 type proof = int list Inttab.table * int |
14 type proof = int list Inttab.table * int |
15 datatype result = SATISFIABLE of assignment |
15 datatype result = SATISFIABLE of assignment |
16 | UNSATISFIABLE of proof option |
16 | UNSATISFIABLE of proof option |
17 | UNKNOWN |
17 | UNKNOWN |
18 type solver = PropLogic.prop_formula -> result |
18 type solver = PropLogic.prop_formula -> result |
19 |
19 |
20 (* auxiliary functions to create external SAT solvers *) |
20 (* auxiliary functions to create external SAT solvers *) |
21 val write_dimacs_cnf_file : Path.T -> PropLogic.prop_formula -> unit |
21 val write_dimacs_cnf_file : Path.T -> PropLogic.prop_formula -> unit |
22 val write_dimacs_sat_file : Path.T -> PropLogic.prop_formula -> unit |
22 val write_dimacs_sat_file : Path.T -> PropLogic.prop_formula -> unit |
23 val read_std_result_file : Path.T -> string * string * string -> result |
23 val read_std_result_file : Path.T -> string * string * string -> result |
24 val make_external_solver : string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver |
24 val make_external_solver : string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver |
25 |
25 |
26 val read_dimacs_cnf_file : Path.T -> PropLogic.prop_formula |
26 val read_dimacs_cnf_file : Path.T -> PropLogic.prop_formula |
27 |
27 |
28 (* generic solver interface *) |
28 (* generic solver interface *) |
29 val solvers : (string * solver) list ref |
29 val solvers : (string * solver) list ref |
30 val add_solver : string * solver -> unit |
30 val add_solver : string * solver -> unit |
31 val invoke_solver : string -> solver (* exception Option *) |
31 val invoke_solver : string -> solver (* exception Option *) |
32 end; |
32 end; |
33 |
33 |
34 structure SatSolver : SAT_SOLVER = |
34 structure SatSolver : SAT_SOLVER = |
35 struct |
35 struct |
36 |
36 |
37 open PropLogic; |
37 open PropLogic; |
38 |
38 |
39 (* ------------------------------------------------------------------------- *) |
39 (* ------------------------------------------------------------------------- *) |
40 (* should be raised by an external SAT solver to indicate that the solver is *) |
40 (* should be raised by an external SAT solver to indicate that the solver is *) |
41 (* not configured properly *) |
41 (* not configured properly *) |
42 (* ------------------------------------------------------------------------- *) |
42 (* ------------------------------------------------------------------------- *) |
43 |
43 |
44 exception NOT_CONFIGURED; |
44 exception NOT_CONFIGURED; |
45 |
45 |
46 (* ------------------------------------------------------------------------- *) |
46 (* ------------------------------------------------------------------------- *) |
47 (* type of partial (satisfying) assignments: 'a i = NONE' means that 'a' is *) |
47 (* type of partial (satisfying) assignments: 'a i = NONE' means that 'a' is *) |
48 (* a satisfying assignment regardless of the value of variable 'i' *) |
48 (* a satisfying assignment regardless of the value of variable 'i' *) |
49 (* ------------------------------------------------------------------------- *) |
49 (* ------------------------------------------------------------------------- *) |
50 |
50 |
51 type assignment = int -> bool option; |
51 type assignment = int -> bool option; |
52 |
52 |
53 (* ------------------------------------------------------------------------- *) |
53 (* ------------------------------------------------------------------------- *) |
54 (* a proof of unsatisfiability, to be interpreted as follows: each integer *) |
54 (* a proof of unsatisfiability, to be interpreted as follows: each integer *) |
55 (* is a clause ID, each list 'xs' stored under the key 'x' in the table *) |
55 (* is a clause ID, each list 'xs' stored under the key 'x' in the table *) |
56 (* contains the IDs of clauses that must be resolved (in the given *) |
56 (* contains the IDs of clauses that must be resolved (in the given *) |
63 (* The clauses of the original problem passed to the SAT solver have *) |
63 (* The clauses of the original problem passed to the SAT solver have *) |
64 (* consecutive IDs starting with 0. Clause IDs must be non-negative, *) |
64 (* consecutive IDs starting with 0. Clause IDs must be non-negative, *) |
65 (* but do not need to be consecutive. *) |
65 (* but do not need to be consecutive. *) |
66 (* ------------------------------------------------------------------------- *) |
66 (* ------------------------------------------------------------------------- *) |
67 |
67 |
68 type proof = int list Inttab.table * int; |
68 type proof = int list Inttab.table * int; |
69 |
69 |
70 (* ------------------------------------------------------------------------- *) |
70 (* ------------------------------------------------------------------------- *) |
71 (* return type of SAT solvers: if the result is 'SATISFIABLE', a satisfying *) |
71 (* return type of SAT solvers: if the result is 'SATISFIABLE', a satisfying *) |
72 (* assignment must be returned as well; if the result is *) |
72 (* assignment must be returned as well; if the result is *) |
73 (* 'UNSATISFIABLE', a proof of unsatisfiability may be returned *) |
73 (* 'UNSATISFIABLE', a proof of unsatisfiability may be returned *) |
74 (* ------------------------------------------------------------------------- *) |
74 (* ------------------------------------------------------------------------- *) |
75 |
75 |
76 datatype result = SATISFIABLE of assignment |
76 datatype result = SATISFIABLE of assignment |
77 | UNSATISFIABLE of proof option |
77 | UNSATISFIABLE of proof option |
78 | UNKNOWN; |
78 | UNKNOWN; |
79 |
79 |
80 (* ------------------------------------------------------------------------- *) |
80 (* ------------------------------------------------------------------------- *) |
81 (* type of SAT solvers: given a propositional formula, a satisfying *) |
81 (* type of SAT solvers: given a propositional formula, a satisfying *) |
82 (* assignment may be returned *) |
82 (* assignment may be returned *) |
83 (* ------------------------------------------------------------------------- *) |
83 (* ------------------------------------------------------------------------- *) |
84 |
84 |
85 type solver = prop_formula -> result; |
85 type solver = prop_formula -> result; |
86 |
86 |
87 (* ------------------------------------------------------------------------- *) |
87 (* ------------------------------------------------------------------------- *) |
88 (* write_dimacs_cnf_file: serializes a formula 'fm' of propositional logic *) |
88 (* write_dimacs_cnf_file: serializes a formula 'fm' of propositional logic *) |
89 (* to a file in DIMACS CNF format (see "Satisfiability Suggested *) |
89 (* to a file in DIMACS CNF format (see "Satisfiability Suggested *) |
90 (* Format", May 8 1993, Section 2.1) *) |
90 (* Format", May 8 1993, Section 2.1) *) |
91 (* Note: 'fm' must not contain a variable index less than 1. *) |
91 (* Note: 'fm' must not contain a variable index less than 1. *) |
92 (* Note: 'fm' must be given in CNF. *) |
92 (* Note: 'fm' must be given in CNF. *) |
93 (* ------------------------------------------------------------------------- *) |
93 (* ------------------------------------------------------------------------- *) |
94 |
94 |
95 (* Path.T -> prop_formula -> unit *) |
95 (* Path.T -> prop_formula -> unit *) |
96 |
96 |
97 fun write_dimacs_cnf_file path fm = |
97 fun write_dimacs_cnf_file path fm = |
98 let |
98 let |
99 (* prop_formula -> prop_formula *) |
99 (* prop_formula -> prop_formula *) |
100 fun cnf_True_False_elim True = |
100 fun cnf_True_False_elim True = |
101 Or (BoolVar 1, Not (BoolVar 1)) |
101 Or (BoolVar 1, Not (BoolVar 1)) |
102 | cnf_True_False_elim False = |
102 | cnf_True_False_elim False = |
103 And (BoolVar 1, Not (BoolVar 1)) |
103 And (BoolVar 1, Not (BoolVar 1)) |
104 | cnf_True_False_elim fm = |
104 | cnf_True_False_elim fm = |
105 fm (* since 'fm' is in CNF, either 'fm'='True'/'False', or 'fm' does not contain 'True'/'False' at all *) |
105 fm (* since 'fm' is in CNF, either 'fm'='True'/'False', or 'fm' does not contain 'True'/'False' at all *) |
106 (* prop_formula -> int *) |
106 (* prop_formula -> int *) |
107 fun cnf_number_of_clauses (And (fm1,fm2)) = |
107 fun cnf_number_of_clauses (And (fm1,fm2)) = |
108 (cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2) |
108 (cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2) |
109 | cnf_number_of_clauses _ = |
109 | cnf_number_of_clauses _ = |
110 1 |
110 1 |
111 (* prop_formula -> string list *) |
111 (* prop_formula -> string list *) |
112 fun cnf_string fm = |
112 fun cnf_string fm = |
113 let |
113 let |
114 (* prop_formula -> string list -> string list *) |
114 (* prop_formula -> string list -> string list *) |
115 fun cnf_string_acc True acc = |
115 fun cnf_string_acc True acc = |
116 error "formula is not in CNF" |
116 error "formula is not in CNF" |
117 | cnf_string_acc False acc = |
117 | cnf_string_acc False acc = |
118 error "formula is not in CNF" |
118 error "formula is not in CNF" |
119 | cnf_string_acc (BoolVar i) acc = |
119 | cnf_string_acc (BoolVar i) acc = |
120 (assert (i>=1) "formula contains a variable index less than 1"; |
120 (i>=1 orelse error "formula contains a variable index less than 1"; |
121 string_of_int i :: acc) |
121 string_of_int i :: acc) |
122 | cnf_string_acc (Not (BoolVar i)) acc = |
122 | cnf_string_acc (Not (BoolVar i)) acc = |
123 "-" :: cnf_string_acc (BoolVar i) acc |
123 "-" :: cnf_string_acc (BoolVar i) acc |
124 | cnf_string_acc (Not _) acc = |
124 | cnf_string_acc (Not _) acc = |
125 error "formula is not in CNF" |
125 error "formula is not in CNF" |
126 | cnf_string_acc (Or (fm1,fm2)) acc = |
126 | cnf_string_acc (Or (fm1,fm2)) acc = |
127 cnf_string_acc fm1 (" " :: cnf_string_acc fm2 acc) |
127 cnf_string_acc fm1 (" " :: cnf_string_acc fm2 acc) |
128 | cnf_string_acc (And (fm1,fm2)) acc = |
128 | cnf_string_acc (And (fm1,fm2)) acc = |
129 cnf_string_acc fm1 (" 0\n" :: cnf_string_acc fm2 acc) |
129 cnf_string_acc fm1 (" 0\n" :: cnf_string_acc fm2 acc) |
130 in |
130 in |
131 cnf_string_acc fm [] |
131 cnf_string_acc fm [] |
132 end |
132 end |
133 val fm' = cnf_True_False_elim fm |
133 val fm' = cnf_True_False_elim fm |
134 val number_of_vars = maxidx fm' |
134 val number_of_vars = maxidx fm' |
135 val number_of_clauses = cnf_number_of_clauses fm' |
135 val number_of_clauses = cnf_number_of_clauses fm' |
136 in |
136 in |
137 File.write path |
137 File.write path |
138 ("c This file was generated by SatSolver.write_dimacs_cnf_file\n" ^ |
138 ("c This file was generated by SatSolver.write_dimacs_cnf_file\n" ^ |
139 "p cnf " ^ string_of_int number_of_vars ^ " " ^ string_of_int number_of_clauses ^ "\n"); |
139 "p cnf " ^ string_of_int number_of_vars ^ " " ^ string_of_int number_of_clauses ^ "\n"); |
140 File.append_list path |
140 File.append_list path |
141 (cnf_string fm'); |
141 (cnf_string fm'); |
142 File.append path |
142 File.append path |
143 " 0\n" |
143 " 0\n" |
144 end; |
144 end; |
145 |
145 |
146 (* ------------------------------------------------------------------------- *) |
146 (* ------------------------------------------------------------------------- *) |
147 (* write_dimacs_sat_file: serializes a formula 'fm' of propositional logic *) |
147 (* write_dimacs_sat_file: serializes a formula 'fm' of propositional logic *) |
148 (* to a file in DIMACS SAT format (see "Satisfiability Suggested *) |
148 (* to a file in DIMACS SAT format (see "Satisfiability Suggested *) |
149 (* Format", May 8 1993, Section 2.2) *) |
149 (* Format", May 8 1993, Section 2.2) *) |
150 (* Note: 'fm' must not contain a variable index less than 1. *) |
150 (* Note: 'fm' must not contain a variable index less than 1. *) |
151 (* ------------------------------------------------------------------------- *) |
151 (* ------------------------------------------------------------------------- *) |
152 |
152 |
153 (* Path.T -> prop_formula -> unit *) |
153 (* Path.T -> prop_formula -> unit *) |
154 |
154 |
155 fun write_dimacs_sat_file path fm = |
155 fun write_dimacs_sat_file path fm = |
156 let |
156 let |
157 (* prop_formula -> string list *) |
157 (* prop_formula -> string list *) |
158 fun sat_string fm = |
158 fun sat_string fm = |
159 let |
159 let |
160 (* prop_formula -> string list -> string list *) |
160 (* prop_formula -> string list -> string list *) |
161 fun sat_string_acc True acc = |
161 fun sat_string_acc True acc = |
162 "*()" :: acc |
162 "*()" :: acc |
163 | sat_string_acc False acc = |
163 | sat_string_acc False acc = |
164 "+()" :: acc |
164 "+()" :: acc |
165 | sat_string_acc (BoolVar i) acc = |
165 | sat_string_acc (BoolVar i) acc = |
166 (assert (i>=1) "formula contains a variable index less than 1"; |
166 (i>=1 orelse error "formula contains a variable index less than 1"; |
167 string_of_int i :: acc) |
167 string_of_int i :: acc) |
168 | sat_string_acc (Not (BoolVar i)) acc = |
168 | sat_string_acc (Not (BoolVar i)) acc = |
169 "-" :: sat_string_acc (BoolVar i) acc |
169 "-" :: sat_string_acc (BoolVar i) acc |
170 | sat_string_acc (Not fm) acc = |
170 | sat_string_acc (Not fm) acc = |
171 "-(" :: sat_string_acc fm (")" :: acc) |
171 "-(" :: sat_string_acc fm (")" :: acc) |
172 | sat_string_acc (Or (fm1,fm2)) acc = |
172 | sat_string_acc (Or (fm1,fm2)) acc = |
173 "+(" :: sat_string_acc_or fm1 (" " :: sat_string_acc_or fm2 (")" :: acc)) |
173 "+(" :: sat_string_acc_or fm1 (" " :: sat_string_acc_or fm2 (")" :: acc)) |
174 | sat_string_acc (And (fm1,fm2)) acc = |
174 | sat_string_acc (And (fm1,fm2)) acc = |
175 "*(" :: sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 (")" :: acc)) |
175 "*(" :: sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 (")" :: acc)) |
176 (* optimization to make use of n-ary disjunction/conjunction *) |
176 (* optimization to make use of n-ary disjunction/conjunction *) |
177 (* prop_formula -> string list -> string list *) |
177 (* prop_formula -> string list -> string list *) |
178 and sat_string_acc_or (Or (fm1,fm2)) acc = |
178 and sat_string_acc_or (Or (fm1,fm2)) acc = |
179 sat_string_acc_or fm1 (" " :: sat_string_acc_or fm2 acc) |
179 sat_string_acc_or fm1 (" " :: sat_string_acc_or fm2 acc) |
180 | sat_string_acc_or fm acc = |
180 | sat_string_acc_or fm acc = |
181 sat_string_acc fm acc |
181 sat_string_acc fm acc |
182 (* prop_formula -> string list -> string list *) |
182 (* prop_formula -> string list -> string list *) |
183 and sat_string_acc_and (And (fm1,fm2)) acc = |
183 and sat_string_acc_and (And (fm1,fm2)) acc = |
184 sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 acc) |
184 sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 acc) |
185 | sat_string_acc_and fm acc = |
185 | sat_string_acc_and fm acc = |
186 sat_string_acc fm acc |
186 sat_string_acc fm acc |
187 in |
187 in |
188 sat_string_acc fm [] |
188 sat_string_acc fm [] |
189 end |
189 end |
190 val number_of_vars = Int.max (maxidx fm, 1) |
190 val number_of_vars = Int.max (maxidx fm, 1) |
191 in |
191 in |
192 File.write path |
192 File.write path |
193 ("c This file was generated by SatSolver.write_dimacs_sat_file\n" ^ |
193 ("c This file was generated by SatSolver.write_dimacs_sat_file\n" ^ |
194 "p sat " ^ string_of_int number_of_vars ^ "\n" ^ |
194 "p sat " ^ string_of_int number_of_vars ^ "\n" ^ |
195 "("); |
195 "("); |
196 File.append_list path |
196 File.append_list path |
197 (sat_string fm); |
197 (sat_string fm); |
198 File.append path |
198 File.append path |
199 ")\n" |
199 ")\n" |
200 end; |
200 end; |
201 |
201 |
202 (* ------------------------------------------------------------------------- *) |
202 (* ------------------------------------------------------------------------- *) |
203 (* read_std_result_file: scans a SAT solver's output file for a satisfying *) |
203 (* read_std_result_file: scans a SAT solver's output file for a satisfying *) |
204 (* variable assignment. Returns the assignment, or 'UNSATISFIABLE' if *) |
204 (* variable assignment. Returns the assignment, or 'UNSATISFIABLE' if *) |
205 (* the file contains 'unsatisfiable', or 'UNKNOWN' if the file contains *) |
205 (* the file contains 'unsatisfiable', or 'UNKNOWN' if the file contains *) |
211 (* assignment, then i is interpreted as 'true'. If ~i is contained in *) |
211 (* assignment, then i is interpreted as 'true'. If ~i is contained in *) |
212 (* the assignment, then i is interpreted as 'false'. Otherwise the *) |
212 (* the assignment, then i is interpreted as 'false'. Otherwise the *) |
213 (* value of i is taken to be unspecified. *) |
213 (* value of i is taken to be unspecified. *) |
214 (* ------------------------------------------------------------------------- *) |
214 (* ------------------------------------------------------------------------- *) |
215 |
215 |
216 (* Path.T -> string * string * string -> result *) |
216 (* Path.T -> string * string * string -> result *) |
217 |
217 |
218 fun read_std_result_file path (satisfiable, assignment_prefix, unsatisfiable) = |
218 fun read_std_result_file path (satisfiable, assignment_prefix, unsatisfiable) = |
219 let |
219 let |
220 (* string -> int list *) |
220 (* string -> int list *) |
221 fun int_list_from_string s = |
221 fun int_list_from_string s = |
222 List.mapPartial Int.fromString (space_explode " " s) |
222 List.mapPartial Int.fromString (space_explode " " s) |
223 (* int list -> assignment *) |
223 (* int list -> assignment *) |
224 fun assignment_from_list [] i = |
224 fun assignment_from_list [] i = |
225 NONE (* the SAT solver didn't provide a value for this variable *) |
225 NONE (* the SAT solver didn't provide a value for this variable *) |
226 | assignment_from_list (x::xs) i = |
226 | assignment_from_list (x::xs) i = |
227 if x=i then (SOME true) |
227 if x=i then (SOME true) |
228 else if x=(~i) then (SOME false) |
228 else if x=(~i) then (SOME false) |
229 else assignment_from_list xs i |
229 else assignment_from_list xs i |
230 (* int list -> string list -> assignment *) |
230 (* int list -> string list -> assignment *) |
231 fun parse_assignment xs [] = |
231 fun parse_assignment xs [] = |
232 assignment_from_list xs |
232 assignment_from_list xs |
233 | parse_assignment xs (line::lines) = |
233 | parse_assignment xs (line::lines) = |
234 if String.isPrefix assignment_prefix line then |
234 if String.isPrefix assignment_prefix line then |
235 parse_assignment (xs @ int_list_from_string line) lines |
235 parse_assignment (xs @ int_list_from_string line) lines |
236 else |
236 else |
237 assignment_from_list xs |
237 assignment_from_list xs |
238 (* string -> string -> bool *) |
238 (* string -> string -> bool *) |
239 fun is_substring needle haystack = |
239 fun is_substring needle haystack = |
240 let |
240 let |
241 val length1 = String.size needle |
241 val length1 = String.size needle |
242 val length2 = String.size haystack |
242 val length2 = String.size haystack |
243 in |
243 in |
244 if length2 < length1 then |
244 if length2 < length1 then |
245 false |
245 false |
246 else if needle = String.substring (haystack, 0, length1) then |
246 else if needle = String.substring (haystack, 0, length1) then |
247 true |
247 true |
248 else is_substring needle (String.substring (haystack, 1, length2-1)) |
248 else is_substring needle (String.substring (haystack, 1, length2-1)) |
249 end |
249 end |
250 (* string list -> result *) |
250 (* string list -> result *) |
251 fun parse_lines [] = |
251 fun parse_lines [] = |
252 UNKNOWN |
252 UNKNOWN |
253 | parse_lines (line::lines) = |
253 | parse_lines (line::lines) = |
254 if is_substring unsatisfiable line then |
254 if is_substring unsatisfiable line then |
255 UNSATISFIABLE NONE |
255 UNSATISFIABLE NONE |
256 else if is_substring satisfiable line then |
256 else if is_substring satisfiable line then |
257 SATISFIABLE (parse_assignment [] lines) |
257 SATISFIABLE (parse_assignment [] lines) |
258 else |
258 else |
259 parse_lines lines |
259 parse_lines lines |
260 in |
260 in |
261 (parse_lines o (List.filter (fn l => l <> "")) o split_lines o File.read) path |
261 (parse_lines o (List.filter (fn l => l <> "")) o split_lines o File.read) path |
262 end; |
262 end; |
263 |
263 |
264 (* ------------------------------------------------------------------------- *) |
264 (* ------------------------------------------------------------------------- *) |
265 (* make_external_solver: call 'writefn', execute 'cmd', call 'readfn' *) |
265 (* make_external_solver: call 'writefn', execute 'cmd', call 'readfn' *) |
266 (* ------------------------------------------------------------------------- *) |
266 (* ------------------------------------------------------------------------- *) |
267 |
267 |
268 (* string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver *) |
268 (* string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver *) |
269 |
269 |
270 fun make_external_solver cmd writefn readfn fm = |
270 fun make_external_solver cmd writefn readfn fm = |
271 (writefn fm; system cmd; readfn ()); |
271 (writefn fm; system cmd; readfn ()); |
272 |
272 |
273 (* ------------------------------------------------------------------------- *) |
273 (* ------------------------------------------------------------------------- *) |
274 (* read_dimacs_cnf_file: returns a propositional formula that corresponds to *) |
274 (* read_dimacs_cnf_file: returns a propositional formula that corresponds to *) |
275 (* a SAT problem given in DIMACS CNF format *) |
275 (* a SAT problem given in DIMACS CNF format *) |
276 (* ------------------------------------------------------------------------- *) |
276 (* ------------------------------------------------------------------------- *) |
277 |
277 |
278 (* Path.T -> PropLogic.prop_formula *) |
278 (* Path.T -> PropLogic.prop_formula *) |
279 |
279 |
280 fun read_dimacs_cnf_file path = |
280 fun read_dimacs_cnf_file path = |
281 let |
281 let |
282 (* string list -> string list *) |
282 (* string list -> string list *) |
283 fun filter_preamble [] = |
283 fun filter_preamble [] = |
284 error "problem line not found in DIMACS CNF file" |
284 error "problem line not found in DIMACS CNF file" |
285 | filter_preamble (line::lines) = |
285 | filter_preamble (line::lines) = |
286 if String.isPrefix "c " line orelse line = "c" then |
286 if String.isPrefix "c " line orelse line = "c" then |
287 (* ignore comments *) |
287 (* ignore comments *) |
288 filter_preamble lines |
288 filter_preamble lines |
289 else if String.isPrefix "p " line then |
289 else if String.isPrefix "p " line then |
290 (* ignore the problem line (which must be the last line of the preamble) *) |
290 (* ignore the problem line (which must be the last line of the preamble) *) |
291 (* Ignoring the problem line implies that if the file contains more clauses *) |
291 (* Ignoring the problem line implies that if the file contains more clauses *) |
292 (* or variables than specified in its preamble, we will accept it anyway. *) |
292 (* or variables than specified in its preamble, we will accept it anyway. *) |
293 lines |
293 lines |
294 else |
294 else |
295 error "preamble in DIMACS CNF file contains a line that does not begin with \"c \" or \"p \"" |
295 error "preamble in DIMACS CNF file contains a line that does not begin with \"c \" or \"p \"" |
296 (* string -> int *) |
296 (* string -> int *) |
297 fun int_from_string s = |
297 fun int_from_string s = |
298 case Int.fromString s of |
298 case Int.fromString s of |
299 SOME i => i |
299 SOME i => i |
300 | NONE => error ("token " ^ quote s ^ "in DIMACS CNF file is not a number") |
300 | NONE => error ("token " ^ quote s ^ "in DIMACS CNF file is not a number") |
301 (* int list -> int list list *) |
301 (* int list -> int list list *) |
302 fun clauses xs = |
302 fun clauses xs = |
303 let |
303 let |
304 val (xs1, xs2) = take_prefix (fn i => i <> 0) xs |
304 val (xs1, xs2) = take_prefix (fn i => i <> 0) xs |
305 in |
305 in |
306 case xs2 of |
306 case xs2 of |
307 [] => [xs1] |
307 [] => [xs1] |
308 | (0::[]) => [xs1] |
308 | (0::[]) => [xs1] |
309 | (0::tl) => xs1 :: clauses tl |
309 | (0::tl) => xs1 :: clauses tl |
310 | _ => sys_error "this cannot happen" |
310 | _ => sys_error "this cannot happen" |
311 end |
311 end |
312 (* int -> PropLogic.prop_formula *) |
312 (* int -> PropLogic.prop_formula *) |
313 fun literal_from_int i = |
313 fun literal_from_int i = |
314 (assert (i<>0) "variable index in DIMACS CNF file is 0"; |
314 (i<>0 orelse error "variable index in DIMACS CNF file is 0"; |
315 if i>0 then |
315 if i>0 then |
316 PropLogic.BoolVar i |
316 PropLogic.BoolVar i |
317 else |
317 else |
318 PropLogic.Not (PropLogic.BoolVar (~i))) |
318 PropLogic.Not (PropLogic.BoolVar (~i))) |
319 (* PropLogic.prop_formula list -> PropLogic.prop_formula *) |
319 (* PropLogic.prop_formula list -> PropLogic.prop_formula *) |
320 fun disjunction [] = |
320 fun disjunction [] = |
321 error "empty clause in DIMACS CNF file" |
321 error "empty clause in DIMACS CNF file" |
322 | disjunction (x::xs) = |
322 | disjunction (x::xs) = |
323 (case xs of |
323 (case xs of |
324 [] => x |
324 [] => x |
325 | _ => PropLogic.Or (x, disjunction xs)) |
325 | _ => PropLogic.Or (x, disjunction xs)) |
326 (* PropLogic.prop_formula list -> PropLogic.prop_formula *) |
326 (* PropLogic.prop_formula list -> PropLogic.prop_formula *) |
327 fun conjunction [] = |
327 fun conjunction [] = |
328 error "no clause in DIMACS CNF file" |
328 error "no clause in DIMACS CNF file" |
329 | conjunction (x::xs) = |
329 | conjunction (x::xs) = |
330 (case xs of |
330 (case xs of |
331 [] => x |
331 [] => x |
332 | _ => PropLogic.And (x, conjunction xs)) |
332 | _ => PropLogic.And (x, conjunction xs)) |
333 in |
333 in |
334 (conjunction |
334 (conjunction |
335 o (map disjunction) |
335 o (map disjunction) |
336 o (map (map literal_from_int)) |
336 o (map (map literal_from_int)) |
337 o clauses |
337 o clauses |
338 o (map int_from_string) |
338 o (map int_from_string) |
339 o List.concat |
339 o List.concat |
340 o (map (String.fields (fn c => c mem [#" ", #"\t", #"\n"]))) |
340 o (map (String.fields (fn c => c mem [#" ", #"\t", #"\n"]))) |
341 o filter_preamble |
341 o filter_preamble |
342 o (List.filter (fn l => l <> "")) |
342 o (List.filter (fn l => l <> "")) |
343 o split_lines |
343 o split_lines |
344 o File.read) |
344 o File.read) |
345 path |
345 path |
346 end; |
346 end; |
347 |
347 |
348 (* ------------------------------------------------------------------------- *) |
348 (* ------------------------------------------------------------------------- *) |
349 (* solvers: a (reference to a) table of all registered SAT solvers *) |
349 (* solvers: a (reference to a) table of all registered SAT solvers *) |
350 (* ------------------------------------------------------------------------- *) |
350 (* ------------------------------------------------------------------------- *) |
351 |
351 |
352 val solvers = ref ([] : (string * solver) list); |
352 val solvers = ref ([] : (string * solver) list); |
353 |
353 |
354 (* ------------------------------------------------------------------------- *) |
354 (* ------------------------------------------------------------------------- *) |
355 (* add_solver: updates 'solvers' by adding a new solver *) |
355 (* add_solver: updates 'solvers' by adding a new solver *) |
356 (* ------------------------------------------------------------------------- *) |
356 (* ------------------------------------------------------------------------- *) |
357 |
357 |
358 (* string * solver -> unit *) |
358 (* string * solver -> unit *) |
359 |
359 |
360 fun add_solver (name, new_solver) = |
360 fun add_solver (name, new_solver) = |
361 let |
361 let |
362 val the_solvers = !solvers; |
362 val the_solvers = !solvers; |
363 val _ = if AList.defined (op =) the_solvers name |
363 val _ = if AList.defined (op =) the_solvers name |
387 (* Internal SAT solver, available as 'SatSolver.invoke_solver "enumerate"' *) |
387 (* Internal SAT solver, available as 'SatSolver.invoke_solver "enumerate"' *) |
388 (* -- simply enumerates assignments until a satisfying assignment is found *) |
388 (* -- simply enumerates assignments until a satisfying assignment is found *) |
389 (* ------------------------------------------------------------------------- *) |
389 (* ------------------------------------------------------------------------- *) |
390 |
390 |
391 let |
391 let |
392 fun enum_solver fm = |
392 fun enum_solver fm = |
393 let |
393 let |
394 (* int list *) |
394 (* int list *) |
395 val indices = PropLogic.indices fm |
395 val indices = PropLogic.indices fm |
396 (* int list -> int list -> int list option *) |
396 (* int list -> int list -> int list option *) |
397 (* binary increment: list 'xs' of current bits, list 'ys' of all bits (lower bits first) *) |
397 (* binary increment: list 'xs' of current bits, list 'ys' of all bits (lower bits first) *) |
398 fun next_list _ ([]:int list) = |
398 fun next_list _ ([]:int list) = |
399 NONE |
399 NONE |
400 | next_list [] (y::ys) = |
400 | next_list [] (y::ys) = |
401 SOME [y] |
401 SOME [y] |
402 | next_list (x::xs) (y::ys) = |
402 | next_list (x::xs) (y::ys) = |
403 if x=y then |
403 if x=y then |
404 (* reset the bit, continue *) |
404 (* reset the bit, continue *) |
405 next_list xs ys |
405 next_list xs ys |
406 else |
406 else |
407 (* set the lowest bit that wasn't set before, keep the higher bits *) |
407 (* set the lowest bit that wasn't set before, keep the higher bits *) |
408 SOME (y::x::xs) |
408 SOME (y::x::xs) |
409 (* int list -> int -> bool *) |
409 (* int list -> int -> bool *) |
410 fun assignment_from_list xs i = |
410 fun assignment_from_list xs i = |
411 i mem xs |
411 i mem xs |
412 (* int list -> SatSolver.result *) |
412 (* int list -> SatSolver.result *) |
413 fun solver_loop xs = |
413 fun solver_loop xs = |
414 if PropLogic.eval (assignment_from_list xs) fm then |
414 if PropLogic.eval (assignment_from_list xs) fm then |
415 SatSolver.SATISFIABLE (SOME o (assignment_from_list xs)) |
415 SatSolver.SATISFIABLE (SOME o (assignment_from_list xs)) |
416 else |
416 else |
417 (case next_list xs indices of |
417 (case next_list xs indices of |
418 SOME xs' => solver_loop xs' |
418 SOME xs' => solver_loop xs' |
419 | NONE => SatSolver.UNSATISFIABLE NONE) |
419 | NONE => SatSolver.UNSATISFIABLE NONE) |
420 in |
420 in |
421 (* start with the "first" assignment (all variables are interpreted as 'false') *) |
421 (* start with the "first" assignment (all variables are interpreted as 'false') *) |
422 solver_loop [] |
422 solver_loop [] |
423 end |
423 end |
424 in |
424 in |
425 SatSolver.add_solver ("enumerate", enum_solver) |
425 SatSolver.add_solver ("enumerate", enum_solver) |
426 end; |
426 end; |
427 |
427 |
428 (* ------------------------------------------------------------------------- *) |
428 (* ------------------------------------------------------------------------- *) |
429 (* Internal SAT solver, available as 'SatSolver.invoke_solver "dpll"' -- a *) |
429 (* Internal SAT solver, available as 'SatSolver.invoke_solver "dpll"' -- a *) |
430 (* simple implementation of the DPLL algorithm (cf. L. Zhang, S. Malik: "The *) |
430 (* simple implementation of the DPLL algorithm (cf. L. Zhang, S. Malik: "The *) |
431 (* Quest for Efficient Boolean Satisfiability Solvers", July 2002, Fig. 1). *) |
431 (* Quest for Efficient Boolean Satisfiability Solvers", July 2002, Fig. 1). *) |
432 (* ------------------------------------------------------------------------- *) |
432 (* ------------------------------------------------------------------------- *) |
433 |
433 |
434 let |
434 let |
435 local |
435 local |
436 open PropLogic |
436 open PropLogic |
437 in |
437 in |
438 fun dpll_solver fm = |
438 fun dpll_solver fm = |
439 let |
439 let |
440 (* We could use 'PropLogic.defcnf fm' instead of 'PropLogic.nnf fm' *) |
440 (* We could use 'PropLogic.defcnf fm' instead of 'PropLogic.nnf fm' *) |
441 (* but that sometimes leads to worse performance due to the *) |
441 (* but that sometimes leads to worse performance due to the *) |
442 (* introduction of additional variables. *) |
442 (* introduction of additional variables. *) |
443 val fm' = PropLogic.nnf fm |
443 val fm' = PropLogic.nnf fm |
444 (* int list *) |
444 (* int list *) |
445 val indices = PropLogic.indices fm' |
445 val indices = PropLogic.indices fm' |
446 (* int list -> int -> prop_formula *) |
446 (* int list -> int -> prop_formula *) |
447 fun partial_var_eval [] i = BoolVar i |
447 fun partial_var_eval [] i = BoolVar i |
448 | partial_var_eval (x::xs) i = if x=i then True else if x=(~i) then False else partial_var_eval xs i |
448 | partial_var_eval (x::xs) i = if x=i then True else if x=(~i) then False else partial_var_eval xs i |
449 (* int list -> prop_formula -> prop_formula *) |
449 (* int list -> prop_formula -> prop_formula *) |
450 fun partial_eval xs True = True |
450 fun partial_eval xs True = True |
451 | partial_eval xs False = False |
451 | partial_eval xs False = False |
452 | partial_eval xs (BoolVar i) = partial_var_eval xs i |
452 | partial_eval xs (BoolVar i) = partial_var_eval xs i |
453 | partial_eval xs (Not fm) = SNot (partial_eval xs fm) |
453 | partial_eval xs (Not fm) = SNot (partial_eval xs fm) |
454 | partial_eval xs (Or (fm1, fm2)) = SOr (partial_eval xs fm1, partial_eval xs fm2) |
454 | partial_eval xs (Or (fm1, fm2)) = SOr (partial_eval xs fm1, partial_eval xs fm2) |
455 | partial_eval xs (And (fm1, fm2)) = SAnd (partial_eval xs fm1, partial_eval xs fm2) |
455 | partial_eval xs (And (fm1, fm2)) = SAnd (partial_eval xs fm1, partial_eval xs fm2) |
456 (* prop_formula -> int list *) |
456 (* prop_formula -> int list *) |
457 fun forced_vars True = [] |
457 fun forced_vars True = [] |
458 | forced_vars False = [] |
458 | forced_vars False = [] |
459 | forced_vars (BoolVar i) = [i] |
459 | forced_vars (BoolVar i) = [i] |
460 | forced_vars (Not (BoolVar i)) = [~i] |
460 | forced_vars (Not (BoolVar i)) = [~i] |
461 | forced_vars (Or (fm1, fm2)) = (forced_vars fm1) inter_int (forced_vars fm2) |
461 | forced_vars (Or (fm1, fm2)) = (forced_vars fm1) inter_int (forced_vars fm2) |
462 | forced_vars (And (fm1, fm2)) = (forced_vars fm1) union_int (forced_vars fm2) |
462 | forced_vars (And (fm1, fm2)) = (forced_vars fm1) union_int (forced_vars fm2) |
463 (* Above, i *and* ~i may be forced. In this case the first occurrence takes *) |
463 (* Above, i *and* ~i may be forced. In this case the first occurrence takes *) |
464 (* precedence, and the next partial evaluation of the formula returns 'False'. *) |
464 (* precedence, and the next partial evaluation of the formula returns 'False'. *) |
465 | forced_vars _ = error "formula is not in negation normal form" |
465 | forced_vars _ = error "formula is not in negation normal form" |
466 (* int list -> prop_formula -> (int list * prop_formula) *) |
466 (* int list -> prop_formula -> (int list * prop_formula) *) |
467 fun eval_and_force xs fm = |
467 fun eval_and_force xs fm = |
468 let |
468 let |
469 val fm' = partial_eval xs fm |
469 val fm' = partial_eval xs fm |
470 val xs' = forced_vars fm' |
470 val xs' = forced_vars fm' |
471 in |
471 in |
472 if null xs' then |
472 if null xs' then |
473 (xs, fm') |
473 (xs, fm') |
474 else |
474 else |
475 eval_and_force (xs@xs') fm' (* xs and xs' should be distinct, so '@' here should have *) |
475 eval_and_force (xs@xs') fm' (* xs and xs' should be distinct, so '@' here should have *) |
476 (* the same effect as 'union_int' *) |
476 (* the same effect as 'union_int' *) |
477 end |
477 end |
478 (* int list -> int option *) |
478 (* int list -> int option *) |
479 fun fresh_var xs = |
479 fun fresh_var xs = |
480 Library.find_first (fn i => not (i mem_int xs) andalso not ((~i) mem_int xs)) indices |
480 Library.find_first (fn i => not (i mem_int xs) andalso not ((~i) mem_int xs)) indices |
481 (* int list -> prop_formula -> int list option *) |
481 (* int list -> prop_formula -> int list option *) |
482 (* partial assignment 'xs' *) |
482 (* partial assignment 'xs' *) |
483 fun dpll xs fm = |
483 fun dpll xs fm = |
484 let |
484 let |
485 val (xs', fm') = eval_and_force xs fm |
485 val (xs', fm') = eval_and_force xs fm |
486 in |
486 in |
487 case fm' of |
487 case fm' of |
488 True => SOME xs' |
488 True => SOME xs' |
489 | False => NONE |
489 | False => NONE |
490 | _ => |
490 | _ => |
491 let |
491 let |
492 val x = valOf (fresh_var xs') (* a fresh variable must exist since 'fm' did not evaluate to 'True'/'False' *) |
492 val x = valOf (fresh_var xs') (* a fresh variable must exist since 'fm' did not evaluate to 'True'/'False' *) |
493 in |
493 in |
494 case dpll (x::xs') fm' of (* passing fm' rather than fm should save some simplification work *) |
494 case dpll (x::xs') fm' of (* passing fm' rather than fm should save some simplification work *) |
495 SOME xs'' => SOME xs'' |
495 SOME xs'' => SOME xs'' |
496 | NONE => dpll ((~x)::xs') fm' (* now try interpreting 'x' as 'False' *) |
496 | NONE => dpll ((~x)::xs') fm' (* now try interpreting 'x' as 'False' *) |
497 end |
497 end |
498 end |
498 end |
499 (* int list -> assignment *) |
499 (* int list -> assignment *) |
500 fun assignment_from_list [] i = |
500 fun assignment_from_list [] i = |
501 NONE (* the DPLL procedure didn't provide a value for this variable *) |
501 NONE (* the DPLL procedure didn't provide a value for this variable *) |
502 | assignment_from_list (x::xs) i = |
502 | assignment_from_list (x::xs) i = |
503 if x=i then (SOME true) |
503 if x=i then (SOME true) |
504 else if x=(~i) then (SOME false) |
504 else if x=(~i) then (SOME false) |
505 else assignment_from_list xs i |
505 else assignment_from_list xs i |
506 in |
506 in |
507 (* initially, no variable is interpreted yet *) |
507 (* initially, no variable is interpreted yet *) |
508 case dpll [] fm' of |
508 case dpll [] fm' of |
509 SOME assignment => SatSolver.SATISFIABLE (assignment_from_list assignment) |
509 SOME assignment => SatSolver.SATISFIABLE (assignment_from_list assignment) |
510 | NONE => SatSolver.UNSATISFIABLE NONE |
510 | NONE => SatSolver.UNSATISFIABLE NONE |
511 end |
511 end |
512 end (* local *) |
512 end (* local *) |
513 in |
513 in |
514 SatSolver.add_solver ("dpll", dpll_solver) |
514 SatSolver.add_solver ("dpll", dpll_solver) |
515 end; |
515 end; |
516 |
516 |
517 (* ------------------------------------------------------------------------- *) |
517 (* ------------------------------------------------------------------------- *) |
518 (* Internal SAT solver, available as 'SatSolver.invoke_solver "auto"': uses *) |
518 (* Internal SAT solver, available as 'SatSolver.invoke_solver "auto"': uses *) |
519 (* the last installed solver (other than "auto" itself) that does not raise *) |
519 (* the last installed solver (other than "auto" itself) that does not raise *) |
520 (* 'NOT_CONFIGURED'. (However, the solver may return 'UNKNOWN'.) *) |
520 (* 'NOT_CONFIGURED'. (However, the solver may return 'UNKNOWN'.) *) |
521 (* ------------------------------------------------------------------------- *) |
521 (* ------------------------------------------------------------------------- *) |
522 |
522 |
523 let |
523 let |
524 fun auto_solver fm = |
524 fun auto_solver fm = |
525 let |
525 let |
526 fun loop [] = |
526 fun loop [] = |
527 SatSolver.UNKNOWN |
527 SatSolver.UNKNOWN |
528 | loop ((name, solver)::solvers) = |
528 | loop ((name, solver)::solvers) = |
529 if name="auto" then |
529 if name="auto" then |
530 (* do not call solver "auto" from within "auto" *) |
530 (* do not call solver "auto" from within "auto" *) |
531 loop solvers |
531 loop solvers |
532 else ( |
532 else ( |
533 (if name="dpll" orelse name="enumerate" then |
533 (if name="dpll" orelse name="enumerate" then |
534 warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.") |
534 warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.") |
535 else |
535 else |
536 tracing ("Using SAT solver " ^ quote name ^ ".")); |
536 tracing ("Using SAT solver " ^ quote name ^ ".")); |
537 (* apply 'solver' to 'fm' *) |
537 (* apply 'solver' to 'fm' *) |
538 solver fm |
538 solver fm |
539 handle SatSolver.NOT_CONFIGURED => loop solvers |
539 handle SatSolver.NOT_CONFIGURED => loop solvers |
540 ) |
540 ) |
541 in |
541 in |
542 loop (!SatSolver.solvers) |
542 loop (!SatSolver.solvers) |
543 end |
543 end |
544 in |
544 in |
545 SatSolver.add_solver ("auto", auto_solver) |
545 SatSolver.add_solver ("auto", auto_solver) |
546 end; |
546 end; |
547 |
547 |
548 (* ------------------------------------------------------------------------- *) |
548 (* ------------------------------------------------------------------------- *) |
549 (* MiniSat 1.14 *) |
549 (* MiniSat 1.14 *) |
550 (* (http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/) *) |
550 (* (http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/) *) |
563 (* introduces IDs for original clauses in the proof trace. It does not (in *) |
563 (* introduces IDs for original clauses in the proof trace. It does not (in *) |
564 (* general) follow the convention that the original clauses are numbered *) |
564 (* general) follow the convention that the original clauses are numbered *) |
565 (* from 0 to n-1 (where n is the number of clauses in the formula). *) |
565 (* from 0 to n-1 (where n is the number of clauses in the formula). *) |
566 |
566 |
567 let |
567 let |
568 exception INVALID_PROOF of string |
568 exception INVALID_PROOF of string |
569 fun minisat_with_proofs fm = |
569 fun minisat_with_proofs fm = |
570 let |
570 let |
571 val _ = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () |
571 val _ = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () |
572 val inpath = File.tmp_path (Path.explode "isabelle.cnf") |
572 val inpath = File.tmp_path (Path.explode "isabelle.cnf") |
573 val outpath = File.tmp_path (Path.explode "result") |
573 val outpath = File.tmp_path (Path.explode "result") |
574 val proofpath = File.tmp_path (Path.explode "result.prf") |
574 val proofpath = File.tmp_path (Path.explode "result.prf") |
575 val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " -t " ^ (Path.implode proofpath) ^ "> /dev/null" |
575 val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " -t " ^ (Path.implode proofpath) ^ "> /dev/null" |
576 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm |
576 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm |
577 fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT") |
577 fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT") |
578 val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () |
578 val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () |
579 val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () |
579 val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () |
580 val cnf = PropLogic.defcnf fm |
580 val cnf = PropLogic.defcnf fm |
581 val result = SatSolver.make_external_solver cmd writefn readfn cnf |
581 val result = SatSolver.make_external_solver cmd writefn readfn cnf |
582 val _ = try File.rm inpath |
582 val _ = try File.rm inpath |
583 val _ = try File.rm outpath |
583 val _ = try File.rm outpath |
584 in case result of |
584 in case result of |
585 SatSolver.UNSATISFIABLE NONE => |
585 SatSolver.UNSATISFIABLE NONE => |
586 (let |
586 (let |
587 (* string list *) |
587 (* string list *) |
588 val proof_lines = (split_lines o File.read) proofpath |
588 val proof_lines = (split_lines o File.read) proofpath |
589 handle IO.Io _ => raise INVALID_PROOF "Could not read file \"result.prf\"" |
589 handle IO.Io _ => raise INVALID_PROOF "Could not read file \"result.prf\"" |
590 (* representation of clauses as ordered lists of literals (with duplicates removed) *) |
590 (* representation of clauses as ordered lists of literals (with duplicates removed) *) |
591 (* prop_formula -> int list *) |
591 (* prop_formula -> int list *) |
592 fun clause_to_lit_list (PropLogic.Or (fm1, fm2)) = |
592 fun clause_to_lit_list (PropLogic.Or (fm1, fm2)) = |
593 OrdList.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2) |
593 OrdList.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2) |
594 | clause_to_lit_list (PropLogic.BoolVar i) = |
594 | clause_to_lit_list (PropLogic.BoolVar i) = |
595 [i] |
595 [i] |
596 | clause_to_lit_list (PropLogic.Not (PropLogic.BoolVar i)) = |
596 | clause_to_lit_list (PropLogic.Not (PropLogic.BoolVar i)) = |
597 [~i] |
597 [~i] |
598 | clause_to_lit_list _ = |
598 | clause_to_lit_list _ = |
599 raise INVALID_PROOF "Error: invalid clause in CNF formula." |
599 raise INVALID_PROOF "Error: invalid clause in CNF formula." |
600 (* prop_formula -> int *) |
600 (* prop_formula -> int *) |
601 fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = |
601 fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = |
602 cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2 |
602 cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2 |
603 | cnf_number_of_clauses _ = |
603 | cnf_number_of_clauses _ = |
604 1 |
604 1 |
605 val number_of_clauses = cnf_number_of_clauses cnf |
605 val number_of_clauses = cnf_number_of_clauses cnf |
606 (* int list array *) |
606 (* int list array *) |
607 val clauses = Array.array (number_of_clauses, []) |
607 val clauses = Array.array (number_of_clauses, []) |
608 (* initialize the 'clauses' array *) |
608 (* initialize the 'clauses' array *) |
609 (* prop_formula * int -> int *) |
609 (* prop_formula * int -> int *) |
610 fun init_array (PropLogic.And (fm1, fm2), n) = |
610 fun init_array (PropLogic.And (fm1, fm2), n) = |
611 init_array (fm2, init_array (fm1, n)) |
611 init_array (fm2, init_array (fm1, n)) |
612 | init_array (fm, n) = |
612 | init_array (fm, n) = |
613 (Array.update (clauses, n, clause_to_lit_list fm); n+1) |
613 (Array.update (clauses, n, clause_to_lit_list fm); n+1) |
614 val _ = init_array (cnf, 0) |
614 val _ = init_array (cnf, 0) |
615 (* optimization for the common case where MiniSat "R"s clauses in their *) |
615 (* optimization for the common case where MiniSat "R"s clauses in their *) |
616 (* original order: *) |
616 (* original order: *) |
617 val last_ref_clause = ref (number_of_clauses - 1) |
617 val last_ref_clause = ref (number_of_clauses - 1) |
618 (* search the 'clauses' array for the given list of literals 'lits', *) |
618 (* search the 'clauses' array for the given list of literals 'lits', *) |
619 (* starting at index '!last_ref_clause + 1' *) |
619 (* starting at index '!last_ref_clause + 1' *) |
620 (* int list -> int option *) |
620 (* int list -> int option *) |
621 fun original_clause_id lits = |
621 fun original_clause_id lits = |
622 let |
622 let |
623 fun original_clause_id_from index = |
623 fun original_clause_id_from index = |
624 if index = number_of_clauses then |
624 if index = number_of_clauses then |
625 (* search from beginning again *) |
625 (* search from beginning again *) |
626 original_clause_id_from 0 |
626 original_clause_id_from 0 |
627 (* both 'lits' and the list of literals used in 'clauses' are sorted, so *) |
627 (* both 'lits' and the list of literals used in 'clauses' are sorted, so *) |
628 (* testing for equality should suffice -- barring duplicate literals *) |
628 (* testing for equality should suffice -- barring duplicate literals *) |
629 else if Array.sub (clauses, index) = lits then ( |
629 else if Array.sub (clauses, index) = lits then ( |
630 (* success *) |
630 (* success *) |
631 last_ref_clause := index; |
631 last_ref_clause := index; |
632 SOME index |
632 SOME index |
633 ) else if index = !last_ref_clause then |
633 ) else if index = !last_ref_clause then |
634 (* failure *) |
634 (* failure *) |
635 NONE |
635 NONE |
636 else |
636 else |
637 (* continue search *) |
637 (* continue search *) |
638 original_clause_id_from (index + 1) |
638 original_clause_id_from (index + 1) |
639 in |
639 in |
640 original_clause_id_from (!last_ref_clause + 1) |
640 original_clause_id_from (!last_ref_clause + 1) |
641 end |
641 end |
642 (* string -> int *) |
642 (* string -> int *) |
643 fun int_from_string s = ( |
643 fun int_from_string s = ( |
644 case Int.fromString s of |
644 case Int.fromString s of |
645 SOME i => i |
645 SOME i => i |
646 | NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).") |
646 | NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).") |
647 ) |
647 ) |
648 (* parse the proof file *) |
648 (* parse the proof file *) |
649 val clause_table = ref (Inttab.empty : int list Inttab.table) |
649 val clause_table = ref (Inttab.empty : int list Inttab.table) |
650 val empty_id = ref ~1 |
650 val empty_id = ref ~1 |
651 (* contains a mapping from clause IDs as used by MiniSat to clause IDs in *) |
651 (* contains a mapping from clause IDs as used by MiniSat to clause IDs in *) |
652 (* our proof format, where original clauses are numbered starting from 0 *) |
652 (* our proof format, where original clauses are numbered starting from 0 *) |
653 val clause_id_map = ref (Inttab.empty : int Inttab.table) |
653 val clause_id_map = ref (Inttab.empty : int Inttab.table) |
654 fun sat_to_proof id = ( |
654 fun sat_to_proof id = ( |
655 case Inttab.lookup (!clause_id_map) id of |
655 case Inttab.lookup (!clause_id_map) id of |
656 SOME id' => id' |
656 SOME id' => id' |
657 | NONE => raise INVALID_PROOF ("Clause ID " ^ Int.toString id ^ " used, but not defined.") |
657 | NONE => raise INVALID_PROOF ("Clause ID " ^ Int.toString id ^ " used, but not defined.") |
658 ) |
658 ) |
659 val next_id = ref (number_of_clauses - 1) |
659 val next_id = ref (number_of_clauses - 1) |
660 (* string list -> unit *) |
660 (* string list -> unit *) |
661 fun process_tokens [] = |
661 fun process_tokens [] = |
662 () |
662 () |
663 | process_tokens (tok::toks) = |
663 | process_tokens (tok::toks) = |
664 if tok="R" then ( |
664 if tok="R" then ( |
665 case toks of |
665 case toks of |
666 id::sep::lits => |
666 id::sep::lits => |
667 let |
667 let |
668 val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"R\" disallowed after \"X\"." |
668 val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"R\" disallowed after \"X\"." |
669 val cid = int_from_string id |
669 val cid = int_from_string id |
670 val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).") |
670 val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).") |
671 val ls = sort int_ord (map int_from_string lits) |
671 val ls = sort int_ord (map int_from_string lits) |
672 val proof_id = case original_clause_id ls of |
672 val proof_id = case original_clause_id ls of |
673 SOME orig_id => orig_id |
673 SOME orig_id => orig_id |
674 | NONE => raise INVALID_PROOF ("Original clause (new ID is " ^ id ^ ") not found.") |
674 | NONE => raise INVALID_PROOF ("Original clause (new ID is " ^ id ^ ") not found.") |
675 in |
675 in |
676 (* extend the mapping of clause IDs with this newly defined ID *) |
676 (* extend the mapping of clause IDs with this newly defined ID *) |
677 clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map) |
677 clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map) |
678 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"R\").") |
678 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"R\").") |
679 (* the proof itself doesn't change *) |
679 (* the proof itself doesn't change *) |
680 end |
680 end |
681 | _ => |
681 | _ => |
682 raise INVALID_PROOF "File format error: \"R\" followed by an insufficient number of tokens." |
682 raise INVALID_PROOF "File format error: \"R\" followed by an insufficient number of tokens." |
683 ) else if tok="C" then ( |
683 ) else if tok="C" then ( |
684 case toks of |
684 case toks of |
685 id::sep::ids => |
685 id::sep::ids => |
686 let |
686 let |
687 val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"C\" disallowed after \"X\"." |
687 val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"C\" disallowed after \"X\"." |
688 val cid = int_from_string id |
688 val cid = int_from_string id |
689 val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).") |
689 val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).") |
690 (* ignore the pivot literals in MiniSat's trace *) |
690 (* ignore the pivot literals in MiniSat's trace *) |
691 fun unevens [] = raise INVALID_PROOF "File format error: \"C\" followed by an even number of IDs." |
691 fun unevens [] = raise INVALID_PROOF "File format error: \"C\" followed by an even number of IDs." |
692 | unevens (x :: []) = x :: [] |
692 | unevens (x :: []) = x :: [] |
693 | unevens (x :: _ :: xs) = x :: unevens xs |
693 | unevens (x :: _ :: xs) = x :: unevens xs |
694 val rs = (map sat_to_proof o unevens o map int_from_string) ids |
694 val rs = (map sat_to_proof o unevens o map int_from_string) ids |
695 (* extend the mapping of clause IDs with this newly defined ID *) |
695 (* extend the mapping of clause IDs with this newly defined ID *) |
696 val proof_id = inc next_id |
696 val proof_id = inc next_id |
697 val _ = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map) |
697 val _ = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map) |
698 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"C\").") |
698 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"C\").") |
699 in |
699 in |
700 (* update clause table *) |
700 (* update clause table *) |
701 clause_table := Inttab.update_new (proof_id, rs) (!clause_table) |
701 clause_table := Inttab.update_new (proof_id, rs) (!clause_table) |
702 handle Inttab.DUP _ => raise INVALID_PROOF ("Error: internal ID for clause " ^ id ^ " already used.") |
702 handle Inttab.DUP _ => raise INVALID_PROOF ("Error: internal ID for clause " ^ id ^ " already used.") |
703 end |
703 end |
704 | _ => |
704 | _ => |
705 raise INVALID_PROOF "File format error: \"C\" followed by an insufficient number of tokens." |
705 raise INVALID_PROOF "File format error: \"C\" followed by an insufficient number of tokens." |
706 ) else if tok="D" then ( |
706 ) else if tok="D" then ( |
707 case toks of |
707 case toks of |
708 [id] => |
708 [id] => |
709 let |
709 let |
710 val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"D\" disallowed after \"X\"." |
710 val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"D\" disallowed after \"X\"." |
711 val _ = sat_to_proof (int_from_string id) |
711 val _ = sat_to_proof (int_from_string id) |
712 in |
712 in |
713 (* simply ignore "D" *) |
713 (* simply ignore "D" *) |
714 () |
714 () |
715 end |
715 end |
716 | _ => |
716 | _ => |
717 raise INVALID_PROOF "File format error: \"D\" followed by an illegal number of tokens." |
717 raise INVALID_PROOF "File format error: \"D\" followed by an illegal number of tokens." |
718 ) else if tok="X" then ( |
718 ) else if tok="X" then ( |
719 case toks of |
719 case toks of |
720 [id1, id2] => |
720 [id1, id2] => |
721 let |
721 let |
722 val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one end-of-proof statement." |
722 val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one end-of-proof statement." |
723 val _ = sat_to_proof (int_from_string id1) |
723 val _ = sat_to_proof (int_from_string id1) |
724 val new_empty_id = sat_to_proof (int_from_string id2) |
724 val new_empty_id = sat_to_proof (int_from_string id2) |
725 in |
725 in |
726 (* update conflict id *) |
726 (* update conflict id *) |
727 empty_id := new_empty_id |
727 empty_id := new_empty_id |
728 end |
728 end |
729 | _ => |
729 | _ => |
730 raise INVALID_PROOF "File format error: \"X\" followed by an illegal number of tokens." |
730 raise INVALID_PROOF "File format error: \"X\" followed by an illegal number of tokens." |
731 ) else |
731 ) else |
732 raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.") |
732 raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.") |
733 (* string list -> unit *) |
733 (* string list -> unit *) |
734 fun process_lines [] = |
734 fun process_lines [] = |
735 () |
735 () |
736 | process_lines (l::ls) = ( |
736 | process_lines (l::ls) = ( |
737 process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l); |
737 process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l); |
738 process_lines ls |
738 process_lines ls |
739 ) |
739 ) |
740 (* proof *) |
740 (* proof *) |
741 val _ = process_lines proof_lines |
741 val _ = process_lines proof_lines |
742 val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified." |
742 val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified." |
743 in |
743 in |
744 SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id)) |
744 SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id)) |
745 end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE)) |
745 end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE)) |
746 | result => |
746 | result => |
747 result |
747 result |
748 end |
748 end |
749 in |
749 in |
750 SatSolver.add_solver ("minisat_with_proofs", minisat_with_proofs) |
750 SatSolver.add_solver ("minisat_with_proofs", minisat_with_proofs) |
751 end; |
751 end; |
752 |
752 |
753 let |
753 let |
754 fun minisat fm = |
754 fun minisat fm = |
755 let |
755 let |
756 val _ = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () |
756 val _ = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () |
757 val inpath = File.tmp_path (Path.explode "isabelle.cnf") |
757 val inpath = File.tmp_path (Path.explode "isabelle.cnf") |
758 val outpath = File.tmp_path (Path.explode "result") |
758 val outpath = File.tmp_path (Path.explode "result") |
759 val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " > /dev/null" |
759 val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " > /dev/null" |
760 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) |
760 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) |
761 fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT") |
761 fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT") |
762 val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () |
762 val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () |
763 val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () |
763 val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () |
764 val result = SatSolver.make_external_solver cmd writefn readfn fm |
764 val result = SatSolver.make_external_solver cmd writefn readfn fm |
765 val _ = try File.rm inpath |
765 val _ = try File.rm inpath |
766 val _ = try File.rm outpath |
766 val _ = try File.rm outpath |
767 in |
767 in |
768 result |
768 result |
769 end |
769 end |
770 in |
770 in |
771 SatSolver.add_solver ("minisat", minisat) |
771 SatSolver.add_solver ("minisat", minisat) |
772 end; |
772 end; |
773 |
773 |
774 (* ------------------------------------------------------------------------- *) |
774 (* ------------------------------------------------------------------------- *) |
775 (* zChaff (http://www.princeton.edu/~chaff/zchaff.html) *) |
775 (* zChaff (http://www.princeton.edu/~chaff/zchaff.html) *) |
776 (* ------------------------------------------------------------------------- *) |
776 (* ------------------------------------------------------------------------- *) |
785 |
785 |
786 (* add "zchaff_with_proofs" _before_ "zchaff" to the available solvers, so *) |
786 (* add "zchaff_with_proofs" _before_ "zchaff" to the available solvers, so *) |
787 (* that the latter is preferred by the "auto" solver *) |
787 (* that the latter is preferred by the "auto" solver *) |
788 |
788 |
789 let |
789 let |
790 exception INVALID_PROOF of string |
790 exception INVALID_PROOF of string |
791 fun zchaff_with_proofs fm = |
791 fun zchaff_with_proofs fm = |
792 case SatSolver.invoke_solver "zchaff" fm of |
792 case SatSolver.invoke_solver "zchaff" fm of |
793 SatSolver.UNSATISFIABLE NONE => |
793 SatSolver.UNSATISFIABLE NONE => |
794 (let |
794 (let |
795 (* string list *) |
795 (* string list *) |
796 val proof_lines = ((split_lines o File.read) (Path.explode "resolve_trace")) |
796 val proof_lines = ((split_lines o File.read) (Path.explode "resolve_trace")) |
797 handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\"" |
797 handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\"" |
798 (* PropLogic.prop_formula -> int *) |
798 (* PropLogic.prop_formula -> int *) |
799 fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2 |
799 fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2 |
800 | cnf_number_of_clauses _ = 1 |
800 | cnf_number_of_clauses _ = 1 |
801 (* string -> int *) |
801 (* string -> int *) |
802 fun int_from_string s = ( |
802 fun int_from_string s = ( |
803 case Int.fromString s of |
803 case Int.fromString s of |
804 SOME i => i |
804 SOME i => i |
805 | NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).") |
805 | NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).") |
806 ) |
806 ) |
807 (* parse the "resolve_trace" file *) |
807 (* parse the "resolve_trace" file *) |
808 val clause_offset = ref ~1 |
808 val clause_offset = ref ~1 |
809 val clause_table = ref (Inttab.empty : int list Inttab.table) |
809 val clause_table = ref (Inttab.empty : int list Inttab.table) |
810 val empty_id = ref ~1 |
810 val empty_id = ref ~1 |
811 (* string list -> unit *) |
811 (* string list -> unit *) |
812 fun process_tokens [] = |
812 fun process_tokens [] = |
813 () |
813 () |
814 | process_tokens (tok::toks) = |
814 | process_tokens (tok::toks) = |
815 if tok="CL:" then ( |
815 if tok="CL:" then ( |
816 case toks of |
816 case toks of |
817 id::sep::ids => |
817 id::sep::ids => |
818 let |
818 let |
819 val _ = if !clause_offset = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"VAR:\".") |
819 val _ = if !clause_offset = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"VAR:\".") |
820 val _ = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"CONF:\".") |
820 val _ = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"CONF:\".") |
821 val cid = int_from_string id |
821 val cid = int_from_string id |
822 val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).") |
822 val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).") |
823 val rs = map int_from_string ids |
823 val rs = map int_from_string ids |
824 in |
824 in |
825 (* update clause table *) |
825 (* update clause table *) |
826 clause_table := Inttab.update_new (cid, rs) (!clause_table) |
826 clause_table := Inttab.update_new (cid, rs) (!clause_table) |
827 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once.") |
827 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once.") |
828 end |
828 end |
829 | _ => |
829 | _ => |
830 raise INVALID_PROOF "File format error: \"CL:\" followed by an insufficient number of tokens." |
830 raise INVALID_PROOF "File format error: \"CL:\" followed by an insufficient number of tokens." |
831 ) else if tok="VAR:" then ( |
831 ) else if tok="VAR:" then ( |
832 case toks of |
832 case toks of |
833 id::levsep::levid::valsep::valid::antesep::anteid::litsep::lits => |
833 id::levsep::levid::valsep::valid::antesep::anteid::litsep::lits => |
834 let |
834 let |
835 val _ = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"VAR:\" disallowed after \"CONF:\".") |
835 val _ = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"VAR:\" disallowed after \"CONF:\".") |
836 (* set 'clause_offset' to the largest used clause ID *) |
836 (* set 'clause_offset' to the largest used clause ID *) |
837 val _ = if !clause_offset = ~1 then clause_offset := |
837 val _ = if !clause_offset = ~1 then clause_offset := |
838 (case Inttab.max_key (!clause_table) of |
838 (case Inttab.max_key (!clause_table) of |
839 SOME id => id |
839 SOME id => id |
840 | NONE => cnf_number_of_clauses (PropLogic.defcnf fm) - 1 (* the first clause ID is 0, not 1 *)) |
840 | NONE => cnf_number_of_clauses (PropLogic.defcnf fm) - 1 (* the first clause ID is 0, not 1 *)) |
841 else |
841 else |
842 () |
842 () |
843 val vid = int_from_string id |
843 val vid = int_from_string id |
844 val _ = if levsep = "L:" then () else raise INVALID_PROOF ("File format error: \"L:\" expected (" ^ quote levsep ^ " encountered).") |
844 val _ = if levsep = "L:" then () else raise INVALID_PROOF ("File format error: \"L:\" expected (" ^ quote levsep ^ " encountered).") |
845 val _ = int_from_string levid |
845 val _ = int_from_string levid |
846 val _ = if valsep = "V:" then () else raise INVALID_PROOF ("File format error: \"V:\" expected (" ^ quote valsep ^ " encountered).") |
846 val _ = if valsep = "V:" then () else raise INVALID_PROOF ("File format error: \"V:\" expected (" ^ quote valsep ^ " encountered).") |
847 val _ = int_from_string valid |
847 val _ = int_from_string valid |
848 val _ = if antesep = "A:" then () else raise INVALID_PROOF ("File format error: \"A:\" expected (" ^ quote antesep ^ " encountered).") |
848 val _ = if antesep = "A:" then () else raise INVALID_PROOF ("File format error: \"A:\" expected (" ^ quote antesep ^ " encountered).") |
849 val aid = int_from_string anteid |
849 val aid = int_from_string anteid |
850 val _ = if litsep = "Lits:" then () else raise INVALID_PROOF ("File format error: \"Lits:\" expected (" ^ quote litsep ^ " encountered).") |
850 val _ = if litsep = "Lits:" then () else raise INVALID_PROOF ("File format error: \"Lits:\" expected (" ^ quote litsep ^ " encountered).") |
851 val ls = map int_from_string lits |
851 val ls = map int_from_string lits |
852 (* convert the data provided by zChaff to our resolution-style proof format *) |
852 (* convert the data provided by zChaff to our resolution-style proof format *) |
853 (* each "VAR:" line defines a unit clause, the resolvents are implicitly *) |
853 (* each "VAR:" line defines a unit clause, the resolvents are implicitly *) |
854 (* given by the literals in the antecedent clause *) |
854 (* given by the literals in the antecedent clause *) |
855 (* we use the sum of '!clause_offset' and the variable ID as clause ID for the unit clause *) |
855 (* we use the sum of '!clause_offset' and the variable ID as clause ID for the unit clause *) |
856 val cid = !clause_offset + vid |
856 val cid = !clause_offset + vid |
857 (* the low bit of each literal gives its sign (positive/negative), therefore *) |
857 (* the low bit of each literal gives its sign (positive/negative), therefore *) |
858 (* we have to divide each literal by 2 to obtain the proper variable ID; then *) |
858 (* we have to divide each literal by 2 to obtain the proper variable ID; then *) |
859 (* we add '!clause_offset' to obtain the ID of the corresponding unit clause *) |
859 (* we add '!clause_offset' to obtain the ID of the corresponding unit clause *) |
860 val vids = filter (not_equal vid) (map (fn l => l div 2) ls) |
860 val vids = filter (not_equal vid) (map (fn l => l div 2) ls) |
861 val rs = aid :: map (fn v => !clause_offset + v) vids |
861 val rs = aid :: map (fn v => !clause_offset + v) vids |
862 in |
862 in |
863 (* update clause table *) |
863 (* update clause table *) |
864 clause_table := Inttab.update_new (cid, rs) (!clause_table) |
864 clause_table := Inttab.update_new (cid, rs) (!clause_table) |
865 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int cid ^ " (derived from antecedent for variable " ^ id ^ ") already defined.") |
865 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int cid ^ " (derived from antecedent for variable " ^ id ^ ") already defined.") |
866 end |
866 end |
867 | _ => |
867 | _ => |
868 raise INVALID_PROOF "File format error: \"VAR:\" followed by an insufficient number of tokens." |
868 raise INVALID_PROOF "File format error: \"VAR:\" followed by an insufficient number of tokens." |
869 ) else if tok="CONF:" then ( |
869 ) else if tok="CONF:" then ( |
870 case toks of |
870 case toks of |
871 id::sep::ids => |
871 id::sep::ids => |
872 let |
872 let |
873 val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one conflicting clause specified." |
873 val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one conflicting clause specified." |
874 val cid = int_from_string id |
874 val cid = int_from_string id |
875 val _ = if sep = "==" then () else raise INVALID_PROOF ("File format error: \"==\" expected (" ^ quote sep ^ " encountered).") |
875 val _ = if sep = "==" then () else raise INVALID_PROOF ("File format error: \"==\" expected (" ^ quote sep ^ " encountered).") |
876 val ls = map int_from_string ids |
876 val ls = map int_from_string ids |
877 (* the conflict clause must be resolved with the unit clauses *) |
877 (* the conflict clause must be resolved with the unit clauses *) |
878 (* for its literals to obtain the empty clause *) |
878 (* for its literals to obtain the empty clause *) |
879 val vids = map (fn l => l div 2) ls |
879 val vids = map (fn l => l div 2) ls |
880 val rs = cid :: map (fn v => !clause_offset + v) vids |
880 val rs = cid :: map (fn v => !clause_offset + v) vids |
881 val new_empty_id = getOpt (Inttab.max_key (!clause_table), !clause_offset) + 1 |
881 val new_empty_id = getOpt (Inttab.max_key (!clause_table), !clause_offset) + 1 |
882 in |
882 in |
883 (* update clause table and conflict id *) |
883 (* update clause table and conflict id *) |
884 clause_table := Inttab.update_new (new_empty_id, rs) (!clause_table) |
884 clause_table := Inttab.update_new (new_empty_id, rs) (!clause_table) |
885 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int new_empty_id ^ " (empty clause derived from clause " ^ id ^ ") already defined."); |
885 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int new_empty_id ^ " (empty clause derived from clause " ^ id ^ ") already defined."); |
886 empty_id := new_empty_id |
886 empty_id := new_empty_id |
887 end |
887 end |
888 | _ => |
888 | _ => |
889 raise INVALID_PROOF "File format error: \"CONF:\" followed by an insufficient number of tokens." |
889 raise INVALID_PROOF "File format error: \"CONF:\" followed by an insufficient number of tokens." |
890 ) else |
890 ) else |
891 raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.") |
891 raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.") |
892 (* string list -> unit *) |
892 (* string list -> unit *) |
893 fun process_lines [] = |
893 fun process_lines [] = |
894 () |
894 () |
895 | process_lines (l::ls) = ( |
895 | process_lines (l::ls) = ( |
896 process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l); |
896 process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l); |
897 process_lines ls |
897 process_lines ls |
898 ) |
898 ) |
899 (* proof *) |
899 (* proof *) |
900 val _ = process_lines proof_lines |
900 val _ = process_lines proof_lines |
901 val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified." |
901 val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified." |
902 in |
902 in |
903 SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id)) |
903 SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id)) |
904 end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE)) |
904 end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE)) |
905 | result => |
905 | result => |
906 result |
906 result |
907 in |
907 in |
908 SatSolver.add_solver ("zchaff_with_proofs", zchaff_with_proofs) |
908 SatSolver.add_solver ("zchaff_with_proofs", zchaff_with_proofs) |
909 end; |
909 end; |
910 |
910 |
911 let |
911 let |
912 fun zchaff fm = |
912 fun zchaff fm = |
913 let |
913 let |
914 val _ = if (getenv "ZCHAFF_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () |
914 val _ = if (getenv "ZCHAFF_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () |
915 val _ = if (getenv "ZCHAFF_VERSION") <> "2004.5.13" andalso |
915 val _ = if (getenv "ZCHAFF_VERSION") <> "2004.5.13" andalso |
916 (getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else () |
916 (getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else () |
917 (* both versions of zChaff appear to have the same interface, so we do *) |
917 (* both versions of zChaff appear to have the same interface, so we do *) |
918 (* not actually need to distinguish between them in the following code *) |
918 (* not actually need to distinguish between them in the following code *) |
919 val inpath = File.tmp_path (Path.explode "isabelle.cnf") |
919 val inpath = File.tmp_path (Path.explode "isabelle.cnf") |
920 val outpath = File.tmp_path (Path.explode "result") |
920 val outpath = File.tmp_path (Path.explode "result") |
921 val cmd = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath) |
921 val cmd = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath) |
922 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) |
922 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) |
923 fun readfn () = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable") |
923 fun readfn () = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable") |
924 val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () |
924 val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () |
925 val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () |
925 val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () |
926 val result = SatSolver.make_external_solver cmd writefn readfn fm |
926 val result = SatSolver.make_external_solver cmd writefn readfn fm |
927 val _ = try File.rm inpath |
927 val _ = try File.rm inpath |
928 val _ = try File.rm outpath |
928 val _ = try File.rm outpath |
929 in |
929 in |
930 result |
930 result |
931 end |
931 end |
932 in |
932 in |
933 SatSolver.add_solver ("zchaff", zchaff) |
933 SatSolver.add_solver ("zchaff", zchaff) |
934 end; |
934 end; |
935 |
935 |
936 (* ------------------------------------------------------------------------- *) |
936 (* ------------------------------------------------------------------------- *) |
937 (* BerkMin 561 (http://eigold.tripod.com/BerkMin.html) *) |
937 (* BerkMin 561 (http://eigold.tripod.com/BerkMin.html) *) |
938 (* ------------------------------------------------------------------------- *) |
938 (* ------------------------------------------------------------------------- *) |
939 |
939 |
940 let |
940 let |
941 fun berkmin fm = |
941 fun berkmin fm = |
942 let |
942 let |
943 val _ = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else () |
943 val _ = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else () |
944 val inpath = File.tmp_path (Path.explode "isabelle.cnf") |
944 val inpath = File.tmp_path (Path.explode "isabelle.cnf") |
945 val outpath = File.tmp_path (Path.explode "result") |
945 val outpath = File.tmp_path (Path.explode "result") |
946 val cmd = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath) |
946 val cmd = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath) |
947 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) |
947 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) |
948 fun readfn () = SatSolver.read_std_result_file outpath ("Satisfiable !!", "solution =", "UNSATISFIABLE !!") |
948 fun readfn () = SatSolver.read_std_result_file outpath ("Satisfiable !!", "solution =", "UNSATISFIABLE !!") |
949 val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () |
949 val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () |
950 val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () |
950 val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () |
951 val result = SatSolver.make_external_solver cmd writefn readfn fm |
951 val result = SatSolver.make_external_solver cmd writefn readfn fm |
952 val _ = try File.rm inpath |
952 val _ = try File.rm inpath |
953 val _ = try File.rm outpath |
953 val _ = try File.rm outpath |
954 in |
954 in |
955 result |
955 result |
956 end |
956 end |
957 in |
957 in |
958 SatSolver.add_solver ("berkmin", berkmin) |
958 SatSolver.add_solver ("berkmin", berkmin) |
959 end; |
959 end; |
960 |
960 |
961 (* ------------------------------------------------------------------------- *) |
961 (* ------------------------------------------------------------------------- *) |
962 (* Jerusat 1.3 (http://www.cs.tau.ac.il/~ale1/) *) |
962 (* Jerusat 1.3 (http://www.cs.tau.ac.il/~ale1/) *) |
963 (* ------------------------------------------------------------------------- *) |
963 (* ------------------------------------------------------------------------- *) |
964 |
964 |
965 let |
965 let |
966 fun jerusat fm = |
966 fun jerusat fm = |
967 let |
967 let |
968 val _ = if (getenv "JERUSAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () |
968 val _ = if (getenv "JERUSAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () |
969 val inpath = File.tmp_path (Path.explode "isabelle.cnf") |
969 val inpath = File.tmp_path (Path.explode "isabelle.cnf") |
970 val outpath = File.tmp_path (Path.explode "result") |
970 val outpath = File.tmp_path (Path.explode "result") |
971 val cmd = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath) |
971 val cmd = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath) |
972 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) |
972 fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) |
973 fun readfn () = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE") |
973 fun readfn () = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE") |
974 val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () |
974 val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else () |
975 val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () |
975 val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else () |
976 val result = SatSolver.make_external_solver cmd writefn readfn fm |
976 val result = SatSolver.make_external_solver cmd writefn readfn fm |
977 val _ = try File.rm inpath |
977 val _ = try File.rm inpath |
978 val _ = try File.rm outpath |
978 val _ = try File.rm outpath |
979 in |
979 in |
980 result |
980 result |
981 end |
981 end |
982 in |
982 in |
983 SatSolver.add_solver ("jerusat", jerusat) |
983 SatSolver.add_solver ("jerusat", jerusat) |
984 end; |
984 end; |
985 |
985 |
986 (* ------------------------------------------------------------------------- *) |
986 (* ------------------------------------------------------------------------- *) |
987 (* Add code for other SAT solvers below. *) |
987 (* Add code for other SAT solvers below. *) |
988 (* ------------------------------------------------------------------------- *) |
988 (* ------------------------------------------------------------------------- *) |
989 |
989 |
990 (* |
990 (* |
991 let |
991 let |
992 fun mysolver fm = ... |
992 fun mysolver fm = ... |
993 in |
993 in |
994 SatSolver.add_solver ("myname", (fn fm => if mysolver_is_configured then mysolver fm else raise SatSolver.NOT_CONFIGURED)); -- register the solver |
994 SatSolver.add_solver ("myname", (fn fm => if mysolver_is_configured then mysolver fm else raise SatSolver.NOT_CONFIGURED)); -- register the solver |
995 end; |
995 end; |
996 |
996 |
997 -- the solver is now available as SatSolver.invoke_solver "myname" |
997 -- the solver is now available as SatSolver.invoke_solver "myname" |
998 *) |
998 *) |