# HG changeset patch
# User webertj
# Date 1122384577 -7200
# Node ID bca4c3b1afca6f51d7f2d6c26c39d19067a90cf8
# Parent  e68528b4fc0bce387af31c0063de433500ab1b37
write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks

diff -r e68528b4fc0b -r bca4c3b1afca src/HOL/Tools/sat_solver.ML
--- 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;
 
 (* ------------------------------------------------------------------------- *)