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