write_dimacs_sat_file now generates slightly smaller files
authorwebertj
Thu Jul 21 18:52:17 2005 +0200 (2005-07-21)
changeset 16899ee4d620bcc1c
parent 16898 543ee8fabe1a
child 16900 e294033d1c0f
write_dimacs_sat_file now generates slightly smaller files
src/HOL/Tools/sat_solver.ML
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Wed Jul 20 17:01:20 2005 +0200
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Thu Jul 21 18:52:17 2005 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4  
     1.5  	val read_dimacs_cnf_file : Path.T -> PropLogic.prop_formula
     1.6  
     1.7 -	(* generic interface *)
     1.8 +	(* generic solver interface *)
     1.9  	val solvers       : (string * solver) list ref
    1.10  	val add_solver    : string * solver -> unit
    1.11  	val invoke_solver : string -> solver  (* exception Option *)
    1.12 @@ -147,12 +147,25 @@
    1.13  			  | sat_string_acc (BoolVar i) acc =
    1.14  				(assert (i>=1) "formula contains a variable index less than 1";
    1.15  				string_of_int i :: acc)
    1.16 +			  | sat_string_acc (Not (BoolVar i)) acc =
    1.17 +				"-" :: sat_string_acc (BoolVar i) acc
    1.18  			  | sat_string_acc (Not fm) acc =
    1.19  				"-(" :: sat_string_acc fm (")" :: acc)
    1.20  			  | sat_string_acc (Or (fm1,fm2)) acc =
    1.21 -				"+(" :: sat_string_acc fm1 (" " :: sat_string_acc fm2 (")" :: acc))
    1.22 +				"+(" :: sat_string_acc_or fm1 (" " :: sat_string_acc_or fm2 (")" :: acc))
    1.23  			  | sat_string_acc (And (fm1,fm2)) acc =
    1.24 -				"*(" :: sat_string_acc fm1 (" " :: sat_string_acc fm2 (")" :: acc))
    1.25 +				"*(" :: sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 (")" :: acc))
    1.26 +			(* optimization to make use of n-ary disjunction/conjunction *)
    1.27 +			(* prop_formula -> string list -> string list *)
    1.28 +			and sat_string_acc_or (Or (fm1,fm2)) acc =
    1.29 +				sat_string_acc_or fm1 (" " :: sat_string_acc_or fm2 acc)
    1.30 +			  | sat_string_acc_or fm acc =
    1.31 +				sat_string_acc fm acc
    1.32 +			(* prop_formula -> string list -> string list *)
    1.33 +			and sat_string_acc_and (And (fm1,fm2)) acc =
    1.34 +				sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 acc)
    1.35 +			  | sat_string_acc_and fm acc =
    1.36 +				sat_string_acc fm acc
    1.37  		in
    1.38  			concat (sat_string_acc fm [])
    1.39  		end
    1.40 @@ -164,7 +177,7 @@
    1.41  				"c This file was generated by SatSolver.write_dimacs_sat_file\n" ^
    1.42  				"c (c) Tjark Weber\n" ^
    1.43  				"p sat " ^ string_of_int number_of_vars ^ "\n" ^
    1.44 -				"(" ^ sat_string fm ^ ")\n"
    1.45 +				(*"(" ^*) sat_string fm ^ "\n" (*")\n"*)
    1.46  			end)
    1.47  	end;
    1.48  
    1.49 @@ -521,10 +534,11 @@
    1.50  		                    (getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else ()
    1.51  			(* both versions of zChaff appear to have the same interface, so we do *)
    1.52  			(* not actually need to distinguish between them in the following code *)
    1.53 +		val satpath    = File.tmp_path (Path.unpack "isabelle.sat")
    1.54  		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
    1.55  		val outpath    = File.tmp_path (Path.unpack "result")
    1.56  		val cmd        = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
    1.57 -		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
    1.58 +		fun writefn fm = (SatSolver.write_dimacs_sat_file satpath fm; SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm))
    1.59  		fun readfn ()  = SatSolver.parse_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
    1.60  		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
    1.61  		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()