# HG changeset patch
# User webertj
# Date 1121964737 -7200
# Node ID ee4d620bcc1c6a8980e3f890b0733fdd85ce78f0
# Parent  543ee8fabe1a14a091e11d42a1ae5bc9edfecbb8
write_dimacs_sat_file now generates slightly smaller files

diff -r 543ee8fabe1a -r ee4d620bcc1c src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Wed Jul 20 17:01:20 2005 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Thu Jul 21 18:52:17 2005 +0200
@@ -24,7 +24,7 @@
 
 	val read_dimacs_cnf_file : Path.T -> PropLogic.prop_formula
 
-	(* generic interface *)
+	(* generic solver interface *)
 	val solvers       : (string * solver) list ref
 	val add_solver    : string * solver -> unit
 	val invoke_solver : string -> solver  (* exception Option *)
@@ -147,12 +147,25 @@
 			  | sat_string_acc (BoolVar i) acc =
 				(assert (i>=1) "formula contains a variable index less than 1";
 				string_of_int i :: acc)
+			  | sat_string_acc (Not (BoolVar i)) acc =
+				"-" :: sat_string_acc (BoolVar i) acc
 			  | sat_string_acc (Not fm) acc =
 				"-(" :: sat_string_acc fm (")" :: acc)
 			  | sat_string_acc (Or (fm1,fm2)) acc =
-				"+(" :: sat_string_acc fm1 (" " :: sat_string_acc fm2 (")" :: acc))
+				"+(" :: sat_string_acc_or fm1 (" " :: sat_string_acc_or fm2 (")" :: acc))
 			  | sat_string_acc (And (fm1,fm2)) acc =
-				"*(" :: sat_string_acc fm1 (" " :: sat_string_acc fm2 (")" :: acc))
+				"*(" :: sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 (")" :: acc))
+			(* optimization to make use of n-ary disjunction/conjunction *)
+			(* prop_formula -> string list -> string list *)
+			and sat_string_acc_or (Or (fm1,fm2)) acc =
+				sat_string_acc_or fm1 (" " :: sat_string_acc_or fm2 acc)
+			  | sat_string_acc_or fm acc =
+				sat_string_acc fm acc
+			(* prop_formula -> string list -> string list *)
+			and sat_string_acc_and (And (fm1,fm2)) acc =
+				sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 acc)
+			  | sat_string_acc_and fm acc =
+				sat_string_acc fm acc
 		in
 			concat (sat_string_acc fm [])
 		end
@@ -164,7 +177,7 @@
 				"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"
+				(*"(" ^*) sat_string fm ^ "\n" (*")\n"*)
 			end)
 	end;
 
@@ -521,10 +534,11 @@
 		                    (getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else ()
 			(* both versions of zChaff appear to have the same interface, so we do *)
 			(* not actually need to distinguish between them in the following code *)
+		val satpath    = File.tmp_path (Path.unpack "isabelle.sat")
 		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
 		val outpath    = File.tmp_path (Path.unpack "result")
 		val cmd        = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
-		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
+		fun writefn fm = (SatSolver.write_dimacs_sat_file satpath fm; SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm))
 		fun readfn ()  = SatSolver.parse_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
 		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
 		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()