127 error "formula is not in CNF" |
127 error "formula is not in CNF" |
128 | write_formula False = |
128 | write_formula False = |
129 error "formula is not in CNF" |
129 error "formula is not in CNF" |
130 | write_formula (BoolVar i) = |
130 | write_formula (BoolVar i) = |
131 (i>=1 orelse error "formula contains a variable index less than 1"; |
131 (i>=1 orelse error "formula contains a variable index less than 1"; |
132 TextIO.output (out, string_of_int i)) |
132 File.output out (string_of_int i)) |
133 | write_formula (Not (BoolVar i)) = |
133 | write_formula (Not (BoolVar i)) = |
134 (TextIO.output (out, "-"); |
134 (File.output out "-"; |
135 write_formula (BoolVar i)) |
135 write_formula (BoolVar i)) |
136 | write_formula (Not _) = |
136 | write_formula (Not _) = |
137 error "formula is not in CNF" |
137 error "formula is not in CNF" |
138 | write_formula (Or (fm1, fm2)) = |
138 | write_formula (Or (fm1, fm2)) = |
139 (write_formula fm1; |
139 (write_formula fm1; |
140 TextIO.output (out, " "); |
140 File.output out " "; |
141 write_formula fm2) |
141 write_formula fm2) |
142 | write_formula (And (fm1, fm2)) = |
142 | write_formula (And (fm1, fm2)) = |
143 (write_formula fm1; |
143 (write_formula fm1; |
144 TextIO.output (out, " 0\n"); |
144 File.output out " 0\n"; |
145 write_formula fm2) |
145 write_formula fm2) |
146 val fm' = cnf_True_False_elim fm |
146 val fm' = cnf_True_False_elim fm |
147 val number_of_vars = maxidx fm' |
147 val number_of_vars = maxidx fm' |
148 val number_of_clauses = cnf_number_of_clauses fm' |
148 val number_of_clauses = cnf_number_of_clauses fm' |
149 in |
149 in |
150 TextIO.output (out, "c This file was generated by SAT_Solver.write_dimacs_cnf_file\n"); |
150 File.output out "c This file was generated by SAT_Solver.write_dimacs_cnf_file\n"; |
151 TextIO.output (out, "p cnf " ^ string_of_int number_of_vars ^ " " ^ |
151 File.output out ("p cnf " ^ string_of_int number_of_vars ^ " " ^ |
152 string_of_int number_of_clauses ^ "\n"); |
152 string_of_int number_of_clauses ^ "\n"); |
153 write_formula fm'; |
153 write_formula fm'; |
154 TextIO.output (out, " 0\n") |
154 File.output out " 0\n" |
155 end |
155 end |
156 in |
156 in |
157 File.open_output write_cnf_file path |
157 File.open_output write_cnf_file path |
158 end; |
158 end; |
159 |
159 |
167 fun write_dimacs_sat_file path fm = |
167 fun write_dimacs_sat_file path fm = |
168 let |
168 let |
169 fun write_sat_file out = |
169 fun write_sat_file out = |
170 let |
170 let |
171 fun write_formula True = |
171 fun write_formula True = |
172 TextIO.output (out, "*()") |
172 File.output out "*()" |
173 | write_formula False = |
173 | write_formula False = |
174 TextIO.output (out, "+()") |
174 File.output out "+()" |
175 | write_formula (BoolVar i) = |
175 | write_formula (BoolVar i) = |
176 (i>=1 orelse error "formula contains a variable index less than 1"; |
176 (i>=1 orelse error "formula contains a variable index less than 1"; |
177 TextIO.output (out, string_of_int i)) |
177 File.output out (string_of_int i)) |
178 | write_formula (Not (BoolVar i)) = |
178 | write_formula (Not (BoolVar i)) = |
179 (TextIO.output (out, "-"); |
179 (File.output out "-"; |
180 write_formula (BoolVar i)) |
180 write_formula (BoolVar i)) |
181 | write_formula (Not fm) = |
181 | write_formula (Not fm) = |
182 (TextIO.output (out, "-("); |
182 (File.output out "-("; |
183 write_formula fm; |
183 write_formula fm; |
184 TextIO.output (out, ")")) |
184 File.output out ")") |
185 | write_formula (Or (fm1, fm2)) = |
185 | write_formula (Or (fm1, fm2)) = |
186 (TextIO.output (out, "+("); |
186 (File.output out "+("; |
187 write_formula_or fm1; |
187 write_formula_or fm1; |
188 TextIO.output (out, " "); |
188 File.output out " "; |
189 write_formula_or fm2; |
189 write_formula_or fm2; |
190 TextIO.output (out, ")")) |
190 File.output out ")") |
191 | write_formula (And (fm1, fm2)) = |
191 | write_formula (And (fm1, fm2)) = |
192 (TextIO.output (out, "*("); |
192 (File.output out "*("; |
193 write_formula_and fm1; |
193 write_formula_and fm1; |
194 TextIO.output (out, " "); |
194 File.output out " "; |
195 write_formula_and fm2; |
195 write_formula_and fm2; |
196 TextIO.output (out, ")")) |
196 File.output out ")") |
197 (* optimization to make use of n-ary disjunction/conjunction *) |
197 (* optimization to make use of n-ary disjunction/conjunction *) |
198 and write_formula_or (Or (fm1, fm2)) = |
198 and write_formula_or (Or (fm1, fm2)) = |
199 (write_formula_or fm1; |
199 (write_formula_or fm1; |
200 TextIO.output (out, " "); |
200 File.output out " "; |
201 write_formula_or fm2) |
201 write_formula_or fm2) |
202 | write_formula_or fm = |
202 | write_formula_or fm = |
203 write_formula fm |
203 write_formula fm |
204 and write_formula_and (And (fm1, fm2)) = |
204 and write_formula_and (And (fm1, fm2)) = |
205 (write_formula_and fm1; |
205 (write_formula_and fm1; |
206 TextIO.output (out, " "); |
206 File.output out " "; |
207 write_formula_and fm2) |
207 write_formula_and fm2) |
208 | write_formula_and fm = |
208 | write_formula_and fm = |
209 write_formula fm |
209 write_formula fm |
210 val number_of_vars = Int.max (maxidx fm, 1) |
210 val number_of_vars = Int.max (maxidx fm, 1) |
211 in |
211 in |
212 TextIO.output (out, "c This file was generated by SAT_Solver.write_dimacs_sat_file\n"); |
212 File.output out "c This file was generated by SAT_Solver.write_dimacs_sat_file\n"; |
213 TextIO.output (out, "p sat " ^ string_of_int number_of_vars ^ "\n"); |
213 File.output out ("p sat " ^ string_of_int number_of_vars ^ "\n"); |
214 TextIO.output (out, "("); |
214 File.output out "("; |
215 write_formula fm; |
215 write_formula fm; |
216 TextIO.output (out, ")\n") |
216 File.output out ")\n" |
217 end |
217 end |
218 in |
218 in |
219 File.open_output write_sat_file path |
219 File.open_output write_sat_file path |
220 end; |
220 end; |
221 |
221 |