faster conversion into DIMACS CNF and DIMACS SAT format
authorwebertj
Tue Jun 22 14:14:08 2004 +0200 (2004-06-22)
changeset 149992c39efba8f67
parent 14998 9606c6224933
child 15000 3d6245229e48
faster conversion into DIMACS CNF and DIMACS SAT format
src/HOL/Tools/sat_solver.ML
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Tue Jun 22 10:05:47 2004 +0200
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Tue Jun 22 14:14:08 2004 +0200
     1.3 @@ -88,31 +88,38 @@
     1.4  		  | cnf_number_of_clauses _ =
     1.5  			1
     1.6  		(* prop_formula -> string *)
     1.7 -		fun cnf_string True =
     1.8 -			error "formula is not in CNF"
     1.9 -		  | cnf_string False =
    1.10 -			error "formula is not in CNF"
    1.11 -		  | cnf_string (BoolVar i) =
    1.12 -			(assert (i>=1) "formula contains a variable index less than 1";
    1.13 -			string_of_int i)
    1.14 -		  | cnf_string (Not fm) =
    1.15 -			"-" ^ cnf_string fm
    1.16 -		  | cnf_string (Or (fm1,fm2)) =
    1.17 -			cnf_string fm1 ^ " " ^ cnf_string fm2
    1.18 -		  | cnf_string (And (fm1,fm2)) =
    1.19 -			cnf_string fm1 ^ " 0\n" ^ cnf_string fm2
    1.20 +		fun cnf_string fm =
    1.21 +		let
    1.22 +			(* prop_formula -> string list -> string list *)
    1.23 +			fun cnf_string_acc True acc =
    1.24 +				error "formula is not in CNF"
    1.25 +			  | cnf_string_acc False acc =
    1.26 +				error "formula is not in CNF"
    1.27 +			  | cnf_string_acc (BoolVar i) acc =
    1.28 +				(assert (i>=1) "formula contains a variable index less than 1";
    1.29 +				string_of_int i :: acc)
    1.30 +			  | cnf_string_acc (Not (BoolVar i)) acc =
    1.31 +				"-" :: cnf_string_acc (BoolVar i) acc
    1.32 +			  | cnf_string_acc (Not _) acc =
    1.33 +				error "formula is not in CNF"
    1.34 +			  | cnf_string_acc (Or (fm1,fm2)) acc =
    1.35 +				cnf_string_acc fm1 (" " :: cnf_string_acc fm2 acc)
    1.36 +			  | cnf_string_acc (And (fm1,fm2)) acc =
    1.37 +				cnf_string_acc fm1 (" 0\n" :: cnf_string_acc fm2 acc)
    1.38 +		in
    1.39 +			concat (cnf_string_acc fm [])
    1.40 +		end
    1.41  	in
    1.42  		File.write path
    1.43  			(let
    1.44  				val fm'               = cnf_True_False_elim fm
    1.45  				val number_of_vars    = maxidx fm'
    1.46  				val number_of_clauses = cnf_number_of_clauses fm'
    1.47 -				val cnfstring         = cnf_string fm'
    1.48  			in
    1.49  				"c This file was generated by SatSolver.write_dimacs_cnf_file\n" ^
    1.50  				"c (c) Tjark Weber\n" ^
    1.51  				"p cnf " ^ string_of_int number_of_vars ^ " " ^ string_of_int number_of_clauses ^ "\n" ^
    1.52 -				cnfstring ^ " 0\n"
    1.53 +				cnf_string fm' ^ " 0\n"
    1.54  			end)
    1.55  	end;
    1.56  
    1.57 @@ -128,19 +135,25 @@
    1.58  	fun write_dimacs_sat_file path fm =
    1.59  	let
    1.60  		(* prop_formula -> string *)
    1.61 -		fun sat_string True =
    1.62 -			"*()"
    1.63 -		  | sat_string False =
    1.64 -			"+()"
    1.65 -		  | sat_string (BoolVar i) =
    1.66 -			(assert (i>=1) "formula contains a variable index less than 1";
    1.67 -			string_of_int i)
    1.68 -		  | sat_string (Not fm) =
    1.69 -			"-(" ^ sat_string fm ^ ")"
    1.70 -		  | sat_string (Or (fm1,fm2)) =
    1.71 -			"+(" ^ sat_string fm1 ^ " " ^ sat_string fm2 ^ ")"
    1.72 -		  | sat_string (And (fm1,fm2)) =
    1.73 -			"*(" ^ sat_string fm1 ^ " " ^ sat_string fm2 ^ ")"
    1.74 +		fun sat_string fm =
    1.75 +		let
    1.76 +			(* prop_formula -> string list -> string list *)
    1.77 +			fun sat_string_acc True acc =
    1.78 +				"*()" :: acc
    1.79 +			  | sat_string_acc False acc =
    1.80 +				"+()" :: acc
    1.81 +			  | sat_string_acc (BoolVar i) acc =
    1.82 +				(assert (i>=1) "formula contains a variable index less than 1";
    1.83 +				string_of_int i :: acc)
    1.84 +			  | sat_string_acc (Not fm) acc =
    1.85 +				"-(" :: sat_string_acc fm (")" :: acc)
    1.86 +			  | sat_string_acc (Or (fm1,fm2)) acc =
    1.87 +				"+(" :: sat_string_acc fm1 (" " :: sat_string_acc fm2 (")" :: acc))
    1.88 +			  | sat_string_acc (And (fm1,fm2)) acc =
    1.89 +				"*(" :: sat_string_acc fm1 (" " :: sat_string_acc fm2 (")" :: acc))
    1.90 +		in
    1.91 +			concat (sat_string_acc fm [])
    1.92 +		end
    1.93  	in
    1.94  		File.write path
    1.95  			(let