author  webertj 
Sat, 02 Sep 2006 01:10:10 +0200  
changeset 20463  062c4e9bf3bb 
parent 20441  a9034285b96b 
child 21267  5294ecae6708 
permissions  rwrr 
14453  1 
(* Title: HOL/Tools/sat_solver.ML 
2 
ID: $Id$ 

3 
Author: Tjark Weber 

16911
20a139ca2f62
replaced calls to PropLogic.defcnf by PropLogic.auxcnf
webertj
parents:
16899
diff
changeset

4 
Copyright 20042005 
14453  5 

6 
Interface to external SAT solvers, and (simple) builtin SAT solvers. 

7 
*) 

8 

9 
signature SAT_SOLVER = 

10 
sig 

14965  11 
exception NOT_CONFIGURED 
14453  12 

14965  13 
type assignment = int > bool option 
17493
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

14 
type proof = int list Inttab.table * int 
14965  15 
datatype result = SATISFIABLE of assignment 
17493
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

16 
 UNSATISFIABLE of proof option 
14965  17 
 UNKNOWN 
18 
type solver = PropLogic.prop_formula > result 

19 

20 
(* auxiliary functions to create external SAT solvers *) 

14453  21 
val write_dimacs_cnf_file : Path.T > PropLogic.prop_formula > unit 
22 
val write_dimacs_sat_file : Path.T > PropLogic.prop_formula > unit 

17620
49568e5e0450
parse_std_result_file renamed to read_std_result_file
webertj
parents:
17581
diff
changeset

23 
val read_std_result_file : Path.T > string * string * string > result 
14965  24 
val make_external_solver : string > (PropLogic.prop_formula > unit) > (unit > result) > solver 
14453  25 

15040  26 
val read_dimacs_cnf_file : Path.T > PropLogic.prop_formula 
27 

16899
ee4d620bcc1c
write_dimacs_sat_file now generates slightly smaller files
webertj
parents:
16270
diff
changeset

28 
(* generic solver interface *) 
14487
157d0ea7b2da
Installed solvers now determined at call time (as opposed to compile time)
webertj
parents:
14460
diff
changeset

29 
val solvers : (string * solver) list ref 
157d0ea7b2da
Installed solvers now determined at call time (as opposed to compile time)
webertj
parents:
14460
diff
changeset

30 
val add_solver : string * solver > unit 
15605  31 
val invoke_solver : string > solver (* exception Option *) 
14453  32 
end; 
33 

34 
structure SatSolver : SAT_SOLVER = 

35 
struct 

36 

37 
open PropLogic; 

38 

39 
(*  *) 

14965  40 
(* should be raised by an external SAT solver to indicate that the solver is *) 
41 
(* not configured properly *) 

42 
(*  *) 

43 

44 
exception NOT_CONFIGURED; 

45 

46 
(*  *) 

15531  47 
(* type of partial (satisfying) assignments: 'a i = NONE' means that 'a' is *) 
19190  48 
(* a satisfying assignment regardless of the value of variable 'i' *) 
14453  49 
(*  *) 
50 

14965  51 
type assignment = int > bool option; 
52 

53 
(*  *) 

17493
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

