src/HOL/Tools/sat_solver.ML
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 56853 a265e41cc33b
child 60982 67e389f67073
permissions -rw-r--r--
specialized specification: avoid trivial instances
     1 (*  Title:      HOL/Tools/sat_solver.ML
     2     Author:     Tjark Weber
     3     Copyright   2004-2009
     4 
     5 Interface to external SAT solvers, and (simple) built-in SAT solvers.
     6 
     7 Relevant Isabelle environment settings:
     8 
     9   # MiniSat 1.14
    10   #MINISAT_HOME=/usr/local/bin
    11 
    12   # zChaff
    13   #ZCHAFF_HOME=/usr/local/bin
    14 
    15   # BerkMin561
    16   #BERKMIN_HOME=/usr/local/bin
    17   #BERKMIN_EXE=BerkMin561-linux
    18   #BERKMIN_EXE=BerkMin561-solaris
    19 
    20   # Jerusat 1.3
    21   #JERUSAT_HOME=/usr/local/bin
    22 *)
    23 
    24 signature SAT_SOLVER =
    25 sig
    26   exception NOT_CONFIGURED
    27 
    28   type assignment = int -> bool option
    29   type proof      = int list Inttab.table * int
    30   datatype result = SATISFIABLE of assignment
    31                   | UNSATISFIABLE of proof option
    32                   | UNKNOWN
    33   type solver     = Prop_Logic.prop_formula -> result
    34 
    35   (* auxiliary functions to create external SAT solvers *)
    36   val write_dimacs_cnf_file : Path.T -> Prop_Logic.prop_formula -> unit
    37   val write_dimacs_sat_file : Path.T -> Prop_Logic.prop_formula -> unit
    38   val read_std_result_file : Path.T -> string * string * string -> result
    39   val make_external_solver : string -> (Prop_Logic.prop_formula -> unit) ->
    40     (unit -> result) -> solver
    41 
    42   val read_dimacs_cnf_file : Path.T -> Prop_Logic.prop_formula
    43 
    44   (* generic solver interface *)
    45   val get_solvers   : unit -> (string * solver) list
    46   val add_solver    : string * solver -> unit
    47   val invoke_solver : string -> solver  (* exception Option *)
    48 end;
    49 
    50 structure SAT_Solver : SAT_SOLVER =
    51 struct
    52 
    53   open Prop_Logic;
    54 
    55 (* ------------------------------------------------------------------------- *)
    56 (* should be raised by an external SAT solver to indicate that the solver is *)
    57 (* not configured properly                                                   *)
    58 (* ------------------------------------------------------------------------- *)
    59 
    60   exception NOT_CONFIGURED;
    61 
    62 (* ------------------------------------------------------------------------- *)
    63 (* type of partial (satisfying) assignments: 'a i = NONE' means that 'a' is  *)
    64 (*      a satisfying assignment regardless of the value of variable 'i'      *)
    65 (* ------------------------------------------------------------------------- *)
    66 
    67   type assignment = int -> bool option;
    68 
    69 (* ------------------------------------------------------------------------- *)
    70 (* a proof of unsatisfiability, to be interpreted as follows: each integer   *)
    71 (*      is a clause ID, each list 'xs' stored under the key 'x' in the table *)
    72 (*      contains the IDs of clauses that must be resolved (in the given      *)
    73 (*      order) to obtain the new clause 'x'.  Each list 'xs' must be         *)
    74 (*      non-empty, and the literal to be resolved upon must always be unique *)
    75 (*      (e.g. "A | ~B" must not be resolved with "~A | B").  Circular        *)
    76 (*      dependencies of clauses are not allowed.  (At least) one of the      *)
    77 (*      clauses in the table must be the empty clause (i.e. contain no       *)
    78 (*      literals); its ID is given by the second component of the proof.     *)
    79 (*      The clauses of the original problem passed to the SAT solver have    *)
    80 (*      consecutive IDs starting with 0.  Clause IDs must be non-negative,   *)
    81 (*      but do not need to be consecutive.                                   *)
    82 (* ------------------------------------------------------------------------- *)
    83 
    84   type proof = int list Inttab.table * int;
    85 
    86 (* ------------------------------------------------------------------------- *)
    87 (* return type of SAT solvers: if the result is 'SATISFIABLE', a satisfying  *)
    88 (*      assignment must be returned as well; if the result is                *)
    89 (*      'UNSATISFIABLE', a proof of unsatisfiability may be returned         *)
    90 (* ------------------------------------------------------------------------- *)
    91 
    92   datatype result = SATISFIABLE of assignment
    93                   | UNSATISFIABLE of proof option
    94                   | UNKNOWN;
    95 
    96 (* ------------------------------------------------------------------------- *)
    97 (* type of SAT solvers: given a propositional formula, a satisfying          *)
    98 (*      assignment may be returned                                           *)
    99 (* ------------------------------------------------------------------------- *)
   100 
   101   type solver = prop_formula -> result;
   102 
   103 (* ------------------------------------------------------------------------- *)
   104 (* write_dimacs_cnf_file: serializes a formula 'fm' of propositional logic   *)
   105 (*      to a file in DIMACS CNF format (see "Satisfiability Suggested        *)
   106 (*      Format", May 8 1993, Section 2.1)                                    *)
   107 (* Note: 'fm' must not contain a variable index less than 1.                 *)
   108 (* Note: 'fm' must be given in CNF.                                          *)
   109 (* ------------------------------------------------------------------------- *)
   110 
   111   fun write_dimacs_cnf_file path fm =
   112   let
   113     fun cnf_True_False_elim True =
   114       Or (BoolVar 1, Not (BoolVar 1))
   115       | cnf_True_False_elim False =
   116       And (BoolVar 1, Not (BoolVar 1))
   117       | cnf_True_False_elim fm =
   118       fm  (* since 'fm' is in CNF, either 'fm'='True'/'False',
   119              or 'fm' does not contain 'True'/'False' at all *)
   120     fun cnf_number_of_clauses (And (fm1, fm2)) =
   121       (cnf_number_of_clauses fm1) + (cnf_number_of_clauses fm2)
   122       | cnf_number_of_clauses _ =
   123       1
   124     fun write_cnf_file out =
   125     let
   126       fun write_formula True =
   127           error "formula is not in CNF"
   128         | write_formula False =
   129           error "formula is not in CNF"
   130         | write_formula (BoolVar i) =
   131           (i>=1 orelse error "formula contains a variable index less than 1";
   132            TextIO.output (out, string_of_int i))
   133         | write_formula (Not (BoolVar i)) =
   134           (TextIO.output (out, "-");
   135            write_formula (BoolVar i))
   136         | write_formula (Not _) =
   137           error "formula is not in CNF"
   138         | write_formula (Or (fm1, fm2)) =
   139           (write_formula fm1;
   140            TextIO.output (out, " ");
   141            write_formula fm2)
   142         | write_formula (And (fm1, fm2)) =
   143           (write_formula fm1;
   144            TextIO.output (out, " 0\n");
   145            write_formula fm2)
   146       val fm'               = cnf_True_False_elim fm
   147       val number_of_vars    = maxidx fm'
   148       val number_of_clauses = cnf_number_of_clauses fm'
   149     in
   150       TextIO.output (out, "c This file was generated by SAT_Solver.write_dimacs_cnf_file\n");
   151       TextIO.output (out, "p cnf " ^ string_of_int number_of_vars ^ " " ^
   152                             string_of_int number_of_clauses ^ "\n");
   153       write_formula fm';
   154       TextIO.output (out, " 0\n")
   155     end
   156   in
   157     File.open_output write_cnf_file path
   158   end;
   159 
   160 (* ------------------------------------------------------------------------- *)
   161 (* write_dimacs_sat_file: serializes a formula 'fm' of propositional logic   *)
   162 (*      to a file in DIMACS SAT format (see "Satisfiability Suggested        *)
   163 (*      Format", May 8 1993, Section 2.2)                                    *)
   164 (* Note: 'fm' must not contain a variable index less than 1.                 *)
   165 (* ------------------------------------------------------------------------- *)
   166 
   167   fun write_dimacs_sat_file path fm =
   168   let
   169     fun write_sat_file out =
   170     let
   171       fun write_formula True =
   172           TextIO.output (out, "*()")
   173         | write_formula False =
   174           TextIO.output (out, "+()")
   175         | write_formula (BoolVar i) =
   176           (i>=1 orelse error "formula contains a variable index less than 1";
   177            TextIO.output (out, string_of_int i))
   178         | write_formula (Not (BoolVar i)) =
   179           (TextIO.output (out, "-");
   180            write_formula (BoolVar i))
   181         | write_formula (Not fm) =
   182           (TextIO.output (out, "-(");
   183            write_formula fm;
   184            TextIO.output (out, ")"))
   185         | write_formula (Or (fm1, fm2)) =
   186           (TextIO.output (out, "+(");
   187            write_formula_or fm1;
   188            TextIO.output (out, " ");
   189            write_formula_or fm2;
   190            TextIO.output (out, ")"))
   191         | write_formula (And (fm1, fm2)) =
   192           (TextIO.output (out, "*(");
   193            write_formula_and fm1;
   194            TextIO.output (out, " ");
   195            write_formula_and fm2;
   196            TextIO.output (out, ")"))
   197       (* optimization to make use of n-ary disjunction/conjunction *)
   198       and write_formula_or (Or (fm1, fm2)) =
   199           (write_formula_or fm1;
   200            TextIO.output (out, " ");
   201            write_formula_or fm2)
   202         | write_formula_or fm =
   203           write_formula fm
   204       and write_formula_and (And (fm1, fm2)) =
   205           (write_formula_and fm1;
   206            TextIO.output (out, " ");
   207            write_formula_and fm2)
   208         | write_formula_and fm =
   209           write_formula fm
   210       val number_of_vars = Int.max (maxidx fm, 1)
   211     in
   212       TextIO.output (out, "c This file was generated by SAT_Solver.write_dimacs_sat_file\n");
   213       TextIO.output (out, "p sat " ^ string_of_int number_of_vars ^ "\n");
   214       TextIO.output (out, "(");
   215       write_formula fm;
   216       TextIO.output (out, ")\n")
   217     end
   218   in
   219     File.open_output write_sat_file path
   220   end;
   221 
   222 (* ------------------------------------------------------------------------- *)
   223 (* read_std_result_file: scans a SAT solver's output file for a satisfying   *)
   224 (*      variable assignment.  Returns the assignment, or 'UNSATISFIABLE' if  *)
   225 (*      the file contains 'unsatisfiable', or 'UNKNOWN' if the file contains *)
   226 (*      neither 'satisfiable' nor 'unsatisfiable'.  Empty lines are ignored. *)
   227 (*      The assignment must be given in one or more lines immediately after  *)
   228 (*      the line that contains 'satisfiable'.  These lines must begin with   *)
   229 (*      'assignment_prefix'.  Variables must be separated by " ".  Non-      *)
   230 (*      integer strings are ignored.  If variable i is contained in the      *)
   231 (*      assignment, then i is interpreted as 'true'.  If ~i is contained in  *)
   232 (*      the assignment, then i is interpreted as 'false'.  Otherwise the     *)
   233 (*      value of i is taken to be unspecified.                               *)
   234 (* ------------------------------------------------------------------------- *)
   235 
   236   fun read_std_result_file path (satisfiable, assignment_prefix, unsatisfiable) =
   237   let
   238     fun int_list_from_string s =
   239       map_filter Int.fromString (space_explode " " s)
   240     fun assignment_from_list [] i =
   241       NONE  (* the SAT solver didn't provide a value for this variable *)
   242       | assignment_from_list (x::xs) i =
   243       if x=i then (SOME true)
   244       else if x=(~i) then (SOME false)
   245       else assignment_from_list xs i
   246     fun parse_assignment xs [] =
   247       assignment_from_list xs
   248       | parse_assignment xs (line::lines) =
   249       if String.isPrefix assignment_prefix line then
   250         parse_assignment (xs @ int_list_from_string line) lines
   251       else
   252         assignment_from_list xs
   253     fun is_substring needle haystack =
   254     let
   255       val length1 = String.size needle
   256       val length2 = String.size haystack
   257     in
   258       if length2 < length1 then
   259         false
   260       else if needle = String.substring (haystack, 0, length1) then
   261         true
   262       else is_substring needle (String.substring (haystack, 1, length2-1))
   263     end
   264     fun parse_lines [] =
   265       UNKNOWN
   266       | parse_lines (line::lines) =
   267       if is_substring unsatisfiable line then
   268         UNSATISFIABLE NONE
   269       else if is_substring satisfiable line then
   270         SATISFIABLE (parse_assignment [] lines)
   271       else
   272         parse_lines lines
   273   in
   274     (parse_lines o filter (fn l => l <> "") o split_lines o File.read) path
   275   end;
   276 
   277 (* ------------------------------------------------------------------------- *)
   278 (* make_external_solver: call 'writefn', execute 'cmd', call 'readfn'        *)
   279 (* ------------------------------------------------------------------------- *)
   280 
   281   fun make_external_solver cmd writefn readfn fm =
   282     (writefn fm; Isabelle_System.bash cmd; readfn ());
   283 
   284 (* ------------------------------------------------------------------------- *)
   285 (* read_dimacs_cnf_file: returns a propositional formula that corresponds to *)
   286 (*      a SAT problem given in DIMACS CNF format                             *)
   287 (* ------------------------------------------------------------------------- *)
   288 
   289   fun read_dimacs_cnf_file path =
   290   let
   291     fun filter_preamble [] =
   292       error "problem line not found in DIMACS CNF file"
   293       | filter_preamble (line::lines) =
   294       if String.isPrefix "c " line orelse line = "c" then
   295         (* ignore comments *)
   296         filter_preamble lines
   297       else if String.isPrefix "p " line then
   298         (* ignore the problem line (which must be the last line of the preamble) *)
   299         (* Ignoring the problem line implies that if the file contains more clauses *)
   300         (* or variables than specified in its preamble, we will accept it anyway.   *)
   301         lines
   302       else
   303         error "preamble in DIMACS CNF file contains a line that does not begin with \"c \" or \"p \""
   304     fun int_from_string s =
   305       case Int.fromString s of
   306         SOME i => i
   307       | NONE   => error ("token " ^ quote s ^ " in DIMACS CNF file is not a number")
   308     fun clauses xs =
   309       let
   310         val (xs1, xs2) = take_prefix (fn i => i <> 0) xs
   311       in
   312         case xs2 of
   313           []      => [xs1]
   314         | (0::[]) => [xs1]
   315         | (0::tl) => xs1 :: clauses tl
   316         | _       => raise Fail "SAT_Solver.clauses"
   317       end
   318     fun literal_from_int i =
   319       (i<>0 orelse error "variable index in DIMACS CNF file is 0";
   320       if i>0 then
   321         Prop_Logic.BoolVar i
   322       else
   323         Prop_Logic.Not (Prop_Logic.BoolVar (~i)))
   324     fun disjunction [] =
   325       error "empty clause in DIMACS CNF file"
   326       | disjunction (x::xs) =
   327       (case xs of
   328         [] => x
   329       | _  => Prop_Logic.Or (x, disjunction xs))
   330     fun conjunction [] =
   331       error "no clause in DIMACS CNF file"
   332       | conjunction (x::xs) =
   333       (case xs of
   334         [] => x
   335       | _  => Prop_Logic.And (x, conjunction xs))
   336   in
   337     (conjunction
   338     o (map disjunction)
   339     o (map (map literal_from_int))
   340     o clauses
   341     o (map int_from_string)
   342     o (maps (String.tokens (member (op =) [#" ", #"\t", #"\n"])))
   343     o filter_preamble
   344     o filter (fn l => l <> "")
   345     o split_lines
   346     o File.read)
   347       path
   348   end;
   349 
   350 (* ------------------------------------------------------------------------- *)
   351 (* solvers: a table of all registered SAT solvers                            *)
   352 (* ------------------------------------------------------------------------- *)
   353 
   354   val solvers = Synchronized.var "solvers" ([] : (string * solver) list);
   355 
   356   fun get_solvers () = Synchronized.value solvers;
   357 
   358 (* ------------------------------------------------------------------------- *)
   359 (* add_solver: updates 'solvers' by adding a new solver                      *)
   360 (* ------------------------------------------------------------------------- *)
   361 
   362   fun add_solver (name, new_solver) =
   363     Synchronized.change solvers (fn the_solvers =>
   364       let
   365         val _ = if AList.defined (op =) the_solvers name
   366           then warning ("SAT solver " ^ quote name ^ " was defined before")
   367           else ();
   368       in AList.update (op =) (name, new_solver) the_solvers end);
   369 
   370 (* ------------------------------------------------------------------------- *)
   371 (* invoke_solver: returns the solver associated with the given 'name'        *)
   372 (* Note: If no solver is associated with 'name', exception 'Option' will be  *)
   373 (*       raised.                                                             *)
   374 (* ------------------------------------------------------------------------- *)
   375 
   376   fun invoke_solver name =
   377     the (AList.lookup (op =) (get_solvers ()) name);
   378 
   379 end;  (* SAT_Solver *)
   380 
   381 
   382 (* ------------------------------------------------------------------------- *)
   383 (* Predefined SAT solvers                                                    *)
   384 (* ------------------------------------------------------------------------- *)
   385 
   386 (* ------------------------------------------------------------------------- *)
   387 (* Internal SAT solver, available as 'SAT_Solver.invoke_solver "cdclite"' --  *)
   388 (* a simplified implementation of the conflict-driven clause-learning        *)
   389 (* algorithm (cf. L. Zhang, S. Malik: "The Quest for Efficient Boolean       *)
   390 (* Satisfiability Solvers", July 2002, Fig. 2). This solver produces models  *)
   391 (* and proof traces.                                                         *)
   392 (* ------------------------------------------------------------------------- *)
   393 
   394 let
   395   type clause = int list * int
   396   type value = bool option
   397   datatype reason = Decided | Implied of clause | Level0 of int
   398   type variable = bool option * reason * int * int
   399   type proofs = int * int list Inttab.table
   400   type state =
   401     int * int list * variable Inttab.table * clause list Inttab.table * proofs
   402   exception CONFLICT of clause * state
   403   exception UNSAT of clause * state
   404 
   405   fun neg i = ~i
   406 
   407   fun lit_value lit value = if lit > 0 then value else Option.map not value
   408 
   409   fun var_of vars lit: variable = the (Inttab.lookup vars (abs lit))
   410   fun value_of vars lit = lit_value lit (#1 (var_of vars lit))
   411   fun reason_of vars lit = #2 (var_of vars lit)
   412   fun level_of vars lit = #3 (var_of vars lit)
   413 
   414   fun is_true vars lit = (value_of vars lit = SOME true)
   415   fun is_false vars lit = (value_of vars lit = SOME false)
   416   fun is_unassigned vars lit = (value_of vars lit = NONE)
   417   fun assignment_of vars lit = the_default NONE (try (value_of vars) lit)
   418 
   419   fun put_var value reason level (_, _, _, rank) = (value, reason, level, rank)
   420   fun incr_rank (value, reason, level, rank) = (value, reason, level, rank + 1)
   421   fun update_var lit f = Inttab.map_entry (abs lit) f
   422   fun add_var lit = Inttab.update (abs lit, (NONE, Decided, ~1, 0))
   423 
   424   fun assign lit r l = update_var lit (put_var (SOME (lit > 0)) r l)
   425   fun unassign lit = update_var lit (put_var NONE Decided ~1)
   426 
   427   fun add_proof [] (idx, ptab) = (idx, (idx + 1, ptab))
   428     | add_proof ps (idx, ptab) = (idx, (idx + 1, Inttab.update (idx, ps) ptab))
   429 
   430   fun level0_proof_of (Level0 idx) = SOME idx
   431     | level0_proof_of _ = NONE
   432 
   433   fun level0_proofs_of vars = map_filter (level0_proof_of o reason_of vars)
   434   fun prems_of vars (lits, p) = p :: level0_proofs_of vars lits
   435   fun mk_proof vars cls proofs = add_proof (prems_of vars cls) proofs
   436 
   437   fun push lit cls (level, trail, vars, clss, proofs) =
   438     let
   439       val (reason, proofs) =
   440         if level = 0 then apfst Level0 (mk_proof vars cls proofs)
   441         else (Implied cls, proofs)
   442     in (level, lit :: trail, assign lit reason level vars, clss, proofs) end
   443 
   444   fun push_decided lit (level, trail, vars, clss, proofs) =
   445     let val vars' = assign lit Decided (level + 1) vars
   446     in (level + 1, lit :: 0 :: trail, vars', clss, proofs) end
   447 
   448   fun prop (cls as (lits, _)) (cx as (units, state as (level, _, vars, _, _))) =
   449     if exists (is_true vars) lits then cx
   450     else if forall (is_false vars) lits then
   451       if level = 0 then raise UNSAT (cls, state)
   452       else raise CONFLICT (cls, state)
   453     else
   454       (case filter (is_unassigned vars) lits of
   455         [lit] => (lit :: units, push lit cls state)
   456       | _ => cx)
   457 
   458   fun propagate units (state as (_, _, _, clss, _)) =
   459     (case fold (fold prop o Inttab.lookup_list clss) units ([], state) of
   460       ([], state') => (NONE, state')
   461     | (units', state') => propagate units' state')
   462     handle CONFLICT (cls, state') => (SOME cls, state')
   463 
   464   fun max_unassigned (v, (NONE, _, _, rank)) (x as (_, r)) =
   465         if rank > r then (SOME v, rank) else x
   466     | max_unassigned _  x = x
   467 
   468   fun decide (state as (_, _, vars, _, _)) =
   469     (case Inttab.fold max_unassigned vars (NONE, 0) of
   470       (SOME lit, _) => SOME (lit, push_decided lit state)
   471     | (NONE, _) => NONE)
   472 
   473   fun mark lit = Inttab.update (abs lit, true)
   474   fun marked ms lit = the_default false (Inttab.lookup ms (abs lit))
   475   fun ignore l ms lit = ((lit = l) orelse marked ms lit)
   476 
   477   fun first_lit _ [] = raise Empty
   478     | first_lit _ (0 :: _) = raise Empty
   479     | first_lit pred (lit :: lits) =
   480         if pred lit then (lit, lits) else first_lit pred lits
   481 
   482   fun reason_cls_of vars lit =
   483     (case reason_of vars lit of
   484       Implied cls => cls
   485     | _ => raise Option)
   486 
   487   fun analyze conflicting_cls (level, trail, vars, _, _) =
   488     let
   489       fun back i lit (lits, p) trail ms ls ps =
   490         let
   491           val (lits0, lits') = List.partition (equal 0 o level_of vars) lits
   492           val lits1 = filter_out (ignore lit ms) lits'
   493           val lits2 = filter_out (equal level o level_of vars) lits1
   494           val i' = length lits1 - length lits2 + i
   495           val ms' = fold mark lits1 ms
   496           val ls' = lits2 @ ls
   497           val ps' = level0_proofs_of vars lits0 @ (p :: ps)
   498           val (lit', trail') = first_lit (marked ms') trail
   499         in 
   500           if i' = 1 then (neg lit', ls', rev ps')
   501           else back (i' - 1) lit' (reason_cls_of vars lit') trail' ms' ls' ps'
   502         end
   503     in back 0 0 conflicting_cls trail Inttab.empty [] [] end
   504 
   505   fun keep_clause (cls as (lits, _)) (level, trail, vars, clss, proofs) =
   506     let
   507       val vars' = fold (fn lit => update_var lit incr_rank) lits vars
   508       val clss' = fold (fn lit => Inttab.cons_list (neg lit, cls)) lits clss
   509     in (level, trail, vars', clss', proofs) end
   510 
   511   fun learn (cls as (lits, _)) = (length lits <= 2) ? keep_clause cls
   512 
   513   fun backjump _ (state as (_, [], _, _, _)) = state 
   514     | backjump i (level, 0 :: trail, vars, clss, proofs) =
   515         (level - 1, trail, vars, clss, proofs) |> (i > 1) ? backjump (i - 1)
   516     | backjump i (level, lit :: trail, vars, clss, proofs) =
   517         backjump i (level, trail, unassign lit vars, clss, proofs)
   518 
   519   fun search units state =
   520     (case propagate units state of
   521       (NONE, state' as (_, _, vars, _, _)) =>
   522         (case decide state' of
   523           NONE => SAT_Solver.SATISFIABLE (assignment_of vars)
   524         | SOME (lit, state'') => search [lit] state'')
   525     | (SOME conflicting_cls, state' as (level, trail, vars, clss, proofs)) =>
   526         let 
   527           val (lit, lits, ps) = analyze conflicting_cls state'
   528           val (idx, proofs') = add_proof ps proofs
   529           val cls = (lit :: lits, idx)
   530         in
   531           (level, trail, vars, clss, proofs')
   532           |> backjump (level - fold (Integer.max o level_of vars) lits 0)
   533           |> learn cls
   534           |> push lit cls
   535           |> search [lit]
   536         end)
   537 
   538   fun has_opposing_lits [] = false
   539     | has_opposing_lits (lit :: lits) =
   540         member (op =) lits (neg lit) orelse has_opposing_lits lits
   541 
   542   fun add_clause (cls as ([_], _)) (units, state) =
   543         let val (units', state') = prop cls (units, state)
   544         in (units', state') end
   545     | add_clause (cls as (lits, _)) (cx as (units, state)) =
   546         if has_opposing_lits lits then cx
   547         else (units, keep_clause cls state)
   548 
   549   fun mk_clause lits proofs =
   550     apfst (pair (distinct (op =) lits)) (add_proof [] proofs)
   551 
   552   fun solve litss =
   553     let
   554       val (clss, proofs) = fold_map mk_clause litss (0, Inttab.empty)
   555       val vars = fold (fold add_var) litss Inttab.empty
   556       val state = (0, [], vars, Inttab.empty, proofs)
   557     in uncurry search (fold add_clause clss ([], state)) end
   558     handle UNSAT (conflicting_cls, (_, _, vars, _, proofs)) =>
   559       let val (idx, (_, ptab)) = mk_proof vars conflicting_cls proofs
   560       in SAT_Solver.UNSATISFIABLE (SOME (ptab, idx)) end
   561 
   562   fun variable_of (Prop_Logic.BoolVar 0) = error "bad propositional variable"
   563     | variable_of (Prop_Logic.BoolVar i) = i
   564     | variable_of _ = error "expected formula in CNF"
   565   fun literal_of (Prop_Logic.Not fm) = neg (variable_of fm)
   566     | literal_of fm = variable_of fm
   567   fun clause_of (Prop_Logic.Or (fm1, fm2)) = clause_of fm1 @ clause_of fm2
   568     | clause_of fm = [literal_of fm]
   569   fun clauses_of (Prop_Logic.And (fm1, fm2)) = clauses_of fm1 @ clauses_of fm2
   570     | clauses_of Prop_Logic.True = [[1, ~1]]
   571     | clauses_of Prop_Logic.False = [[1], [~1]]
   572     | clauses_of fm = [clause_of fm]
   573 
   574   fun dpll_solver fm =
   575     let val fm' = if Prop_Logic.is_cnf fm then fm else Prop_Logic.defcnf fm
   576     in solve (clauses_of fm') end
   577 in
   578   SAT_Solver.add_solver ("cdclite", dpll_solver)
   579 end;
   580 
   581 (* ------------------------------------------------------------------------- *)
   582 (* Internal SAT solver, available as 'SAT_Solver.invoke_solver "auto"': uses *)
   583 (* the last installed solver (other than "auto" itself) that does not raise  *)
   584 (* 'NOT_CONFIGURED'.  (However, the solver may return 'UNKNOWN'.)            *)
   585 (* ------------------------------------------------------------------------- *)
   586 
   587 let
   588   fun auto_solver fm =
   589   let
   590     fun loop [] =
   591       SAT_Solver.UNKNOWN
   592       | loop ((name, solver)::solvers) =
   593       if name="auto" then
   594         (* do not call solver "auto" from within "auto" *)
   595         loop solvers
   596       else (
   597         (* apply 'solver' to 'fm' *)
   598         solver fm
   599           handle SAT_Solver.NOT_CONFIGURED => loop solvers
   600       )
   601   in
   602     loop (SAT_Solver.get_solvers ())
   603   end
   604 in
   605   SAT_Solver.add_solver ("auto", auto_solver)
   606 end;
   607 
   608 (* ------------------------------------------------------------------------- *)
   609 (* MiniSat 1.14                                                              *)
   610 (* (http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/)            *)
   611 (* ------------------------------------------------------------------------- *)
   612 
   613 (* ------------------------------------------------------------------------- *)
   614 (* "minisat_with_proofs" requires a modified version of MiniSat 1.14 by John *)
   615 (* Matthews, which can output ASCII proof traces.  Replaying binary proof    *)
   616 (* traces generated by MiniSat-p_v1.14 has _not_ been implemented.           *)
   617 (* ------------------------------------------------------------------------- *)
   618 
   619 (* add "minisat_with_proofs" _before_ "minisat" to the available solvers, so *)
   620 (* that the latter is preferred by the "auto" solver                         *)
   621 
   622 (* There is a complication that is dealt with in the code below: MiniSat     *)
   623 (* introduces IDs for original clauses in the proof trace.  It does not (in  *)
   624 (* general) follow the convention that the original clauses are numbered     *)
   625 (* from 0 to n-1 (where n is the number of clauses in the formula).          *)
   626 
   627 let
   628   exception INVALID_PROOF of string
   629   fun minisat_with_proofs fm =
   630   let
   631     val _          = if (getenv "MINISAT_HOME") = "" then raise SAT_Solver.NOT_CONFIGURED else ()
   632     val serial_str = serial_string ()
   633     val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
   634     val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
   635     val proofpath  = File.tmp_path (Path.explode ("result" ^ serial_str ^ ".prf"))
   636     val cmd        = getenv "MINISAT_HOME" ^ "/minisat " ^ File.shell_path inpath ^ " -r " ^ File.shell_path outpath ^ " -t " ^ File.shell_path proofpath ^ "> /dev/null"
   637     fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath fm
   638     fun readfn ()  = SAT_Solver.read_std_result_file outpath ("SAT", "", "UNSAT")
   639     val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
   640     val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else ()
   641     val cnf        = Prop_Logic.defcnf fm
   642     val result     = SAT_Solver.make_external_solver cmd writefn readfn cnf
   643     val _          = try File.rm inpath
   644     val _          = try File.rm outpath
   645   in  case result of
   646     SAT_Solver.UNSATISFIABLE NONE =>
   647     (let
   648       val proof_lines = (split_lines o File.read) proofpath
   649         handle IO.Io _ => raise INVALID_PROOF "Could not read file \"result.prf\""
   650       (* representation of clauses as ordered lists of literals (with duplicates removed) *)
   651       fun clause_to_lit_list (Prop_Logic.Or (fm1, fm2)) =
   652         Ord_List.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2)
   653         | clause_to_lit_list (Prop_Logic.BoolVar i) =
   654         [i]
   655         | clause_to_lit_list (Prop_Logic.Not (Prop_Logic.BoolVar i)) =
   656         [~i]
   657         | clause_to_lit_list _ =
   658         raise INVALID_PROOF "Error: invalid clause in CNF formula."
   659       fun cnf_number_of_clauses (Prop_Logic.And (fm1, fm2)) =
   660         cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
   661         | cnf_number_of_clauses _ =
   662         1
   663       val number_of_clauses = cnf_number_of_clauses cnf
   664       (* int list array *)
   665       val clauses = Array.array (number_of_clauses, [])
   666       (* initialize the 'clauses' array *)
   667       fun init_array (Prop_Logic.And (fm1, fm2), n) =
   668         init_array (fm2, init_array (fm1, n))
   669         | init_array (fm, n) =
   670         (Array.update (clauses, n, clause_to_lit_list fm); n+1)
   671       val _ = init_array (cnf, 0)
   672       (* optimization for the common case where MiniSat "R"s clauses in their *)
   673       (* original order:                                                      *)
   674       val last_ref_clause = Unsynchronized.ref (number_of_clauses - 1)
   675       (* search the 'clauses' array for the given list of literals 'lits', *)
   676       (* starting at index '!last_ref_clause + 1'                          *)
   677       fun original_clause_id lits =
   678       let
   679         fun original_clause_id_from index =
   680           if index = number_of_clauses then
   681             (* search from beginning again *)
   682             original_clause_id_from 0
   683           (* both 'lits' and the list of literals used in 'clauses' are sorted, so *)
   684           (* testing for equality should suffice -- barring duplicate literals     *)
   685           else if Array.sub (clauses, index) = lits then (
   686             (* success *)
   687             last_ref_clause := index;
   688             SOME index
   689           ) else if index = !last_ref_clause then
   690             (* failure *)
   691             NONE
   692           else
   693             (* continue search *)
   694             original_clause_id_from (index + 1)
   695       in
   696         original_clause_id_from (!last_ref_clause + 1)
   697       end
   698       fun int_from_string s =
   699         (case Int.fromString s of
   700           SOME i => i
   701         | NONE   => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered)."))
   702       (* parse the proof file *)
   703       val clause_table  = Unsynchronized.ref (Inttab.empty : int list Inttab.table)
   704       val empty_id      = Unsynchronized.ref ~1
   705       (* contains a mapping from clause IDs as used by MiniSat to clause IDs in *)
   706       (* our proof format, where original clauses are numbered starting from 0  *)
   707       val clause_id_map = Unsynchronized.ref (Inttab.empty : int Inttab.table)
   708       fun sat_to_proof id = (
   709         case Inttab.lookup (!clause_id_map) id of
   710           SOME id' => id'
   711         | NONE     => raise INVALID_PROOF ("Clause ID " ^ string_of_int id ^ " used, but not defined.")
   712       )
   713       val next_id = Unsynchronized.ref (number_of_clauses - 1)
   714       fun process_tokens [] =
   715         ()
   716         | process_tokens (tok::toks) =
   717         if tok="R" then (
   718           case toks of
   719             id::sep::lits =>
   720             let
   721               val _        = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"R\" disallowed after \"X\"."
   722               val cid      = int_from_string id
   723               val _        = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
   724               val ls       = sort int_ord (map int_from_string lits)
   725               val proof_id = case original_clause_id ls of
   726                                SOME orig_id => orig_id
   727                              | NONE         => raise INVALID_PROOF ("Original clause (new ID is " ^ id ^ ") not found.")
   728             in
   729               (* extend the mapping of clause IDs with this newly defined ID *)
   730               clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map)
   731                 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"R\").")
   732               (* the proof itself doesn't change *)
   733             end
   734           | _ =>
   735             raise INVALID_PROOF "File format error: \"R\" followed by an insufficient number of tokens."
   736         ) else if tok="C" then (
   737           case toks of
   738             id::sep::ids =>
   739             let
   740               val _        = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"C\" disallowed after \"X\"."
   741               val cid      = int_from_string id
   742               val _        = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
   743               (* ignore the pivot literals in MiniSat's trace *)
   744               fun unevens []             = raise INVALID_PROOF "File format error: \"C\" followed by an even number of IDs."
   745                 | unevens (x :: [])      = x :: []
   746                 | unevens (x :: _ :: xs) = x :: unevens xs
   747               val rs       = (map sat_to_proof o unevens o map int_from_string) ids
   748               (* extend the mapping of clause IDs with this newly defined ID *)
   749               val proof_id = Unsynchronized.inc next_id
   750               val _        = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map)
   751                                handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"C\").")
   752             in
   753               (* update clause table *)
   754               clause_table := Inttab.update_new (proof_id, rs) (!clause_table)
   755                 handle Inttab.DUP _ => raise INVALID_PROOF ("Error: internal ID for clause " ^ id ^ " already used.")
   756             end
   757           | _ =>
   758             raise INVALID_PROOF "File format error: \"C\" followed by an insufficient number of tokens."
   759         ) else if tok="D" then (
   760           case toks of
   761             [id] =>
   762             let
   763               val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"D\" disallowed after \"X\"."
   764               val _ = sat_to_proof (int_from_string id)
   765             in
   766               (* simply ignore "D" *)
   767               ()
   768             end
   769           | _ =>
   770             raise INVALID_PROOF "File format error: \"D\" followed by an illegal number of tokens."
   771         ) else if tok="X" then (
   772           case toks of
   773             [id1, id2] =>
   774             let
   775               val _            = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one end-of-proof statement."
   776               val _            = sat_to_proof (int_from_string id1)
   777               val new_empty_id = sat_to_proof (int_from_string id2)
   778             in
   779               (* update conflict id *)
   780               empty_id := new_empty_id
   781             end
   782           | _ =>
   783             raise INVALID_PROOF "File format error: \"X\" followed by an illegal number of tokens."
   784         ) else
   785           raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.")
   786       fun process_lines [] =
   787         ()
   788         | process_lines (l::ls) = (
   789           process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l);
   790           process_lines ls
   791         )
   792       (* proof *)
   793       val _ = process_lines proof_lines
   794       val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
   795     in
   796       SAT_Solver.UNSATISFIABLE (SOME (!clause_table, !empty_id))
   797     end handle INVALID_PROOF reason => (warning reason; SAT_Solver.UNSATISFIABLE NONE))
   798   | result =>
   799     result
   800   end
   801 in
   802   SAT_Solver.add_solver ("minisat_with_proofs", minisat_with_proofs)
   803 end;
   804 
   805 let
   806   fun minisat fm =
   807   let
   808     val _          = if getenv "MINISAT_HOME" = "" then raise SAT_Solver.NOT_CONFIGURED else ()
   809     val serial_str = serial_string ()
   810     val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
   811     val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
   812     val cmd        = getenv "MINISAT_HOME" ^ "/minisat " ^ File.shell_path inpath ^ " -r " ^ File.shell_path outpath ^ " > /dev/null"
   813     fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
   814     fun readfn ()  = SAT_Solver.read_std_result_file outpath ("SAT", "", "UNSAT")
   815     val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
   816     val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else ()
   817     val result     = SAT_Solver.make_external_solver cmd writefn readfn fm
   818     val _          = try File.rm inpath
   819     val _          = try File.rm outpath
   820   in
   821     result
   822   end
   823 in
   824   SAT_Solver.add_solver ("minisat", minisat)
   825 end;
   826 
   827 (* ------------------------------------------------------------------------- *)
   828 (* zChaff (http://www.princeton.edu/~chaff/zchaff.html)                      *)
   829 (* ------------------------------------------------------------------------- *)
   830 
   831 (* ------------------------------------------------------------------------- *)
   832 (* 'zchaff_with_proofs' applies the "zchaff" prover to a formula, and if     *)
   833 (* zChaff finds that the formula is unsatisfiable, a proof of this is read   *)
   834 (* from a file "resolve_trace" that was generated by zChaff.  See the code   *)
   835 (* below for the expected format of the "resolve_trace" file.  Aside from    *)
   836 (* some basic syntactic checks, no verification of the proof is performed.   *)
   837 (* ------------------------------------------------------------------------- *)
   838 
   839 (* add "zchaff_with_proofs" _before_ "zchaff" to the available solvers, so   *)
   840 (* that the latter is preferred by the "auto" solver                         *)
   841 
   842 let
   843   exception INVALID_PROOF of string
   844   fun zchaff_with_proofs fm =
   845   case SAT_Solver.invoke_solver "zchaff" fm of
   846     SAT_Solver.UNSATISFIABLE NONE =>
   847     (let
   848       (* FIXME File.tmp_path (!?) *)
   849       val proof_lines = ((split_lines o File.read) (Path.explode "resolve_trace"))
   850         handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\""
   851       fun cnf_number_of_clauses (Prop_Logic.And (fm1, fm2)) =
   852             cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
   853         | cnf_number_of_clauses _ = 1
   854       fun int_from_string s = (
   855         case Int.fromString s of
   856           SOME i => i
   857         | NONE   => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).")
   858       )
   859       (* parse the "resolve_trace" file *)
   860       val clause_offset = Unsynchronized.ref ~1
   861       val clause_table  = Unsynchronized.ref (Inttab.empty : int list Inttab.table)
   862       val empty_id      = Unsynchronized.ref ~1
   863       fun process_tokens [] =
   864         ()
   865         | process_tokens (tok::toks) =
   866         if tok="CL:" then (
   867           case toks of
   868             id::sep::ids =>
   869             let
   870               val _   = if !clause_offset = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"VAR:\".")
   871               val _   = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"CONF:\".")
   872               val cid = int_from_string id
   873               val _   = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
   874               val rs  = map int_from_string ids
   875             in
   876               (* update clause table *)
   877               clause_table := Inttab.update_new (cid, rs) (!clause_table)
   878                 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once.")
   879             end
   880           | _ =>
   881             raise INVALID_PROOF "File format error: \"CL:\" followed by an insufficient number of tokens."
   882         ) else if tok="VAR:" then (
   883           case toks of
   884             id::levsep::levid::valsep::valid::antesep::anteid::litsep::lits =>
   885             let
   886               val _   = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"VAR:\" disallowed after \"CONF:\".")
   887               (* set 'clause_offset' to the largest used clause ID *)
   888               val _   = if !clause_offset = ~1 then clause_offset :=
   889                 (case Inttab.max (!clause_table) of
   890                   SOME (id, _) => id
   891                 | NONE => cnf_number_of_clauses (Prop_Logic.defcnf fm) - 1  (* the first clause ID is 0, not 1 *))
   892                 else
   893                   ()
   894               val vid = int_from_string id
   895               val _   = if levsep = "L:" then () else raise INVALID_PROOF ("File format error: \"L:\" expected (" ^ quote levsep ^ " encountered).")
   896               val _   = int_from_string levid
   897               val _   = if valsep = "V:" then () else raise INVALID_PROOF ("File format error: \"V:\" expected (" ^ quote valsep ^ " encountered).")
   898               val _   = int_from_string valid
   899               val _   = if antesep = "A:" then () else raise INVALID_PROOF ("File format error: \"A:\" expected (" ^ quote antesep ^ " encountered).")
   900               val aid = int_from_string anteid
   901               val _   = if litsep = "Lits:" then () else raise INVALID_PROOF ("File format error: \"Lits:\" expected (" ^ quote litsep ^ " encountered).")
   902               val ls  = map int_from_string lits
   903               (* convert the data provided by zChaff to our resolution-style proof format *)
   904               (* each "VAR:" line defines a unit clause, the resolvents are implicitly    *)
   905               (* given by the literals in the antecedent clause                           *)
   906               (* we use the sum of '!clause_offset' and the variable ID as clause ID for the unit clause *)
   907               val cid = !clause_offset + vid
   908               (* the low bit of each literal gives its sign (positive/negative), therefore  *)
   909               (* we have to divide each literal by 2 to obtain the proper variable ID; then *)
   910               (* we add '!clause_offset' to obtain the ID of the corresponding unit clause  *)
   911               val vids = filter (not_equal vid) (map (fn l => l div 2) ls)
   912               val rs   = aid :: map (fn v => !clause_offset + v) vids
   913             in
   914               (* update clause table *)
   915               clause_table := Inttab.update_new (cid, rs) (!clause_table)
   916                 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int cid ^ " (derived from antecedent for variable " ^ id ^ ") already defined.")
   917             end
   918           | _ =>
   919             raise INVALID_PROOF "File format error: \"VAR:\" followed by an insufficient number of tokens."
   920         ) else if tok="CONF:" then (
   921           case toks of
   922             id::sep::ids =>
   923             let
   924               val _   = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one conflicting clause specified."
   925               val cid = int_from_string id
   926               val _   = if sep = "==" then () else raise INVALID_PROOF ("File format error: \"==\" expected (" ^ quote sep ^ " encountered).")
   927               val ls  = map int_from_string ids
   928               (* the conflict clause must be resolved with the unit clauses *)
   929               (* for its literals to obtain the empty clause                *)
   930               val vids         = map (fn l => l div 2) ls
   931               val rs           = cid :: map (fn v => !clause_offset + v) vids
   932               val new_empty_id = the_default (!clause_offset) (Option.map fst (Inttab.max (!clause_table))) + 1
   933             in
   934               (* update clause table and conflict id *)
   935               clause_table := Inttab.update_new (new_empty_id, rs) (!clause_table)
   936                 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int new_empty_id ^ " (empty clause derived from clause " ^ id ^ ") already defined.");
   937               empty_id     := new_empty_id
   938             end
   939           | _ =>
   940             raise INVALID_PROOF "File format error: \"CONF:\" followed by an insufficient number of tokens."
   941         ) else
   942           raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.")
   943       fun process_lines [] =
   944         ()
   945         | process_lines (l::ls) = (
   946           process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l);
   947           process_lines ls
   948         )
   949       (* proof *)
   950       val _ = process_lines proof_lines
   951       val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
   952     in
   953       SAT_Solver.UNSATISFIABLE (SOME (!clause_table, !empty_id))
   954     end handle INVALID_PROOF reason => (warning reason; SAT_Solver.UNSATISFIABLE NONE))
   955   | result =>
   956     result
   957 in
   958   SAT_Solver.add_solver ("zchaff_with_proofs", zchaff_with_proofs)
   959 end;
   960 
   961 let
   962   fun zchaff fm =
   963   let
   964     val _          = if getenv "ZCHAFF_HOME" = "" then raise SAT_Solver.NOT_CONFIGURED else ()
   965     val serial_str = serial_string ()
   966     val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
   967     val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
   968     val cmd        = getenv "ZCHAFF_HOME" ^ "/zchaff " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath
   969     fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
   970     fun readfn ()  = SAT_Solver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
   971     val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
   972     val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else ()
   973     val result     = SAT_Solver.make_external_solver cmd writefn readfn fm
   974     val _          = try File.rm inpath
   975     val _          = try File.rm outpath
   976   in
   977     result
   978   end
   979 in
   980   SAT_Solver.add_solver ("zchaff", zchaff)
   981 end;
   982 
   983 (* ------------------------------------------------------------------------- *)
   984 (* BerkMin 561 (http://eigold.tripod.com/BerkMin.html)                       *)
   985 (* ------------------------------------------------------------------------- *)
   986 
   987 let
   988   fun berkmin fm =
   989   let
   990     val _          = if (getenv "BERKMIN_HOME") = "" then raise SAT_Solver.NOT_CONFIGURED else ()
   991     val serial_str = serial_string ()
   992     val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
   993     val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
   994     val exec       = getenv "BERKMIN_EXE"
   995     val cmd        = getenv "BERKMIN_HOME" ^ "/" ^ (if exec = "" then "BerkMin561" else exec) ^ " " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath
   996     fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
   997     fun readfn ()  = SAT_Solver.read_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
   998     val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
   999     val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else ()
  1000     val result     = SAT_Solver.make_external_solver cmd writefn readfn fm
  1001     val _          = try File.rm inpath
  1002     val _          = try File.rm outpath
  1003   in
  1004     result
  1005   end
  1006 in
  1007   SAT_Solver.add_solver ("berkmin", berkmin)
  1008 end;
  1009 
  1010 (* ------------------------------------------------------------------------- *)
  1011 (* Jerusat 1.3 (http://www.cs.tau.ac.il/~ale1/)                              *)
  1012 (* ------------------------------------------------------------------------- *)
  1013 
  1014 let
  1015   fun jerusat fm =
  1016   let
  1017     val _          = if (getenv "JERUSAT_HOME") = "" then raise SAT_Solver.NOT_CONFIGURED else ()
  1018     val serial_str = serial_string ()
  1019     val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
  1020     val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
  1021     val cmd        = getenv "JERUSAT_HOME" ^ "/Jerusat1.3 " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath
  1022     fun writefn fm = SAT_Solver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
  1023     fun readfn ()  = SAT_Solver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
  1024     val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
  1025     val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else ()
  1026     val result     = SAT_Solver.make_external_solver cmd writefn readfn fm
  1027     val _          = try File.rm inpath
  1028     val _          = try File.rm outpath
  1029   in
  1030     result
  1031   end
  1032 in
  1033   SAT_Solver.add_solver ("jerusat", jerusat)
  1034 end;