src/HOL/Tools/sat_solver.ML
author wenzelm
Wed Oct 21 00:36:12 2009 +0200 (2009-10-21)
changeset 33035 15eab423e573
parent 32952 aeb1e44fbc19
child 33039 5018f6a76b3f
permissions -rw-r--r--
standardized basic operations on type option;
     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 (List.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; system 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         | _       => sys_error "this cannot happen"
   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.fields (fn c => c mem [#" ", #"\t", #"\n"])))
   354     o filter_preamble
   355     o (List.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) =
   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       i mem xs
   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))   = (forced_vars fm1) inter_int (forced_vars fm2)
   475         | forced_vars (And (fm1, fm2))  = (forced_vars fm1) union_int (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         Library.find_first (fn i => not (i mem_int xs) andalso not ((~i) mem_int xs)) 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         (if name="dpll" orelse name="enumerate" then
   547           warning ("Using SAT solver " ^ quote name ^ "; for better performance, consider using an external solver.")
   548         else
   549           tracing ("Using SAT solver " ^ quote name ^ "."));
   550         (* apply 'solver' to 'fm' *)
   551         solver fm
   552           handle SatSolver.NOT_CONFIGURED => loop solvers
   553       )
   554   in
   555     loop (!SatSolver.solvers)
   556   end
   557 in
   558   SatSolver.add_solver ("auto", auto_solver)
   559 end;
   560 
   561 (* ------------------------------------------------------------------------- *)
   562 (* MiniSat 1.14                                                              *)
   563 (* (http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/)            *)
   564 (* ------------------------------------------------------------------------- *)
   565 
   566 (* ------------------------------------------------------------------------- *)
   567 (* "minisat_with_proofs" requires a modified version of MiniSat 1.14 by John *)
   568 (* Matthews, which can output ASCII proof traces.  Replaying binary proof    *)
   569 (* traces generated by MiniSat-p_v1.14 has _not_ been implemented.           *)
   570 (* ------------------------------------------------------------------------- *)
   571 
   572 (* add "minisat_with_proofs" _before_ "minisat" to the available solvers, so *)
   573 (* that the latter is preferred by the "auto" solver                         *)
   574 
   575 (* There is a complication that is dealt with in the code below: MiniSat     *)
   576 (* introduces IDs for original clauses in the proof trace.  It does not (in  *)
   577 (* general) follow the convention that the original clauses are numbered     *)
   578 (* from 0 to n-1 (where n is the number of clauses in the formula).          *)
   579 
   580 let
   581   exception INVALID_PROOF of string
   582   fun minisat_with_proofs fm =
   583   let
   584     val _          = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
   585     val serial_str = serial_string ()
   586     val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
   587     val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
   588     val proofpath  = File.tmp_path (Path.explode ("result" ^ serial_str ^ ".prf"))
   589     val cmd        = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " -t " ^ (Path.implode proofpath) ^ "> /dev/null"
   590     fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm
   591     fun readfn ()  = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
   592     val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
   593     val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
   594     val cnf        = PropLogic.defcnf fm
   595     val result     = SatSolver.make_external_solver cmd writefn readfn cnf
   596     val _          = try File.rm inpath
   597     val _          = try File.rm outpath
   598   in  case result of
   599     SatSolver.UNSATISFIABLE NONE =>
   600     (let
   601       (* string list *)
   602       val proof_lines = (split_lines o File.read) proofpath
   603         handle IO.Io _ => raise INVALID_PROOF "Could not read file \"result.prf\""
   604       (* representation of clauses as ordered lists of literals (with duplicates removed) *)
   605       (* prop_formula -> int list *)
   606       fun clause_to_lit_list (PropLogic.Or (fm1, fm2)) =
   607         OrdList.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2)
   608         | clause_to_lit_list (PropLogic.BoolVar i) =
   609         [i]
   610         | clause_to_lit_list (PropLogic.Not (PropLogic.BoolVar i)) =
   611         [~i]
   612         | clause_to_lit_list _ =
   613         raise INVALID_PROOF "Error: invalid clause in CNF formula."
   614       (* prop_formula -> int *)
   615       fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) =
   616         cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
   617         | cnf_number_of_clauses _ =
   618         1
   619       val number_of_clauses = cnf_number_of_clauses cnf
   620       (* int list array *)
   621       val clauses = Array.array (number_of_clauses, [])
   622       (* initialize the 'clauses' array *)
   623       (* prop_formula * int -> int *)
   624       fun init_array (PropLogic.And (fm1, fm2), n) =
   625         init_array (fm2, init_array (fm1, n))
   626         | init_array (fm, n) =
   627         (Array.update (clauses, n, clause_to_lit_list fm); n+1)
   628       val _ = init_array (cnf, 0)
   629       (* optimization for the common case where MiniSat "R"s clauses in their *)
   630       (* original order:                                                      *)
   631       val last_ref_clause = Unsynchronized.ref (number_of_clauses - 1)
   632       (* search the 'clauses' array for the given list of literals 'lits', *)
   633       (* starting at index '!last_ref_clause + 1'                          *)
   634       (* int list -> int option *)
   635       fun original_clause_id lits =
   636       let
   637         fun original_clause_id_from index =
   638           if index = number_of_clauses then
   639             (* search from beginning again *)
   640             original_clause_id_from 0
   641           (* both 'lits' and the list of literals used in 'clauses' are sorted, so *)
   642           (* testing for equality should suffice -- barring duplicate literals     *)
   643           else if Array.sub (clauses, index) = lits then (
   644             (* success *)
   645             last_ref_clause := index;
   646             SOME index
   647           ) else if index = !last_ref_clause then
   648             (* failure *)
   649             NONE
   650           else
   651             (* continue search *)
   652             original_clause_id_from (index + 1)
   653       in
   654         original_clause_id_from (!last_ref_clause + 1)
   655       end
   656       (* string -> int *)
   657       fun int_from_string s = (
   658         case Int.fromString s of
   659           SOME i => i
   660         | NONE   => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).")
   661       )
   662       (* parse the proof file *)
   663       val clause_table  = Unsynchronized.ref (Inttab.empty : int list Inttab.table)
   664       val empty_id      = Unsynchronized.ref ~1
   665       (* contains a mapping from clause IDs as used by MiniSat to clause IDs in *)
   666       (* our proof format, where original clauses are numbered starting from 0  *)
   667       val clause_id_map = Unsynchronized.ref (Inttab.empty : int Inttab.table)
   668       fun sat_to_proof id = (
   669         case Inttab.lookup (!clause_id_map) id of
   670           SOME id' => id'
   671         | NONE     => raise INVALID_PROOF ("Clause ID " ^ Int.toString id ^ " used, but not defined.")
   672       )
   673       val next_id = Unsynchronized.ref (number_of_clauses - 1)
   674       (* string list -> unit *)
   675       fun process_tokens [] =
   676         ()
   677         | process_tokens (tok::toks) =
   678         if tok="R" then (
   679           case toks of
   680             id::sep::lits =>
   681             let
   682               val _        = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"R\" disallowed after \"X\"."
   683               val cid      = int_from_string id
   684               val _        = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
   685               val ls       = sort int_ord (map int_from_string lits)
   686               val proof_id = case original_clause_id ls of
   687                                SOME orig_id => orig_id
   688                              | NONE         => raise INVALID_PROOF ("Original clause (new ID is " ^ id ^ ") not found.")
   689             in
   690               (* extend the mapping of clause IDs with this newly defined ID *)
   691               clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map)
   692                 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"R\").")
   693               (* the proof itself doesn't change *)
   694             end
   695           | _ =>
   696             raise INVALID_PROOF "File format error: \"R\" followed by an insufficient number of tokens."
   697         ) else if tok="C" then (
   698           case toks of
   699             id::sep::ids =>
   700             let
   701               val _        = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"C\" disallowed after \"X\"."
   702               val cid      = int_from_string id
   703               val _        = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
   704               (* ignore the pivot literals in MiniSat's trace *)
   705               fun unevens []             = raise INVALID_PROOF "File format error: \"C\" followed by an even number of IDs."
   706                 | unevens (x :: [])      = x :: []
   707                 | unevens (x :: _ :: xs) = x :: unevens xs
   708               val rs       = (map sat_to_proof o unevens o map int_from_string) ids
   709               (* extend the mapping of clause IDs with this newly defined ID *)
   710               val proof_id = Unsynchronized.inc next_id
   711               val _        = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map)
   712                                handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"C\").")
   713             in
   714               (* update clause table *)
   715               clause_table := Inttab.update_new (proof_id, rs) (!clause_table)
   716                 handle Inttab.DUP _ => raise INVALID_PROOF ("Error: internal ID for clause " ^ id ^ " already used.")
   717             end
   718           | _ =>
   719             raise INVALID_PROOF "File format error: \"C\" followed by an insufficient number of tokens."
   720         ) else if tok="D" then (
   721           case toks of
   722             [id] =>
   723             let
   724               val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"D\" disallowed after \"X\"."
   725               val _ = sat_to_proof (int_from_string id)
   726             in
   727               (* simply ignore "D" *)
   728               ()
   729             end
   730           | _ =>
   731             raise INVALID_PROOF "File format error: \"D\" followed by an illegal number of tokens."
   732         ) else if tok="X" then (
   733           case toks of
   734             [id1, id2] =>
   735             let
   736               val _            = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one end-of-proof statement."
   737               val _            = sat_to_proof (int_from_string id1)
   738               val new_empty_id = sat_to_proof (int_from_string id2)
   739             in
   740               (* update conflict id *)
   741               empty_id := new_empty_id
   742             end
   743           | _ =>
   744             raise INVALID_PROOF "File format error: \"X\" followed by an illegal number of tokens."
   745         ) else
   746           raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.")
   747       (* string list -> unit *)
   748       fun process_lines [] =
   749         ()
   750         | process_lines (l::ls) = (
   751           process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l);
   752           process_lines ls
   753         )
   754       (* proof *)
   755       val _ = process_lines proof_lines
   756       val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
   757     in
   758       SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id))
   759     end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE))
   760   | result =>
   761     result
   762   end
   763 in
   764   SatSolver.add_solver ("minisat_with_proofs", minisat_with_proofs)
   765 end;
   766 
   767 let
   768   fun minisat fm =
   769   let
   770     val _          = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
   771     val serial_str = serial_string ()
   772     val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
   773     val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
   774     val cmd        = (getenv "MINISAT_HOME") ^ "/minisat " ^ (Path.implode inpath) ^ " -r " ^ (Path.implode outpath) ^ " > /dev/null"
   775     fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
   776     fun readfn ()  = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
   777     val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
   778     val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
   779     val result     = SatSolver.make_external_solver cmd writefn readfn fm
   780     val _          = try File.rm inpath
   781     val _          = try File.rm outpath
   782   in
   783     result
   784   end
   785 in
   786   SatSolver.add_solver ("minisat", minisat)
   787 end;
   788 
   789 (* ------------------------------------------------------------------------- *)
   790 (* zChaff (http://www.princeton.edu/~chaff/zchaff.html)                      *)
   791 (* ------------------------------------------------------------------------- *)
   792 
   793 (* ------------------------------------------------------------------------- *)
   794 (* 'zchaff_with_proofs' applies the "zchaff" prover to a formula, and if     *)
   795 (* zChaff finds that the formula is unsatisfiable, a proof of this is read   *)
   796 (* from a file "resolve_trace" that was generated by zChaff.  See the code   *)
   797 (* below for the expected format of the "resolve_trace" file.  Aside from    *)
   798 (* some basic syntactic checks, no verification of the proof is performed.   *)
   799 (* ------------------------------------------------------------------------- *)
   800 
   801 (* add "zchaff_with_proofs" _before_ "zchaff" to the available solvers, so   *)
   802 (* that the latter is preferred by the "auto" solver                         *)
   803 
   804 let
   805   exception INVALID_PROOF of string
   806   fun zchaff_with_proofs fm =
   807   case SatSolver.invoke_solver "zchaff" fm of
   808     SatSolver.UNSATISFIABLE NONE =>
   809     (let
   810       (* string list *)
   811       val proof_lines = ((split_lines o File.read) (Path.explode "resolve_trace"))
   812         handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\""
   813       (* PropLogic.prop_formula -> int *)
   814       fun cnf_number_of_clauses (PropLogic.And (fm1, fm2)) = cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
   815         | cnf_number_of_clauses _                          = 1
   816       (* string -> int *)
   817       fun int_from_string s = (
   818         case Int.fromString s of
   819           SOME i => i
   820         | NONE   => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).")
   821       )
   822       (* parse the "resolve_trace" file *)
   823       val clause_offset = Unsynchronized.ref ~1
   824       val clause_table  = Unsynchronized.ref (Inttab.empty : int list Inttab.table)
   825       val empty_id      = Unsynchronized.ref ~1
   826       (* string list -> unit *)
   827       fun process_tokens [] =
   828         ()
   829         | process_tokens (tok::toks) =
   830         if tok="CL:" then (
   831           case toks of
   832             id::sep::ids =>
   833             let
   834               val _   = if !clause_offset = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"VAR:\".")
   835               val _   = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"CONF:\".")
   836               val cid = int_from_string id
   837               val _   = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
   838               val rs  = map int_from_string ids
   839             in
   840               (* update clause table *)
   841               clause_table := Inttab.update_new (cid, rs) (!clause_table)
   842                 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once.")
   843             end
   844           | _ =>
   845             raise INVALID_PROOF "File format error: \"CL:\" followed by an insufficient number of tokens."
   846         ) else if tok="VAR:" then (
   847           case toks of
   848             id::levsep::levid::valsep::valid::antesep::anteid::litsep::lits =>
   849             let
   850               val _   = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"VAR:\" disallowed after \"CONF:\".")
   851               (* set 'clause_offset' to the largest used clause ID *)
   852               val _   = if !clause_offset = ~1 then clause_offset :=
   853                 (case Inttab.max_key (!clause_table) of
   854                   SOME id => id
   855                 | NONE    => cnf_number_of_clauses (PropLogic.defcnf fm) - 1  (* the first clause ID is 0, not 1 *))
   856                 else
   857                   ()
   858               val vid = int_from_string id
   859               val _   = if levsep = "L:" then () else raise INVALID_PROOF ("File format error: \"L:\" expected (" ^ quote levsep ^ " encountered).")
   860               val _   = int_from_string levid
   861               val _   = if valsep = "V:" then () else raise INVALID_PROOF ("File format error: \"V:\" expected (" ^ quote valsep ^ " encountered).")
   862               val _   = int_from_string valid
   863               val _   = if antesep = "A:" then () else raise INVALID_PROOF ("File format error: \"A:\" expected (" ^ quote antesep ^ " encountered).")
   864               val aid = int_from_string anteid
   865               val _   = if litsep = "Lits:" then () else raise INVALID_PROOF ("File format error: \"Lits:\" expected (" ^ quote litsep ^ " encountered).")
   866               val ls  = map int_from_string lits
   867               (* convert the data provided by zChaff to our resolution-style proof format *)
   868               (* each "VAR:" line defines a unit clause, the resolvents are implicitly    *)
   869               (* given by the literals in the antecedent clause                           *)
   870               (* we use the sum of '!clause_offset' and the variable ID as clause ID for the unit clause *)
   871               val cid = !clause_offset + vid
   872               (* the low bit of each literal gives its sign (positive/negative), therefore  *)
   873               (* we have to divide each literal by 2 to obtain the proper variable ID; then *)
   874               (* we add '!clause_offset' to obtain the ID of the corresponding unit clause  *)
   875               val vids = filter (not_equal vid) (map (fn l => l div 2) ls)
   876               val rs   = aid :: map (fn v => !clause_offset + v) vids
   877             in
   878               (* update clause table *)
   879               clause_table := Inttab.update_new (cid, rs) (!clause_table)
   880                 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int cid ^ " (derived from antecedent for variable " ^ id ^ ") already defined.")
   881             end
   882           | _ =>
   883             raise INVALID_PROOF "File format error: \"VAR:\" followed by an insufficient number of tokens."
   884         ) else if tok="CONF:" then (
   885           case toks of
   886             id::sep::ids =>
   887             let
   888               val _   = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one conflicting clause specified."
   889               val cid = int_from_string id
   890               val _   = if sep = "==" then () else raise INVALID_PROOF ("File format error: \"==\" expected (" ^ quote sep ^ " encountered).")
   891               val ls  = map int_from_string ids
   892               (* the conflict clause must be resolved with the unit clauses *)
   893               (* for its literals to obtain the empty clause                *)
   894               val vids         = map (fn l => l div 2) ls
   895               val rs           = cid :: map (fn v => !clause_offset + v) vids
   896               val new_empty_id = the_default (!clause_offset) (Inttab.max_key (!clause_table)) + 1
   897             in
   898               (* update clause table and conflict id *)
   899               clause_table := Inttab.update_new (new_empty_id, rs) (!clause_table)
   900                 handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int new_empty_id ^ " (empty clause derived from clause " ^ id ^ ") already defined.");
   901               empty_id     := new_empty_id
   902             end
   903           | _ =>
   904             raise INVALID_PROOF "File format error: \"CONF:\" followed by an insufficient number of tokens."
   905         ) else
   906           raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.")
   907       (* string list -> unit *)
   908       fun process_lines [] =
   909         ()
   910         | process_lines (l::ls) = (
   911           process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l);
   912           process_lines ls
   913         )
   914       (* proof *)
   915       val _ = process_lines proof_lines
   916       val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
   917     in
   918       SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id))
   919     end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE))
   920   | result =>
   921     result
   922 in
   923   SatSolver.add_solver ("zchaff_with_proofs", zchaff_with_proofs)
   924 end;
   925 
   926 let
   927   fun zchaff fm =
   928   let
   929     val _          = if (getenv "ZCHAFF_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
   930     val serial_str = serial_string ()
   931     val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
   932     val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
   933     val cmd        = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
   934     fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
   935     fun readfn ()  = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
   936     val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
   937     val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
   938     val result     = SatSolver.make_external_solver cmd writefn readfn fm
   939     val _          = try File.rm inpath
   940     val _          = try File.rm outpath
   941   in
   942     result
   943   end
   944 in
   945   SatSolver.add_solver ("zchaff", zchaff)
   946 end;
   947 
   948 (* ------------------------------------------------------------------------- *)
   949 (* BerkMin 561 (http://eigold.tripod.com/BerkMin.html)                       *)
   950 (* ------------------------------------------------------------------------- *)
   951 
   952 let
   953   fun berkmin fm =
   954   let
   955     val _          = if (getenv "BERKMIN_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
   956     val serial_str = serial_string ()
   957     val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
   958     val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
   959     val exec       = getenv "BERKMIN_EXE"
   960     val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (if exec = "" then "BerkMin561" else exec) ^ " " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
   961     fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
   962     fun readfn ()  = SatSolver.read_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
   963     val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
   964     val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
   965     val result     = SatSolver.make_external_solver cmd writefn readfn fm
   966     val _          = try File.rm inpath
   967     val _          = try File.rm outpath
   968   in
   969     result
   970   end
   971 in
   972   SatSolver.add_solver ("berkmin", berkmin)
   973 end;
   974 
   975 (* ------------------------------------------------------------------------- *)
   976 (* Jerusat 1.3 (http://www.cs.tau.ac.il/~ale1/)                              *)
   977 (* ------------------------------------------------------------------------- *)
   978 
   979 let
   980   fun jerusat fm =
   981   let
   982     val _          = if (getenv "JERUSAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
   983     val serial_str = serial_string ()
   984     val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
   985     val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
   986     val cmd        = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.implode inpath) ^ " > " ^ (Path.implode outpath)
   987     fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
   988     fun readfn ()  = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
   989     val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.implode inpath)) else ()
   990     val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.implode outpath)) else ()
   991     val result     = SatSolver.make_external_solver cmd writefn readfn fm
   992     val _          = try File.rm inpath
   993     val _          = try File.rm outpath
   994   in
   995     result
   996   end
   997 in
   998   SatSolver.add_solver ("jerusat", jerusat)
   999 end;
  1000 
  1001 (* ------------------------------------------------------------------------- *)
  1002 (* Add code for other SAT solvers below.                                     *)
  1003 (* ------------------------------------------------------------------------- *)
  1004 
  1005 (*
  1006 let
  1007   fun mysolver fm = ...
  1008 in
  1009   SatSolver.add_solver ("myname", (fn fm => if mysolver_is_configured then mysolver fm else raise SatSolver.NOT_CONFIGURED));  -- register the solver
  1010 end;
  1011 
  1012 -- the solver is now available as SatSolver.invoke_solver "myname"
  1013 *)