--- a/src/HOL/Tools/sat_solver.ML Tue Jul 26 14:31:42 2005 +0200
+++ b/src/HOL/Tools/sat_solver.ML Tue Jul 26 15:29:37 2005 +0200
@@ -89,7 +89,7 @@
(cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2)
| cnf_number_of_clauses _ =
1
- (* prop_formula -> string *)
+ (* prop_formula -> string list *)
fun cnf_string fm =
let
(* prop_formula -> string list -> string list *)
@@ -109,20 +109,20 @@
| cnf_string_acc (And (fm1,fm2)) acc =
cnf_string_acc fm1 (" 0\n" :: cnf_string_acc fm2 acc)
in
- concat (cnf_string_acc fm [])
+ cnf_string_acc fm []
end
+ val fm' = cnf_True_False_elim fm
+ val number_of_vars = maxidx fm'
+ val number_of_clauses = cnf_number_of_clauses fm'
in
File.write path
- (let
- val fm' = cnf_True_False_elim fm
- val number_of_vars = maxidx fm'
- val number_of_clauses = cnf_number_of_clauses fm'
- in
- "c This file was generated by SatSolver.write_dimacs_cnf_file\n" ^
- "c (c) Tjark Weber\n" ^
- "p cnf " ^ string_of_int number_of_vars ^ " " ^ string_of_int number_of_clauses ^ "\n" ^
- cnf_string fm' ^ " 0\n"
- end)
+ ("c This file was generated by SatSolver.write_dimacs_cnf_file\n" ^
+ "c (c) Tjark Weber\n" ^
+ "p cnf " ^ string_of_int number_of_vars ^ " " ^ string_of_int number_of_clauses ^ "\n");
+ File.append_list path
+ (cnf_string fm');
+ File.append path
+ " 0\n"
end;
(* ------------------------------------------------------------------------- *)
@@ -136,7 +136,7 @@
fun write_dimacs_sat_file path fm =
let
- (* prop_formula -> string *)
+ (* prop_formula -> string list *)
fun sat_string fm =
let
(* prop_formula -> string list -> string list *)
@@ -167,18 +167,19 @@
| sat_string_acc_and fm acc =
sat_string_acc fm acc
in
- concat (sat_string_acc fm [])
+ sat_string_acc fm []
end
+ val number_of_vars = Int.max (maxidx fm, 1)
in
File.write path
- (let
- val number_of_vars = Int.max (maxidx fm, 1)
- in
- "c This file was generated by SatSolver.write_dimacs_sat_file\n" ^
- "c (c) Tjark Weber\n" ^
- "p sat " ^ string_of_int number_of_vars ^ "\n" ^
- "(" ^ sat_string fm ^ ")\n"
- end)
+ ("c This file was generated by SatSolver.write_dimacs_sat_file\n" ^
+ "c (c) Tjark Weber\n" ^
+ "p sat " ^ string_of_int number_of_vars ^ "\n" ^
+ "(");
+ File.append_list path
+ (sat_string fm);
+ File.append path
+ ")\n"
end;
(* ------------------------------------------------------------------------- *)