--- a/src/HOL/Tools/sat_solver.ML Fri Jun 24 23:11:59 2022 +0200
+++ b/src/HOL/Tools/sat_solver.ML Fri Jun 24 23:31:28 2022 +0200
@@ -129,32 +129,32 @@
error "formula is not in CNF"
| write_formula (BoolVar i) =
(i>=1 orelse error "formula contains a variable index less than 1";
- File.output out (string_of_int i))
+ File_Stream.output out (string_of_int i))
| write_formula (Not (BoolVar i)) =
- (File.output out "-";
+ (File_Stream.output out "-";
write_formula (BoolVar i))
| write_formula (Not _) =
error "formula is not in CNF"
| write_formula (Or (fm1, fm2)) =
(write_formula fm1;
- File.output out " ";
+ File_Stream.output out " ";
write_formula fm2)
| write_formula (And (fm1, fm2)) =
(write_formula fm1;
- File.output out " 0\n";
+ File_Stream.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
- 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 ^ " " ^
+ File_Stream.output out "c This file was generated by SAT_Solver.write_dimacs_cnf_file\n";
+ File_Stream.output out ("p cnf " ^ string_of_int number_of_vars ^ " " ^
string_of_int number_of_clauses ^ "\n");
write_formula fm';
- File.output out " 0\n"
+ File_Stream.output out " 0\n"
end
in
- File.open_output write_cnf_file path
+ File_Stream.open_output write_cnf_file path
end;
(* ------------------------------------------------------------------------- *)
@@ -169,54 +169,54 @@
fun write_sat_file out =
let
fun write_formula True =
- File.output out "*()"
+ File_Stream.output out "*()"
| write_formula False =
- File.output out "+()"
+ File_Stream.output out "+()"
| write_formula (BoolVar i) =
(i>=1 orelse error "formula contains a variable index less than 1";
- File.output out (string_of_int i))
+ File_Stream.output out (string_of_int i))
| write_formula (Not (BoolVar i)) =
- (File.output out "-";
+ (File_Stream.output out "-";
write_formula (BoolVar i))
| write_formula (Not fm) =
- (File.output out "-(";
+ (File_Stream.output out "-(";
write_formula fm;
- File.output out ")")
+ File_Stream.output out ")")
| write_formula (Or (fm1, fm2)) =
- (File.output out "+(";
+ (File_Stream.output out "+(";
write_formula_or fm1;
- File.output out " ";
+ File_Stream.output out " ";
write_formula_or fm2;
- File.output out ")")
+ File_Stream.output out ")")
| write_formula (And (fm1, fm2)) =
- (File.output out "*(";
+ (File_Stream.output out "*(";
write_formula_and fm1;
- File.output out " ";
+ File_Stream.output out " ";
write_formula_and fm2;
- File.output out ")")
+ File_Stream.output out ")")
(* optimization to make use of n-ary disjunction/conjunction *)
and write_formula_or (Or (fm1, fm2)) =
(write_formula_or fm1;
- File.output out " ";
+ File_Stream.output out " ";
write_formula_or fm2)
| write_formula_or fm =
write_formula fm
and write_formula_and (And (fm1, fm2)) =
(write_formula_and fm1;
- File.output out " ";
+ File_Stream.output out " ";
write_formula_and fm2)
| write_formula_and fm =
write_formula fm
val number_of_vars = Int.max (maxidx fm, 1)
in
- 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 "(";
+ File_Stream.output out "c This file was generated by SAT_Solver.write_dimacs_sat_file\n";
+ File_Stream.output out ("p sat " ^ string_of_int number_of_vars ^ "\n");
+ File_Stream.output out "(";
write_formula fm;
- File.output out ")\n"
+ File_Stream.output out ")\n"
end
in
- File.open_output write_sat_file path
+ File_Stream.open_output write_sat_file path
end;
(* ------------------------------------------------------------------------- *)