src/HOL/Tools/sat_solver.ML
changeset 75615 4494cd69f97f
parent 68224 1f7308050349
child 77888 3c837f8c8ed5
--- 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;
 
 (* ------------------------------------------------------------------------- *)