87 (* prop_formula -> int *) |
87 (* prop_formula -> int *) |
88 fun cnf_number_of_clauses (And (fm1,fm2)) = |
88 fun cnf_number_of_clauses (And (fm1,fm2)) = |
89 (cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2) |
89 (cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2) |
90 | cnf_number_of_clauses _ = |
90 | cnf_number_of_clauses _ = |
91 1 |
91 1 |
92 (* prop_formula -> string *) |
92 (* prop_formula -> string list *) |
93 fun cnf_string fm = |
93 fun cnf_string fm = |
94 let |
94 let |
95 (* prop_formula -> string list -> string list *) |
95 (* prop_formula -> string list -> string list *) |
96 fun cnf_string_acc True acc = |
96 fun cnf_string_acc True acc = |
97 error "formula is not in CNF" |
97 error "formula is not in CNF" |
107 | cnf_string_acc (Or (fm1,fm2)) acc = |
107 | cnf_string_acc (Or (fm1,fm2)) acc = |
108 cnf_string_acc fm1 (" " :: cnf_string_acc fm2 acc) |
108 cnf_string_acc fm1 (" " :: cnf_string_acc fm2 acc) |
109 | cnf_string_acc (And (fm1,fm2)) acc = |
109 | cnf_string_acc (And (fm1,fm2)) acc = |
110 cnf_string_acc fm1 (" 0\n" :: cnf_string_acc fm2 acc) |
110 cnf_string_acc fm1 (" 0\n" :: cnf_string_acc fm2 acc) |
111 in |
111 in |
112 concat (cnf_string_acc fm []) |
112 cnf_string_acc fm [] |
113 end |
113 end |
|
114 val fm' = cnf_True_False_elim fm |
|
115 val number_of_vars = maxidx fm' |
|
116 val number_of_clauses = cnf_number_of_clauses fm' |
114 in |
117 in |
115 File.write path |
118 File.write path |
116 (let |
119 ("c This file was generated by SatSolver.write_dimacs_cnf_file\n" ^ |
117 val fm' = cnf_True_False_elim fm |
120 "c (c) Tjark Weber\n" ^ |
118 val number_of_vars = maxidx fm' |
121 "p cnf " ^ string_of_int number_of_vars ^ " " ^ string_of_int number_of_clauses ^ "\n"); |
119 val number_of_clauses = cnf_number_of_clauses fm' |
122 File.append_list path |
120 in |
123 (cnf_string fm'); |
121 "c This file was generated by SatSolver.write_dimacs_cnf_file\n" ^ |
124 File.append path |
122 "c (c) Tjark Weber\n" ^ |
125 " 0\n" |
123 "p cnf " ^ string_of_int number_of_vars ^ " " ^ string_of_int number_of_clauses ^ "\n" ^ |
|
124 cnf_string fm' ^ " 0\n" |
|
125 end) |
|
126 end; |
126 end; |
127 |
127 |
128 (* ------------------------------------------------------------------------- *) |
128 (* ------------------------------------------------------------------------- *) |
129 (* write_dimacs_sat_file: serializes a formula 'fm' of propositional logic *) |
129 (* write_dimacs_sat_file: serializes a formula 'fm' of propositional logic *) |
130 (* to a file in DIMACS SAT format (see "Satisfiability Suggested *) |
130 (* to a file in DIMACS SAT format (see "Satisfiability Suggested *) |
134 |
134 |
135 (* Path.T -> prop_formula -> unit *) |
135 (* Path.T -> prop_formula -> unit *) |
136 |
136 |
137 fun write_dimacs_sat_file path fm = |
137 fun write_dimacs_sat_file path fm = |
138 let |
138 let |
139 (* prop_formula -> string *) |
139 (* prop_formula -> string list *) |
140 fun sat_string fm = |
140 fun sat_string fm = |
141 let |
141 let |
142 (* prop_formula -> string list -> string list *) |
142 (* prop_formula -> string list -> string list *) |
143 fun sat_string_acc True acc = |
143 fun sat_string_acc True acc = |
144 "*()" :: acc |
144 "*()" :: acc |
165 and sat_string_acc_and (And (fm1,fm2)) acc = |
165 and sat_string_acc_and (And (fm1,fm2)) acc = |
166 sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 acc) |
166 sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 acc) |
167 | sat_string_acc_and fm acc = |
167 | sat_string_acc_and fm acc = |
168 sat_string_acc fm acc |
168 sat_string_acc fm acc |
169 in |
169 in |
170 concat (sat_string_acc fm []) |
170 sat_string_acc fm [] |
171 end |
171 end |
|
172 val number_of_vars = Int.max (maxidx fm, 1) |
172 in |
173 in |
173 File.write path |
174 File.write path |
174 (let |
175 ("c This file was generated by SatSolver.write_dimacs_sat_file\n" ^ |
175 val number_of_vars = Int.max (maxidx fm, 1) |
176 "c (c) Tjark Weber\n" ^ |
176 in |
177 "p sat " ^ string_of_int number_of_vars ^ "\n" ^ |
177 "c This file was generated by SatSolver.write_dimacs_sat_file\n" ^ |
178 "("); |
178 "c (c) Tjark Weber\n" ^ |
179 File.append_list path |
179 "p sat " ^ string_of_int number_of_vars ^ "\n" ^ |
180 (sat_string fm); |
180 "(" ^ sat_string fm ^ ")\n" |
181 File.append path |
181 end) |
182 ")\n" |
182 end; |
183 end; |
183 |
184 |
184 (* ------------------------------------------------------------------------- *) |
185 (* ------------------------------------------------------------------------- *) |
185 (* parse_std_result_file: scans a SAT solver's output file for a satisfying *) |
186 (* parse_std_result_file: scans a SAT solver's output file for a satisfying *) |
186 (* variable assignment. Returns the assignment, or 'UNSATISFIABLE' if *) |
187 (* variable assignment. Returns the assignment, or 'UNSATISFIABLE' if *) |