54 
(* a proof of unsatisfiability, to be interpreted as follows: each integer *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

55 
(* is a clause ID, each list 'xs' stored under the key 'x' in the table *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

56 
(* contains the IDs of clauses that must be resolved (in the given *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

57 
(* order) to obtain the new clause 'x'. Each list 'xs' must be *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

58 
(* nonempty, and the literal to be resolved upon must always be unique *) 
17494  59 
(* (e.g. "A  ~B" must not be resolved with "~A  B"). Circular *) 
17493
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

60 
(* dependencies of clauses are not allowed. (At least) one of the *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

61 
(* clauses in the table must be the empty clause (i.e. contain no *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

62 
(* literals); its ID is given by the second component of the proof. *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

63 
(* The clauses of the original problem passed to the SAT solver have *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

64 
(* consecutive IDs starting with 0. Clause IDs must be nonnegative, *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

65 
(* but do not need to be consecutive. *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

66 
(*  *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

67 

cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

68 
type proof = int list Inttab.table * int; 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

69 

cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

70 
(*  *) 
14965  71 
(* return type of SAT solvers: if the result is 'SATISFIABLE', a satisfying *) 
17493
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

72 
(* assignment must be returned as well; if the result is *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

73 
(* 'UNSATISFIABLE', a proof of unsatisfiability may be returned *) 
14965  74 
(*  *) 
75 

76 
datatype result = SATISFIABLE of assignment 

17493
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

77 
 UNSATISFIABLE of proof option 
14965  78 
 UNKNOWN; 
79 

80 
(*  *) 

81 
(* type of SAT solvers: given a propositional formula, a satisfying *) 

82 
(* assignment may be returned *) 

83 
(*  *) 

84 

85 
type solver = prop_formula > result; 

14453  86 

87 
(*  *) 

88 
(* write_dimacs_cnf_file: serializes a formula 'fm' of propositional logic *) 

89 
(* to a file in DIMACS CNF format (see "Satisfiability Suggested *) 

90 
(* Format", May 8 1993, Section 2.1) *) 

91 
(* Note: 'fm' must not contain a variable index less than 1. *) 

14965  92 
(* Note: 'fm' must be given in CNF. *) 
14453  93 
(*  *) 
94 

95 
(* Path.T > prop_formula > unit *) 

96 

97 
fun write_dimacs_cnf_file path fm = 

98 
let 

99 
(* prop_formula > prop_formula *) 

100 
fun cnf_True_False_elim True = 

101 
Or (BoolVar 1, Not (BoolVar 1)) 

102 
 cnf_True_False_elim False = 

103 
And (BoolVar 1, Not (BoolVar 1)) 

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 *) 

106 
(* prop_formula > int *) 

107 
fun cnf_number_of_clauses (And (fm1,fm2)) = 

108 
(cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2) 

109 
 cnf_number_of_clauses _ = 

110 
1 

16915
bca4c3b1afca
write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
webertj
parents:
16914
diff
changeset

111 
(* prop_formula > string list *) 
14999
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

112 
fun cnf_string fm = 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

113 
let 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

114 
(* prop_formula > string list > string list *) 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

115 
fun cnf_string_acc True acc = 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

116 
error "formula is not in CNF" 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

117 
 cnf_string_acc False acc = 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

118 
error "formula is not in CNF" 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

119 
 cnf_string_acc (BoolVar i) acc = 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

120 
(assert (i>=1) "formula contains a variable index less than 1"; 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

121 
string_of_int i :: acc) 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

122 
 cnf_string_acc (Not (BoolVar i)) acc = 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

123 
"" :: cnf_string_acc (BoolVar i) acc 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

124 
 cnf_string_acc (Not _) acc = 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

125 
error "formula is not in CNF" 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

126 
 cnf_string_acc (Or (fm1,fm2)) acc = 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

127 
cnf_string_acc fm1 (" " :: cnf_string_acc fm2 acc) 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

128 
 cnf_string_acc (And (fm1,fm2)) acc = 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

129 
cnf_string_acc fm1 (" 0\n" :: cnf_string_acc fm2 acc) 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

130 
in 
16915
bca4c3b1afca
write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
webertj
parents:
16914
diff
changeset

131 
cnf_string_acc fm [] 
14999
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

132 
end 
16915
bca4c3b1afca
write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
webertj
parents:
16914
diff
changeset

133 
val fm' = cnf_True_False_elim fm 
bca4c3b1afca
write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
webertj
parents:
16914
diff
changeset

134 
val number_of_vars = maxidx fm' 
bca4c3b1afca
write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
webertj
parents:
16914
diff
changeset

135 
val number_of_clauses = cnf_number_of_clauses fm' 
14453  136 
in 
137 
File.write path 

16915
bca4c3b1afca
write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
webertj
parents:
16914
diff
changeset

138 
("c This file was generated by SatSolver.write_dimacs_cnf_file\n" ^ 
bca4c3b1afca
write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
webertj
parents:
16914
diff
changeset

139 
"p cnf " ^ string_of_int number_of_vars ^ " " ^ string_of_int number_of_clauses ^ "\n"); 
bca4c3b1afca
write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
webertj
parents:
16914
diff
changeset

140 
File.append_list path 
bca4c3b1afca
write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
webertj
parents:
16914
diff
changeset

141 
(cnf_string fm'); 
bca4c3b1afca
write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
webertj
parents:
16914
diff
changeset

142 
File.append path 
bca4c3b1afca
write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
webertj
parents:
16914
diff
changeset

143 
" 0\n" 
14453  144 
end; 
145 

146 
(*  *) 

147 
(* write_dimacs_sat_file: serializes a formula 'fm' of propositional logic *) 

148 
(* to a file in DIMACS SAT format (see "Satisfiability Suggested *) 

149 
(* Format", May 8 1993, Section 2.2) *) 

150 
(* Note: 'fm' must not contain a variable index less than 1. *) 

151 
(*  *) 

152 

153 
(* Path.T > prop_formula > unit *) 

154 

155 
fun write_dimacs_sat_file path fm = 

156 
let 

16915
bca4c3b1afca
write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
webertj
parents:
16914
diff
changeset

157 
(* prop_formula > string list *) 
14999
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

158 
fun sat_string fm = 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

159 
let 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

160 
(* prop_formula > string list > string list *) 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

161 
fun sat_string_acc True acc = 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

162 
"*()" :: acc 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

163 
 sat_string_acc False acc = 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

164 
"+()" :: acc 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

165 
 sat_string_acc (BoolVar i) acc = 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

166 
(assert (i>=1) "formula contains a variable index less than 1"; 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

167 
string_of_int i :: acc) 
16899
ee4d620bcc1c
write_dimacs_sat_file now generates slightly smaller files
webertj
parents:
16270
diff
changeset

168 
 sat_string_acc (Not (BoolVar i)) acc = 
ee4d620bcc1c
write_dimacs_sat_file now generates slightly smaller files
webertj
parents:
16270
diff
changeset

169 
"" :: sat_string_acc (BoolVar i) acc 
14999
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

170 
 sat_string_acc (Not fm) acc = 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

171 
"(" :: sat_string_acc fm (")" :: acc) 
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

172 
 sat_string_acc (Or (fm1,fm2)) acc = 
16899
ee4d620bcc1c
write_dimacs_sat_file now generates slightly smaller files
webertj
parents:
16270
diff
changeset

173 
"+(" :: sat_string_acc_or fm1 (" " :: sat_string_acc_or fm2 (")" :: acc)) 
14999
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

174 
 sat_string_acc (And (fm1,fm2)) acc = 
16899
ee4d620bcc1c
write_dimacs_sat_file now generates slightly smaller files
webertj
parents:
16270
diff
changeset

175 
"*(" :: sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 (")" :: acc)) 
ee4d620bcc1c
write_dimacs_sat_file now generates slightly smaller files
webertj
parents:
16270
diff
changeset

176 
(* optimization to make use of nary disjunction/conjunction *) 
ee4d620bcc1c
write_dimacs_sat_file now generates slightly smaller files
webertj
parents:
16270
diff
changeset

177 
(* prop_formula > string list > string list *) 
ee4d620bcc1c
write_dimacs_sat_file now generates slightly smaller files
webertj
parents:
16270
diff
changeset

178 
and sat_string_acc_or (Or (fm1,fm2)) acc = 
ee4d620bcc1c
write_dimacs_sat_file now generates slightly smaller files
webertj
parents:
16270
diff
changeset

179 
sat_string_acc_or fm1 (" " :: sat_string_acc_or fm2 acc) 
ee4d620bcc1c
write_dimacs_sat_file now generates slightly smaller files
webertj
parents:
16270
diff
changeset

180 
 sat_string_acc_or fm acc = 
ee4d620bcc1c
write_dimacs_sat_file now generates slightly smaller files
webertj
parents:
16270
diff
changeset

181 
sat_string_acc fm acc 
ee4d620bcc1c
write_dimacs_sat_file now generates slightly smaller files
webertj
parents:
16270
diff
changeset

182 
(* prop_formula > string list > string list *) 
ee4d620bcc1c
write_dimacs_sat_file now generates slightly smaller files
webertj
parents:
16270
diff
changeset

183 
and sat_string_acc_and (And (fm1,fm2)) acc = 
ee4d620bcc1c
write_dimacs_sat_file now generates slightly smaller files
webertj
parents:
16270
diff
changeset

184 
sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 acc) 
ee4d620bcc1c
write_dimacs_sat_file now generates slightly smaller files
webertj
parents:
16270
diff
changeset

185 
 sat_string_acc_and fm acc = 
ee4d620bcc1c
write_dimacs_sat_file now generates slightly smaller files
webertj
parents:
16270
diff
changeset

186 
sat_string_acc fm acc 
14999
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

187 
in 
16915
bca4c3b1afca
write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
webertj
parents:
16914
diff
changeset

188 
sat_string_acc fm [] 
14999
2c39efba8f67
faster conversion into DIMACS CNF and DIMACS SAT format
webertj
parents:
14965
diff
changeset

189 
end 
16915
bca4c3b1afca
write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
webertj
parents:
16914
diff
changeset

190 
val number_of_vars = Int.max (maxidx fm, 1) 
14453  191 
in 
192 
File.write path 

16915
bca4c3b1afca
write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
webertj
parents:
16914
diff
changeset

193 
("c This file was generated by SatSolver.write_dimacs_sat_file\n" ^ 
bca4c3b1afca
write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
webertj
parents:
16914
diff
changeset

194 
"p sat " ^ string_of_int number_of_vars ^ "\n" ^ 
bca4c3b1afca
write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
webertj
parents:
16914
diff
changeset

195 
"("); 
bca4c3b1afca
write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
webertj
parents:
16914
diff
changeset

196 
File.append_list path 
bca4c3b1afca
write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
webertj
parents:
16914
diff
changeset

197 
(sat_string fm); 
bca4c3b1afca
write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
webertj
parents:
16914
diff
changeset

198 
File.append path 
bca4c3b1afca
write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
webertj
parents:
16914
diff
changeset

199 
")\n" 
14453  200 
end; 
201 

202 
(*  *) 

17620
49568e5e0450
parse_std_result_file renamed to read_std_result_file
webertj
parents:
17581
diff
changeset

203 
(* read_std_result_file: scans a SAT solver's output file for a satisfying *) 
14965  204 
(* variable assignment. Returns the assignment, or 'UNSATISFIABLE' if *) 
205 
(* the file contains 'unsatisfiable', or 'UNKNOWN' if the file contains *) 

206 
(* neither 'satisfiable' nor 'unsatisfiable'. Empty lines are ignored. *) 

207 
(* The assignment must be given in one or more lines immediately after *) 

208 
(* the line that contains 'satisfiable'. These lines must begin with *) 

209 
(* 'assignment_prefix'. Variables must be separated by " ". Non *) 

210 
(* integer strings are ignored. If variable i is contained in the *) 

211 
(* assignment, then i is interpreted as 'true'. If ~i is contained in *) 

212 
(* the assignment, then i is interpreted as 'false'. Otherwise the *) 

213 
(* value of i is taken to be unspecified. *) 

14453  214 
(*  *) 
215 

14965  216 
(* Path.T > string * string * string > result *) 
14453  217 

17620
49568e5e0450
parse_std_result_file renamed to read_std_result_file
webertj
parents:
17581
diff
changeset

218 
fun read_std_result_file path (satisfiable, assignment_prefix, unsatisfiable) = 
14453  219 
let 
220 
(* string > int list *) 

221 
fun int_list_from_string s = 

15605  222 
List.mapPartial Int.fromString (space_explode " " s) 
14965  223 
(* int list > assignment *) 
14453  224 
fun assignment_from_list [] i = 
15531  225 
NONE (* the SAT solver didn't provide a value for this variable *) 
14453  226 
 assignment_from_list (x::xs) i = 
15531  227 
if x=i then (SOME true) 
228 
else if x=(~i) then (SOME false) 

14453  229 
else assignment_from_list xs i 
14965  230 
(* int list > string list > assignment *) 
231 
fun parse_assignment xs [] = 

232 
assignment_from_list xs 

233 
 parse_assignment xs (line::lines) = 

234 
if String.isPrefix assignment_prefix line then 

235 
parse_assignment (xs @ int_list_from_string line) lines 

236 
else 

237 
assignment_from_list xs 

14453  238 
(* string > string > bool *) 
239 
fun is_substring needle haystack = 

240 
let 

241 
val length1 = String.size needle 

242 
val length2 = String.size haystack 

243 
in 

244 
if length2 < length1 then 

245 
false 

246 
else if needle = String.substring (haystack, 0, length1) then 

247 
true 

248 
else is_substring needle (String.substring (haystack, 1, length21)) 

249 
end 

14965  250 
(* string list > result *) 
14453  251 
fun parse_lines [] = 
14965  252 
UNKNOWN 
14453  253 
 parse_lines (line::lines) = 
20033  254 
if is_substring unsatisfiable line then 
255 
UNSATISFIABLE NONE 

256 
else if is_substring satisfiable line then 

14965  257 
SATISFIABLE (parse_assignment [] lines) 
14453  258 
else 
259 
parse_lines lines 

260 
in 

15570  261 
(parse_lines o (List.filter (fn l => l <> "")) o split_lines o File.read) path 
14453  262 
end; 
263 

264 
(*  *) 

265 
(* make_external_solver: call 'writefn', execute 'cmd', call 'readfn' *) 

266 
(*  *) 

267 

14965  268 
(* string > (PropLogic.prop_formula > unit) > (unit > result) > solver *) 
14453  269 

270 
fun make_external_solver cmd writefn readfn fm = 

14965  271 
(writefn fm; system cmd; readfn ()); 
14453  272 

273 
(*  *) 

15040  274 
(* read_dimacs_cnf_file: returns a propositional formula that corresponds to *) 
275 
(* a SAT problem given in DIMACS CNF format *) 

276 
(*  *) 

277 

278 
(* Path.T > PropLogic.prop_formula *) 

279 

280 
fun read_dimacs_cnf_file path = 

281 
let 

282 
(* string list > string list *) 

283 
fun filter_preamble [] = 

284 
error "problem line not found in DIMACS CNF file" 

285 
 filter_preamble (line::lines) = 

20441  286 
if String.isPrefix "c " line orelse line = "c" then 
15040  287 
(* ignore comments *) 
288 
filter_preamble lines 

289 
else if String.isPrefix "p " line then 

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 *) 

292 
(* or variables than specified in its preamble, we will accept it anyway. *) 

293 
lines 

294 
else 

295 
error "preamble in DIMACS CNF file contains a line that does not begin with \"c \" or \"p \"" 

296 
(* string > int *) 

297 
fun int_from_string s = 

298 
case Int.fromString s of 

299 
SOME i => i 

300 
 NONE => error ("token " ^ quote s ^ "in DIMACS CNF file is not a number") 

301 
(* int list > int list list *) 

302 
fun clauses xs = 

303 
let 

304 
val (xs1, xs2) = take_prefix (fn i => i <> 0) xs 

305 
in 

15128  306 
case xs2 of 
307 
[] => [xs1] 

308 
 (0::[]) => [xs1] 

309 
 (0::tl) => xs1 :: clauses tl 

18678  310 
 _ => sys_error "this cannot happen" 
15040  311 
end 
312 
(* int > PropLogic.prop_formula *) 

313 
fun literal_from_int i = 

314 
(assert (i<>0) "variable index in DIMACS CNF file is 0"; 

315 
if i>0 then 

316 
PropLogic.BoolVar i 

317 
else 

318 
PropLogic.Not (PropLogic.BoolVar (~i))) 

319 
(* PropLogic.prop_formula list > PropLogic.prop_formula *) 

320 
fun disjunction [] = 

321 
error "empty clause in DIMACS CNF file" 

322 
 disjunction (x::xs) = 

323 
(case xs of 

324 
[] => x 

325 
 _ => PropLogic.Or (x, disjunction xs)) 

326 
(* PropLogic.prop_formula list > PropLogic.prop_formula *) 

327 
fun conjunction [] = 

328 
error "no clause in DIMACS CNF file" 

329 
 conjunction (x::xs) = 

330 
(case xs of 

331 
[] => x 

332 
 _ => PropLogic.And (x, conjunction xs)) 

333 
in 

334 
(conjunction 

335 
o (map disjunction) 

336 
o (map (map literal_from_int)) 

337 
o clauses 

338 
o (map int_from_string) 

15570  339 
o List.concat 
15040  340 
o (map (String.fields (fn c => c mem [#" ", #"\t", #"\n"]))) 
341 
o filter_preamble 

15570  342 
o (List.filter (fn l => l <> "")) 
15040  343 
o split_lines 
344 
o File.read) 

345 
path 

346 
end; 

347 

348 
(*  *) 

14453  349 
(* solvers: a (reference to a) table of all registered SAT solvers *) 
350 
(*  *) 

351 

14487
157d0ea7b2da
Installed solvers now determined at call time (as opposed to compile time)
webertj
parents:
14460
diff
changeset

352 
val solvers = ref ([] : (string * solver) list); 
14453  353 

354 
(*  *) 

355 
(* add_solver: updates 'solvers' by adding a new solver *) 

356 
(*  *) 

357 

358 
(* string * solver > unit *) 

359 

360 
fun add_solver (name, new_solver) = 

17541  361 
(solvers := update_warn (op =) ("SAT solver " ^ quote name ^ " was defined before") (name, new_solver) (!solvers)); 
14453  362 

363 
(*  *) 

364 
(* invoke_solver: returns the solver associated with the given 'name' *) 

15605  365 
(* Note: If no solver is associated with 'name', exception 'Option' will be *) 
14453  366 
(* raised. *) 
367 
(*  *) 

368 

369 
(* string > solver *) 

370 

371 
fun invoke_solver name = 

17541  372 
(the o AList.lookup (op =) (!solvers)) name; 
14453  373 

374 
end; (* SatSolver *) 

375 

376 

377 
(*  *) 

378 
(* Predefined SAT solvers *) 

379 
(*  *) 

380 

381 
(*  *) 

14753  382 
(* Internal SAT solver, available as 'SatSolver.invoke_solver "enumerate"' *) 
383 
(*  simply enumerates assignments until a satisfying assignment is found *) 

14453  384 
(*  *) 
385 

386 
let 

387 
fun enum_solver fm = 

388 
let 

389 
(* int list *) 

390 
val indices = PropLogic.indices fm 

391 
(* int list > int list > int list option *) 

392 
(* binary increment: list 'xs' of current bits, list 'ys' of all bits (lower bits first) *) 

393 
fun next_list _ ([]:int list) = 

15531  394 
NONE 
14453  395 
 next_list [] (y::ys) = 
15531  396 
SOME [y] 
14453  397 
 next_list (x::xs) (y::ys) = 
398 
if x=y then 

399 
(* reset the bit, continue *) 

400 
next_list xs ys 

401 
else 

402 
(* set the lowest bit that wasn't set before, keep the higher bits *) 

15531  403 
SOME (y::x::xs) 
14453  404 
(* int list > int > bool *) 
405 
fun assignment_from_list xs i = 

406 
i mem xs 

14965  407 
(* int list > SatSolver.result *) 
14453  408 
fun solver_loop xs = 
409 
if PropLogic.eval (assignment_from_list xs) fm then 

15531  410 
SatSolver.SATISFIABLE (SOME o (assignment_from_list xs)) 
14453  411 
else 
412 
(case next_list xs indices of 

15531  413 
SOME xs' => solver_loop xs' 
17493
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

414 
 NONE => SatSolver.UNSATISFIABLE NONE) 
14453  415 
in 
14965  416 
(* start with the "first" assignment (all variables are interpreted as 'false') *) 
14453  417 
solver_loop [] 
418 
end 

419 
in 

14965  420 
SatSolver.add_solver ("enumerate", enum_solver) 
14453  421 
end; 
422 

423 
(*  *) 

14753  424 
(* Internal SAT solver, available as 'SatSolver.invoke_solver "dpll"'  a *) 
425 
(* simple implementation of the DPLL algorithm (cf. L. Zhang, S. Malik: "The *) 

426 
(* Quest for Efficient Boolean Satisfiability Solvers", July 2002, Fig. 1). *) 

14453  427 
(*  *) 
428 

429 
let 

430 
local 

431 
open PropLogic 

432 
in 

433 
fun dpll_solver fm = 

434 
let 

16914
e68528b4fc0b
replaced calls to PropLogic.auxcnf by PropLogic.defcnf again
webertj
parents:
16912
diff
changeset

435 
(* We could use 'PropLogic.defcnf fm' instead of 'PropLogic.nnf fm' *) 
17493
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

436 
(* but that sometimes leads to worse performance due to the *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

437 
(* introduction of additional variables. *) 
14514  438 
val fm' = PropLogic.nnf fm 
14453  439 
(* int list *) 
14514  440 
val indices = PropLogic.indices fm' 
14453  441 
(* int list > int > prop_formula *) 
442 
fun partial_var_eval [] i = BoolVar i 

443 
 partial_var_eval (x::xs) i = if x=i then True else if x=(~i) then False else partial_var_eval xs i 

444 
(* int list > prop_formula > prop_formula *) 

445 
fun partial_eval xs True = True 

446 
 partial_eval xs False = False 

447 
 partial_eval xs (BoolVar i) = partial_var_eval xs i 

448 
 partial_eval xs (Not fm) = SNot (partial_eval xs fm) 

449 
 partial_eval xs (Or (fm1, fm2)) = SOr (partial_eval xs fm1, partial_eval xs fm2) 

450 
 partial_eval xs (And (fm1, fm2)) = SAnd (partial_eval xs fm1, partial_eval xs fm2) 

451 
(* prop_formula > int list *) 

452 
fun forced_vars True = [] 

453 
 forced_vars False = [] 

454 
 forced_vars (BoolVar i) = [i] 

455 
 forced_vars (Not (BoolVar i)) = [~i] 

456 
 forced_vars (Or (fm1, fm2)) = (forced_vars fm1) inter_int (forced_vars fm2) 

457 
 forced_vars (And (fm1, fm2)) = (forced_vars fm1) union_int (forced_vars fm2) 

458 
(* Above, i *and* ~i may be forced. In this case the first occurrence takes *) 

459 
(* precedence, and the next partial evaluation of the formula returns 'False'. *) 

18678  460 
 forced_vars _ = error "formula is not in negation normal form" 
14453  461 
(* int list > prop_formula > (int list * prop_formula) *) 
462 
fun eval_and_force xs fm = 

463 
let 

464 
val fm' = partial_eval xs fm 

465 
val xs' = forced_vars fm' 

466 
in 

467 
if null xs' then 

468 
(xs, fm') 

469 
else 

470 
eval_and_force (xs@xs') fm' (* xs and xs' should be distinct, so '@' here should have *) 

471 
(* the same effect as 'union_int' *) 

472 
end 

473 
(* int list > int option *) 

474 
fun fresh_var xs = 

475 
Library.find_first (fn i => not (i mem_int xs) andalso not ((~i) mem_int xs)) indices 

476 
(* int list > prop_formula > int list option *) 

477 
(* partial assignment 'xs' *) 

478 
fun dpll xs fm = 

479 
let 

480 
val (xs', fm') = eval_and_force xs fm 

481 
in 

482 
case fm' of 

15531  483 
True => SOME xs' 
484 
 False => NONE 

14453  485 
 _ => 
486 
let 

15570  487 
val x = valOf (fresh_var xs') (* a fresh variable must exist since 'fm' did not evaluate to 'True'/'False' *) 
14453  488 
in 
489 
case dpll (x::xs') fm' of (* passing fm' rather than fm should save some simplification work *) 

15531  490 
SOME xs'' => SOME xs'' 
491 
 NONE => dpll ((~x)::xs') fm' (* now try interpreting 'x' as 'False' *) 

14453  492 
end 
493 
end 

14965  494 
(* int list > assignment *) 
14453  495 
fun assignment_from_list [] i = 
15531  496 
NONE (* the DPLL procedure didn't provide a value for this variable *) 
14453  497 
 assignment_from_list (x::xs) i = 
15531  498 
if x=i then (SOME true) 
499 
else if x=(~i) then (SOME false) 

14453  500 
else assignment_from_list xs i 
501 
in 

502 
(* initially, no variable is interpreted yet *) 

14965  503 
case dpll [] fm' of 
15531  504 
SOME assignment => SatSolver.SATISFIABLE (assignment_from_list assignment) 
17493
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

505 
 NONE => SatSolver.UNSATISFIABLE NONE 
14453  506 
end 
507 
end (* local *) 

508 
in 

14965  509 
SatSolver.add_solver ("dpll", dpll_solver) 
14453  510 
end; 
511 

512 
(*  *) 

14753  513 
(* Internal SAT solver, available as 'SatSolver.invoke_solver "auto"': uses *) 
17577
e87bf1d8f17a
zchaff_with_proofs does not delete zChaff\s resolve_trace file anymore
webertj
parents:
17541
diff
changeset

514 
(* the last installed solver (other than "auto" itself) that does not raise *) 
15299
576fd0b65ed8
solver auto now returns the result of the first solver that does not raise NOT_CONFIGURED (which may be UNKNOWN)
webertj
parents:
15128
diff
changeset

515 
(* 'NOT_CONFIGURED'. (However, the solver may return 'UNKNOWN'.) *) 
14453  516 
(*  *) 
517 

518 
let 

519 
fun auto_solver fm = 

14965  520 
let 
521 
fun loop [] = 

522 
SatSolver.UNKNOWN 

523 
 loop ((name, solver)::solvers) = 

14487
157d0ea7b2da
Installed solvers now determined at call time (as opposed to compile time)
webertj
parents:
14460
diff
changeset

524 
if name="auto" then 
14965  525 
(* do not call solver "auto" from within "auto" *) 
526 
loop solvers 

15299
576fd0b65ed8
solver auto now returns the result of the first solver that does not raise NOT_CONFIGURED (which may be UNKNOWN)
webertj
parents:
15128
diff
changeset

527 
else ( 
14965  528 
(if name="dpll" orelse name="enumerate" then 
14805
eff7b9df27e9
solver "auto" now issues a warning when it uses solver "enumerate"
webertj
parents:
14753
diff
changeset

529 
warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.") 
14487
157d0ea7b2da
Installed solvers now determined at call time (as opposed to compile time)
webertj
parents:
14460
diff
changeset

530 
else 
20135  531 
tracing ("Using SAT solver " ^ quote name ^ ".")); 
14965  532 
(* apply 'solver' to 'fm' *) 
15299
576fd0b65ed8
solver auto now returns the result of the first solver that does not raise NOT_CONFIGURED (which may be UNKNOWN)
webertj
parents:
15128
diff
changeset

533 
solver fm 
576fd0b65ed8
solver auto now returns the result of the first solver that does not raise NOT_CONFIGURED (which may be UNKNOWN)
webertj
parents:
15128
diff
changeset

534 
handle SatSolver.NOT_CONFIGURED => loop solvers 
14965  535 
) 
536 
in 

17581
a50a53081808
solver "auto" does not reverse the list of solvers anymore
webertj
parents:
17577
diff
changeset

537 
loop (!SatSolver.solvers) 
14965  538 
end 
14453  539 
in 
540 
SatSolver.add_solver ("auto", auto_solver) 

541 
end; 

542 

543 
(*  *) 

20033  544 
(* MiniSat 1.14 *) 
545 
(* (http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/) *) 

546 
(*  *) 

547 

20135  548 
(*  *) 
549 
(* "minisat_with_proofs" requires a modified version of MiniSat 1.14 by John *) 

550 
(* Matthews, which can output ASCII proof traces. Replaying binary proof *) 

551 
(* traces generated by MiniSatp_v1.14 has _not_ been implemented. *) 

552 
(*  *) 

553 

554 
(* add "minisat_with_proofs" _before_ "minisat" to the available solvers, so *) 

555 
(* that the latter is preferred by the "auto" solver *) 

556 

20152
b6373fe199e1
MiniSat proof trace format changed; MiniSat is now expected to produce a proof also for "trivial" problems
webertj
parents:
20137
diff
changeset

557 
(* There is a complication that is dealt with in the code below: MiniSat *) 
b6373fe199e1
MiniSat proof trace format changed; MiniSat is now expected to produce a proof also for "trivial" problems
webertj
parents:
20137
diff
changeset

558 
(* introduces IDs for original clauses in the proof trace. It does not (in *) 
b6373fe199e1
MiniSat proof trace format changed; MiniSat is now expected to produce a proof also for "trivial" problems
webertj
parents:
20137
diff
changeset

559 
(* general) follow the convention that the original clauses are numbered *) 
b6373fe199e1
MiniSat proof trace format changed; MiniSat is now expected to produce a proof also for "trivial" problems
webertj
parents:
20137
diff
changeset

560 
(* from 0 to n1 (where n is the number of clauses in the formula). *) 
20135  561 

562 
let 

563 
exception INVALID_PROOF of string 

564 
fun minisat_with_proofs fm = 

565 
let 

566 
val _ = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () 

567 
val inpath = File.tmp_path (Path.unpack "isabelle.cnf") 

568 
val outpath = File.tmp_path (Path.unpack "result") 

569 
val proofpath = File.tmp_path (Path.unpack "result.prf") 

570 
val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.pack inpath) ^ " r " ^ (Path.pack outpath) ^ " t " ^ (Path.pack proofpath) ^ "> /dev/null" 

571 
fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm 

572 
fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT") 

573 
val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else () 

574 
val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else () 

575 
val cnf = PropLogic.defcnf fm 

576 
val result = SatSolver.make_external_solver cmd writefn readfn cnf 

577 
val _ = try File.rm inpath 

578 
val _ = try File.rm outpath 

579 
in case result of 

580 
SatSolver.UNSATISFIABLE NONE => 

581 
(let 

20152
b6373fe199e1
MiniSat proof trace format changed; MiniSat is now expected to produce a proof also for "trivial" problems
webertj
parents:
20137
diff
changeset

582 
(* string list *) 
b6373fe199e1
MiniSat proof trace format changed; MiniSat is now expected to produce a proof also for "trivial" problems
webertj
parents:
20137
diff
changeset

583 
val proof_lines = ((split_lines o File.read) proofpath) 
b6373fe199e1
MiniSat proof trace format changed; MiniSat is now expected to produce a proof also for "trivial" problems
webertj
parents:
20137
diff
changeset

584 
handle IO.Io _ => raise INVALID_PROOF "Could not read file \"result.prf\"" 
20135  585 
(* a simple representation of the CNF formula as list of clauses (paired with their ID), *) 
586 
(* where each clause is a sorted list of literals, where each literal is an int *) 

587 
(* removes duplicates from an ordered list *) 

588 
(* int list > int list *) 

589 
fun remove_dups [] = [] 

590 
 remove_dups [x] = [x] 

591 
 remove_dups (x :: y :: xs) = if x = y then remove_dups (y :: xs) else x :: remove_dups (y :: xs) 

592 
(* prop_formula > int list *) 

593 
fun clause_to_lit_list (PropLogic.Or (fm1, fm2)) = clause_to_lit_list fm1 @ clause_to_lit_list fm2 

594 
 clause_to_lit_list (PropLogic.BoolVar i) = [i] 

595 
 clause_to_lit_list (PropLogic.Not (PropLogic.BoolVar i)) = [~i] 

596 
 clause_to_lit_list _ = raise INVALID_PROOF "Error: invalid clause in CNF formula." 

597 
(* prop_formula > int list list *) 

598 
fun cnf_to_clause_list (PropLogic.And (fm1, fm2)) = cnf_to_clause_list fm1 @ cnf_to_clause_list fm2 

599 
 cnf_to_clause_list fm = [(remove_dups o sort int_ord o clause_to_lit_list) fm] 

600 
(* (int list * int) list * int *) 

601 
val (clauses, length_clauses) = fold_map (fn clause => fn n => ((clause, n), n+1)) (cnf_to_clause_list cnf) 0 

602 
(* string > int *) 

603 
fun int_from_string s = ( 

604 
case Int.fromString s of 

605 
SOME i => i 

606 
 NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).") 

607 
) 

608 
(* parse the proof file *) 

609 
(* contains a mapping from clause IDs as used by MiniSat to clause IDs in *) 

610 
(* our proof format, where original clauses are numbered starting from 0 *) 

611 
val clause_id_map = ref (Inttab.empty : int Inttab.table) 

612 
fun sat_to_proof id = ( 

613 
case Inttab.lookup (!clause_id_map) id of 

614 
SOME id' => id' 

615 
 NONE => raise INVALID_PROOF ("Clause ID " ^ Int.toString id ^ " used, but not defined.") 

616 
) 

617 
val next_id = ref (length_clauses  1) 

618 
(* string list > proof > proof *) 

619 
fun process_tokens [] proof = 

620 
proof 

621 
 process_tokens (tok::toks) (clause_table, empty_id) = 

622 
if tok="R" then ( 

623 
case toks of 

624 
id::sep::lits => 

625 
let 

626 
val _ = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"R\" disallowed after \"X\"." 

627 
val cid = int_from_string id 

628 
val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).") 

20152
b6373fe199e1
MiniSat proof trace format changed; MiniSat is now expected to produce a proof also for "trivial" problems
webertj
parents:
20137
diff
changeset

629 
val ls = sort int_ord (map int_from_string lits) 
20135  630 
val proof_id = (* both 'ls' and the list of literals used as key in 'clauses' are sorted, *) 
631 
(* so testing for equality should suffice  barring duplicate literals *) 

632 
case AList.lookup (op =) clauses ls of 

633 
SOME orig_id => orig_id 

634 
 NONE => raise INVALID_PROOF ("Original clause (new ID is " ^ id ^ ") not found.") 

635 
(* extend the mapping of clause IDs with this newly defined ID *) 

636 
val _ = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map) 

637 
handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"R\").") 

638 
in 

639 
(* the proof itself doesn't change *) 

640 
(clause_table, empty_id) 

641 
end 

642 
 _ => 

643 
raise INVALID_PROOF "File format error: \"R\" followed by an insufficient number of tokens." 

644 
) else if tok="C" then ( 

645 
case toks of 

646 
id::sep::ids => 

647 
let 

648 
val _ = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"C\" disallowed after \"X\"." 

649 
val cid = int_from_string id 

650 
val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).") 

651 
(* ignore the pivot literals in MiniSat's trace *) 

652 
fun unevens [] = raise INVALID_PROOF "File format error: \"C\" followed by an even number of IDs." 

653 
 unevens (x :: []) = x :: [] 

654 
 unevens (x :: _ :: xs) = x :: unevens xs 

20152
b6373fe199e1
MiniSat proof trace format changed; MiniSat is now expected to produce a proof also for "trivial" problems
webertj
parents:
20137
diff
changeset

655 
val rs = (map sat_to_proof o unevens o map int_from_string) ids 
20135  656 
(* extend the mapping of clause IDs with this newly defined ID *) 
657 
val proof_id = inc next_id 

658 
val _ = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map) 

659 
handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"C\").") 

660 
in 

661 
(* update clause table *) 

662 
(Inttab.update_new (proof_id, rs) clause_table, empty_id) 

663 
handle Inttab.DUP _ => raise INVALID_PROOF ("Error: internal ID for clause " ^ id ^ " already used.") 

664 
end 

665 
 _ => 

666 
raise INVALID_PROOF "File format error: \"C\" followed by an insufficient number of tokens." 

667 
) else if tok="D" then ( 

668 
case toks of 

669 
[id] => 

670 
let 

671 
val _ = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"D\" disallowed after \"X\"." 

672 
val _ = sat_to_proof (int_from_string id) 

673 
in 

674 
(* simply ignore "D" *) 

675 
(clause_table, empty_id) 

676 
end 

677 
 _ => 

678 
raise INVALID_PROOF "File format error: \"D\" followed by an illegal number of tokens." 

679 
) else if tok="X" then ( 

680 
case toks of 

681 
[id1, id2] => 

682 
let 

683 
val _ = if empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one endofproof statement." 

684 
val _ = sat_to_proof (int_from_string id1) 

685 
val new_empty_id = sat_to_proof (int_from_string id2) 

686 
in 

687 
(* update conflict id *) 

688 
(clause_table, new_empty_id) 

689 
end 

690 
 _ => 

691 
raise INVALID_PROOF "File format error: \"X\" followed by an illegal number of tokens." 

692 
) else 

693 
raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.") 

694 
(* string list > proof > proof *) 

695 
fun process_lines [] proof = 

696 
proof 

697 
 process_lines (l::ls) proof = 

698 
process_lines ls (process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l) proof) 

699 
(* proof *) 

700 
val (clause_table, empty_id) = process_lines proof_lines (Inttab.empty, ~1) 

701 
val _ = if empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified." 

702 
in 

703 
SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) 

20152
b6373fe199e1
MiniSat proof trace format changed; MiniSat is now expected to produce a proof also for "trivial" problems
webertj
parents:
20137
diff
changeset

704 
end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE)) 
20135  705 
 result => 
706 
result 

707 
end 

708 
in 

709 
SatSolver.add_solver ("minisat_with_proofs", minisat_with_proofs) 

710 
end; 

711 

20033  712 
let 
713 
fun minisat fm = 

714 
let 

715 
val _ = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () 

716 
val inpath = File.tmp_path (Path.unpack "isabelle.cnf") 

717 
val outpath = File.tmp_path (Path.unpack "result") 

718 
val cmd = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.pack inpath) ^ " r " ^ (Path.pack outpath) ^ " > /dev/null" 

719 
fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) 

720 
fun readfn () = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT") 

721 
val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else () 

722 
val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else () 

723 
val result = SatSolver.make_external_solver cmd writefn readfn fm 

724 
val _ = try File.rm inpath 

725 
val _ = try File.rm outpath 

726 
in 

727 
result 

728 
end 

729 
in 

730 
SatSolver.add_solver ("minisat", minisat) 

731 
end; 

732 

733 
(*  *) 

15332  734 
(* zChaff (http://www.princeton.edu/~chaff/zchaff.html) *) 
14453  735 
(*  *) 
736 

17493
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

737 
(*  *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

738 
(* 'zchaff_with_proofs' applies the "zchaff" prover to a formula, and if *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

739 
(* zChaff finds that the formula is unsatisfiable, a proof of this is read *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

740 
(* from a file "resolve_trace" that was generated by zChaff. See the code *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

741 
(* below for the expected format of the "resolve_trace" file. Aside from *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

742 
(* some basic syntactic checks, no verification of the proof is performed. *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

743 
(*  *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

744 

cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

745 
(* add "zchaff_with_proofs" _before_ "zchaff" to the available solvers, so *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

746 
(* that the latter is preferred by the "auto" solver *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

747 

cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

748 
let 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

749 
exception INVALID_PROOF of string 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

750 
fun zchaff_with_proofs fm = 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

751 
case SatSolver.invoke_solver "zchaff" fm of 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

752 
SatSolver.UNSATISFIABLE NONE => 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

753 
(let 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

754 
(* string list *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

755 
val proof_lines = ((split_lines o File.read) (Path.unpack "resolve_trace")) 
20135  756 
handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\"" 
17493
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

757 
(* PropLogic.prop_formula > int *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

758 
fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

759 
 cnf_number_of_clauses _ = 1 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

760 
(* string > int *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

761 
fun int_from_string s = ( 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

762 
case Int.fromString s of 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

763 
SOME i => i 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

764 
 NONE => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).") 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

765 
) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

766 
(* parse the "resolve_trace" file *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

767 
val clause_offset = ref ~1 
20463  768 
val clause_table = ref (Inttab.empty : int list Inttab.table) 
769 
val empty_id = ref ~1 

770 
(* string list > unit *) 

771 
fun process_tokens [] = 

772 
() 

773 
 process_tokens (tok::toks) = 

17493
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

774 
if tok="CL:" then ( 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

775 
case toks of 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

776 
id::sep::ids => 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

777 
let 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

778 
val _ = if !clause_offset = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"VAR:\".") 
20463  779 
val _ = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"CONF:\".") 
17493
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

780 
val cid = int_from_string id 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

781 
val _ = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).") 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

782 
val rs = map int_from_string ids 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

783 
in 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

784 
(* update clause table *) 
20463  785 
clause_table := Inttab.update_new (cid, rs) (!clause_table) 
17493
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

786 
handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once.") 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

787 
end 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

788 
 _ => 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

789 
raise INVALID_PROOF "File format error: \"CL:\" followed by an insufficient number of tokens." 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

790 
) else if tok="VAR:" then ( 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

791 
case toks of 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

792 
id::levsep::levid::valsep::valid::antesep::anteid::litsep::lits => 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

793 
let 
20463  794 
val _ = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"VAR:\" disallowed after \"CONF:\".") 
17493
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

795 
(* set 'clause_offset' to the largest used clause ID *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

796 
val _ = if !clause_offset = ~1 then clause_offset := 
20463  797 
(case Inttab.max_key (!clause_table) of 
17493
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

798 
SOME id => id 
17527  799 
 NONE => cnf_number_of_clauses (PropLogic.defcnf fm)  1 (* the first clause ID is 0, not 1 *)) 
17493
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

800 
else 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

801 
() 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

802 
val vid = int_from_string id 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

803 
val _ = if levsep = "L:" then () else raise INVALID_PROOF ("File format error: \"L:\" expected (" ^ quote levsep ^ " encountered).") 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

804 
val _ = int_from_string levid 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

805 
val _ = if valsep = "V:" then () else raise INVALID_PROOF ("File format error: \"V:\" expected (" ^ quote valsep ^ " encountered).") 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

806 
val _ = int_from_string valid 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

807 
val _ = if antesep = "A:" then () else raise INVALID_PROOF ("File format error: \"A:\" expected (" ^ quote antesep ^ " encountered).") 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

808 
val aid = int_from_string anteid 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

809 
val _ = if litsep = "Lits:" then () else raise INVALID_PROOF ("File format error: \"Lits:\" expected (" ^ quote litsep ^ " encountered).") 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

810 
val ls = map int_from_string lits 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

811 
(* convert the data provided by zChaff to our resolutionstyle proof format *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

812 
(* each "VAR:" line defines a unit clause, the resolvents are implicitly *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

813 
(* given by the literals in the antecedent clause *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

814 
(* we use the sum of '!clause_offset' and the variable ID as clause ID for the unit clause *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

815 
val cid = !clause_offset + vid 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

816 
(* the low bit of each literal gives its sign (positive/negative), therefore *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

817 
(* we have to divide each literal by 2 to obtain the proper variable ID; then *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

818 
(* we add '!clause_offset' to obtain the ID of the corresponding unit clause *) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

819 
val vids = filter (not_equal vid) (map (fn l => l div 2) ls) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

820 
val rs = aid :: map (fn v => !clause_offset + v) vids 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

821 
in 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

822 
(* update clause table *) 
20463  823 
clause_table := Inttab.update_new (cid, rs) (!clause_table) 
17527  824 
handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int cid ^ " (derived from antecedent for variable " ^ id ^ ") already defined.") 
17493
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

825 
end 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

826 
 _ => 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

827 
raise INVALID_PROOF "File format error: \"VAR:\" followed by an insufficient number of tokens." 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

828 
) else if tok="CONF:" then ( 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

829 
case toks of 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

830 
id::sep::ids => 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

831 
let 
20463  832 
val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one conflicting clause specified." 
17493
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

833 
val cid = int_from_string id 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

834 
val _ = if sep = "==" then () else raise INVALID_PROOF ("File format error: \"==\" expected (" ^ quote sep ^ " encountered).") 
17527  835 
val ls = map int_from_string ids 
836 
(* the conflict clause must be resolved with the unit clauses *) 

837 
(* for its literals to obtain the empty clause *) 

17621  838 
val vids = map (fn l => l div 2) ls 
839 
val rs = cid :: map (fn v => !clause_offset + v) vids 

20463  840 
val new_empty_id = getOpt (Inttab.max_key (!clause_table), !clause_offset) + 1 
17493
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

841 
in 
17527  842 
(* update clause table and conflict id *) 
20463  843 
clause_table := Inttab.update_new (new_empty_id, rs) (!clause_table) 
844 
handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int new_empty_id ^ " (empty clause derived from clause " ^ id ^ ") already defined."); 

845 
empty_id := new_empty_id 

17493
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

846 
end 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

847 
 _ => 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

848 
raise INVALID_PROOF "File format error: \"CONF:\" followed by an insufficient number of tokens." 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

849 
) else 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

850 
raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.") 
20463  851 
(* string list > unit *) 
852 
fun process_lines [] = 

853 
() 

854 
 process_lines (l::ls) = ( 

855 
process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l); 

856 
process_lines ls 

857 
) 

17493
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

858 
(* proof *) 
20463  859 
val _ = process_lines proof_lines 
860 
val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified." 

17493
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

861 
in 
20463  862 
SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id)) 
17493
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

863 
end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE)) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

864 
 result => 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

865 
result 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

866 
in 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

867 
SatSolver.add_solver ("zchaff_with_proofs", zchaff_with_proofs) 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

868 
end; 
cf8713d880b1
SAT solver interface modified to support proofs of unsatisfiability
webertj
parents:
16915
diff
changeset

869 

14487
157d0ea7b2da
Installed solvers now determined at call time (as opposed to compile time)
webertj
parents:
14460
diff
changeset

870 
let 
157d0ea7b2da
Installed solvers now determined at call time (as opposed to compile time)
webertj
parents:
14460
diff
changeset

871 
fun zchaff fm = 
14453  872 
let 
14965  873 
val _ = if (getenv "ZCHAFF_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () 
15332  874 
val _ = if (getenv "ZCHAFF_VERSION") <> "2004.5.13" andalso 
875 
(getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else () 

876 
(* both versions of zChaff appear to have the same interface, so we do *) 

877 
(* not actually need to distinguish between them in the following code *) 

14965  878 
val inpath = File.tmp_path (Path.unpack "isabelle.cnf") 
879 
val outpath = File.tmp_path (Path.unpack "result") 

14453  880 
val cmd = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath) 
16914
e68528b4fc0b
replaced calls to PropLogic.auxcnf by PropLogic.defcnf again
webertj
parents:
16912
diff
changeset

881 
fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) 
17620
49568e5e0450
parse_std_result_file renamed to read_std_result_file
webertj
parents:
17581
diff
changeset

882 
fun readfn () = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable") 
16270  883 
val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else () 
884 
val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else () 

14965  885 
val result = SatSolver.make_external_solver cmd writefn readfn fm 
16270  886 
val _ = try File.rm inpath 
887 
val _ = try File.rm outpath 

14453  888 
in 
14965  889 
result 
14453  890 
end 
14487
157d0ea7b2da
Installed solvers now determined at call time (as opposed to compile time)
webertj
parents:
14460
diff
changeset

891 
in 
14965  892 
SatSolver.add_solver ("zchaff", zchaff) 
893 
end; 

894 

895 
(*  *) 

896 
(* BerkMin 561 (http://eigold.tripod.com/BerkMin.html) *) 

897 
(*  *) 

898 

899 
let 

900 
fun berkmin fm = 

901 
let 

902 
val _ = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else () 

903 
val inpath = File.tmp_path (Path.unpack "isabelle.cnf") 

904 
val outpath = File.tmp_path (Path.unpack "result") 

905 
val cmd = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath) 

16914
e68528b4fc0b
replaced calls to PropLogic.auxcnf by PropLogic.defcnf again
webertj
parents:
16912
diff
changeset

906 
fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) 
17620
49568e5e0450
parse_std_result_file renamed to read_std_result_file
webertj
parents:
17581
diff
changeset

907 
fun readfn () = SatSolver.read_std_result_file outpath ("Satisfiable !!", "solution =", "UNSATISFIABLE !!") 
16270  908 
val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else () 
909 
val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else () 

14965  910 
val result = SatSolver.make_external_solver cmd writefn readfn fm 
16270  911 
val _ = try File.rm inpath 
912 
val _ = try File.rm outpath 

14965  913 
in 
914 
result 

915 
end 

916 
in 

917 
SatSolver.add_solver ("berkmin", berkmin) 

918 
end; 

919 

920 
(*  *) 

921 
(* Jerusat 1.3 (http://www.cs.tau.ac.il/~ale1/) *) 

922 
(*  *) 

923 

924 
let 

925 
fun jerusat fm = 

926 
let 

927 
val _ = if (getenv "JERUSAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else () 

928 
val inpath = File.tmp_path (Path.unpack "isabelle.cnf") 

929 
val outpath = File.tmp_path (Path.unpack "result") 

930 
val cmd = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath) 

16914
e68528b4fc0b
replaced calls to PropLogic.auxcnf by PropLogic.defcnf again
webertj
parents:
16912
diff
changeset

931 
fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) 
17620
49568e5e0450
parse_std_result_file renamed to read_std_result_file
webertj
parents:
17581
diff
changeset

932 
fun readfn () = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE") 
16270  933 
val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else () 
934 
val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else () 

14965  935 
val result = SatSolver.make_external_solver cmd writefn readfn fm 
16270  936 
val _ = try File.rm inpath 
937 
val _ = try File.rm outpath 

14965  938 
in 
939 
result 

940 
end 

941 
in 

942 
SatSolver.add_solver ("jerusat", jerusat) 

14487
157d0ea7b2da
Installed solvers now determined at call time (as opposed to compile time)
webertj
parents:
14460
diff
changeset

943 
end; 
14453  944 

945 
(*  *) 

946 
(* Add code for other SAT solvers below. *) 

947 
(*  *) 

948 

949 
(* 

14487
157d0ea7b2da
Installed solvers now determined at call time (as opposed to compile time)
webertj
parents:
14460
diff
changeset

950 
let 
157d0ea7b2da
Installed solvers now determined at call time (as opposed to compile time)
webertj
parents:
14460
diff
changeset

951 
fun mysolver fm = ... 
157d0ea7b2da
Installed solvers now determined at call time (as opposed to compile time)
webertj
parents:
14460
diff
changeset

952 
in 
14965  953 
SatSolver.add_solver ("myname", (fn fm => if mysolver_is_configured then mysolver fm else raise SatSolver.NOT_CONFIGURED));  register the solver 
14487
157d0ea7b2da
Installed solvers now determined at call time (as opposed to compile time)
webertj
parents:
14460
diff
changeset

954 
end; 
14453  955 

956 
 the solver is now available as SatSolver.invoke_solver "myname" 

957 
*) 