Installed solvers now determined at call time (as opposed to compile time)
authorwebertj
Fri Mar 26 12:21:50 2004 +0100 (2004-03-26)
changeset 14487157d0ea7b2da
parent 14486 74c053a25513
child 14488 863258b0cdca
Installed solvers now determined at call time (as opposed to compile time)
src/HOL/Tools/sat_solver.ML
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Fri Mar 26 05:32:00 2004 +0100
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Fri Mar 26 12:21:50 2004 +0100
     1.3 @@ -8,19 +8,19 @@
     1.4  
     1.5  signature SAT_SOLVER =
     1.6  sig
     1.7 -	type solver  (* PropLogic.prop_formula -> (int -> bool) option *)
     1.8 +	type solver  (* PropLogic.prop_formula -> (int -> bool) option option *)
     1.9  
    1.10  	(* external SAT solvers *)
    1.11  	val write_dimacs_cnf_file : Path.T -> PropLogic.prop_formula -> unit
    1.12  	val write_dimacs_sat_file : Path.T -> PropLogic.prop_formula -> unit
    1.13  	val parse_std_result_file : Path.T -> string -> (int -> bool) option
    1.14 -	val make_external_solver  : string -> (PropLogic.prop_formula -> unit) -> (unit -> (int -> bool) option) -> solver
    1.15 +	val make_external_solver  : string -> (PropLogic.prop_formula -> unit) -> (unit -> (int -> bool) option)
    1.16 +			-> PropLogic.prop_formula -> (int -> bool) option
    1.17  
    1.18  	(* generic interface *)
    1.19 -	val solvers       : (solver Symtab.table) ref
    1.20 -	val add_solver    : string * solver -> unit  (* exception DUP *)
    1.21 -	val invoke_solver : string -> solver         (* exception OPTION *)
    1.22 -	val preferred     : string ref
    1.23 +	val solvers       : (string * solver) list ref
    1.24 +	val add_solver    : string * solver -> unit
    1.25 +	val invoke_solver : string -> solver  (* exception OPTION *)
    1.26  end;
    1.27  
    1.28  structure SatSolver : SAT_SOLVER =
    1.29 @@ -31,9 +31,11 @@
    1.30  (* ------------------------------------------------------------------------- *)
    1.31  (* Type of SAT solvers: given a propositional formula, a satisfying          *)
    1.32  (*      assignment may be returned                                           *)
    1.33 +(*      - 'Some None' means that no satisfying assignment was found          *)
    1.34 +(*      - 'None' means that the solver was not configured/installed properly *)
    1.35  (* ------------------------------------------------------------------------- *)
    1.36  
    1.37 -	type solver = prop_formula -> (int -> bool) option;
    1.38 +	type solver = prop_formula -> (int -> bool) option option;
    1.39  
    1.40  (* ------------------------------------------------------------------------- *)
    1.41  (* write_dimacs_cnf_file: serializes a formula 'fm' of propositional logic   *)
    1.42 @@ -187,7 +189,7 @@
    1.43  (* make_external_solver: call 'writefn', execute 'cmd', call 'readfn'        *)
    1.44  (* ------------------------------------------------------------------------- *)
    1.45  
    1.46 -	(* string -> (prop_formula -> unit) -> (unit -> (int -> bool) option) -> solver *)
    1.47 +	(* string -> (prop_formula -> unit) -> (unit -> (int -> bool) option) -> prop_formula -> (int -> bool) option *)
    1.48  
    1.49  	fun make_external_solver cmd writefn readfn fm =
    1.50  		(writefn fm;
    1.51 @@ -198,18 +200,16 @@
    1.52  (* solvers: a (reference to a) table of all registered SAT solvers           *)
    1.53  (* ------------------------------------------------------------------------- *)
    1.54  
    1.55 -	val solvers = ref (Symtab.empty : solver Symtab.table);
    1.56 +	val solvers = ref ([] : (string * solver) list);
    1.57  
    1.58  (* ------------------------------------------------------------------------- *)
    1.59  (* add_solver: updates 'solvers' by adding a new solver                      *)
    1.60 -(* Note: No two solvers may have the same 'name'; otherwise exception 'DUP'  *)
    1.61 -(*       will be raised.                                                     *)
    1.62  (* ------------------------------------------------------------------------- *)
    1.63  
    1.64  	(* string * solver -> unit *)
    1.65  
    1.66  	fun add_solver (name, new_solver) =
    1.67 -		(solvers := Symtab.update_new ((name, new_solver), !solvers));
    1.68 +		(solvers := overwrite_warn (!solvers, (name, new_solver)) ("SAT solver " ^ quote name ^ " was defined before"));
    1.69  
    1.70  (* ------------------------------------------------------------------------- *)
    1.71  (* invoke_solver: returns the solver associated with the given 'name'        *)
    1.72 @@ -220,13 +220,7 @@
    1.73  	(* string -> solver *)
    1.74  
    1.75  	fun invoke_solver name =
    1.76 -		(the o Symtab.lookup) (!solvers, name);
    1.77 -
    1.78 -(* ------------------------------------------------------------------------- *)
    1.79 -(* preferred: the name of the preferred SAT solver                           *)
    1.80 -(* ------------------------------------------------------------------------- *)
    1.81 -
    1.82 -	val preferred = ref "";
    1.83 +		(the o assoc) (!solvers, name);
    1.84  
    1.85  end;  (* SatSolver *)
    1.86  
    1.87 @@ -274,7 +268,7 @@
    1.88  		solver_loop []
    1.89  	end
    1.90  in
    1.91 -	SatSolver.add_solver ("enumerate", enum_solver)
    1.92 +	SatSolver.add_solver ("enumerate", Some o enum_solver)
    1.93  end;
    1.94  
    1.95  (* ------------------------------------------------------------------------- *)
    1.96 @@ -359,33 +353,25 @@
    1.97  		end
    1.98  	end  (* local *)
    1.99  in
   1.100 -	SatSolver.add_solver ("dpll", dpll_solver);
   1.101 -	SatSolver.preferred := "dpll"
   1.102 +	SatSolver.add_solver ("dpll", Some o dpll_solver)
   1.103  end;
   1.104  
   1.105  (* ------------------------------------------------------------------------- *)
   1.106  (* Internal SAT solver, available as 'SatSolver.solve "auto"': uses the      *)
   1.107 -(* preferred solver, or "dpll" if the preferred solver isn't present         *)
   1.108 +(* first installed solver (other than "auto" itself)                         *)
   1.109  (* ------------------------------------------------------------------------- *)
   1.110  
   1.111  let
   1.112  	fun auto_solver fm =
   1.113 -	let
   1.114 -		val preferred = !SatSolver.preferred
   1.115 -		val fallback  = "dpll"
   1.116 -	in
   1.117 -		if preferred="auto" then  (* prevent infinite recursion *)
   1.118 -			(warning ("Preferred SAT solver \"auto\": using solver " ^ quote fallback ^ " instead.");
   1.119 -			SatSolver.invoke_solver fallback fm)
   1.120 -		else if preferred=fallback then
   1.121 -			(warning ("Preferred SAT solver is " ^ quote fallback ^ "; for better performance, consider using an external solver.");
   1.122 -			SatSolver.invoke_solver fallback fm)
   1.123 -		else
   1.124 -			(SatSolver.invoke_solver preferred fm
   1.125 -			handle OPTION =>
   1.126 -				(warning ("Preferred SAT solver " ^ quote preferred ^ " not installed; using solver " ^ quote fallback ^ " instead.");
   1.127 -				SatSolver.invoke_solver fallback fm))
   1.128 -	end
   1.129 +		get_first (fn (name,solver) =>
   1.130 +			if name="auto" then
   1.131 +				None
   1.132 +			else
   1.133 +				((if name="dpll" then
   1.134 +					warning ("Using SAT solver \"dpll\"; for better performance, consider using an external solver.")
   1.135 +				else
   1.136 +					());
   1.137 +				solver fm)) (rev (!SatSolver.solvers))
   1.138  in
   1.139  	SatSolver.add_solver ("auto", auto_solver)
   1.140  end;
   1.141 @@ -394,7 +380,8 @@
   1.142  (* ZChaff, Version 2003.12.04                                                *)
   1.143  (* ------------------------------------------------------------------------- *)
   1.144  
   1.145 -if getenv "ZCHAFF_HOME" <> "" then
   1.146 +let
   1.147 +	fun zchaff fm =
   1.148  	let
   1.149  		val inname     = "isabelle.cnf"
   1.150  		val outname    = "result"
   1.151 @@ -403,37 +390,28 @@
   1.152  		val cmd        = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
   1.153  		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm
   1.154  		fun readfn ()  = SatSolver.parse_std_result_file outpath "Verify Solution successful. Instance satisfiable"
   1.155 -		fun zchaff fm =
   1.156 -		let
   1.157 -			val _          = assert (not (File.exists inpath)) ("file " ^ quote (Path.pack inpath) ^ " exists, please delete (will not overwrite)")
   1.158 -			val _          = assert (not (File.exists outpath)) ("file " ^ quote (Path.pack outpath) ^ " exists, please delete (will not overwrite)")
   1.159 -			val assignment = SatSolver.make_external_solver cmd writefn readfn fm
   1.160 -			val _          = (File.rm inpath handle _ => ())
   1.161 -			val _          = (File.rm outpath handle _ => ())
   1.162 -		in
   1.163 -			assignment
   1.164 -		end
   1.165 +		val _          = assert (not (File.exists inpath)) ("file " ^ quote (Path.pack inpath) ^ " exists, please delete (will not overwrite)")
   1.166 +		val _          = assert (not (File.exists outpath)) ("file " ^ quote (Path.pack outpath) ^ " exists, please delete (will not overwrite)")
   1.167 +		val assignment = SatSolver.make_external_solver cmd writefn readfn fm
   1.168 +		val _          = (File.rm inpath handle _ => ())
   1.169 +		val _          = (File.rm outpath handle _ => ())
   1.170  	in
   1.171 -		SatSolver.add_solver ("zchaff", zchaff);
   1.172 -		SatSolver.preferred := "zchaff"
   1.173 +		assignment
   1.174  	end
   1.175 -else
   1.176 -	();
   1.177 +in
   1.178 +		SatSolver.add_solver ("zchaff", (fn fm => if getenv "ZCHAFF_HOME" <> "" then Some (zchaff fm) else None))
   1.179 +end;
   1.180  
   1.181  (* ------------------------------------------------------------------------- *)
   1.182  (* Add code for other SAT solvers below.                                     *)
   1.183  (* ------------------------------------------------------------------------- *)
   1.184  
   1.185  (*
   1.186 -if mysolver_is_installed then
   1.187 -	let
   1.188 -		fun mysolver fm = ...
   1.189 -	in
   1.190 -		SatSolver.add_solver ("myname", mysolver);  -- register the solver
   1.191 -		SatSolver.preferred := "myname"             -- make it the preferred solver (optional)
   1.192 -	end
   1.193 -else
   1.194 -	();
   1.195 +let
   1.196 +	fun mysolver fm = ...
   1.197 +in
   1.198 +	SatSolver.add_solver ("myname", (fn fm => if mysolver_is_installed then Some (mysolver fm) else None));  -- register the solver
   1.199 +end;
   1.200  
   1.201  -- the solver is now available as SatSolver.invoke_solver "myname"
   1.202  *)