src/HOL/Tools/sat_solver.ML
changeset 14965 7155b319eafa
parent 14805 eff7b9df27e9
child 14999 2c39efba8f67
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Thu Jun 17 21:58:51 2004 +0200
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Thu Jun 17 22:01:23 2004 +0200
     1.3 @@ -8,14 +8,19 @@
     1.4  
     1.5  signature SAT_SOLVER =
     1.6  sig
     1.7 -	type solver  (* PropLogic.prop_formula -> (int -> bool) option option *)
     1.8 +	exception NOT_CONFIGURED
     1.9  
    1.10 -	(* external SAT solvers *)
    1.11 +	type assignment = int -> bool option
    1.12 +	datatype result = SATISFIABLE of assignment
    1.13 +	                | UNSATISFIABLE
    1.14 +	                | UNKNOWN
    1.15 +	type solver     = PropLogic.prop_formula -> result
    1.16 +
    1.17 +	(* auxiliary functions to create external SAT solvers *)
    1.18  	val write_dimacs_cnf_file : Path.T -> PropLogic.prop_formula -> unit
    1.19  	val write_dimacs_sat_file : Path.T -> PropLogic.prop_formula -> unit
    1.20 -	val parse_std_result_file : Path.T -> string -> (int -> bool) option
    1.21 -	val make_external_solver  : string -> (PropLogic.prop_formula -> unit) -> (unit -> (int -> bool) option)
    1.22 -			-> PropLogic.prop_formula -> (int -> bool) option
    1.23 +	val parse_std_result_file : Path.T -> string * string * string -> result
    1.24 +	val make_external_solver  : string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver
    1.25  
    1.26  	(* generic interface *)
    1.27  	val solvers       : (string * solver) list ref
    1.28 @@ -29,20 +34,41 @@
    1.29  	open PropLogic;
    1.30  
    1.31  (* ------------------------------------------------------------------------- *)
    1.32 -(* Type of SAT solvers: given a propositional formula, a satisfying          *)
    1.33 -(*      assignment may be returned                                           *)
    1.34 -(*      - 'Some None' means that no satisfying assignment was found          *)
    1.35 -(*      - 'None' means that the solver was not configured/installed properly *)
    1.36 +(* should be raised by an external SAT solver to indicate that the solver is *)
    1.37 +(* not configured properly                                                   *)
    1.38 +(* ------------------------------------------------------------------------- *)
    1.39 +
    1.40 +	exception NOT_CONFIGURED;
    1.41 +
    1.42 +(* ------------------------------------------------------------------------- *)
    1.43 +(* type of partial (satisfying) assignments: 'a i = None' means that 'a' is  *)
    1.44 +(*      a satisfying assigment regardless of the value of variable 'i'       *)
    1.45  (* ------------------------------------------------------------------------- *)
    1.46  
    1.47 -	type solver = prop_formula -> (int -> bool) option option;
    1.48 +	type assignment = int -> bool option;
    1.49 +
    1.50 +(* ------------------------------------------------------------------------- *)
    1.51 +(* return type of SAT solvers: if the result is 'SATISFIABLE', a satisfying  *)
    1.52 +(*      assignment must be returned as well                                  *)
    1.53 +(* ------------------------------------------------------------------------- *)
    1.54 +
    1.55 +	datatype result = SATISFIABLE of assignment
    1.56 +	                | UNSATISFIABLE
    1.57 +	                | UNKNOWN;
    1.58 +
    1.59 +(* ------------------------------------------------------------------------- *)
    1.60 +(* type of SAT solvers: given a propositional formula, a satisfying          *)
    1.61 +(*      assignment may be returned                                           *)
    1.62 +(* ------------------------------------------------------------------------- *)
    1.63 +
    1.64 +	type solver = prop_formula -> result;
    1.65  
    1.66  (* ------------------------------------------------------------------------- *)
    1.67  (* write_dimacs_cnf_file: serializes a formula 'fm' of propositional logic   *)
    1.68  (*      to a file in DIMACS CNF format (see "Satisfiability Suggested        *)
    1.69  (*      Format", May 8 1993, Section 2.1)                                    *)
    1.70  (* Note: 'fm' must not contain a variable index less than 1.                 *)
    1.71 -(* Note: 'fm' is converted into (definitional) CNF.                          *)
    1.72 +(* Note: 'fm' must be given in CNF.                                          *)
    1.73  (* ------------------------------------------------------------------------- *)
    1.74  
    1.75  	(* Path.T -> prop_formula -> unit *)
    1.76 @@ -70,22 +96,23 @@
    1.77  			(assert (i>=1) "formula contains a variable index less than 1";
    1.78  			string_of_int i)
    1.79  		  | cnf_string (Not fm) =
    1.80 -			"-" ^ (cnf_string fm)
    1.81 +			"-" ^ cnf_string fm
    1.82  		  | cnf_string (Or (fm1,fm2)) =
    1.83 -			(cnf_string fm1) ^ " " ^ (cnf_string fm2)
    1.84 +			cnf_string fm1 ^ " " ^ cnf_string fm2
    1.85  		  | cnf_string (And (fm1,fm2)) =
    1.86 -			(cnf_string fm1) ^ " 0\n" ^ (cnf_string fm2)
    1.87 +			cnf_string fm1 ^ " 0\n" ^ cnf_string fm2
    1.88  	in
    1.89  		File.write path
    1.90  			(let
    1.91 -				val cnf               = (cnf_True_False_elim o defcnf) fm  (* conversion into def. CNF *)
    1.92 -				val number_of_vars    = maxidx cnf
    1.93 -				val number_of_clauses = cnf_number_of_clauses cnf
    1.94 +				val fm'               = cnf_True_False_elim fm
    1.95 +				val number_of_vars    = maxidx fm'
    1.96 +				val number_of_clauses = cnf_number_of_clauses fm'
    1.97 +				val cnfstring         = cnf_string fm'
    1.98  			in
    1.99  				"c This file was generated by SatSolver.write_dimacs_cnf_file\n" ^
   1.100  				"c (c) Tjark Weber\n" ^
   1.101 -				"p cnf " ^ (string_of_int number_of_vars) ^ " " ^ (string_of_int number_of_clauses) ^ "\n" ^
   1.102 -				(cnf_string cnf) ^ "\n"
   1.103 +				"p cnf " ^ string_of_int number_of_vars ^ " " ^ string_of_int number_of_clauses ^ "\n" ^
   1.104 +				cnfstring ^ " 0\n"
   1.105  			end)
   1.106  	end;
   1.107  
   1.108 @@ -109,11 +136,11 @@
   1.109  			(assert (i>=1) "formula contains a variable index less than 1";
   1.110  			string_of_int i)
   1.111  		  | sat_string (Not fm) =
   1.112 -			"-(" ^ (sat_string fm) ^ ")"
   1.113 +			"-(" ^ sat_string fm ^ ")"
   1.114  		  | sat_string (Or (fm1,fm2)) =
   1.115 -			"+(" ^ (sat_string fm1) ^ " " ^ (sat_string fm2) ^ ")"
   1.116 +			"+(" ^ sat_string fm1 ^ " " ^ sat_string fm2 ^ ")"
   1.117  		  | sat_string (And (fm1,fm2)) =
   1.118 -			"*(" ^ (sat_string fm1) ^ " " ^ (sat_string fm2) ^ ")"
   1.119 +			"*(" ^ sat_string fm1 ^ " " ^ sat_string fm2 ^ ")"
   1.120  	in
   1.121  		File.write path
   1.122  			(let
   1.123 @@ -121,29 +148,28 @@
   1.124  			in
   1.125  				"c This file was generated by SatSolver.write_dimacs_sat_file\n" ^
   1.126  				"c (c) Tjark Weber\n" ^
   1.127 -				"p sat " ^ (string_of_int number_of_vars) ^ "\n" ^
   1.128 -				"(" ^ (sat_string fm) ^ ")\n"
   1.129 +				"p sat " ^ string_of_int number_of_vars ^ "\n" ^
   1.130 +				"(" ^ sat_string fm ^ ")\n"
   1.131  			end)
   1.132  	end;
   1.133  
   1.134  (* ------------------------------------------------------------------------- *)
   1.135  (* parse_std_result_file: scans a SAT solver's output file for a satisfying  *)
   1.136 -(*      variable assignment.  Returns the assignment, or 'None' if the SAT   *)
   1.137 -(*      solver did not find one.  The file format must be as follows:        *)
   1.138 -(*      ,-----                                                               *)
   1.139 -(*      | 0 or more lines not containing 'success'                           *)
   1.140 -(*      | A line containing 'success' as a substring                         *)
   1.141 -(*      | A line ASSIGNMENT containing integers, separated by " "            *)
   1.142 -(*      | 0 or more lines                                                    *)
   1.143 -(*      `-----                                                               *)
   1.144 -(*      If variable i is contained in ASSIGNMENT, then i is interpreted as   *)
   1.145 -(*      'true'.  If ~i is contained in ASSIGNMENT, then i is interpreted as  *)
   1.146 -(*      'false'.                                                             *)
   1.147 +(*      variable assignment.  Returns the assignment, or 'UNSATISFIABLE' if  *)
   1.148 +(*      the file contains 'unsatisfiable', or 'UNKNOWN' if the file contains *)
   1.149 +(*      neither 'satisfiable' nor 'unsatisfiable'.  Empty lines are ignored. *)
   1.150 +(*      The assignment must be given in one or more lines immediately after  *)
   1.151 +(*      the line that contains 'satisfiable'.  These lines must begin with   *)
   1.152 +(*      'assignment_prefix'.  Variables must be separated by " ".  Non-      *)
   1.153 +(*      integer strings are ignored.  If variable i is contained in the      *)
   1.154 +(*      assignment, then i is interpreted as 'true'.  If ~i is contained in  *)
   1.155 +(*      the assignment, then i is interpreted as 'false'.  Otherwise the     *)
   1.156 +(*      value of i is taken to be unspecified.                               *)
   1.157  (* ------------------------------------------------------------------------- *)
   1.158  
   1.159 -	(* Path.T -> string -> (int -> bool) option *)
   1.160 +	(* Path.T -> string * string * string -> result *)
   1.161  
   1.162 -	fun parse_std_result_file path success =
   1.163 +	fun parse_std_result_file path (satisfiable, assignment_prefix, unsatisfiable) =
   1.164  	let
   1.165  		(* 'a option -> 'a Library.option *)
   1.166  		fun option (SOME a) =
   1.167 @@ -153,13 +179,21 @@
   1.168  		(* string -> int list *)
   1.169  		fun int_list_from_string s =
   1.170  			mapfilter (option o Int.fromString) (space_explode " " s)
   1.171 -		(* int list -> int -> bool *)
   1.172 +		(* int list -> assignment *)
   1.173  		fun assignment_from_list [] i =
   1.174 -			false  (* could be 'true' just as well; the SAT solver didn't provide a value for this variable *)
   1.175 +			None  (* the SAT solver didn't provide a value for this variable *)
   1.176  		  | assignment_from_list (x::xs) i =
   1.177 -			if x=i then true
   1.178 -			else if x=(~i) then false
   1.179 +			if x=i then (Some true)
   1.180 +			else if x=(~i) then (Some false)
   1.181  			else assignment_from_list xs i
   1.182 +		(* int list -> string list -> assignment *)
   1.183 +		fun parse_assignment xs [] =
   1.184 +			assignment_from_list xs
   1.185 +		  | parse_assignment xs (line::lines) =
   1.186 +			if String.isPrefix assignment_prefix line then
   1.187 +				parse_assignment (xs @ int_list_from_string line) lines
   1.188 +			else
   1.189 +				assignment_from_list xs
   1.190  		(* string -> string -> bool *)
   1.191  		fun is_substring needle haystack =
   1.192  		let
   1.193 @@ -172,29 +206,28 @@
   1.194  				true
   1.195  			else is_substring needle (String.substring (haystack, 1, length2-1))
   1.196  		end
   1.197 -		(* string list -> int list option *)
   1.198 +		(* string list -> result *)
   1.199  		fun parse_lines [] =
   1.200 -			None
   1.201 +			UNKNOWN
   1.202  		  | parse_lines (line::lines) =
   1.203 -			if is_substring success line then
   1.204 -				(* the next line must be a list of integers *)
   1.205 -				(Some o assignment_from_list o int_list_from_string o hd) lines
   1.206 +			if is_substring satisfiable line then
   1.207 +				SATISFIABLE (parse_assignment [] lines)
   1.208 +			else if is_substring unsatisfiable line then
   1.209 +				UNSATISFIABLE
   1.210  			else
   1.211  				parse_lines lines
   1.212  	in
   1.213 -		(parse_lines o split_lines o File.read) path
   1.214 +		(parse_lines o (filter (fn l => l <> "")) o split_lines o File.read) path
   1.215  	end;
   1.216  
   1.217  (* ------------------------------------------------------------------------- *)
   1.218  (* make_external_solver: call 'writefn', execute 'cmd', call 'readfn'        *)
   1.219  (* ------------------------------------------------------------------------- *)
   1.220  
   1.221 -	(* string -> (prop_formula -> unit) -> (unit -> (int -> bool) option) -> prop_formula -> (int -> bool) option *)
   1.222 +	(* string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver *)
   1.223  
   1.224  	fun make_external_solver cmd writefn readfn fm =
   1.225 -		(writefn fm;
   1.226 -		assert ((system cmd)=0) ("system command " ^ quote cmd ^ " failed (make sure the SAT solver is installed)");
   1.227 -		readfn ());
   1.228 +		(writefn fm; system cmd; readfn ());
   1.229  
   1.230  (* ------------------------------------------------------------------------- *)
   1.231  (* solvers: a (reference to a) table of all registered SAT solvers           *)
   1.232 @@ -255,20 +288,20 @@
   1.233  		(* int list -> int -> bool *)
   1.234  		fun assignment_from_list xs i =
   1.235  			i mem xs
   1.236 -		(* int list -> (int -> bool) option *)
   1.237 +		(* int list -> SatSolver.result *)
   1.238  		fun solver_loop xs =
   1.239  			if PropLogic.eval (assignment_from_list xs) fm then
   1.240 -				Some (assignment_from_list xs)
   1.241 +				SatSolver.SATISFIABLE (Some o (assignment_from_list xs))
   1.242  			else
   1.243  				(case next_list xs indices of
   1.244  				  Some xs' => solver_loop xs'
   1.245 -				| None     => None)
   1.246 +				| None     => SatSolver.UNSATISFIABLE)
   1.247  	in
   1.248 -		(* start with the "first" assignment (all variables are interpreted as 'False') *)
   1.249 +		(* start with the "first" assignment (all variables are interpreted as 'false') *)
   1.250  		solver_loop []
   1.251  	end
   1.252  in
   1.253 -	SatSolver.add_solver ("enumerate", Some o enum_solver)
   1.254 +	SatSolver.add_solver ("enumerate", enum_solver)
   1.255  end;
   1.256  
   1.257  (* ------------------------------------------------------------------------- *)
   1.258 @@ -283,9 +316,9 @@
   1.259  	in
   1.260  		fun dpll_solver fm =
   1.261  		let
   1.262 -			(* We could use 'PropLogic.defcnf fm' instead of 'nnf fm', but that *)
   1.263 -			(* sometimes introduces more boolean variables than we can handle   *)
   1.264 -			(* efficiently.                                                     *)
   1.265 +			(* We could use 'PropLogic.defcnf fm' instead of 'PropLogic.nnf fm' *)
   1.266 +			(* but that sometimes introduces more boolean variables than we can *)
   1.267 +			(* handle efficiently.                                              *)
   1.268  			val fm' = PropLogic.nnf fm
   1.269  			(* int list *)
   1.270  			val indices = PropLogic.indices fm'
   1.271 @@ -342,66 +375,132 @@
   1.272  						| None      => dpll ((~x)::xs') fm'  (* now try interpreting 'x' as 'False' *)
   1.273  					end
   1.274  			end
   1.275 -			(* int list -> int -> bool *)
   1.276 +			(* int list -> assignment *)
   1.277  			fun assignment_from_list [] i =
   1.278 -				false  (* could be 'true' just as well; the DPLL procedure didn't provide a value for this variable *)
   1.279 +				None  (* the DPLL procedure didn't provide a value for this variable *)
   1.280  			  | assignment_from_list (x::xs) i =
   1.281 -				if x=i then true
   1.282 -				else if x=(~i) then false
   1.283 +				if x=i then (Some true)
   1.284 +				else if x=(~i) then (Some false)
   1.285  				else assignment_from_list xs i
   1.286  		in
   1.287  			(* initially, no variable is interpreted yet *)
   1.288 -			apsome assignment_from_list (dpll [] fm')
   1.289 +			case dpll [] fm' of
   1.290 +			  Some assignment => SatSolver.SATISFIABLE (assignment_from_list assignment)
   1.291 +			| None            => SatSolver.UNSATISFIABLE
   1.292  		end
   1.293  	end  (* local *)
   1.294  in
   1.295 -	SatSolver.add_solver ("dpll", Some o dpll_solver)
   1.296 +	SatSolver.add_solver ("dpll", dpll_solver)
   1.297  end;
   1.298  
   1.299  (* ------------------------------------------------------------------------- *)
   1.300  (* Internal SAT solver, available as 'SatSolver.invoke_solver "auto"': uses  *)
   1.301 -(* the first installed solver (other than "auto" itself)                     *)
   1.302 +(* all installed solvers (other than "auto" itself) until one returns either *)
   1.303 +(* SATISFIABLE or UNSATISFIABLE                                              *)
   1.304  (* ------------------------------------------------------------------------- *)
   1.305  
   1.306  let
   1.307  	fun auto_solver fm =
   1.308 -		get_first (fn (name,solver) =>
   1.309 +	let
   1.310 +		fun loop [] =
   1.311 +			SatSolver.UNKNOWN
   1.312 +		  | loop ((name, solver)::solvers) =
   1.313  			if name="auto" then
   1.314 -				None
   1.315 +				(* do not call solver "auto" from within "auto" *)
   1.316 +				loop solvers
   1.317  			else
   1.318 -				((if name="dpll" orelse name="enumerate" then
   1.319 +			(
   1.320 +				(if name="dpll" orelse name="enumerate" then
   1.321  					warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.")
   1.322  				else
   1.323  					());
   1.324 -				solver fm)) (rev (!SatSolver.solvers))
   1.325 +				(* apply 'solver' to 'fm' *)
   1.326 +				(case solver fm of
   1.327 +				  SatSolver.SATISFIABLE a => SatSolver.SATISFIABLE a
   1.328 +				| SatSolver.UNSATISFIABLE => SatSolver.UNSATISFIABLE
   1.329 +				| SatSolver.UNKNOWN       => loop solvers)
   1.330 +				handle SatSolver.NOT_CONFIGURED => loop solvers
   1.331 +			)
   1.332 +	in
   1.333 +		loop (rev (!SatSolver.solvers))
   1.334 +	end
   1.335  in
   1.336  	SatSolver.add_solver ("auto", auto_solver)
   1.337  end;
   1.338  
   1.339  (* ------------------------------------------------------------------------- *)
   1.340 -(* ZChaff, Version 2003.12.04                                                *)
   1.341 +(* ZChaff, Version 2003.12.04 (http://www.princeton.edu/~chaff/zchaff.html)  *)
   1.342  (* ------------------------------------------------------------------------- *)
   1.343  
   1.344  let
   1.345  	fun zchaff fm =
   1.346  	let
   1.347 -		val inname     = "isabelle.cnf"
   1.348 -		val outname    = "result"
   1.349 -		val inpath     = File.tmp_path (Path.unpack inname)
   1.350 -		val outpath    = File.tmp_path (Path.unpack outname)
   1.351 +		val _          = if (getenv "ZCHAFF_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
   1.352 +		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
   1.353 +		val outpath    = File.tmp_path (Path.unpack "result")
   1.354  		val cmd        = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
   1.355 -		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm
   1.356 -		fun readfn ()  = SatSolver.parse_std_result_file outpath "Verify Solution successful. Instance satisfiable"
   1.357 +		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
   1.358 +		fun readfn ()  = SatSolver.parse_std_result_file outpath ("Verify Solution successful. Instance satisfiable", "", "Instance unsatisfiable")
   1.359  		val _          = assert (not (File.exists inpath)) ("file " ^ quote (Path.pack inpath) ^ " exists, please delete (will not overwrite)")
   1.360  		val _          = assert (not (File.exists outpath)) ("file " ^ quote (Path.pack outpath) ^ " exists, please delete (will not overwrite)")
   1.361 -		val assignment = SatSolver.make_external_solver cmd writefn readfn fm
   1.362 +		val result     = SatSolver.make_external_solver cmd writefn readfn fm
   1.363  		val _          = (File.rm inpath handle _ => ())
   1.364  		val _          = (File.rm outpath handle _ => ())
   1.365  	in
   1.366 -		assignment
   1.367 +		result
   1.368  	end
   1.369  in
   1.370 -		SatSolver.add_solver ("zchaff", (fn fm => if getenv "ZCHAFF_HOME" <> "" then Some (zchaff fm) else None))
   1.371 +	SatSolver.add_solver ("zchaff", zchaff)
   1.372 +end;
   1.373 +
   1.374 +(* ------------------------------------------------------------------------- *)
   1.375 +(* BerkMin 561 (http://eigold.tripod.com/BerkMin.html)                       *)
   1.376 +(* ------------------------------------------------------------------------- *)
   1.377 +
   1.378 +let
   1.379 +	fun berkmin fm =
   1.380 +	let
   1.381 +		val _          = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else ()
   1.382 +		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
   1.383 +		val outpath    = File.tmp_path (Path.unpack "result")
   1.384 +		val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
   1.385 +		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
   1.386 +		fun readfn ()  = SatSolver.parse_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
   1.387 +		val _          = assert (not (File.exists inpath)) ("file " ^ quote (Path.pack inpath) ^ " exists, please delete (will not overwrite)")
   1.388 +		val _          = assert (not (File.exists outpath)) ("file " ^ quote (Path.pack outpath) ^ " exists, please delete (will not overwrite)")
   1.389 +		val result     = SatSolver.make_external_solver cmd writefn readfn fm
   1.390 +		val _          = (File.rm inpath handle _ => ())
   1.391 +		val _          = (File.rm outpath handle _ => ())
   1.392 +	in
   1.393 +		result
   1.394 +	end
   1.395 +in
   1.396 +	SatSolver.add_solver ("berkmin", berkmin)
   1.397 +end;
   1.398 +
   1.399 +(* ------------------------------------------------------------------------- *)
   1.400 +(* Jerusat 1.3 (http://www.cs.tau.ac.il/~ale1/)                              *)
   1.401 +(* ------------------------------------------------------------------------- *)
   1.402 +
   1.403 +let
   1.404 +	fun jerusat fm =
   1.405 +	let
   1.406 +		val _          = if (getenv "JERUSAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
   1.407 +		val inpath     = File.tmp_path (Path.unpack "isabelle.cnf")
   1.408 +		val outpath    = File.tmp_path (Path.unpack "result")
   1.409 +		val cmd        = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
   1.410 +		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
   1.411 +		fun readfn ()  = SatSolver.parse_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
   1.412 +		val _          = assert (not (File.exists inpath)) ("file " ^ quote (Path.pack inpath) ^ " exists, please delete (will not overwrite)")
   1.413 +		val _          = assert (not (File.exists outpath)) ("file " ^ quote (Path.pack outpath) ^ " exists, please delete (will not overwrite)")
   1.414 +		val result     = SatSolver.make_external_solver cmd writefn readfn fm
   1.415 +		val _          = (File.rm inpath handle _ => ())
   1.416 +		val _          = (File.rm outpath handle _ => ())
   1.417 +	in
   1.418 +		result
   1.419 +	end
   1.420 +in
   1.421 +	SatSolver.add_solver ("jerusat", jerusat)
   1.422  end;
   1.423  
   1.424  (* ------------------------------------------------------------------------- *)
   1.425 @@ -412,7 +511,7 @@
   1.426  let
   1.427  	fun mysolver fm = ...
   1.428  in
   1.429 -	SatSolver.add_solver ("myname", (fn fm => if mysolver_is_installed then Some (mysolver fm) else None));  -- register the solver
   1.430 +	SatSolver.add_solver ("myname", (fn fm => if mysolver_is_configured then mysolver fm else raise SatSolver.NOT_CONFIGURED));  -- register the solver
   1.431  end;
   1.432  
   1.433  -- the solver is now available as SatSolver.invoke_solver "myname"