write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
authorwebertj
Tue Jul 26 15:29:37 2005 +0200 (2005-07-26)
changeset 16915bca4c3b1afca
parent 16914 e68528b4fc0b
child 16916 da331e0a4a81
write_dimacs_sat_file and write_dimacs_cnf_file now write the file in chunks
src/HOL/Tools/sat_solver.ML
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Tue Jul 26 14:31:42 2005 +0200
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Tue Jul 26 15:29:37 2005 +0200
     1.3 @@ -89,7 +89,7 @@
     1.4  			(cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2)
     1.5  		  | cnf_number_of_clauses _ =
     1.6  			1
     1.7 -		(* prop_formula -> string *)
     1.8 +		(* prop_formula -> string list *)
     1.9  		fun cnf_string fm =
    1.10  		let
    1.11  			(* prop_formula -> string list -> string list *)
    1.12 @@ -109,20 +109,20 @@
    1.13  			  | cnf_string_acc (And (fm1,fm2)) acc =
    1.14  				cnf_string_acc fm1 (" 0\n" :: cnf_string_acc fm2 acc)
    1.15  		in
    1.16 -			concat (cnf_string_acc fm [])
    1.17 +			cnf_string_acc fm []
    1.18  		end
    1.19 +		val fm'               = cnf_True_False_elim fm
    1.20 +		val number_of_vars    = maxidx fm'
    1.21 +		val number_of_clauses = cnf_number_of_clauses fm'
    1.22  	in
    1.23  		File.write path
    1.24 -			(let
    1.25 -				val fm'               = cnf_True_False_elim fm
    1.26 -				val number_of_vars    = maxidx fm'
    1.27 -				val number_of_clauses = cnf_number_of_clauses fm'
    1.28 -			in
    1.29 -				"c This file was generated by SatSolver.write_dimacs_cnf_file\n" ^
    1.30 -				"c (c) Tjark Weber\n" ^
    1.31 -				"p cnf " ^ string_of_int number_of_vars ^ " " ^ string_of_int number_of_clauses ^ "\n" ^
    1.32 -				cnf_string fm' ^ " 0\n"
    1.33 -			end)
    1.34 +			("c This file was generated by SatSolver.write_dimacs_cnf_file\n" ^
    1.35 +			 "c (c) Tjark Weber\n" ^
    1.36 +			 "p cnf " ^ string_of_int number_of_vars ^ " " ^ string_of_int number_of_clauses ^ "\n");
    1.37 +		File.append_list path
    1.38 +			(cnf_string fm');
    1.39 +		File.append path
    1.40 +			" 0\n"
    1.41  	end;
    1.42  
    1.43  (* ------------------------------------------------------------------------- *)
    1.44 @@ -136,7 +136,7 @@
    1.45  
    1.46  	fun write_dimacs_sat_file path fm =
    1.47  	let
    1.48 -		(* prop_formula -> string *)
    1.49 +		(* prop_formula -> string list *)
    1.50  		fun sat_string fm =
    1.51  		let
    1.52  			(* prop_formula -> string list -> string list *)
    1.53 @@ -167,18 +167,19 @@
    1.54  			  | sat_string_acc_and fm acc =
    1.55  				sat_string_acc fm acc
    1.56  		in
    1.57 -			concat (sat_string_acc fm [])
    1.58 +			sat_string_acc fm []
    1.59  		end
    1.60 +		val number_of_vars = Int.max (maxidx fm, 1)
    1.61  	in
    1.62  		File.write path
    1.63 -			(let
    1.64 -				val number_of_vars = Int.max (maxidx fm, 1)
    1.65 -			in
    1.66 -				"c This file was generated by SatSolver.write_dimacs_sat_file\n" ^
    1.67 -				"c (c) Tjark Weber\n" ^
    1.68 -				"p sat " ^ string_of_int number_of_vars ^ "\n" ^
    1.69 -				"(" ^ sat_string fm ^ ")\n"
    1.70 -			end)
    1.71 +			("c This file was generated by SatSolver.write_dimacs_sat_file\n" ^
    1.72 +			 "c (c) Tjark Weber\n" ^
    1.73 +			 "p sat " ^ string_of_int number_of_vars ^ "\n" ^
    1.74 +			 "(");
    1.75 +		File.append_list path
    1.76 +			(sat_string fm);
    1.77 +		File.append path
    1.78 +			")\n"
    1.79  	end;
    1.80  
    1.81  (* ------------------------------------------------------------------------- *)