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', |
|
106 or 'fm' does not contain 'True'/'False' at all *) |
106 (* prop_formula -> int *) |
107 (* prop_formula -> int *) |
107 fun cnf_number_of_clauses (And (fm1,fm2)) = |
108 fun cnf_number_of_clauses (And (fm1, fm2)) = |
108 (cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2) |
109 (cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2) |
109 | cnf_number_of_clauses _ = |
110 | cnf_number_of_clauses _ = |
110 1 |
111 1 |
111 (* prop_formula -> string list *) |
112 (* TextIO.outstream -> unit *) |
112 fun cnf_string fm = |
113 fun write_cnf_file out = |
113 let |
114 let |
114 (* prop_formula -> string list -> string list *) |
115 (* prop_formula -> unit *) |
115 fun cnf_string_acc True acc = |
116 fun write_formula True = |
116 error "formula is not in CNF" |
117 error "formula is not in CNF" |
117 | cnf_string_acc False acc = |
118 | write_formula False = |
118 error "formula is not in CNF" |
119 error "formula is not in CNF" |
119 | cnf_string_acc (BoolVar i) acc = |
120 | write_formula (BoolVar i) = |
120 (i>=1 orelse error "formula contains a variable index less than 1"; |
121 (i>=1 orelse error "formula contains a variable index less than 1"; |
121 string_of_int i :: acc) |
122 TextIO.output (out, string_of_int i)) |
122 | cnf_string_acc (Not (BoolVar i)) acc = |
123 | write_formula (Not (BoolVar i)) = |
123 "-" :: cnf_string_acc (BoolVar i) acc |
124 (TextIO.output (out, "-"); |
124 | cnf_string_acc (Not _) acc = |
125 write_formula (BoolVar i)) |
125 error "formula is not in CNF" |
126 | write_formula (Not _) = |
126 | cnf_string_acc (Or (fm1,fm2)) acc = |
127 error "formula is not in CNF" |
127 cnf_string_acc fm1 (" " :: cnf_string_acc fm2 acc) |
128 | write_formula (Or (fm1, fm2)) = |
128 | cnf_string_acc (And (fm1,fm2)) acc = |
129 (write_formula fm1; |
129 cnf_string_acc fm1 (" 0\n" :: cnf_string_acc fm2 acc) |
130 TextIO.output (out, " "); |
|
131 write_formula fm2) |
|
132 | write_formula (And (fm1, fm2)) = |
|
133 (write_formula fm1; |
|
134 TextIO.output (out, " 0\n"); |
|
135 write_formula fm2) |
|
136 val fm' = cnf_True_False_elim fm |
|
137 val number_of_vars = maxidx fm' |
|
138 val number_of_clauses = cnf_number_of_clauses fm' |
130 in |
139 in |
131 cnf_string_acc fm [] |
140 TextIO.output (out, "c This file was generated by SatSolver.write_dimacs_cnf_file\n"); |
|
141 TextIO.output (out, "p cnf " ^ string_of_int number_of_vars ^ " " ^ |
|
142 string_of_int number_of_clauses ^ "\n"); |
|
143 write_formula fm'; |
|
144 TextIO.output (out, " 0\n") |
132 end |
145 end |
133 val fm' = cnf_True_False_elim fm |
|
134 val number_of_vars = maxidx fm' |
|
135 val number_of_clauses = cnf_number_of_clauses fm' |
|
136 in |
146 in |
137 File.write path |
147 File.open_output write_cnf_file path |
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"); |
|
140 File.append_list path |
|
141 (cnf_string fm'); |
|
142 File.append path |
|
143 " 0\n" |
|
144 end; |
148 end; |
145 |
149 |
146 (* ------------------------------------------------------------------------- *) |
150 (* ------------------------------------------------------------------------- *) |
147 (* write_dimacs_sat_file: serializes a formula 'fm' of propositional logic *) |
151 (* write_dimacs_sat_file: serializes a formula 'fm' of propositional logic *) |
148 (* to a file in DIMACS SAT format (see "Satisfiability Suggested *) |
152 (* to a file in DIMACS SAT format (see "Satisfiability Suggested *) |
152 |
156 |
153 (* Path.T -> prop_formula -> unit *) |
157 (* Path.T -> prop_formula -> unit *) |
154 |
158 |
155 fun write_dimacs_sat_file path fm = |
159 fun write_dimacs_sat_file path fm = |
156 let |
160 let |
157 (* prop_formula -> string list *) |
161 (* TextIO.outstream -> unit *) |
158 fun sat_string fm = |
162 fun write_sat_file out = |
159 let |
163 let |
160 (* prop_formula -> string list -> string list *) |
164 (* prop_formula -> unit *) |
161 fun sat_string_acc True acc = |
165 fun write_formula True = |
162 "*()" :: acc |
166 TextIO.output (out, "*()") |
163 | sat_string_acc False acc = |
167 | write_formula False = |
164 "+()" :: acc |
168 TextIO.output (out, "+()") |
165 | sat_string_acc (BoolVar i) acc = |
169 | write_formula (BoolVar i) = |
166 (i>=1 orelse error "formula contains a variable index less than 1"; |
170 (i>=1 orelse error "formula contains a variable index less than 1"; |
167 string_of_int i :: acc) |
171 TextIO.output (out, string_of_int i)) |
168 | sat_string_acc (Not (BoolVar i)) acc = |
172 | write_formula (Not (BoolVar i)) = |
169 "-" :: sat_string_acc (BoolVar i) acc |
173 (TextIO.output (out, "-"); |
170 | sat_string_acc (Not fm) acc = |
174 write_formula (BoolVar i)) |
171 "-(" :: sat_string_acc fm (")" :: acc) |
175 | write_formula (Not fm) = |
172 | sat_string_acc (Or (fm1,fm2)) acc = |
176 (TextIO.output (out, "-("); |
173 "+(" :: sat_string_acc_or fm1 (" " :: sat_string_acc_or fm2 (")" :: acc)) |
177 write_formula fm; |
174 | sat_string_acc (And (fm1,fm2)) acc = |
178 TextIO.output (out, ")")) |
175 "*(" :: sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 (")" :: acc)) |
179 | write_formula (Or (fm1, fm2)) = |
|
180 (TextIO.output (out, "+("); |
|
181 write_formula_or fm1; |
|
182 TextIO.output (out, " "); |
|
183 write_formula_or fm2; |
|
184 TextIO.output (out, ")")) |
|
185 | write_formula (And (fm1, fm2)) = |
|
186 (TextIO.output (out, "*("); |
|
187 write_formula_and fm1; |
|
188 TextIO.output (out, " "); |
|
189 write_formula_and fm2; |
|
190 TextIO.output (out, ")")) |
176 (* optimization to make use of n-ary disjunction/conjunction *) |
191 (* optimization to make use of n-ary disjunction/conjunction *) |
177 (* prop_formula -> string list -> string list *) |
192 and write_formula_or (Or (fm1, fm2)) = |
178 and sat_string_acc_or (Or (fm1,fm2)) acc = |
193 (write_formula_or fm1; |
179 sat_string_acc_or fm1 (" " :: sat_string_acc_or fm2 acc) |
194 TextIO.output (out, " "); |
180 | sat_string_acc_or fm acc = |
195 write_formula_or fm2) |
181 sat_string_acc fm acc |
196 | write_formula_or fm = |
182 (* prop_formula -> string list -> string list *) |
197 write_formula fm |
183 and sat_string_acc_and (And (fm1,fm2)) acc = |
198 and write_formula_and (And (fm1, fm2)) = |
184 sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 acc) |
199 (write_formula_and fm1; |
185 | sat_string_acc_and fm acc = |
200 TextIO.output (out, " "); |
186 sat_string_acc fm acc |
201 write_formula_and fm2) |
|
202 | write_formula_and fm = |
|
203 write_formula fm |
|
204 val number_of_vars = Int.max (maxidx fm, 1) |
187 in |
205 in |
188 sat_string_acc fm [] |
206 TextIO.output (out, "c This file was generated by SatSolver.write_dimacs_sat_file\n"); |
|
207 TextIO.output (out, "p sat " ^ string_of_int number_of_vars ^ "\n"); |
|
208 TextIO.output (out, "("); |
|
209 write_formula fm; |
|
210 TextIO.output (out, ")\n") |
189 end |
211 end |
190 val number_of_vars = Int.max (maxidx fm, 1) |
|
191 in |
212 in |
192 File.write path |
213 File.open_output write_sat_file path |
193 ("c This file was generated by SatSolver.write_dimacs_sat_file\n" ^ |
|
194 "p sat " ^ string_of_int number_of_vars ^ "\n" ^ |
|
195 "("); |
|
196 File.append_list path |
|
197 (sat_string fm); |
|
198 File.append path |
|
199 ")\n" |
|
200 end; |
214 end; |
201 |
215 |
202 (* ------------------------------------------------------------------------- *) |
216 (* ------------------------------------------------------------------------- *) |
203 (* read_std_result_file: scans a SAT solver's output file for a satisfying *) |
217 (* read_std_result_file: scans a SAT solver's output file for a satisfying *) |
204 (* variable assignment. Returns the assignment, or 'UNSATISFIABLE' if *) |
218 (* variable assignment. Returns the assignment, or 'UNSATISFIABLE' if *) |