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