--- a/src/HOL/Tools/sat_solver.ML Wed Aug 19 22:40:41 2015 +0200
+++ b/src/HOL/Tools/sat_solver.ML Thu Aug 20 13:41:53 2015 +0200
@@ -129,29 +129,29 @@
error "formula is not in CNF"
| write_formula (BoolVar i) =
(i>=1 orelse error "formula contains a variable index less than 1";
- TextIO.output (out, string_of_int i))
+ File.output out (string_of_int i))
| write_formula (Not (BoolVar i)) =
- (TextIO.output (out, "-");
+ (File.output out "-";
write_formula (BoolVar i))
| write_formula (Not _) =
error "formula is not in CNF"
| write_formula (Or (fm1, fm2)) =
(write_formula fm1;
- TextIO.output (out, " ");
+ File.output out " ";
write_formula fm2)
| write_formula (And (fm1, fm2)) =
(write_formula fm1;
- TextIO.output (out, " 0\n");
+ File.output out " 0\n";
write_formula fm2)
val fm' = cnf_True_False_elim fm
val number_of_vars = maxidx fm'
val number_of_clauses = cnf_number_of_clauses fm'
in
- TextIO.output (out, "c This file was generated by SAT_Solver.write_dimacs_cnf_file\n");
- TextIO.output (out, "p cnf " ^ string_of_int number_of_vars ^ " " ^
+ File.output out "c This file was generated by SAT_Solver.write_dimacs_cnf_file\n";
+ File.output out ("p cnf " ^ string_of_int number_of_vars ^ " " ^
string_of_int number_of_clauses ^ "\n");
write_formula fm';
- TextIO.output (out, " 0\n")
+ File.output out " 0\n"
end
in
File.open_output write_cnf_file path
@@ -169,51 +169,51 @@
fun write_sat_file out =
let
fun write_formula True =
- TextIO.output (out, "*()")
+ File.output out "*()"
| write_formula False =
- TextIO.output (out, "+()")
+ File.output out "+()"
| write_formula (BoolVar i) =
(i>=1 orelse error "formula contains a variable index less than 1";
- TextIO.output (out, string_of_int i))
+ File.output out (string_of_int i))
| write_formula (Not (BoolVar i)) =
- (TextIO.output (out, "-");
+ (File.output out "-";
write_formula (BoolVar i))
| write_formula (Not fm) =
- (TextIO.output (out, "-(");
+ (File.output out "-(";
write_formula fm;
- TextIO.output (out, ")"))
+ File.output out ")")
| write_formula (Or (fm1, fm2)) =
- (TextIO.output (out, "+(");
+ (File.output out "+(";
write_formula_or fm1;
- TextIO.output (out, " ");
+ File.output out " ";
write_formula_or fm2;
- TextIO.output (out, ")"))
+ File.output out ")")
| write_formula (And (fm1, fm2)) =
- (TextIO.output (out, "*(");
+ (File.output out "*(";
write_formula_and fm1;
- TextIO.output (out, " ");
+ File.output out " ";
write_formula_and fm2;
- TextIO.output (out, ")"))
+ File.output out ")")
(* optimization to make use of n-ary disjunction/conjunction *)
and write_formula_or (Or (fm1, fm2)) =
(write_formula_or fm1;
- TextIO.output (out, " ");
+ File.output out " ";
write_formula_or fm2)
| write_formula_or fm =
write_formula fm
and write_formula_and (And (fm1, fm2)) =
(write_formula_and fm1;
- TextIO.output (out, " ");
+ File.output out " ";
write_formula_and fm2)
| write_formula_and fm =
write_formula fm
val number_of_vars = Int.max (maxidx fm, 1)
in
- TextIO.output (out, "c This file was generated by SAT_Solver.write_dimacs_sat_file\n");
- TextIO.output (out, "p sat " ^ string_of_int number_of_vars ^ "\n");
- TextIO.output (out, "(");
+ File.output out "c This file was generated by SAT_Solver.write_dimacs_sat_file\n";
+ File.output out ("p sat " ^ string_of_int number_of_vars ^ "\n");
+ File.output out "(";
write_formula fm;
- TextIO.output (out, ")\n")
+ File.output out ")\n"
end
in
File.open_output write_sat_file path