src/HOL/Tools/sat_solver.ML
changeset 22567 1565d476a9e2
parent 22220 6dc8d0dca678
child 29872 14e208d607af
     1.1 --- a/src/HOL/Tools/sat_solver.ML	Tue Apr 03 19:24:10 2007 +0200
     1.2 +++ b/src/HOL/Tools/sat_solver.ML	Tue Apr 03 19:24:11 2007 +0200
     1.3 @@ -8,47 +8,47 @@
     1.4  
     1.5  signature SAT_SOLVER =
     1.6  sig
     1.7 -	exception NOT_CONFIGURED
     1.8 +  exception NOT_CONFIGURED
     1.9  
    1.10 -	type assignment = int -> bool option
    1.11 -	type proof      = int list Inttab.table * int
    1.12 -	datatype result = SATISFIABLE of assignment
    1.13 -	                | UNSATISFIABLE of proof option
    1.14 -	                | UNKNOWN
    1.15 -	type solver     = PropLogic.prop_formula -> result
    1.16 +  type assignment = int -> bool option
    1.17 +  type proof      = int list Inttab.table * int
    1.18 +  datatype result = SATISFIABLE of assignment
    1.19 +                  | UNSATISFIABLE of proof option
    1.20 +                  | UNKNOWN
    1.21 +  type solver     = PropLogic.prop_formula -> result
    1.22  
    1.23 -	(* auxiliary functions to create external SAT solvers *)
    1.24 -	val write_dimacs_cnf_file : Path.T -> PropLogic.prop_formula -> unit
    1.25 -	val write_dimacs_sat_file : Path.T -> PropLogic.prop_formula -> unit
    1.26 -	val read_std_result_file  : Path.T -> string * string * string -> result
    1.27 -	val make_external_solver  : string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver
    1.28 +  (* auxiliary functions to create external SAT solvers *)
    1.29 +  val write_dimacs_cnf_file : Path.T -> PropLogic.prop_formula -> unit
    1.30 +  val write_dimacs_sat_file : Path.T -> PropLogic.prop_formula -> unit
    1.31 +  val read_std_result_file  : Path.T -> string * string * string -> result
    1.32 +  val make_external_solver  : string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver
    1.33  
    1.34 -	val read_dimacs_cnf_file : Path.T -> PropLogic.prop_formula
    1.35 +  val read_dimacs_cnf_file : Path.T -> PropLogic.prop_formula
    1.36  
    1.37 -	(* generic solver interface *)
    1.38 -	val solvers       : (string * solver) list ref
    1.39 -	val add_solver    : string * solver -> unit
    1.40 -	val invoke_solver : string -> solver  (* exception Option *)
    1.41 +  (* generic solver interface *)
    1.42 +  val solvers       : (string * solver) list ref
    1.43 +  val add_solver    : string * solver -> unit
    1.44 +  val invoke_solver : string -> solver  (* exception Option *)
    1.45  end;
    1.46  
    1.47  structure SatSolver : SAT_SOLVER =
    1.48  struct
    1.49  
    1.50 -	open PropLogic;
    1.51 +  open PropLogic;
    1.52  
    1.53  (* ------------------------------------------------------------------------- *)
    1.54  (* should be raised by an external SAT solver to indicate that the solver is *)
    1.55  (* not configured properly                                                   *)
    1.56  (* ------------------------------------------------------------------------- *)
    1.57  
    1.58 -	exception NOT_CONFIGURED;
    1.59 +  exception NOT_CONFIGURED;
    1.60  
    1.61  (* ------------------------------------------------------------------------- *)
    1.62  (* type of partial (satisfying) assignments: 'a i = NONE' means that 'a' is  *)
    1.63  (*      a satisfying assignment regardless of the value of variable 'i'      *)
    1.64  (* ------------------------------------------------------------------------- *)
    1.65  
    1.66 -	type assignment = int -> bool option;
    1.67 +  type assignment = int -> bool option;
    1.68  
    1.69  (* ------------------------------------------------------------------------- *)
    1.70  (* a proof of unsatisfiability, to be interpreted as follows: each integer   *)
    1.71 @@ -65,7 +65,7 @@
    1.72  (*      but do not need to be consecutive.                                   *)
    1.73  (* ------------------------------------------------------------------------- *)
    1.74  
    1.75 -	type proof = int list Inttab.table * int;
    1.76 +  type proof = int list Inttab.table * int;
    1.77  
    1.78  (* ------------------------------------------------------------------------- *)
    1.79  (* return type of SAT solvers: if the result is 'SATISFIABLE', a satisfying  *)
    1.80 @@ -73,16 +73,16 @@
    1.81  (*      'UNSATISFIABLE', a proof of unsatisfiability may be returned         *)
    1.82  (* ------------------------------------------------------------------------- *)
    1.83  
    1.84 -	datatype result = SATISFIABLE of assignment
    1.85 -	                | UNSATISFIABLE of proof option
    1.86 -	                | UNKNOWN;
    1.87 +  datatype result = SATISFIABLE of assignment
    1.88 +                  | UNSATISFIABLE of proof option
    1.89 +                  | UNKNOWN;
    1.90  
    1.91  (* ------------------------------------------------------------------------- *)
    1.92  (* type of SAT solvers: given a propositional formula, a satisfying          *)
    1.93  (*      assignment may be returned                                           *)
    1.94  (* ------------------------------------------------------------------------- *)
    1.95  
    1.96 -	type solver = prop_formula -> result;
    1.97 +  type solver = prop_formula -> result;
    1.98  
    1.99  (* ------------------------------------------------------------------------- *)
   1.100  (* write_dimacs_cnf_file: serializes a formula 'fm' of propositional logic   *)
   1.101 @@ -92,56 +92,56 @@
   1.102  (* Note: 'fm' must be given in CNF.                                          *)
   1.103  (* ------------------------------------------------------------------------- *)
   1.104  
   1.105 -	(* Path.T -> prop_formula -> unit *)
   1.106 +  (* Path.T -> prop_formula -> unit *)
   1.107  
   1.108 -	fun write_dimacs_cnf_file path fm =
   1.109 -	let
   1.110 -		(* prop_formula -> prop_formula *)
   1.111 -		fun cnf_True_False_elim True =
   1.112 -			Or (BoolVar 1, Not (BoolVar 1))
   1.113 -		  | cnf_True_False_elim False =
   1.114 -			And (BoolVar 1, Not (BoolVar 1))
   1.115 -		  | cnf_True_False_elim fm =
   1.116 -			fm  (* since 'fm' is in CNF, either 'fm'='True'/'False', or 'fm' does not contain 'True'/'False' at all *)
   1.117 -		(* prop_formula -> int *)
   1.118 -		fun cnf_number_of_clauses (And (fm1,fm2)) =
   1.119 -			(cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2)
   1.120 -		  | cnf_number_of_clauses _ =
   1.121 -			1
   1.122 -		(* prop_formula -> string list *)
   1.123 -		fun cnf_string fm =
   1.124 -		let
   1.125 -			(* prop_formula -> string list -> string list *)
   1.126 -			fun cnf_string_acc True acc =
   1.127 -				error "formula is not in CNF"
   1.128 -			  | cnf_string_acc False acc =
   1.129 -				error "formula is not in CNF"
   1.130 -			  | cnf_string_acc (BoolVar i) acc =
   1.131 -				(assert (i>=1) "formula contains a variable index less than 1";
   1.132 -				string_of_int i :: acc)
   1.133 -			  | cnf_string_acc (Not (BoolVar i)) acc =
   1.134 -				"-" :: cnf_string_acc (BoolVar i) acc
   1.135 -			  | cnf_string_acc (Not _) acc =
   1.136 -				error "formula is not in CNF"
   1.137 -			  | cnf_string_acc (Or (fm1,fm2)) acc =
   1.138 -				cnf_string_acc fm1 (" " :: cnf_string_acc fm2 acc)
   1.139 -			  | cnf_string_acc (And (fm1,fm2)) acc =
   1.140 -				cnf_string_acc fm1 (" 0\n" :: cnf_string_acc fm2 acc)
   1.141 -		in
   1.142 -			cnf_string_acc fm []
   1.143 -		end
   1.144 -		val fm'               = cnf_True_False_elim fm
   1.145 -		val number_of_vars    = maxidx fm'
   1.146 -		val number_of_clauses = cnf_number_of_clauses fm'
   1.147 -	in
   1.148 -		File.write path
   1.149 -			("c This file was generated by SatSolver.write_dimacs_cnf_file\n" ^
   1.150 -			 "p cnf " ^ string_of_int number_of_vars ^ " " ^ string_of_int number_of_clauses ^ "\n");
   1.151 -		File.append_list path
   1.152 -			(cnf_string fm');
   1.153 -		File.append path
   1.154 -			" 0\n"
   1.155 -	end;
   1.156 +  fun write_dimacs_cnf_file path fm =
   1.157 +  let
   1.158 +    (* prop_formula -> prop_formula *)
   1.159 +    fun cnf_True_False_elim True =
   1.160 +      Or (BoolVar 1, Not (BoolVar 1))
   1.161 +      | cnf_True_False_elim False =
   1.162 +      And (BoolVar 1, Not (BoolVar 1))
   1.163 +      | cnf_True_False_elim fm =
   1.164 +      fm  (* since 'fm' is in CNF, either 'fm'='True'/'False', or 'fm' does not contain 'True'/'False' at all *)
   1.165 +    (* prop_formula -> int *)
   1.166 +    fun cnf_number_of_clauses (And (fm1,fm2)) =
   1.167 +      (cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2)
   1.168 +      | cnf_number_of_clauses _ =
   1.169 +      1
   1.170 +    (* prop_formula -> string list *)
   1.171 +    fun cnf_string fm =
   1.172 +    let
   1.173 +      (* prop_formula -> string list -> string list *)
   1.174 +      fun cnf_string_acc True acc =
   1.175 +        error "formula is not in CNF"
   1.176 +        | cnf_string_acc False acc =
   1.177 +        error "formula is not in CNF"
   1.178 +        | cnf_string_acc (BoolVar i) acc =
   1.179 +        (i>=1 orelse error "formula contains a variable index less than 1";
   1.180 +        string_of_int i :: acc)
   1.181 +        | cnf_string_acc (Not (BoolVar i)) acc =
   1.182 +        "-" :: cnf_string_acc (BoolVar i) acc
   1.183 +        | cnf_string_acc (Not _) acc =
   1.184 +        error "formula is not in CNF"
   1.185 +        | cnf_string_acc (Or (fm1,fm2)) acc =
   1.186 +        cnf_string_acc fm1 (" " :: cnf_string_acc fm2 acc)
   1.187 +        | cnf_string_acc (And (fm1,fm2)) acc =
   1.188 +        cnf_string_acc fm1 (" 0\n" :: cnf_string_acc fm2 acc)
   1.189 +    in
   1.190 +      cnf_string_acc fm []
   1.191 +    end
   1.192 +    val fm'               = cnf_True_False_elim fm
   1.193 +    val number_of_vars    = maxidx fm'
   1.194 +    val number_of_clauses = cnf_number_of_clauses fm'
   1.195 +  in
   1.196 +    File.write path
   1.197 +      ("c This file was generated by SatSolver.write_dimacs_cnf_file\n" ^
   1.198 +       "p cnf " ^ string_of_int number_of_vars ^ " " ^ string_of_int number_of_clauses ^ "\n");
   1.199 +    File.append_list path
   1.200 +      (cnf_string fm');
   1.201 +    File.append path
   1.202 +      " 0\n"
   1.203 +  end;
   1.204  
   1.205  (* ------------------------------------------------------------------------- *)
   1.206  (* write_dimacs_sat_file: serializes a formula 'fm' of propositional logic   *)
   1.207 @@ -150,54 +150,54 @@
   1.208  (* Note: 'fm' must not contain a variable index less than 1.                 *)
   1.209  (* ------------------------------------------------------------------------- *)
   1.210  
   1.211 -	(* Path.T -> prop_formula -> unit *)
   1.212 +  (* Path.T -> prop_formula -> unit *)
   1.213  
   1.214 -	fun write_dimacs_sat_file path fm =
   1.215 -	let
   1.216 -		(* prop_formula -> string list *)
   1.217 -		fun sat_string fm =
   1.218 -		let
   1.219 -			(* prop_formula -> string list -> string list *)
   1.220 -			fun sat_string_acc True acc =
   1.221 -				"*()" :: acc
   1.222 -			  | sat_string_acc False acc =
   1.223 -				"+()" :: acc
   1.224 -			  | sat_string_acc (BoolVar i) acc =
   1.225 -				(assert (i>=1) "formula contains a variable index less than 1";
   1.226 -				string_of_int i :: acc)
   1.227 -			  | sat_string_acc (Not (BoolVar i)) acc =
   1.228 -				"-" :: sat_string_acc (BoolVar i) acc
   1.229 -			  | sat_string_acc (Not fm) acc =
   1.230 -				"-(" :: sat_string_acc fm (")" :: acc)
   1.231 -			  | sat_string_acc (Or (fm1,fm2)) acc =
   1.232 -				"+(" :: sat_string_acc_or fm1 (" " :: sat_string_acc_or fm2 (")" :: acc))
   1.233 -			  | sat_string_acc (And (fm1,fm2)) acc =
   1.234 -				"*(" :: sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 (")" :: acc))
   1.235 -			(* optimization to make use of n-ary disjunction/conjunction *)
   1.236 -			(* prop_formula -> string list -> string list *)
   1.237 -			and sat_string_acc_or (Or (fm1,fm2)) acc =
   1.238 -				sat_string_acc_or fm1 (" " :: sat_string_acc_or fm2 acc)
   1.239 -			  | sat_string_acc_or fm acc =
   1.240 -				sat_string_acc fm acc
   1.241 -			(* prop_formula -> string list -> string list *)
   1.242 -			and sat_string_acc_and (And (fm1,fm2)) acc =
   1.243 -				sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 acc)
   1.244 -			  | sat_string_acc_and fm acc =
   1.245 -				sat_string_acc fm acc
   1.246 -		in
   1.247 -			sat_string_acc fm []
   1.248 -		end
   1.249 -		val number_of_vars = Int.max (maxidx fm, 1)
   1.250 -	in
   1.251 -		File.write path
   1.252 -			("c This file was generated by SatSolver.write_dimacs_sat_file\n" ^
   1.253 -			 "p sat " ^ string_of_int number_of_vars ^ "\n" ^
   1.254 -			 "(");
   1.255 -		File.append_list path
   1.256 -			(sat_string fm);
   1.257 -		File.append path
   1.258 -			")\n"
   1.259 -	end;
   1.260 +  fun write_dimacs_sat_file path fm =
   1.261 +  let
   1.262 +    (* prop_formula -> string list *)
   1.263 +    fun sat_string fm =
   1.264 +    let
   1.265 +      (* prop_formula -> string list -> string list *)
   1.266 +      fun sat_string_acc True acc =
   1.267 +        "*()" :: acc
   1.268 +        | sat_string_acc False acc =
   1.269 +        "+()" :: acc
   1.270 +        | sat_string_acc (BoolVar i) acc =
   1.271 +        (i>=1 orelse error "formula contains a variable index less than 1";
   1.272 +        string_of_int i :: acc)
   1.273 +        | sat_string_acc (Not (BoolVar i)) acc =
   1.274 +        "-" :: sat_string_acc (BoolVar i) acc
   1.275 +        | sat_string_acc (Not fm) acc =
   1.276 +        "-(" :: sat_string_acc fm (")" :: acc)
   1.277 +        | sat_string_acc (Or (fm1,fm2)) acc =
   1.278 +        "+(" :: sat_string_acc_or fm1 (" " :: sat_string_acc_or fm2 (")" :: acc))
   1.279 +        | sat_string_acc (And (fm1,fm2)) acc =
   1.280 +        "*(" :: sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 (")" :: acc))
   1.281 +      (* optimization to make use of n-ary disjunction/conjunction *)
   1.282 +      (* prop_formula -> string list -> string list *)
   1.283 +      and sat_string_acc_or (Or (fm1,fm2)) acc =
   1.284 +        sat_string_acc_or fm1 (" " :: sat_string_acc_or fm2 acc)
   1.285 +        | sat_string_acc_or fm acc =
   1.286 +        sat_string_acc fm acc
   1.287 +      (* prop_formula -> string list -> string list *)
   1.288 +      and sat_string_acc_and (And (fm1,fm2)) acc =
   1.289 +        sat_string_acc_and fm1 (" " :: sat_string_acc_and fm2 acc)
   1.290 +        | sat_string_acc_and fm acc =
   1.291 +        sat_string_acc fm acc
   1.292 +    in
   1.293 +      sat_string_acc fm []
   1.294 +    end
   1.295 +    val number_of_vars = Int.max (maxidx fm, 1)
   1.296 +  in
   1.297 +    File.write path
   1.298 +      ("c This file was generated by SatSolver.write_dimacs_sat_file\n" ^
   1.299 +       "p sat " ^ string_of_int number_of_vars ^ "\n" ^
   1.300 +       "(");
   1.301 +    File.append_list path
   1.302 +      (sat_string fm);
   1.303 +    File.append path
   1.304 +      ")\n"
   1.305 +  end;
   1.306  
   1.307  (* ------------------------------------------------------------------------- *)
   1.308  (* read_std_result_file: scans a SAT solver's output file for a satisfying   *)
   1.309 @@ -213,149 +213,149 @@
   1.310  (*      value of i is taken to be unspecified.                               *)
   1.311  (* ------------------------------------------------------------------------- *)
   1.312  
   1.313 -	(* Path.T -> string * string * string -> result *)
   1.314 +  (* Path.T -> string * string * string -> result *)
   1.315  
   1.316 -	fun read_std_result_file path (satisfiable, assignment_prefix, unsatisfiable) =
   1.317 -	let
   1.318 -		(* string -> int list *)
   1.319 -		fun int_list_from_string s =
   1.320 -			List.mapPartial Int.fromString (space_explode " " s)
   1.321 -		(* int list -> assignment *)
   1.322 -		fun assignment_from_list [] i =
   1.323 -			NONE  (* the SAT solver didn't provide a value for this variable *)
   1.324 -		  | assignment_from_list (x::xs) i =
   1.325 -			if x=i then (SOME true)
   1.326 -			else if x=(~i) then (SOME false)
   1.327 -			else assignment_from_list xs i
   1.328 -		(* int list -> string list -> assignment *)
   1.329 -		fun parse_assignment xs [] =
   1.330 -			assignment_from_list xs
   1.331 -		  | parse_assignment xs (line::lines) =
   1.332 -			if String.isPrefix assignment_prefix line then
   1.333 -				parse_assignment (xs @ int_list_from_string line) lines
   1.334 -			else
   1.335 -				assignment_from_list xs
   1.336 -		(* string -> string -> bool *)
   1.337 -		fun is_substring needle haystack =
   1.338 -		let
   1.339 -			val length1 = String.size needle
   1.340 -			val length2 = String.size haystack
   1.341 -		in
   1.342 -			if length2 < length1 then
   1.343 -				false
   1.344 -			else if needle = String.substring (haystack, 0, length1) then
   1.345 -				true
   1.346 -			else is_substring needle (String.substring (haystack, 1, length2-1))
   1.347 -		end
   1.348 -		(* string list -> result *)
   1.349 -		fun parse_lines [] =
   1.350 -			UNKNOWN
   1.351 -		  | parse_lines (line::lines) =
   1.352 -			if is_substring unsatisfiable line then
   1.353 -				UNSATISFIABLE NONE
   1.354 -			else if is_substring satisfiable line then
   1.355 -				SATISFIABLE (parse_assignment [] lines)
   1.356 -			else
   1.357 -				parse_lines lines
   1.358 -	in
   1.359 -		(parse_lines o (List.filter (fn l => l <> "")) o split_lines o File.read) path
   1.360 -	end;
   1.361 +  fun read_std_result_file path (satisfiable, assignment_prefix, unsatisfiable) =
   1.362 +  let
   1.363 +    (* string -> int list *)
   1.364 +    fun int_list_from_string s =
   1.365 +      List.mapPartial Int.fromString (space_explode " " s)
   1.366 +    (* int list -> assignment *)
   1.367 +    fun assignment_from_list [] i =
   1.368 +      NONE  (* the SAT solver didn't provide a value for this variable *)
   1.369 +      | assignment_from_list (x::xs) i =
   1.370 +      if x=i then (SOME true)
   1.371 +      else if x=(~i) then (SOME false)
   1.372 +      else assignment_from_list xs i
   1.373 +    (* int list -> string list -> assignment *)
   1.374 +    fun parse_assignment xs [] =
   1.375 +      assignment_from_list xs
   1.376 +      | parse_assignment xs (line::lines) =
   1.377 +      if String.isPrefix assignment_prefix line then
   1.378 +        parse_assignment (xs @ int_list_from_string line) lines
   1.379 +      else
   1.380 +        assignment_from_list xs
   1.381 +    (* string -> string -> bool *)
   1.382 +    fun is_substring needle haystack =
   1.383 +    let
   1.384 +      val length1 = String.size needle
   1.385 +      val length2 = String.size haystack
   1.386 +    in
   1.387 +      if length2 < length1 then
   1.388 +        false
   1.389 +      else if needle = String.substring (haystack, 0, length1) then
   1.390 +        true
   1.391 +      else is_substring needle (String.substring (haystack, 1, length2-1))
   1.392 +    end
   1.393 +    (* string list -> result *)
   1.394 +    fun parse_lines [] =
   1.395 +      UNKNOWN
   1.396 +      | parse_lines (line::lines) =
   1.397 +      if is_substring unsatisfiable line then
   1.398 +        UNSATISFIABLE NONE
   1.399 +      else if is_substring satisfiable line then
   1.400 +        SATISFIABLE (parse_assignment [] lines)
   1.401 +      else
   1.402 +        parse_lines lines
   1.403 +  in
   1.404 +    (parse_lines o (List.filter (fn l => l <> "")) o split_lines o File.read) path
   1.405 +  end;
   1.406  
   1.407  (* ------------------------------------------------------------------------- *)
   1.408  (* make_external_solver: call 'writefn', execute 'cmd', call 'readfn'        *)
   1.409  (* ------------------------------------------------------------------------- *)
   1.410  
   1.411 -	(* string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver *)
   1.412 +  (* string -> (PropLogic.prop_formula -> unit) -> (unit -> result) -> solver *)
   1.413  
   1.414 -	fun make_external_solver cmd writefn readfn fm =
   1.415 -		(writefn fm; system cmd; readfn ());
   1.416 +  fun make_external_solver cmd writefn readfn fm =
   1.417 +    (writefn fm; system cmd; readfn ());
   1.418  
   1.419  (* ------------------------------------------------------------------------- *)
   1.420  (* read_dimacs_cnf_file: returns a propositional formula that corresponds to *)
   1.421  (*      a SAT problem given in DIMACS CNF format                             *)
   1.422  (* ------------------------------------------------------------------------- *)
   1.423  
   1.424 -	(* Path.T -> PropLogic.prop_formula *)
   1.425 +  (* Path.T -> PropLogic.prop_formula *)
   1.426  
   1.427 -	fun read_dimacs_cnf_file path =
   1.428 -	let
   1.429 -		(* string list -> string list *)
   1.430 -		fun filter_preamble [] =
   1.431 -			error "problem line not found in DIMACS CNF file"
   1.432 -		  | filter_preamble (line::lines) =
   1.433 -			if String.isPrefix "c " line orelse line = "c" then
   1.434 -				(* ignore comments *)
   1.435 -				filter_preamble lines
   1.436 -			else if String.isPrefix "p " line then
   1.437 -				(* ignore the problem line (which must be the last line of the preamble) *)
   1.438 -				(* Ignoring the problem line implies that if the file contains more clauses *)
   1.439 -				(* or variables than specified in its preamble, we will accept it anyway.   *)
   1.440 -				lines
   1.441 -			else
   1.442 -				error "preamble in DIMACS CNF file contains a line that does not begin with \"c \" or \"p \""
   1.443 -		(* string -> int *)
   1.444 -		fun int_from_string s =
   1.445 -			case Int.fromString s of
   1.446 -			  SOME i => i
   1.447 -			| NONE   => error ("token " ^ quote s ^ "in DIMACS CNF file is not a number")
   1.448 -		(* int list -> int list list *)
   1.449 -		fun clauses xs =
   1.450 -			let
   1.451 -				val (xs1, xs2) = take_prefix (fn i => i <> 0) xs
   1.452 -			in
   1.453 -				case xs2 of
   1.454 -				  []      => [xs1]
   1.455 -				| (0::[]) => [xs1]
   1.456 -				| (0::tl) => xs1 :: clauses tl
   1.457 -				| _       => sys_error "this cannot happen"
   1.458 -			end
   1.459 -		(* int -> PropLogic.prop_formula *)
   1.460 -		fun literal_from_int i =
   1.461 -			(assert (i<>0) "variable index in DIMACS CNF file is 0";
   1.462 -			if i>0 then
   1.463 -				PropLogic.BoolVar i
   1.464 -			else
   1.465 -				PropLogic.Not (PropLogic.BoolVar (~i)))
   1.466 -		(* PropLogic.prop_formula list -> PropLogic.prop_formula *)
   1.467 -		fun disjunction [] =
   1.468 -			error "empty clause in DIMACS CNF file"
   1.469 -		  | disjunction (x::xs) =
   1.470 -			(case xs of
   1.471 -			  [] => x
   1.472 -			| _  => PropLogic.Or (x, disjunction xs))
   1.473 -		(* PropLogic.prop_formula list -> PropLogic.prop_formula *)
   1.474 -		fun conjunction [] =
   1.475 -			error "no clause in DIMACS CNF file"
   1.476 -		  | conjunction (x::xs) =
   1.477 -			(case xs of
   1.478 -			  [] => x
   1.479 -			| _  => PropLogic.And (x, conjunction xs))
   1.480 -	in
   1.481 -		(conjunction
   1.482 -		o (map disjunction)
   1.483 -		o (map (map literal_from_int))
   1.484 -		o clauses
   1.485 -		o (map int_from_string)
   1.486 -		o List.concat
   1.487 -		o (map (String.fields (fn c => c mem [#" ", #"\t", #"\n"])))
   1.488 -		o filter_preamble
   1.489 -		o (List.filter (fn l => l <> ""))
   1.490 -		o split_lines
   1.491 -		o File.read)
   1.492 -			path
   1.493 -	end;
   1.494 +  fun read_dimacs_cnf_file path =
   1.495 +  let
   1.496 +    (* string list -> string list *)
   1.497 +    fun filter_preamble [] =
   1.498 +      error "problem line not found in DIMACS CNF file"
   1.499 +      | filter_preamble (line::lines) =
   1.500 +      if String.isPrefix "c " line orelse line = "c" then
   1.501 +        (* ignore comments *)
   1.502 +        filter_preamble lines
   1.503 +      else if String.isPrefix "p " line then
   1.504 +        (* ignore the problem line (which must be the last line of the preamble) *)
   1.505 +        (* Ignoring the problem line implies that if the file contains more clauses *)
   1.506 +        (* or variables than specified in its preamble, we will accept it anyway.   *)
   1.507 +        lines
   1.508 +      else
   1.509 +        error "preamble in DIMACS CNF file contains a line that does not begin with \"c \" or \"p \""
   1.510 +    (* string -> int *)
   1.511 +    fun int_from_string s =
   1.512 +      case Int.fromString s of
   1.513 +        SOME i => i
   1.514 +      | NONE   => error ("token " ^ quote s ^ "in DIMACS CNF file is not a number")
   1.515 +    (* int list -> int list list *)
   1.516 +    fun clauses xs =
   1.517 +      let
   1.518 +        val (xs1, xs2) = take_prefix (fn i => i <> 0) xs
   1.519 +      in
   1.520 +        case xs2 of
   1.521 +          []      => [xs1]
   1.522 +        | (0::[]) => [xs1]
   1.523 +        | (0::tl) => xs1 :: clauses tl
   1.524 +        | _       => sys_error "this cannot happen"
   1.525 +      end
   1.526 +    (* int -> PropLogic.prop_formula *)
   1.527 +    fun literal_from_int i =
   1.528 +      (i<>0 orelse error "variable index in DIMACS CNF file is 0";
   1.529 +      if i>0 then
   1.530 +        PropLogic.BoolVar i
   1.531 +      else
   1.532 +        PropLogic.Not (PropLogic.BoolVar (~i)))
   1.533 +    (* PropLogic.prop_formula list -> PropLogic.prop_formula *)
   1.534 +    fun disjunction [] =
   1.535 +      error "empty clause in DIMACS CNF file"
   1.536 +      | disjunction (x::xs) =
   1.537 +      (case xs of
   1.538 +        [] => x
   1.539 +      | _  => PropLogic.Or (x, disjunction xs))
   1.540 +    (* PropLogic.prop_formula list -> PropLogic.prop_formula *)
   1.541 +    fun conjunction [] =
   1.542 +      error "no clause in DIMACS CNF file"
   1.543 +      | conjunction (x::xs) =
   1.544 +      (case xs of
   1.545 +        [] => x
   1.546 +      | _  => PropLogic.And (x, conjunction xs))
   1.547 +  in
   1.548 +    (conjunction
   1.549 +    o (map disjunction)
   1.550 +    o (map (map literal_from_int))
   1.551 +    o clauses
   1.552 +    o (map int_from_string)
   1.553 +    o List.concat
   1.554 +    o (map (String.fields (fn c => c mem [#" ", #"\t", #"\n"])))
   1.555 +    o filter_preamble
   1.556 +    o (List.filter (fn l => l <> ""))
   1.557 +    o split_lines
   1.558 +    o File.read)
   1.559 +      path
   1.560 +  end;
   1.561  
   1.562  (* ------------------------------------------------------------------------- *)
   1.563  (* solvers: a (reference to a) table of all registered SAT solvers           *)
   1.564  (* ------------------------------------------------------------------------- *)
   1.565  
   1.566 -	val solvers = ref ([] : (string * solver) list);
   1.567 +  val solvers = ref ([] : (string * solver) list);
   1.568  
   1.569  (* ------------------------------------------------------------------------- *)
   1.570  (* add_solver: updates 'solvers' by adding a new solver                      *)
   1.571  (* ------------------------------------------------------------------------- *)
   1.572  
   1.573 -	(* string * solver -> unit *)
   1.574 +  (* string * solver -> unit *)
   1.575  
   1.576      fun add_solver (name, new_solver) =
   1.577        let
   1.578 @@ -371,10 +371,10 @@
   1.579  (*       raised.                                                             *)
   1.580  (* ------------------------------------------------------------------------- *)
   1.581  
   1.582 -	(* string -> solver *)
   1.583 +  (* string -> solver *)
   1.584  
   1.585 -	fun invoke_solver name =
   1.586 -		(the o AList.lookup (op =) (!solvers)) name;
   1.587 +  fun invoke_solver name =
   1.588 +    (the o AList.lookup (op =) (!solvers)) name;
   1.589  
   1.590  end;  (* SatSolver *)
   1.591  
   1.592 @@ -389,40 +389,40 @@
   1.593  (* ------------------------------------------------------------------------- *)
   1.594  
   1.595  let
   1.596 -	fun enum_solver fm =
   1.597 -	let
   1.598 -		(* int list *)
   1.599 -		val indices = PropLogic.indices fm
   1.600 -		(* int list -> int list -> int list option *)
   1.601 -		(* binary increment: list 'xs' of current bits, list 'ys' of all bits (lower bits first) *)
   1.602 -		fun next_list _ ([]:int list) =
   1.603 -			NONE
   1.604 -		  | next_list [] (y::ys) =
   1.605 -			SOME [y]
   1.606 -		  | next_list (x::xs) (y::ys) =
   1.607 -			if x=y then
   1.608 -				(* reset the bit, continue *)
   1.609 -				next_list xs ys
   1.610 -			else
   1.611 -				(* set the lowest bit that wasn't set before, keep the higher bits *)
   1.612 -				SOME (y::x::xs)
   1.613 -		(* int list -> int -> bool *)
   1.614 -		fun assignment_from_list xs i =
   1.615 -			i mem xs
   1.616 -		(* int list -> SatSolver.result *)
   1.617 -		fun solver_loop xs =
   1.618 -			if PropLogic.eval (assignment_from_list xs) fm then
   1.619 -				SatSolver.SATISFIABLE (SOME o (assignment_from_list xs))
   1.620 -			else
   1.621 -				(case next_list xs indices of
   1.622 -				  SOME xs' => solver_loop xs'
   1.623 -				| NONE     => SatSolver.UNSATISFIABLE NONE)
   1.624 -	in
   1.625 -		(* start with the "first" assignment (all variables are interpreted as 'false') *)
   1.626 -		solver_loop []
   1.627 -	end
   1.628 +  fun enum_solver fm =
   1.629 +  let
   1.630 +    (* int list *)
   1.631 +    val indices = PropLogic.indices fm
   1.632 +    (* int list -> int list -> int list option *)
   1.633 +    (* binary increment: list 'xs' of current bits, list 'ys' of all bits (lower bits first) *)
   1.634 +    fun next_list _ ([]:int list) =
   1.635 +      NONE
   1.636 +      | next_list [] (y::ys) =
   1.637 +      SOME [y]
   1.638 +      | next_list (x::xs) (y::ys) =
   1.639 +      if x=y then
   1.640 +        (* reset the bit, continue *)
   1.641 +        next_list xs ys
   1.642 +      else
   1.643 +        (* set the lowest bit that wasn't set before, keep the higher bits *)
   1.644 +        SOME (y::x::xs)
   1.645 +    (* int list -> int -> bool *)
   1.646 +    fun assignment_from_list xs i =
   1.647 +      i mem xs
   1.648 +    (* int list -> SatSolver.result *)
   1.649 +    fun solver_loop xs =
   1.650 +      if PropLogic.eval (assignment_from_list xs) fm then
   1.651 +        SatSolver.SATISFIABLE (SOME o (assignment_from_list xs))
   1.652 +      else
   1.653 +        (case next_list xs indices of
   1.654 +          SOME xs' => solver_loop xs'
   1.655 +        | NONE     => SatSolver.UNSATISFIABLE NONE)
   1.656 +  in
   1.657 +    (* start with the "first" assignment (all variables are interpreted as 'false') *)
   1.658 +    solver_loop []
   1.659 +  end
   1.660  in
   1.661 -	SatSolver.add_solver ("enumerate", enum_solver)
   1.662 +  SatSolver.add_solver ("enumerate", enum_solver)
   1.663  end;
   1.664  
   1.665  (* ------------------------------------------------------------------------- *)
   1.666 @@ -432,86 +432,86 @@
   1.667  (* ------------------------------------------------------------------------- *)
   1.668  
   1.669  let
   1.670 -	local
   1.671 -		open PropLogic
   1.672 -	in
   1.673 -		fun dpll_solver fm =
   1.674 -		let
   1.675 -			(* We could use 'PropLogic.defcnf fm' instead of 'PropLogic.nnf fm' *)
   1.676 -			(* but that sometimes leads to worse performance due to the         *)
   1.677 -			(* introduction of additional variables.                            *)
   1.678 -			val fm' = PropLogic.nnf fm
   1.679 -			(* int list *)
   1.680 -			val indices = PropLogic.indices fm'
   1.681 -			(* int list -> int -> prop_formula *)
   1.682 -			fun partial_var_eval []      i = BoolVar i
   1.683 -			  | partial_var_eval (x::xs) i = if x=i then True else if x=(~i) then False else partial_var_eval xs i
   1.684 -			(* int list -> prop_formula -> prop_formula *)
   1.685 -			fun partial_eval xs True             = True
   1.686 -			  | partial_eval xs False            = False
   1.687 -			  | partial_eval xs (BoolVar i)      = partial_var_eval xs i
   1.688 -			  | partial_eval xs (Not fm)         = SNot (partial_eval xs fm)
   1.689 -			  | partial_eval xs (Or (fm1, fm2))  = SOr (partial_eval xs fm1, partial_eval xs fm2)
   1.690 -			  | partial_eval xs (And (fm1, fm2)) = SAnd (partial_eval xs fm1, partial_eval xs fm2)
   1.691 -			(* prop_formula -> int list *)
   1.692 -			fun forced_vars True              = []
   1.693 -			  | forced_vars False             = []
   1.694 -			  | forced_vars (BoolVar i)       = [i]
   1.695 -			  | forced_vars (Not (BoolVar i)) = [~i]
   1.696 -			  | forced_vars (Or (fm1, fm2))   = (forced_vars fm1) inter_int (forced_vars fm2)
   1.697 -			  | forced_vars (And (fm1, fm2))  = (forced_vars fm1) union_int (forced_vars fm2)
   1.698 -			  (* Above, i *and* ~i may be forced.  In this case the first occurrence takes   *)
   1.699 -			  (* precedence, and the next partial evaluation of the formula returns 'False'. *)
   1.700 -			  | forced_vars _                 = error "formula is not in negation normal form"
   1.701 -			(* int list -> prop_formula -> (int list * prop_formula) *)
   1.702 -			fun eval_and_force xs fm =
   1.703 -			let
   1.704 -				val fm' = partial_eval xs fm
   1.705 -				val xs' = forced_vars fm'
   1.706 -			in
   1.707 -				if null xs' then
   1.708 -					(xs, fm')
   1.709 -				else
   1.710 -					eval_and_force (xs@xs') fm'  (* xs and xs' should be distinct, so '@' here should have *)
   1.711 -					                             (* the same effect as 'union_int'                         *)
   1.712 -			end
   1.713 -			(* int list -> int option *)
   1.714 -			fun fresh_var xs =
   1.715 -				Library.find_first (fn i => not (i mem_int xs) andalso not ((~i) mem_int xs)) indices
   1.716 -			(* int list -> prop_formula -> int list option *)
   1.717 -			(* partial assignment 'xs' *)
   1.718 -			fun dpll xs fm =
   1.719 -			let
   1.720 -				val (xs', fm') = eval_and_force xs fm
   1.721 -			in
   1.722 -				case fm' of
   1.723 -				  True  => SOME xs'
   1.724 -				| False => NONE
   1.725 -				| _     =>
   1.726 -					let
   1.727 -						val x = valOf (fresh_var xs')  (* a fresh variable must exist since 'fm' did not evaluate to 'True'/'False' *)
   1.728 -					in
   1.729 -						case dpll (x::xs') fm' of  (* passing fm' rather than fm should save some simplification work *)
   1.730 -						  SOME xs'' => SOME xs''
   1.731 -						| NONE      => dpll ((~x)::xs') fm'  (* now try interpreting 'x' as 'False' *)
   1.732 -					end
   1.733 -			end
   1.734 -			(* int list -> assignment *)
   1.735 -			fun assignment_from_list [] i =
   1.736 -				NONE  (* the DPLL procedure didn't provide a value for this variable *)
   1.737 -			  | assignment_from_list (x::xs) i =
   1.738 -				if x=i then (SOME true)
   1.739 -				else if x=(~i) then (SOME false)
   1.740 -				else assignment_from_list xs i
   1.741 -		in
   1.742 -			(* initially, no variable is interpreted yet *)
   1.743 -			case dpll [] fm' of
   1.744 -			  SOME assignment => SatSolver.SATISFIABLE (assignment_from_list assignment)
   1.745 -			| NONE            => SatSolver.UNSATISFIABLE NONE
   1.746 -		end
   1.747 -	end  (* local *)
   1.748 +  local
   1.749 +    open PropLogic
   1.750 +  in
   1.751 +    fun dpll_solver fm =
   1.752 +    let
   1.753 +      (* We could use 'PropLogic.defcnf fm' instead of 'PropLogic.nnf fm' *)
   1.754 +      (* but that sometimes leads to worse performance due to the         *)
   1.755 +      (* introduction of additional variables.                            *)
   1.756 +      val fm' = PropLogic.nnf fm
   1.757 +      (* int list *)
   1.758 +      val indices = PropLogic.indices fm'
   1.759 +      (* int list -> int -> prop_formula *)
   1.760 +      fun partial_var_eval []      i = BoolVar i
   1.761 +        | partial_var_eval (x::xs) i = if x=i then True else if x=(~i) then False else partial_var_eval xs i
   1.762 +      (* int list -> prop_formula -> prop_formula *)
   1.763 +      fun partial_eval xs True             = True
   1.764 +        | partial_eval xs False            = False
   1.765 +        | partial_eval xs (BoolVar i)      = partial_var_eval xs i
   1.766 +        | partial_eval xs (Not fm)         = SNot (partial_eval xs fm)
   1.767 +        | partial_eval xs (Or (fm1, fm2))  = SOr (partial_eval xs fm1, partial_eval xs fm2)
   1.768 +        | partial_eval xs (And (fm1, fm2)) = SAnd (partial_eval xs fm1, partial_eval xs fm2)
   1.769 +      (* prop_formula -> int list *)
   1.770 +      fun forced_vars True              = []
   1.771 +        | forced_vars False             = []
   1.772 +        | forced_vars (BoolVar i)       = [i]
   1.773 +        | forced_vars (Not (BoolVar i)) = [~i]
   1.774 +        | forced_vars (Or (fm1, fm2))   = (forced_vars fm1) inter_int (forced_vars fm2)
   1.775 +        | forced_vars (And (fm1, fm2))  = (forced_vars fm1) union_int (forced_vars fm2)
   1.776 +        (* Above, i *and* ~i may be forced.  In this case the first occurrence takes   *)
   1.777 +        (* precedence, and the next partial evaluation of the formula returns 'False'. *)
   1.778 +        | forced_vars _                 = error "formula is not in negation normal form"
   1.779 +      (* int list -> prop_formula -> (int list * prop_formula) *)
   1.780 +      fun eval_and_force xs fm =
   1.781 +      let
   1.782 +        val fm' = partial_eval xs fm
   1.783 +        val xs' = forced_vars fm'
   1.784 +      in
   1.785 +        if null xs' then
   1.786 +          (xs, fm')
   1.787 +        else
   1.788 +          eval_and_force (xs@xs') fm'  (* xs and xs' should be distinct, so '@' here should have *)
   1.789 +                                       (* the same effect as 'union_int'                         *)
   1.790 +      end
   1.791 +      (* int list -> int option *)
   1.792 +      fun fresh_var xs =
   1.793 +        Library.find_first (fn i => not (i mem_int xs) andalso not ((~i) mem_int xs)) indices
   1.794 +      (* int list -> prop_formula -> int list option *)
   1.795 +      (* partial assignment 'xs' *)
   1.796 +      fun dpll xs fm =
   1.797 +      let
   1.798 +        val (xs', fm') = eval_and_force xs fm
   1.799 +      in
   1.800 +        case fm' of
   1.801 +          True  => SOME xs'
   1.802 +        | False => NONE
   1.803 +        | _     =>
   1.804 +          let
   1.805 +            val x = valOf (fresh_var xs')  (* a fresh variable must exist since 'fm' did not evaluate to 'True'/'False' *)
   1.806 +          in
   1.807 +            case dpll (x::xs') fm' of  (* passing fm' rather than fm should save some simplification work *)
   1.808 +              SOME xs'' => SOME xs''
   1.809 +            | NONE      => dpll ((~x)::xs') fm'  (* now try interpreting 'x' as 'False' *)
   1.810 +          end
   1.811 +      end
   1.812 +      (* int list -> assignment *)
   1.813 +      fun assignment_from_list [] i =
   1.814 +        NONE  (* the DPLL procedure didn't provide a value for this variable *)
   1.815 +        | assignment_from_list (x::xs) i =
   1.816 +        if x=i then (SOME true)
   1.817 +        else if x=(~i) then (SOME false)
   1.818 +        else assignment_from_list xs i
   1.819 +    in
   1.820 +      (* initially, no variable is interpreted yet *)
   1.821 +      case dpll [] fm' of
   1.822 +        SOME assignment => SatSolver.SATISFIABLE (assignment_from_list assignment)
   1.823 +      | NONE            => SatSolver.UNSATISFIABLE NONE
   1.824 +    end
   1.825 +  end  (* local *)
   1.826  in
   1.827 -	SatSolver.add_solver ("dpll", dpll_solver)
   1.828 +  SatSolver.add_solver ("dpll", dpll_solver)
   1.829  end;
   1.830  
   1.831  (* ------------------------------------------------------------------------- *)
   1.832 @@ -521,28 +521,28 @@
   1.833  (* ------------------------------------------------------------------------- *)
   1.834  
   1.835  let
   1.836 -	fun auto_solver fm =
   1.837 -	let
   1.838 -		fun loop [] =
   1.839 -			SatSolver.UNKNOWN
   1.840 -		  | loop ((name, solver)::solvers) =
   1.841 -			if name="auto" then
   1.842 -				(* do not call solver "auto" from within "auto" *)
   1.843 -				loop solvers
   1.844 -			else (
   1.845 -				(if name="dpll" orelse name="enumerate" then
   1.846 -					warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.")
   1.847 -				else
   1.848 -					tracing ("Using SAT solver " ^ quote name ^ "."));
   1.849 -				(* apply 'solver' to 'fm' *)
   1.850 -				solver fm
   1.851 -					handle SatSolver.NOT_CONFIGURED => loop solvers
   1.852 -			)
   1.853 -	in
   1.854 -		loop (!SatSolver.solvers)
   1.855 -	end
   1.856 +  fun auto_solver fm =
   1.857 +  let
   1.858 +    fun loop [] =
   1.859 +      SatSolver.UNKNOWN
   1.860 +      | loop ((name, solver)::solvers) =
   1.861 +      if name="auto" then
   1.862 +        (* do not call solver "auto" from within "auto" *)
   1.863 +        loop solvers
   1.864 +      else (
   1.865 +        (if name="dpll" orelse name="enumerate" then
   1.866 +          warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.")
   1.867 +        else
   1.868 +          tracing ("Using SAT solver " ^ quote name ^ "."));
   1.869 +        (* apply 'solver' to 'fm' *)
   1.870 +        solver fm
   1.871 +          handle SatSolver.NOT_CONFIGURED => loop solvers
   1.872 +      )
   1.873 +  in
   1.874 +    loop (!SatSolver.solvers)
   1.875 +  end
   1.876  in
   1.877 -	SatSolver.add_solver ("auto", auto_solver)
   1.878 +  SatSolver.add_solver ("auto", auto_solver)
   1.879  end;
   1.880  
   1.881  (* ------------------------------------------------------------------------- *)
   1.882 @@ -565,210 +565,210 @@
   1.883  (* from 0 to n-1 (where n is the number of clauses in the formula).          *)
   1.884  
   1.885  let
   1.886 -	exception INVALID_PROOF of string
   1.887 -	fun minisat_with_proofs fm =
   1.888 -	let
   1.889 -		val _          = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
   1.890 -		val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
   1.891 -		val outpath    = File.tmp_path (Path.explode "result")
   1.892 -		val proofpath  = File.tmp_path (Path.explode "result.prf")
   1.893 -		val cmd        = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " -t " ^ (Path.implode proofpath) ^ "> /dev/null"
   1.894 -		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm
   1.895 -		fun readfn ()  = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
   1.896 -		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
   1.897 -		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
   1.898 -		val cnf        = PropLogic.defcnf fm
   1.899 -		val result     = SatSolver.make_external_solver cmd writefn readfn cnf
   1.900 -		val _          = try File.rm inpath
   1.901 -		val _          = try File.rm outpath
   1.902 -	in  case result of
   1.903 -	  SatSolver.UNSATISFIABLE NONE =>
   1.904 -		(let
   1.905 -			(* string list *)
   1.906 -			val proof_lines = (split_lines o File.read) proofpath
   1.907 -				handle IO.Io _ => raise INVALID_PROOF "Could not read file \"result.prf\""
   1.908 -			(* representation of clauses as ordered lists of literals (with duplicates removed) *)
   1.909 -			(* prop_formula -> int list *)
   1.910 -			fun clause_to_lit_list (PropLogic.Or (fm1, fm2)) =
   1.911 -				OrdList.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2)
   1.912 -			  | clause_to_lit_list (PropLogic.BoolVar i) =
   1.913 -				[i]
   1.914 -			  | clause_to_lit_list (PropLogic.Not (PropLogic.BoolVar i)) =
   1.915 -				[~i]
   1.916 -			  | clause_to_lit_list _ =
   1.917 -				raise INVALID_PROOF "Error: invalid clause in CNF formula."
   1.918 -			(* prop_formula -> int *)
   1.919 -			fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) =
   1.920 -				cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
   1.921 -			  | cnf_number_of_clauses _ =
   1.922 -				1
   1.923 -			val number_of_clauses = cnf_number_of_clauses cnf
   1.924 -			(* int list array *)
   1.925 -			val clauses = Array.array (number_of_clauses, [])
   1.926 -			(* initialize the 'clauses' array *)
   1.927 -			(* prop_formula * int -> int *)
   1.928 -			fun init_array (PropLogic.And (fm1, fm2), n) =
   1.929 -				init_array (fm2, init_array (fm1, n))
   1.930 -			  | init_array (fm, n) =
   1.931 -				(Array.update (clauses, n, clause_to_lit_list fm); n+1)
   1.932 -			val _ = init_array (cnf, 0)
   1.933 -			(* optimization for the common case where MiniSat "R"s clauses in their *)
   1.934 -			(* original order:                                                      *)
   1.935 -			val last_ref_clause = ref (number_of_clauses - 1)
   1.936 -			(* search the 'clauses' array for the given list of literals 'lits', *)
   1.937 -			(* starting at index '!last_ref_clause + 1'                          *)
   1.938 -			(* int list -> int option *)
   1.939 -			fun original_clause_id lits =
   1.940 -			let
   1.941 -				fun original_clause_id_from index =
   1.942 -					if index = number_of_clauses then
   1.943 -						(* search from beginning again *)
   1.944 -						original_clause_id_from 0
   1.945 -					(* both 'lits' and the list of literals used in 'clauses' are sorted, so *)
   1.946 -					(* testing for equality should suffice -- barring duplicate literals     *)
   1.947 -					else if Array.sub (clauses, index) = lits then (
   1.948 -						(* success *)
   1.949 -						last_ref_clause := index;
   1.950 -						SOME index
   1.951 -					) else if index = !last_ref_clause then
   1.952 -						(* failure *)
   1.953 -						NONE
   1.954 -					else
   1.955 -						(* continue search *)
   1.956 -						original_clause_id_from (index + 1)
   1.957 -			in
   1.958 -				original_clause_id_from (!last_ref_clause + 1)
   1.959 -			end
   1.960 -			(* string -> int *)
   1.961 -			fun int_from_string s = (
   1.962 -				case Int.fromString s of
   1.963 -				  SOME i => i
   1.964 -				| NONE   => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).")
   1.965 -			)
   1.966 -			(* parse the proof file *)
   1.967 -			val clause_table  = ref (Inttab.empty : int list Inttab.table)
   1.968 -			val empty_id      = ref ~1
   1.969 -			(* contains a mapping from clause IDs as used by MiniSat to clause IDs in *)
   1.970 -			(* our proof format, where original clauses are numbered starting from 0  *)
   1.971 -			val clause_id_map = ref (Inttab.empty : int Inttab.table)
   1.972 -			fun sat_to_proof id = (
   1.973 -				case Inttab.lookup (!clause_id_map) id of
   1.974 -				  SOME id' => id'
   1.975 -				| NONE     => raise INVALID_PROOF ("Clause ID " ^ Int.toString id ^ " used, but not defined.")
   1.976 -			)
   1.977 -			val next_id = ref (number_of_clauses - 1)
   1.978 -			(* string list -> unit *)
   1.979 -			fun process_tokens [] =
   1.980 -				()
   1.981 -			  | process_tokens (tok::toks) =
   1.982 -				if tok="R" then (
   1.983 -					case toks of
   1.984 -					  id::sep::lits =>
   1.985 -						let
   1.986 -							val _        = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"R\" disallowed after \"X\"."
   1.987 -							val cid      = int_from_string id
   1.988 -							val _        = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
   1.989 -							val ls       = sort int_ord (map int_from_string lits)
   1.990 -							val proof_id = case original_clause_id ls of
   1.991 -							                 SOME orig_id => orig_id
   1.992 -							               | NONE         => raise INVALID_PROOF ("Original clause (new ID is " ^ id ^ ") not found.")
   1.993 -						in
   1.994 -							(* extend the mapping of clause IDs with this newly defined ID *)
   1.995 -							clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map)
   1.996 -								handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"R\").")
   1.997 -							(* the proof itself doesn't change *)
   1.998 -						end
   1.999 -					| _ =>
  1.1000 -						raise INVALID_PROOF "File format error: \"R\" followed by an insufficient number of tokens."
  1.1001 -				) else if tok="C" then (
  1.1002 -					case toks of
  1.1003 -					  id::sep::ids =>
  1.1004 -						let
  1.1005 -							val _        = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"C\" disallowed after \"X\"."
  1.1006 -							val cid      = int_from_string id
  1.1007 -							val _        = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
  1.1008 -							(* ignore the pivot literals in MiniSat's trace *)
  1.1009 -							fun unevens []             = raise INVALID_PROOF "File format error: \"C\" followed by an even number of IDs."
  1.1010 -							  | unevens (x :: [])      = x :: []
  1.1011 -							  | unevens (x :: _ :: xs) = x :: unevens xs
  1.1012 -							val rs       = (map sat_to_proof o unevens o map int_from_string) ids
  1.1013 -							(* extend the mapping of clause IDs with this newly defined ID *)
  1.1014 -							val proof_id = inc next_id
  1.1015 -							val _        = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map)
  1.1016 -							                 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"C\").")
  1.1017 -						in
  1.1018 -							(* update clause table *)
  1.1019 -							clause_table := Inttab.update_new (proof_id, rs) (!clause_table)
  1.1020 -								handle Inttab.DUP _ => raise INVALID_PROOF ("Error: internal ID for clause " ^ id ^ " already used.")
  1.1021 -						end
  1.1022 -					| _ =>
  1.1023 -						raise INVALID_PROOF "File format error: \"C\" followed by an insufficient number of tokens."
  1.1024 -				) else if tok="D" then (
  1.1025 -					case toks of
  1.1026 -					  [id] =>
  1.1027 -						let
  1.1028 -							val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"D\" disallowed after \"X\"."
  1.1029 -							val _ = sat_to_proof (int_from_string id)
  1.1030 -						in
  1.1031 -							(* simply ignore "D" *)
  1.1032 -							()
  1.1033 -						end
  1.1034 -					| _ =>
  1.1035 -						raise INVALID_PROOF "File format error: \"D\" followed by an illegal number of tokens."
  1.1036 -				) else if tok="X" then (
  1.1037 -					case toks of
  1.1038 -					  [id1, id2] =>
  1.1039 -						let
  1.1040 -							val _            = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one end-of-proof statement."
  1.1041 -							val _            = sat_to_proof (int_from_string id1)
  1.1042 -							val new_empty_id = sat_to_proof (int_from_string id2)
  1.1043 -						in
  1.1044 -							(* update conflict id *)
  1.1045 -							empty_id := new_empty_id
  1.1046 -						end
  1.1047 -					| _ =>
  1.1048 -						raise INVALID_PROOF "File format error: \"X\" followed by an illegal number of tokens."
  1.1049 -				) else
  1.1050 -					raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.")
  1.1051 -			(* string list -> unit *)
  1.1052 -			fun process_lines [] =
  1.1053 -				()
  1.1054 -			  | process_lines (l::ls) = (
  1.1055 -					process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l);
  1.1056 -					process_lines ls
  1.1057 -				)
  1.1058 -			(* proof *)
  1.1059 -			val _ = process_lines proof_lines
  1.1060 -			val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
  1.1061 -		in
  1.1062 -			SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id))
  1.1063 -		end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE))
  1.1064 -	| result =>
  1.1065 -		result
  1.1066 -	end
  1.1067 +  exception INVALID_PROOF of string
  1.1068 +  fun minisat_with_proofs fm =
  1.1069 +  let
  1.1070 +    val _          = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
  1.1071 +    val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
  1.1072 +    val outpath    = File.tmp_path (Path.explode "result")
  1.1073 +    val proofpath  = File.tmp_path (Path.explode "result.prf")
  1.1074 +    val cmd        = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " -t " ^ (Path.implode proofpath) ^ "> /dev/null"
  1.1075 +    fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm
  1.1076 +    fun readfn ()  = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
  1.1077 +    val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
  1.1078 +    val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
  1.1079 +    val cnf        = PropLogic.defcnf fm
  1.1080 +    val result     = SatSolver.make_external_solver cmd writefn readfn cnf
  1.1081 +    val _          = try File.rm inpath
  1.1082 +    val _          = try File.rm outpath
  1.1083 +  in  case result of
  1.1084 +    SatSolver.UNSATISFIABLE NONE =>
  1.1085 +    (let
  1.1086 +      (* string list *)
  1.1087 +      val proof_lines = (split_lines o File.read) proofpath
  1.1088 +        handle IO.Io _ => raise INVALID_PROOF "Could not read file \"result.prf\""
  1.1089 +      (* representation of clauses as ordered lists of literals (with duplicates removed) *)
  1.1090 +      (* prop_formula -> int list *)
  1.1091 +      fun clause_to_lit_list (PropLogic.Or (fm1, fm2)) =
  1.1092 +        OrdList.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2)
  1.1093 +        | clause_to_lit_list (PropLogic.BoolVar i) =
  1.1094 +        [i]
  1.1095 +        | clause_to_lit_list (PropLogic.Not (PropLogic.BoolVar i)) =
  1.1096 +        [~i]
  1.1097 +        | clause_to_lit_list _ =
  1.1098 +        raise INVALID_PROOF "Error: invalid clause in CNF formula."
  1.1099 +      (* prop_formula -> int *)
  1.1100 +      fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) =
  1.1101 +        cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
  1.1102 +        | cnf_number_of_clauses _ =
  1.1103 +        1
  1.1104 +      val number_of_clauses = cnf_number_of_clauses cnf
  1.1105 +      (* int list array *)
  1.1106 +      val clauses = Array.array (number_of_clauses, [])
  1.1107 +      (* initialize the 'clauses' array *)
  1.1108 +      (* prop_formula * int -> int *)
  1.1109 +      fun init_array (PropLogic.And (fm1, fm2), n) =
  1.1110 +        init_array (fm2, init_array (fm1, n))
  1.1111 +        | init_array (fm, n) =
  1.1112 +        (Array.update (clauses, n, clause_to_lit_list fm); n+1)
  1.1113 +      val _ = init_array (cnf, 0)
  1.1114 +      (* optimization for the common case where MiniSat "R"s clauses in their *)
  1.1115 +      (* original order:                                                      *)
  1.1116 +      val last_ref_clause = ref (number_of_clauses - 1)
  1.1117 +      (* search the 'clauses' array for the given list of literals 'lits', *)
  1.1118 +      (* starting at index '!last_ref_clause + 1'                          *)
  1.1119 +      (* int list -> int option *)
  1.1120 +      fun original_clause_id lits =
  1.1121 +      let
  1.1122 +        fun original_clause_id_from index =
  1.1123 +          if index = number_of_clauses then
  1.1124 +            (* search from beginning again *)
  1.1125 +            original_clause_id_from 0
  1.1126 +          (* both 'lits' and the list of literals used in 'clauses' are sorted, so *)
  1.1127 +          (* testing for equality should suffice -- barring duplicate literals     *)
  1.1128 +          else if Array.sub (clauses, index) = lits then (
  1.1129 +            (* success *)
  1.1130 +            last_ref_clause := index;
  1.1131 +            SOME index
  1.1132 +          ) else if index = !last_ref_clause then
  1.1133 +            (* failure *)
  1.1134 +            NONE
  1.1135 +          else
  1.1136 +            (* continue search *)
  1.1137 +            original_clause_id_from (index + 1)
  1.1138 +      in
  1.1139 +        original_clause_id_from (!last_ref_clause + 1)
  1.1140 +      end
  1.1141 +      (* string -> int *)
  1.1142 +      fun int_from_string s = (
  1.1143 +        case Int.fromString s of
  1.1144 +          SOME i => i
  1.1145 +        | NONE   => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).")
  1.1146 +      )
  1.1147 +      (* parse the proof file *)
  1.1148 +      val clause_table  = ref (Inttab.empty : int list Inttab.table)
  1.1149 +      val empty_id      = ref ~1
  1.1150 +      (* contains a mapping from clause IDs as used by MiniSat to clause IDs in *)
  1.1151 +      (* our proof format, where original clauses are numbered starting from 0  *)
  1.1152 +      val clause_id_map = ref (Inttab.empty : int Inttab.table)
  1.1153 +      fun sat_to_proof id = (
  1.1154 +        case Inttab.lookup (!clause_id_map) id of
  1.1155 +          SOME id' => id'
  1.1156 +        | NONE     => raise INVALID_PROOF ("Clause ID " ^ Int.toString id ^ " used, but not defined.")
  1.1157 +      )
  1.1158 +      val next_id = ref (number_of_clauses - 1)
  1.1159 +      (* string list -> unit *)
  1.1160 +      fun process_tokens [] =
  1.1161 +        ()
  1.1162 +        | process_tokens (tok::toks) =
  1.1163 +        if tok="R" then (
  1.1164 +          case toks of
  1.1165 +            id::sep::lits =>
  1.1166 +            let
  1.1167 +              val _        = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"R\" disallowed after \"X\"."
  1.1168 +              val cid      = int_from_string id
  1.1169 +              val _        = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
  1.1170 +              val ls       = sort int_ord (map int_from_string lits)
  1.1171 +              val proof_id = case original_clause_id ls of
  1.1172 +                               SOME orig_id => orig_id
  1.1173 +                             | NONE         => raise INVALID_PROOF ("Original clause (new ID is " ^ id ^ ") not found.")
  1.1174 +            in
  1.1175 +              (* extend the mapping of clause IDs with this newly defined ID *)
  1.1176 +              clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map)
  1.1177 +                handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"R\").")
  1.1178 +              (* the proof itself doesn't change *)
  1.1179 +            end
  1.1180 +          | _ =>
  1.1181 +            raise INVALID_PROOF "File format error: \"R\" followed by an insufficient number of tokens."
  1.1182 +        ) else if tok="C" then (
  1.1183 +          case toks of
  1.1184 +            id::sep::ids =>
  1.1185 +            let
  1.1186 +              val _        = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"C\" disallowed after \"X\"."
  1.1187 +              val cid      = int_from_string id
  1.1188 +              val _        = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
  1.1189 +              (* ignore the pivot literals in MiniSat's trace *)
  1.1190 +              fun unevens []             = raise INVALID_PROOF "File format error: \"C\" followed by an even number of IDs."
  1.1191 +                | unevens (x :: [])      = x :: []
  1.1192 +                | unevens (x :: _ :: xs) = x :: unevens xs
  1.1193 +              val rs       = (map sat_to_proof o unevens o map int_from_string) ids
  1.1194 +              (* extend the mapping of clause IDs with this newly defined ID *)
  1.1195 +              val proof_id = inc next_id
  1.1196 +              val _        = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map)
  1.1197 +                               handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"C\").")
  1.1198 +            in
  1.1199 +              (* update clause table *)
  1.1200 +              clause_table := Inttab.update_new (proof_id, rs) (!clause_table)
  1.1201 +                handle Inttab.DUP _ => raise INVALID_PROOF ("Error: internal ID for clause " ^ id ^ " already used.")
  1.1202 +            end
  1.1203 +          | _ =>
  1.1204 +            raise INVALID_PROOF "File format error: \"C\" followed by an insufficient number of tokens."
  1.1205 +        ) else if tok="D" then (
  1.1206 +          case toks of
  1.1207 +            [id] =>
  1.1208 +            let
  1.1209 +              val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"D\" disallowed after \"X\"."
  1.1210 +              val _ = sat_to_proof (int_from_string id)
  1.1211 +            in
  1.1212 +              (* simply ignore "D" *)
  1.1213 +              ()
  1.1214 +            end
  1.1215 +          | _ =>
  1.1216 +            raise INVALID_PROOF "File format error: \"D\" followed by an illegal number of tokens."
  1.1217 +        ) else if tok="X" then (
  1.1218 +          case toks of
  1.1219 +            [id1, id2] =>
  1.1220 +            let
  1.1221 +              val _            = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one end-of-proof statement."
  1.1222 +              val _            = sat_to_proof (int_from_string id1)
  1.1223 +              val new_empty_id = sat_to_proof (int_from_string id2)
  1.1224 +            in
  1.1225 +              (* update conflict id *)
  1.1226 +              empty_id := new_empty_id
  1.1227 +            end
  1.1228 +          | _ =>
  1.1229 +            raise INVALID_PROOF "File format error: \"X\" followed by an illegal number of tokens."
  1.1230 +        ) else
  1.1231 +          raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.")
  1.1232 +      (* string list -> unit *)
  1.1233 +      fun process_lines [] =
  1.1234 +        ()
  1.1235 +        | process_lines (l::ls) = (
  1.1236 +          process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l);
  1.1237 +          process_lines ls
  1.1238 +        )
  1.1239 +      (* proof *)
  1.1240 +      val _ = process_lines proof_lines
  1.1241 +      val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
  1.1242 +    in
  1.1243 +      SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id))
  1.1244 +    end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE))
  1.1245 +  | result =>
  1.1246 +    result
  1.1247 +  end
  1.1248  in
  1.1249 -	SatSolver.add_solver ("minisat_with_proofs", minisat_with_proofs)
  1.1250 +  SatSolver.add_solver ("minisat_with_proofs", minisat_with_proofs)
  1.1251  end;
  1.1252  
  1.1253  let
  1.1254 -	fun minisat fm =
  1.1255 -	let
  1.1256 -		val _          = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
  1.1257 -		val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
  1.1258 -		val outpath    = File.tmp_path (Path.explode "result")
  1.1259 -		val cmd        = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " > /dev/null"
  1.1260 -		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
  1.1261 -		fun readfn ()  = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
  1.1262 -		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
  1.1263 -		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
  1.1264 -		val result     = SatSolver.make_external_solver cmd writefn readfn fm
  1.1265 -		val _          = try File.rm inpath
  1.1266 -		val _          = try File.rm outpath
  1.1267 -	in
  1.1268 -		result
  1.1269 -	end
  1.1270 +  fun minisat fm =
  1.1271 +  let
  1.1272 +    val _          = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
  1.1273 +    val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
  1.1274 +    val outpath    = File.tmp_path (Path.explode "result")
  1.1275 +    val cmd        = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " > /dev/null"
  1.1276 +    fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
  1.1277 +    fun readfn ()  = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
  1.1278 +    val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
  1.1279 +    val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
  1.1280 +    val result     = SatSolver.make_external_solver cmd writefn readfn fm
  1.1281 +    val _          = try File.rm inpath
  1.1282 +    val _          = try File.rm outpath
  1.1283 +  in
  1.1284 +    result
  1.1285 +  end
  1.1286  in
  1.1287 -	SatSolver.add_solver ("minisat", minisat)
  1.1288 +  SatSolver.add_solver ("minisat", minisat)
  1.1289  end;
  1.1290  
  1.1291  (* ------------------------------------------------------------------------- *)
  1.1292 @@ -787,150 +787,150 @@
  1.1293  (* that the latter is preferred by the "auto" solver                         *)
  1.1294  
  1.1295  let
  1.1296 -	exception INVALID_PROOF of string
  1.1297 -	fun zchaff_with_proofs fm =
  1.1298 -	case SatSolver.invoke_solver "zchaff" fm of
  1.1299 -	  SatSolver.UNSATISFIABLE NONE =>
  1.1300 -		(let
  1.1301 -			(* string list *)
  1.1302 -			val proof_lines = ((split_lines o File.read) (Path.explode "resolve_trace"))
  1.1303 -				handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\""
  1.1304 -			(* PropLogic.prop_formula -> int *)
  1.1305 -			fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
  1.1306 -			  | cnf_number_of_clauses _                          = 1
  1.1307 -			(* string -> int *)
  1.1308 -			fun int_from_string s = (
  1.1309 -				case Int.fromString s of
  1.1310 -				  SOME i => i
  1.1311 -				| NONE   => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).")
  1.1312 -			)
  1.1313 -			(* parse the "resolve_trace" file *)
  1.1314 -			val clause_offset = ref ~1
  1.1315 -			val clause_table  = ref (Inttab.empty : int list Inttab.table)
  1.1316 -			val empty_id      = ref ~1
  1.1317 -			(* string list -> unit *)
  1.1318 -			fun process_tokens [] =
  1.1319 -				()
  1.1320 -			  | process_tokens (tok::toks) =
  1.1321 -				if tok="CL:" then (
  1.1322 -					case toks of
  1.1323 -					  id::sep::ids =>
  1.1324 -						let
  1.1325 -							val _   = if !clause_offset = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"VAR:\".")
  1.1326 -							val _   = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"CONF:\".")
  1.1327 -							val cid = int_from_string id
  1.1328 -							val _   = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
  1.1329 -							val rs  = map int_from_string ids
  1.1330 -						in
  1.1331 -							(* update clause table *)
  1.1332 -							clause_table := Inttab.update_new (cid, rs) (!clause_table)
  1.1333 -								handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once.")
  1.1334 -						end
  1.1335 -					| _ =>
  1.1336 -						raise INVALID_PROOF "File format error: \"CL:\" followed by an insufficient number of tokens."
  1.1337 -				) else if tok="VAR:" then (
  1.1338 -					case toks of
  1.1339 -					  id::levsep::levid::valsep::valid::antesep::anteid::litsep::lits =>
  1.1340 -						let
  1.1341 -							val _   = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"VAR:\" disallowed after \"CONF:\".")
  1.1342 -							(* set 'clause_offset' to the largest used clause ID *)
  1.1343 -							val _   = if !clause_offset = ~1 then clause_offset :=
  1.1344 -								(case Inttab.max_key (!clause_table) of
  1.1345 -								  SOME id => id
  1.1346 -								| NONE    => cnf_number_of_clauses (PropLogic.defcnf fm) - 1  (* the first clause ID is 0, not 1 *))
  1.1347 -								else
  1.1348 -									()
  1.1349 -							val vid = int_from_string id
  1.1350 -							val _   = if levsep = "L:" then () else raise INVALID_PROOF ("File format error: \"L:\" expected (" ^ quote levsep ^ " encountered).")
  1.1351 -							val _   = int_from_string levid
  1.1352 -							val _   = if valsep = "V:" then () else raise INVALID_PROOF ("File format error: \"V:\" expected (" ^ quote valsep ^ " encountered).")
  1.1353 -							val _   = int_from_string valid
  1.1354 -							val _   = if antesep = "A:" then () else raise INVALID_PROOF ("File format error: \"A:\" expected (" ^ quote antesep ^ " encountered).")
  1.1355 -							val aid = int_from_string anteid
  1.1356 -							val _   = if litsep = "Lits:" then () else raise INVALID_PROOF ("File format error: \"Lits:\" expected (" ^ quote litsep ^ " encountered).")
  1.1357 -							val ls  = map int_from_string lits
  1.1358 -							(* convert the data provided by zChaff to our resolution-style proof format *)
  1.1359 -							(* each "VAR:" line defines a unit clause, the resolvents are implicitly    *)
  1.1360 -							(* given by the literals in the antecedent clause                           *)
  1.1361 -							(* we use the sum of '!clause_offset' and the variable ID as clause ID for the unit clause *)
  1.1362 -							val cid = !clause_offset + vid
  1.1363 -							(* the low bit of each literal gives its sign (positive/negative), therefore  *)
  1.1364 -							(* we have to divide each literal by 2 to obtain the proper variable ID; then *)
  1.1365 -							(* we add '!clause_offset' to obtain the ID of the corresponding unit clause  *)
  1.1366 -							val vids = filter (not_equal vid) (map (fn l => l div 2) ls)
  1.1367 -							val rs   = aid :: map (fn v => !clause_offset + v) vids
  1.1368 -						in
  1.1369 -							(* update clause table *)
  1.1370 -							clause_table := Inttab.update_new (cid, rs) (!clause_table)
  1.1371 -								handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int cid ^ " (derived from antecedent for variable " ^ id ^ ") already defined.")
  1.1372 -						end
  1.1373 -					| _ =>
  1.1374 -						raise INVALID_PROOF "File format error: \"VAR:\" followed by an insufficient number of tokens."
  1.1375 -				) else if tok="CONF:" then (
  1.1376 -					case toks of
  1.1377 -					  id::sep::ids =>
  1.1378 -						let
  1.1379 -							val _   = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one conflicting clause specified."
  1.1380 -							val cid = int_from_string id
  1.1381 -							val _   = if sep = "==" then () else raise INVALID_PROOF ("File format error: \"==\" expected (" ^ quote sep ^ " encountered).")
  1.1382 -							val ls  = map int_from_string ids
  1.1383 -							(* the conflict clause must be resolved with the unit clauses *)
  1.1384 -							(* for its literals to obtain the empty clause                *)
  1.1385 -							val vids         = map (fn l => l div 2) ls
  1.1386 -							val rs           = cid :: map (fn v => !clause_offset + v) vids
  1.1387 -							val new_empty_id = getOpt (Inttab.max_key (!clause_table), !clause_offset) + 1
  1.1388 -						in
  1.1389 -							(* update clause table and conflict id *)
  1.1390 -							clause_table := Inttab.update_new (new_empty_id, rs) (!clause_table)
  1.1391 -								handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int new_empty_id ^ " (empty clause derived from clause " ^ id ^ ") already defined.");
  1.1392 -							empty_id     := new_empty_id
  1.1393 -						end
  1.1394 -					| _ =>
  1.1395 -						raise INVALID_PROOF "File format error: \"CONF:\" followed by an insufficient number of tokens."
  1.1396 -				) else
  1.1397 -					raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.")
  1.1398 -			(* string list -> unit *)
  1.1399 -			fun process_lines [] =
  1.1400 -				()
  1.1401 -			  | process_lines (l::ls) = (
  1.1402 -					process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l);
  1.1403 -					process_lines ls
  1.1404 -				)
  1.1405 -			(* proof *)
  1.1406 -			val _ = process_lines proof_lines
  1.1407 -			val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
  1.1408 -		in
  1.1409 -			SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id))
  1.1410 -		end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE))
  1.1411 -	| result =>
  1.1412 -		result
  1.1413 +  exception INVALID_PROOF of string
  1.1414 +  fun zchaff_with_proofs fm =
  1.1415 +  case SatSolver.invoke_solver "zchaff" fm of
  1.1416 +    SatSolver.UNSATISFIABLE NONE =>
  1.1417 +    (let
  1.1418 +      (* string list *)
  1.1419 +      val proof_lines = ((split_lines o File.read) (Path.explode "resolve_trace"))
  1.1420 +        handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\""
  1.1421 +      (* PropLogic.prop_formula -> int *)
  1.1422 +      fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
  1.1423 +        | cnf_number_of_clauses _                          = 1
  1.1424 +      (* string -> int *)
  1.1425 +      fun int_from_string s = (
  1.1426 +        case Int.fromString s of
  1.1427 +          SOME i => i
  1.1428 +        | NONE   => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).")
  1.1429 +      )
  1.1430 +      (* parse the "resolve_trace" file *)
  1.1431 +      val clause_offset = ref ~1
  1.1432 +      val clause_table  = ref (Inttab.empty : int list Inttab.table)
  1.1433 +      val empty_id      = ref ~1
  1.1434 +      (* string list -> unit *)
  1.1435 +      fun process_tokens [] =
  1.1436 +        ()
  1.1437 +        | process_tokens (tok::toks) =
  1.1438 +        if tok="CL:" then (
  1.1439 +          case toks of
  1.1440 +            id::sep::ids =>
  1.1441 +            let
  1.1442 +              val _   = if !clause_offset = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"VAR:\".")
  1.1443 +              val _   = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"CONF:\".")
  1.1444 +              val cid = int_from_string id
  1.1445 +              val _   = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
  1.1446 +              val rs  = map int_from_string ids
  1.1447 +            in
  1.1448 +              (* update clause table *)
  1.1449 +              clause_table := Inttab.update_new (cid, rs) (!clause_table)
  1.1450 +                handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once.")
  1.1451 +            end
  1.1452 +          | _ =>
  1.1453 +            raise INVALID_PROOF "File format error: \"CL:\" followed by an insufficient number of tokens."
  1.1454 +        ) else if tok="VAR:" then (
  1.1455 +          case toks of
  1.1456 +            id::levsep::levid::valsep::valid::antesep::anteid::litsep::lits =>
  1.1457 +            let
  1.1458 +              val _   = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"VAR:\" disallowed after \"CONF:\".")
  1.1459 +              (* set 'clause_offset' to the largest used clause ID *)
  1.1460 +              val _   = if !clause_offset = ~1 then clause_offset :=
  1.1461 +                (case Inttab.max_key (!clause_table) of
  1.1462 +                  SOME id => id
  1.1463 +                | NONE    => cnf_number_of_clauses (PropLogic.defcnf fm) - 1  (* the first clause ID is 0, not 1 *))
  1.1464 +                else
  1.1465 +                  ()
  1.1466 +              val vid = int_from_string id
  1.1467 +              val _   = if levsep = "L:" then () else raise INVALID_PROOF ("File format error: \"L:\" expected (" ^ quote levsep ^ " encountered).")
  1.1468 +              val _   = int_from_string levid
  1.1469 +              val _   = if valsep = "V:" then () else raise INVALID_PROOF ("File format error: \"V:\" expected (" ^ quote valsep ^ " encountered).")
  1.1470 +              val _   = int_from_string valid
  1.1471 +              val _   = if antesep = "A:" then () else raise INVALID_PROOF ("File format error: \"A:\" expected (" ^ quote antesep ^ " encountered).")
  1.1472 +              val aid = int_from_string anteid
  1.1473 +              val _   = if litsep = "Lits:" then () else raise INVALID_PROOF ("File format error: \"Lits:\" expected (" ^ quote litsep ^ " encountered).")
  1.1474 +              val ls  = map int_from_string lits
  1.1475 +              (* convert the data provided by zChaff to our resolution-style proof format *)
  1.1476 +              (* each "VAR:" line defines a unit clause, the resolvents are implicitly    *)
  1.1477 +              (* given by the literals in the antecedent clause                           *)
  1.1478 +              (* we use the sum of '!clause_offset' and the variable ID as clause ID for the unit clause *)
  1.1479 +              val cid = !clause_offset + vid
  1.1480 +              (* the low bit of each literal gives its sign (positive/negative), therefore  *)
  1.1481 +              (* we have to divide each literal by 2 to obtain the proper variable ID; then *)
  1.1482 +              (* we add '!clause_offset' to obtain the ID of the corresponding unit clause  *)
  1.1483 +              val vids = filter (not_equal vid) (map (fn l => l div 2) ls)
  1.1484 +              val rs   = aid :: map (fn v => !clause_offset + v) vids
  1.1485 +            in
  1.1486 +              (* update clause table *)
  1.1487 +              clause_table := Inttab.update_new (cid, rs) (!clause_table)
  1.1488 +                handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int cid ^ " (derived from antecedent for variable " ^ id ^ ") already defined.")
  1.1489 +            end
  1.1490 +          | _ =>
  1.1491 +            raise INVALID_PROOF "File format error: \"VAR:\" followed by an insufficient number of tokens."
  1.1492 +        ) else if tok="CONF:" then (
  1.1493 +          case toks of
  1.1494 +            id::sep::ids =>
  1.1495 +            let
  1.1496 +              val _   = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one conflicting clause specified."
  1.1497 +              val cid = int_from_string id
  1.1498 +              val _   = if sep = "==" then () else raise INVALID_PROOF ("File format error: \"==\" expected (" ^ quote sep ^ " encountered).")
  1.1499 +              val ls  = map int_from_string ids
  1.1500 +              (* the conflict clause must be resolved with the unit clauses *)
  1.1501 +              (* for its literals to obtain the empty clause                *)
  1.1502 +              val vids         = map (fn l => l div 2) ls
  1.1503 +              val rs           = cid :: map (fn v => !clause_offset + v) vids
  1.1504 +              val new_empty_id = getOpt (Inttab.max_key (!clause_table), !clause_offset) + 1
  1.1505 +            in
  1.1506 +              (* update clause table and conflict id *)
  1.1507 +              clause_table := Inttab.update_new (new_empty_id, rs) (!clause_table)
  1.1508 +                handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int new_empty_id ^ " (empty clause derived from clause " ^ id ^ ") already defined.");
  1.1509 +              empty_id     := new_empty_id
  1.1510 +            end
  1.1511 +          | _ =>
  1.1512 +            raise INVALID_PROOF "File format error: \"CONF:\" followed by an insufficient number of tokens."
  1.1513 +        ) else
  1.1514 +          raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.")
  1.1515 +      (* string list -> unit *)
  1.1516 +      fun process_lines [] =
  1.1517 +        ()
  1.1518 +        | process_lines (l::ls) = (
  1.1519 +          process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l);
  1.1520 +          process_lines ls
  1.1521 +        )
  1.1522 +      (* proof *)
  1.1523 +      val _ = process_lines proof_lines
  1.1524 +      val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
  1.1525 +    in
  1.1526 +      SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id))
  1.1527 +    end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE))
  1.1528 +  | result =>
  1.1529 +    result
  1.1530  in
  1.1531 -	SatSolver.add_solver ("zchaff_with_proofs", zchaff_with_proofs)
  1.1532 +  SatSolver.add_solver ("zchaff_with_proofs", zchaff_with_proofs)
  1.1533  end;
  1.1534  
  1.1535  let
  1.1536 -	fun zchaff fm =
  1.1537 -	let
  1.1538 -		val _          = if (getenv "ZCHAFF_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
  1.1539 -		val _          = if (getenv "ZCHAFF_VERSION") <> "2004.5.13" andalso
  1.1540 -		                    (getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else ()
  1.1541 -			(* both versions of zChaff appear to have the same interface, so we do *)
  1.1542 -			(* not actually need to distinguish between them in the following code *)
  1.1543 -		val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
  1.1544 -		val outpath    = File.tmp_path (Path.explode "result")
  1.1545 -		val cmd        = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
  1.1546 -		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
  1.1547 -		fun readfn ()  = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
  1.1548 -		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
  1.1549 -		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
  1.1550 -		val result     = SatSolver.make_external_solver cmd writefn readfn fm
  1.1551 -		val _          = try File.rm inpath
  1.1552 -		val _          = try File.rm outpath
  1.1553 -	in
  1.1554 -		result
  1.1555 -	end
  1.1556 +  fun zchaff fm =
  1.1557 +  let
  1.1558 +    val _          = if (getenv "ZCHAFF_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
  1.1559 +    val _          = if (getenv "ZCHAFF_VERSION") <> "2004.5.13" andalso
  1.1560 +                        (getenv "ZCHAFF_VERSION") <> "2004.11.15" then raise SatSolver.NOT_CONFIGURED else ()
  1.1561 +      (* both versions of zChaff appear to have the same interface, so we do *)
  1.1562 +      (* not actually need to distinguish between them in the following code *)
  1.1563 +    val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
  1.1564 +    val outpath    = File.tmp_path (Path.explode "result")
  1.1565 +    val cmd        = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
  1.1566 +    fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
  1.1567 +    fun readfn ()  = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
  1.1568 +    val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
  1.1569 +    val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
  1.1570 +    val result     = SatSolver.make_external_solver cmd writefn readfn fm
  1.1571 +    val _          = try File.rm inpath
  1.1572 +    val _          = try File.rm outpath
  1.1573 +  in
  1.1574 +    result
  1.1575 +  end
  1.1576  in
  1.1577 -	SatSolver.add_solver ("zchaff", zchaff)
  1.1578 +  SatSolver.add_solver ("zchaff", zchaff)
  1.1579  end;
  1.1580  
  1.1581  (* ------------------------------------------------------------------------- *)
  1.1582 @@ -938,24 +938,24 @@
  1.1583  (* ------------------------------------------------------------------------- *)
  1.1584  
  1.1585  let
  1.1586 -	fun berkmin fm =
  1.1587 -	let
  1.1588 -		val _          = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else ()
  1.1589 -		val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
  1.1590 -		val outpath    = File.tmp_path (Path.explode "result")
  1.1591 -		val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
  1.1592 -		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
  1.1593 -		fun readfn ()  = SatSolver.read_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
  1.1594 -		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
  1.1595 -		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
  1.1596 -		val result     = SatSolver.make_external_solver cmd writefn readfn fm
  1.1597 -		val _          = try File.rm inpath
  1.1598 -		val _          = try File.rm outpath
  1.1599 -	in
  1.1600 -		result
  1.1601 -	end
  1.1602 +  fun berkmin fm =
  1.1603 +  let
  1.1604 +    val _          = if (getenv "BERKMIN_HOME") = "" orelse (getenv "BERKMIN_EXE") = "" then raise SatSolver.NOT_CONFIGURED else ()
  1.1605 +    val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
  1.1606 +    val outpath    = File.tmp_path (Path.explode "result")
  1.1607 +    val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
  1.1608 +    fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
  1.1609 +    fun readfn ()  = SatSolver.read_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
  1.1610 +    val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
  1.1611 +    val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
  1.1612 +    val result     = SatSolver.make_external_solver cmd writefn readfn fm
  1.1613 +    val _          = try File.rm inpath
  1.1614 +    val _          = try File.rm outpath
  1.1615 +  in
  1.1616 +    result
  1.1617 +  end
  1.1618  in
  1.1619 -	SatSolver.add_solver ("berkmin", berkmin)
  1.1620 +  SatSolver.add_solver ("berkmin", berkmin)
  1.1621  end;
  1.1622  
  1.1623  (* ------------------------------------------------------------------------- *)
  1.1624 @@ -963,24 +963,24 @@
  1.1625  (* ------------------------------------------------------------------------- *)
  1.1626  
  1.1627  let
  1.1628 -	fun jerusat fm =
  1.1629 -	let
  1.1630 -		val _          = if (getenv "JERUSAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
  1.1631 -		val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
  1.1632 -		val outpath    = File.tmp_path (Path.explode "result")
  1.1633 -		val cmd        = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
  1.1634 -		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
  1.1635 -		fun readfn ()  = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
  1.1636 -		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
  1.1637 -		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
  1.1638 -		val result     = SatSolver.make_external_solver cmd writefn readfn fm
  1.1639 -		val _          = try File.rm inpath
  1.1640 -		val _          = try File.rm outpath
  1.1641 -	in
  1.1642 -		result
  1.1643 -	end
  1.1644 +  fun jerusat fm =
  1.1645 +  let
  1.1646 +    val _          = if (getenv "JERUSAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
  1.1647 +    val inpath     = File.tmp_path (Path.explode "isabelle.cnf")
  1.1648 +    val outpath    = File.tmp_path (Path.explode "result")
  1.1649 +    val cmd        = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
  1.1650 +    fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
  1.1651 +    fun readfn ()  = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
  1.1652 +    val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
  1.1653 +    val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
  1.1654 +    val result     = SatSolver.make_external_solver cmd writefn readfn fm
  1.1655 +    val _          = try File.rm inpath
  1.1656 +    val _          = try File.rm outpath
  1.1657 +  in
  1.1658 +    result
  1.1659 +  end
  1.1660  in
  1.1661 -	SatSolver.add_solver ("jerusat", jerusat)
  1.1662 +  SatSolver.add_solver ("jerusat", jerusat)
  1.1663  end;
  1.1664  
  1.1665  (* ------------------------------------------------------------------------- *)
  1.1666 @@ -989,9 +989,9 @@
  1.1667  
  1.1668  (*
  1.1669  let
  1.1670 -	fun mysolver fm = ...
  1.1671 +  fun mysolver fm = ...
  1.1672  in
  1.1673 -	SatSolver.add_solver ("myname", (fn fm => if mysolver_is_configured then mysolver fm else raise SatSolver.NOT_CONFIGURED));  -- register the solver
  1.1674 +  SatSolver.add_solver ("myname", (fn fm => if mysolver_is_configured then mysolver fm else raise SatSolver.NOT_CONFIGURED));  -- register the solver
  1.1675  end;
  1.1676  
  1.1677  -- the solver is now available as SatSolver.invoke_solver "myname"