src/HOL/Tools/sat_solver.ML
author boehmes
Thu May 01 22:56:59 2014 +0200 (2014-05-01)
changeset 56815 848d507584db
parent 56147 9589605bcf41
child 56845 691da43fbdd4
permissions -rw-r--r--
added internal proof-producing SAT solver
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
webertj@14453
    50
structure SatSolver : 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
webertj@31219
   150
      TextIO.output (out, "c This file was generated by SatSolver.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
webertj@31219
   212
      TextIO.output (out, "c This file was generated by SatSolver.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
wenzelm@40314
   316
        | _       => raise Fail "SatSolver.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
webertj@14453
   379
end;  (* SatSolver *)
webertj@14453
   380
webertj@14453
   381
webertj@14453
   382
(* ------------------------------------------------------------------------- *)
webertj@14453
   383
(* Predefined SAT solvers                                                    *)
webertj@14453
   384
(* ------------------------------------------------------------------------- *)
webertj@14453
   385
webertj@14453
   386
(* ------------------------------------------------------------------------- *)
webertj@14753
   387
(* Internal SAT solver, available as 'SatSolver.invoke_solver "enumerate"'   *)
webertj@14753
   388
(* -- simply enumerates assignments until a satisfying assignment is found   *)
webertj@14453
   389
(* ------------------------------------------------------------------------- *)
webertj@14453
   390
webertj@14453
   391
let
wenzelm@22567
   392
  fun enum_solver fm =
wenzelm@22567
   393
  let
wenzelm@41471
   394
    val indices = Prop_Logic.indices fm
wenzelm@22567
   395
    (* binary increment: list 'xs' of current bits, list 'ys' of all bits (lower bits first) *)
wenzelm@22567
   396
    fun next_list _ ([]:int list) =
wenzelm@22567
   397
      NONE
wenzelm@22567
   398
      | next_list [] (y::ys) =
wenzelm@22567
   399
      SOME [y]
wenzelm@22567
   400
      | next_list (x::xs) (y::ys) =
wenzelm@22567
   401
      if x=y then
wenzelm@22567
   402
        (* reset the bit, continue *)
wenzelm@22567
   403
        next_list xs ys
wenzelm@22567
   404
      else
wenzelm@22567
   405
        (* set the lowest bit that wasn't set before, keep the higher bits *)
wenzelm@22567
   406
        SOME (y::x::xs)
wenzelm@22567
   407
    fun assignment_from_list xs i =
haftmann@36692
   408
      member (op =) xs i
wenzelm@22567
   409
    fun solver_loop xs =
wenzelm@41471
   410
      if Prop_Logic.eval (assignment_from_list xs) fm then
wenzelm@22567
   411
        SatSolver.SATISFIABLE (SOME o (assignment_from_list xs))
wenzelm@22567
   412
      else
wenzelm@22567
   413
        (case next_list xs indices of
wenzelm@22567
   414
          SOME xs' => solver_loop xs'
wenzelm@22567
   415
        | NONE     => SatSolver.UNSATISFIABLE NONE)
wenzelm@22567
   416
  in
wenzelm@22567
   417
    (* start with the "first" assignment (all variables are interpreted as 'false') *)
wenzelm@22567
   418
    solver_loop []
wenzelm@22567
   419
  end
webertj@14453
   420
in
wenzelm@22567
   421
  SatSolver.add_solver ("enumerate", enum_solver)
webertj@14453
   422
end;
webertj@14453
   423
webertj@14453
   424
(* ------------------------------------------------------------------------- *)
webertj@14753
   425
(* Internal SAT solver, available as 'SatSolver.invoke_solver "dpll"' -- a   *)
webertj@14753
   426
(* simple implementation of the DPLL algorithm (cf. L. Zhang, S. Malik: "The *)
webertj@14753
   427
(* Quest for Efficient Boolean Satisfiability Solvers", July 2002, Fig. 1).  *)
webertj@14453
   428
(* ------------------------------------------------------------------------- *)
webertj@14453
   429
webertj@14453
   430
let
wenzelm@22567
   431
  local
wenzelm@41471
   432
    open Prop_Logic
wenzelm@22567
   433
  in
wenzelm@22567
   434
    fun dpll_solver fm =
wenzelm@22567
   435
    let
wenzelm@41471
   436
      (* We could use 'Prop_Logic.defcnf fm' instead of 'Prop_Logic.nnf fm' *)
wenzelm@22567
   437
      (* but that sometimes leads to worse performance due to the         *)
wenzelm@22567
   438
      (* introduction of additional variables.                            *)
wenzelm@41471
   439
      val fm' = Prop_Logic.nnf fm
wenzelm@41471
   440
      val indices = Prop_Logic.indices fm'
wenzelm@22567
   441
      fun partial_var_eval []      i = BoolVar i
wenzelm@22567
   442
        | partial_var_eval (x::xs) i = if x=i then True else if x=(~i) then False else partial_var_eval xs i
wenzelm@22567
   443
      fun partial_eval xs True             = True
wenzelm@22567
   444
        | partial_eval xs False            = False
wenzelm@22567
   445
        | partial_eval xs (BoolVar i)      = partial_var_eval xs i
wenzelm@22567
   446
        | partial_eval xs (Not fm)         = SNot (partial_eval xs fm)
wenzelm@22567
   447
        | partial_eval xs (Or (fm1, fm2))  = SOr (partial_eval xs fm1, partial_eval xs fm2)
wenzelm@22567
   448
        | partial_eval xs (And (fm1, fm2)) = SAnd (partial_eval xs fm1, partial_eval xs fm2)
wenzelm@22567
   449
      fun forced_vars True              = []
wenzelm@22567
   450
        | forced_vars False             = []
wenzelm@22567
   451
        | forced_vars (BoolVar i)       = [i]
wenzelm@22567
   452
        | forced_vars (Not (BoolVar i)) = [~i]
haftmann@33049
   453
        | forced_vars (Or (fm1, fm2))   = inter (op =) (forced_vars fm1) (forced_vars fm2)
haftmann@33042
   454
        | forced_vars (And (fm1, fm2))  = union (op =) (forced_vars fm1) (forced_vars fm2)
wenzelm@22567
   455
        (* Above, i *and* ~i may be forced.  In this case the first occurrence takes   *)
wenzelm@22567
   456
        (* precedence, and the next partial evaluation of the formula returns 'False'. *)
wenzelm@22567
   457
        | forced_vars _                 = error "formula is not in negation normal form"
wenzelm@22567
   458
      fun eval_and_force xs fm =
wenzelm@22567
   459
      let
wenzelm@22567
   460
        val fm' = partial_eval xs fm
wenzelm@22567
   461
        val xs' = forced_vars fm'
wenzelm@22567
   462
      in
wenzelm@22567
   463
        if null xs' then
wenzelm@22567
   464
          (xs, fm')
wenzelm@22567
   465
        else
wenzelm@22567
   466
          eval_and_force (xs@xs') fm'  (* xs and xs' should be distinct, so '@' here should have *)
wenzelm@22567
   467
                                       (* the same effect as 'union_int'                         *)
wenzelm@22567
   468
      end
wenzelm@22567
   469
      fun fresh_var xs =
haftmann@36692
   470
        find_first (fn i => not (member (op =) xs i) andalso not (member (op =) xs (~i))) indices
wenzelm@22567
   471
      (* partial assignment 'xs' *)
wenzelm@22567
   472
      fun dpll xs fm =
wenzelm@22567
   473
      let
wenzelm@22567
   474
        val (xs', fm') = eval_and_force xs fm
wenzelm@22567
   475
      in
wenzelm@22567
   476
        case fm' of
wenzelm@22567
   477
          True  => SOME xs'
wenzelm@22567
   478
        | False => NONE
wenzelm@22567
   479
        | _     =>
wenzelm@22567
   480
          let
wenzelm@33035
   481
            val x = the (fresh_var xs')  (* a fresh variable must exist since 'fm' did not evaluate to 'True'/'False' *)
wenzelm@22567
   482
          in
wenzelm@22567
   483
            case dpll (x::xs') fm' of  (* passing fm' rather than fm should save some simplification work *)
wenzelm@22567
   484
              SOME xs'' => SOME xs''
wenzelm@22567
   485
            | NONE      => dpll ((~x)::xs') fm'  (* now try interpreting 'x' as 'False' *)
wenzelm@22567
   486
          end
wenzelm@22567
   487
      end
wenzelm@22567
   488
      fun assignment_from_list [] i =
wenzelm@22567
   489
        NONE  (* the DPLL procedure didn't provide a value for this variable *)
wenzelm@22567
   490
        | assignment_from_list (x::xs) i =
wenzelm@22567
   491
        if x=i then (SOME true)
wenzelm@22567
   492
        else if x=(~i) then (SOME false)
wenzelm@22567
   493
        else assignment_from_list xs i
wenzelm@22567
   494
    in
wenzelm@22567
   495
      (* initially, no variable is interpreted yet *)
wenzelm@22567
   496
      case dpll [] fm' of
wenzelm@22567
   497
        SOME assignment => SatSolver.SATISFIABLE (assignment_from_list assignment)
wenzelm@22567
   498
      | NONE            => SatSolver.UNSATISFIABLE NONE
wenzelm@22567
   499
    end
wenzelm@22567
   500
  end  (* local *)
webertj@14453
   501
in
wenzelm@22567
   502
  SatSolver.add_solver ("dpll", dpll_solver)
webertj@14453
   503
end;
webertj@14453
   504
webertj@14453
   505
(* ------------------------------------------------------------------------- *)
boehmes@56815
   506
(* Internal SAT solver, available as 'SatSolver.invoke_solver "dpll_p"' --   *)
boehmes@56815
   507
(* a simple, slightly more efficient implementation of the DPLL algorithm    *)
boehmes@56815
   508
(* (cf. L. Zhang, S. Malik: "The Quest for Efficient Boolean Satisfiability  *)
boehmes@56815
   509
(* Solvers", July 2002, Fig. 2). In contrast to the other two ML solvers     *)
boehmes@56815
   510
(* above, this solver produces proof traces. *)
boehmes@56815
   511
(* ------------------------------------------------------------------------- *)
boehmes@56815
   512
boehmes@56815
   513
let
boehmes@56815
   514
  type clause = int list * int
boehmes@56815
   515
  type value = bool option
boehmes@56815
   516
  datatype reason = Decided | Implied of clause | Level0 of int
boehmes@56815
   517
  type variable = bool option * reason * int * int
boehmes@56815
   518
  type proofs = int * int list Inttab.table
boehmes@56815
   519
  type state =
boehmes@56815
   520
    int * int list * variable Inttab.table * clause list Inttab.table * proofs
boehmes@56815
   521
  exception CONFLICT of clause * state
boehmes@56815
   522
  exception UNSAT of clause * state
boehmes@56815
   523
boehmes@56815
   524
  fun neg i = ~i
boehmes@56815
   525
boehmes@56815
   526
  fun lit_value lit value = if lit > 0 then value else Option.map not value
boehmes@56815
   527
boehmes@56815
   528
  fun var_of vars lit: variable = the (Inttab.lookup vars (abs lit))
boehmes@56815
   529
  fun value_of vars lit = lit_value lit (#1 (var_of vars lit))
boehmes@56815
   530
  fun reason_of vars lit = #2 (var_of vars lit)
boehmes@56815
   531
  fun level_of vars lit = #3 (var_of vars lit)
boehmes@56815
   532
boehmes@56815
   533
  fun is_true vars lit = (value_of vars lit = SOME true)
boehmes@56815
   534
  fun is_false vars lit = (value_of vars lit = SOME false)
boehmes@56815
   535
  fun is_unassigned vars lit = (value_of vars lit = NONE)
boehmes@56815
   536
  fun assignment_of vars lit = the_default NONE (try (value_of vars) lit)
boehmes@56815
   537
boehmes@56815
   538
  fun put_var value reason level (_, _, _, rank) = (value, reason, level, rank)
boehmes@56815
   539
  fun incr_rank (value, reason, level, rank) = (value, reason, level, rank + 1)
boehmes@56815
   540
  fun update_var lit f = Inttab.map_entry (abs lit) f
boehmes@56815
   541
  fun add_var lit = Inttab.update (abs lit, (NONE, Decided, ~1, 0))
boehmes@56815
   542
boehmes@56815
   543
  fun assign lit r l = update_var lit (put_var (SOME (lit > 0)) r l)
boehmes@56815
   544
  fun unassign lit = update_var lit (put_var NONE Decided ~1)
boehmes@56815
   545
boehmes@56815
   546
  fun add_proof [] (idx, ptab) = (idx, (idx + 1, ptab))
boehmes@56815
   547
    | add_proof ps (idx, ptab) = (idx, (idx + 1, Inttab.update (idx, ps) ptab))
boehmes@56815
   548
boehmes@56815
   549
  fun level0_proof_of (Level0 idx) = SOME idx
boehmes@56815
   550
    | level0_proof_of _ = NONE
boehmes@56815
   551
boehmes@56815
   552
  fun level0_proofs_of vars = map_filter (level0_proof_of o reason_of vars)
boehmes@56815
   553
  fun prems_of vars (lits, p) = p :: level0_proofs_of vars lits
boehmes@56815
   554
  fun mk_proof vars cls proofs = add_proof (prems_of vars cls) proofs
boehmes@56815
   555
boehmes@56815
   556
  fun push lit cls (level, trail, vars, clss, proofs) =
boehmes@56815
   557
    let
boehmes@56815
   558
      val (reason, proofs) =
boehmes@56815
   559
        if level = 0 then apfst Level0 (mk_proof vars cls proofs)
boehmes@56815
   560
        else (Implied cls, proofs)
boehmes@56815
   561
    in (level, lit :: trail, assign lit reason level vars, clss, proofs) end
boehmes@56815
   562
boehmes@56815
   563
  fun push_decided lit (level, trail, vars, clss, proofs) =
boehmes@56815
   564
    let val vars' = assign lit Decided (level + 1) vars
boehmes@56815
   565
    in (level + 1, lit :: 0 :: trail, vars', clss, proofs) end
boehmes@56815
   566
boehmes@56815
   567
  fun prop (cls as (lits, _)) (cx as (units, state as (level, _, vars, _, _))) =
boehmes@56815
   568
    if exists (is_true vars) lits then cx
boehmes@56815
   569
    else if forall (is_false vars) lits then
boehmes@56815
   570
      if level = 0 then raise UNSAT (cls, state)
boehmes@56815
   571
      else raise CONFLICT (cls, state)
boehmes@56815
   572
    else
boehmes@56815
   573
      (case filter (is_unassigned vars) lits of
boehmes@56815
   574
        [lit] => (lit :: units, push lit cls state)
boehmes@56815
   575
      | _ => cx)
boehmes@56815
   576
boehmes@56815
   577
  fun propagate units (state as (_, _, _, clss, _)) =
boehmes@56815
   578
    (case fold (fold prop o Inttab.lookup_list clss) units ([], state) of
boehmes@56815
   579
      ([], state') => (NONE, state')
boehmes@56815
   580
    | (units', state') => propagate units' state')
boehmes@56815
   581
    handle CONFLICT (cls, state') => (SOME cls, state')
boehmes@56815
   582
boehmes@56815
   583
  fun max_unassigned (v, (NONE, _, _, rank)) (x as (_, r)) =
boehmes@56815
   584
        if rank > r then (SOME v, rank) else x
boehmes@56815
   585
    | max_unassigned _  x = x
boehmes@56815
   586
boehmes@56815
   587
  fun decide (state as (_, _, vars, _, _)) =
boehmes@56815
   588
    (case Inttab.fold max_unassigned vars (NONE, 0) of
boehmes@56815
   589
      (SOME lit, _) => SOME (lit, push_decided lit state)
boehmes@56815
   590
    | (NONE, _) => NONE)
boehmes@56815
   591
boehmes@56815
   592
  fun mark lit = Inttab.update (abs lit, true)
boehmes@56815
   593
  fun marked ms lit = the_default false (Inttab.lookup ms (abs lit))
boehmes@56815
   594
  fun ignore l ms lit = ((lit = l) orelse marked ms lit)
boehmes@56815
   595
boehmes@56815
   596
  fun first_lit _ [] = raise Empty
boehmes@56815
   597
    | first_lit _ (0 :: _) = raise Empty
boehmes@56815
   598
    | first_lit pred (lit :: lits) =
boehmes@56815
   599
        if pred lit then (lit, lits) else first_lit pred lits
boehmes@56815
   600
boehmes@56815
   601
  fun reason_cls_of vars lit =
boehmes@56815
   602
    (case reason_of vars lit of
boehmes@56815
   603
      Implied cls => cls
boehmes@56815
   604
    | _ => raise Option)
boehmes@56815
   605
boehmes@56815
   606
  fun analyze conflicting_cls (level, trail, vars, _, _) =
boehmes@56815
   607
    let
boehmes@56815
   608
      fun back i lit (lits, p) trail ms ls ps =
boehmes@56815
   609
        let
boehmes@56815
   610
          val (lits0, lits') = List.partition (equal 0 o level_of vars) lits
boehmes@56815
   611
          val lits1 = filter_out (ignore lit ms) lits'
boehmes@56815
   612
          val lits2 = filter_out (equal level o level_of vars) lits1
boehmes@56815
   613
          val i' = length lits1 - length lits2 + i
boehmes@56815
   614
          val ms' = fold mark lits1 ms
boehmes@56815
   615
          val ls' = lits2 @ ls
boehmes@56815
   616
          val ps' = level0_proofs_of vars lits0 @ (p :: ps)
boehmes@56815
   617
          val (lit', trail') = first_lit (marked ms') trail
boehmes@56815
   618
        in 
boehmes@56815
   619
          if i' = 1 then (neg lit', ls', rev ps')
boehmes@56815
   620
          else back (i' - 1) lit' (reason_cls_of vars lit') trail' ms' ls' ps'
boehmes@56815
   621
        end
boehmes@56815
   622
    in back 0 0 conflicting_cls trail Inttab.empty [] [] end
boehmes@56815
   623
boehmes@56815
   624
  fun keep_clause (cls as (lits, _)) (level, trail, vars, clss, proofs) =
boehmes@56815
   625
    let
boehmes@56815
   626
      val vars' = fold (fn lit => update_var lit incr_rank) lits vars
boehmes@56815
   627
      val clss' = fold (fn lit => Inttab.cons_list (neg lit, cls)) lits clss
boehmes@56815
   628
    in (level, trail, vars', clss', proofs) end
boehmes@56815
   629
boehmes@56815
   630
  fun learn (cls as (lits, _)) = (length lits <= 2) ? keep_clause cls
boehmes@56815
   631
boehmes@56815
   632
  fun backjump _ (state as (_, [], _, _, _)) = state 
boehmes@56815
   633
    | backjump i (level, 0 :: trail, vars, clss, proofs) =
boehmes@56815
   634
        (level - 1, trail, vars, clss, proofs) |> (i > 1) ? backjump (i - 1)
boehmes@56815
   635
    | backjump i (level, lit :: trail, vars, clss, proofs) =
boehmes@56815
   636
        backjump i (level, trail, unassign lit vars, clss, proofs)
boehmes@56815
   637
boehmes@56815
   638
  fun search units state =
boehmes@56815
   639
    (case propagate units state of
boehmes@56815
   640
      (NONE, state' as (_, _, vars, _, _)) =>
boehmes@56815
   641
        (case decide state' of
boehmes@56815
   642
          NONE => SatSolver.SATISFIABLE (assignment_of vars)
boehmes@56815
   643
        | SOME (lit, state'') => search [lit] state'')
boehmes@56815
   644
    | (SOME conflicting_cls, state' as (level, trail, vars, clss, proofs)) =>
boehmes@56815
   645
        let 
boehmes@56815
   646
          val (lit, lits, ps) = analyze conflicting_cls state'
boehmes@56815
   647
          val (idx, proofs') = add_proof ps proofs
boehmes@56815
   648
          val cls = (lit :: lits, idx)
boehmes@56815
   649
        in
boehmes@56815
   650
          (level, trail, vars, clss, proofs')
boehmes@56815
   651
          |> backjump (level - fold (Integer.max o level_of vars) lits 0)
boehmes@56815
   652
          |> learn cls
boehmes@56815
   653
          |> push lit cls
boehmes@56815
   654
          |> search [lit]
boehmes@56815
   655
        end)
boehmes@56815
   656
boehmes@56815
   657
  fun has_opposing_lits [] = false
boehmes@56815
   658
    | has_opposing_lits (lit :: lits) =
boehmes@56815
   659
        member (op =) lits (neg lit) orelse has_opposing_lits lits
boehmes@56815
   660
boehmes@56815
   661
  fun add_clause (cls as ([_], _)) (units, state) =
boehmes@56815
   662
        let val (units', state') = prop cls (units, state)
boehmes@56815
   663
        in (units', state') end
boehmes@56815
   664
    | add_clause (cls as (lits, _)) (cx as (units, state)) =
boehmes@56815
   665
        if has_opposing_lits lits then cx
boehmes@56815
   666
        else (units, keep_clause cls state)
boehmes@56815
   667
boehmes@56815
   668
  fun mk_clause lits proofs =
boehmes@56815
   669
    apfst (pair (distinct (op =) lits)) (add_proof [] proofs)
boehmes@56815
   670
boehmes@56815
   671
  fun solve litss =
boehmes@56815
   672
    let
boehmes@56815
   673
      val (clss, proofs) = fold_map mk_clause litss (0, Inttab.empty)
boehmes@56815
   674
      val vars = fold (fold add_var) litss Inttab.empty
boehmes@56815
   675
      val state = (0, [], vars, Inttab.empty, proofs)
boehmes@56815
   676
    in uncurry search (fold add_clause clss ([], state)) end
boehmes@56815
   677
    handle UNSAT (conflicting_cls, (_, _, vars, _, proofs)) =>
boehmes@56815
   678
      let val (idx, (_, ptab)) = mk_proof vars conflicting_cls proofs
boehmes@56815
   679
      in SatSolver.UNSATISFIABLE (SOME (ptab, idx)) end
boehmes@56815
   680
boehmes@56815
   681
  fun variable_of (Prop_Logic.BoolVar 0) = error "bad propositional variable"
boehmes@56815
   682
    | variable_of (Prop_Logic.BoolVar i) = i
boehmes@56815
   683
    | variable_of _ = error "expected formula in CNF"
boehmes@56815
   684
  fun literal_of (Prop_Logic.Not fm) = neg (variable_of fm)
boehmes@56815
   685
    | literal_of fm = variable_of fm
boehmes@56815
   686
  fun clause_of (Prop_Logic.Or (fm1, fm2)) = clause_of fm1 @ clause_of fm2
boehmes@56815
   687
    | clause_of fm = [literal_of fm]
boehmes@56815
   688
  fun clauses_of (Prop_Logic.And (fm1, fm2)) = clauses_of fm1 @ clauses_of fm2
boehmes@56815
   689
    | clauses_of Prop_Logic.True = [[1, ~1]]
boehmes@56815
   690
    | clauses_of Prop_Logic.False = [[1], [~1]]
boehmes@56815
   691
    | clauses_of fm = [clause_of fm]
boehmes@56815
   692
boehmes@56815
   693
  fun dpll_solver fm =
boehmes@56815
   694
    let val fm' = if Prop_Logic.is_cnf fm then fm else Prop_Logic.defcnf fm
boehmes@56815
   695
    in solve (clauses_of fm') end
boehmes@56815
   696
in
boehmes@56815
   697
  SatSolver.add_solver ("dpll_p", dpll_solver)
boehmes@56815
   698
end;
boehmes@56815
   699
boehmes@56815
   700
(* ------------------------------------------------------------------------- *)
webertj@14753
   701
(* Internal SAT solver, available as 'SatSolver.invoke_solver "auto"': uses  *)
webertj@17577
   702
(* the last installed solver (other than "auto" itself) that does not raise  *)
webertj@15299
   703
(* 'NOT_CONFIGURED'.  (However, the solver may return 'UNKNOWN'.)            *)
webertj@14453
   704
(* ------------------------------------------------------------------------- *)
webertj@14453
   705
webertj@14453
   706
let
wenzelm@22567
   707
  fun auto_solver fm =
wenzelm@22567
   708
  let
wenzelm@22567
   709
    fun loop [] =
wenzelm@22567
   710
      SatSolver.UNKNOWN
wenzelm@22567
   711
      | loop ((name, solver)::solvers) =
wenzelm@22567
   712
      if name="auto" then
wenzelm@22567
   713
        (* do not call solver "auto" from within "auto" *)
wenzelm@22567
   714
        loop solvers
wenzelm@22567
   715
      else (
wenzelm@22567
   716
        (* apply 'solver' to 'fm' *)
wenzelm@22567
   717
        solver fm
wenzelm@22567
   718
          handle SatSolver.NOT_CONFIGURED => loop solvers
wenzelm@22567
   719
      )
wenzelm@22567
   720
  in
wenzelm@56147
   721
    loop (SatSolver.get_solvers ())
wenzelm@22567
   722
  end
webertj@14453
   723
in
wenzelm@22567
   724
  SatSolver.add_solver ("auto", auto_solver)
webertj@14453
   725
end;
webertj@14453
   726
webertj@14453
   727
(* ------------------------------------------------------------------------- *)
webertj@20033
   728
(* MiniSat 1.14                                                              *)
webertj@20033
   729
(* (http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/)            *)
webertj@20033
   730
(* ------------------------------------------------------------------------- *)
webertj@20033
   731
webertj@20135
   732
(* ------------------------------------------------------------------------- *)
webertj@20135
   733
(* "minisat_with_proofs" requires a modified version of MiniSat 1.14 by John *)
webertj@20135
   734
(* Matthews, which can output ASCII proof traces.  Replaying binary proof    *)
webertj@20135
   735
(* traces generated by MiniSat-p_v1.14 has _not_ been implemented.           *)
webertj@20135
   736
(* ------------------------------------------------------------------------- *)
webertj@20135
   737
webertj@20135
   738
(* add "minisat_with_proofs" _before_ "minisat" to the available solvers, so *)
webertj@20135
   739
(* that the latter is preferred by the "auto" solver                         *)
webertj@20135
   740
webertj@20152
   741
(* There is a complication that is dealt with in the code below: MiniSat     *)
webertj@20152
   742
(* introduces IDs for original clauses in the proof trace.  It does not (in  *)
webertj@20152
   743
(* general) follow the convention that the original clauses are numbered     *)
webertj@20152
   744
(* from 0 to n-1 (where n is the number of clauses in the formula).          *)
webertj@20135
   745
webertj@20135
   746
let
wenzelm@22567
   747
  exception INVALID_PROOF of string
wenzelm@22567
   748
  fun minisat_with_proofs fm =
wenzelm@22567
   749
  let
wenzelm@22567
   750
    val _          = if (getenv "MINISAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
blanchet@29872
   751
    val serial_str = serial_string ()
blanchet@29872
   752
    val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
blanchet@29872
   753
    val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
blanchet@29872
   754
    val proofpath  = File.tmp_path (Path.explode ("result" ^ serial_str ^ ".prf"))
wenzelm@35011
   755
    val cmd        = getenv "MINISAT_HOME" ^ "/minisat " ^ File.shell_path inpath ^ " -r " ^ File.shell_path outpath ^ " -t " ^ File.shell_path proofpath ^ "> /dev/null"
wenzelm@22567
   756
    fun writefn fm = SatSolver.write_dimacs_cnf_file inpath fm
wenzelm@22567
   757
    fun readfn ()  = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
wenzelm@41944
   758
    val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
wenzelm@41944
   759
    val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else ()
wenzelm@41471
   760
    val cnf        = Prop_Logic.defcnf fm
wenzelm@22567
   761
    val result     = SatSolver.make_external_solver cmd writefn readfn cnf
wenzelm@22567
   762
    val _          = try File.rm inpath
wenzelm@22567
   763
    val _          = try File.rm outpath
wenzelm@22567
   764
  in  case result of
wenzelm@22567
   765
    SatSolver.UNSATISFIABLE NONE =>
wenzelm@22567
   766
    (let
wenzelm@22567
   767
      val proof_lines = (split_lines o File.read) proofpath
wenzelm@22567
   768
        handle IO.Io _ => raise INVALID_PROOF "Could not read file \"result.prf\""
wenzelm@22567
   769
      (* representation of clauses as ordered lists of literals (with duplicates removed) *)
wenzelm@41471
   770
      fun clause_to_lit_list (Prop_Logic.Or (fm1, fm2)) =
wenzelm@39687
   771
        Ord_List.union int_ord (clause_to_lit_list fm1) (clause_to_lit_list fm2)
wenzelm@41471
   772
        | clause_to_lit_list (Prop_Logic.BoolVar i) =
wenzelm@22567
   773
        [i]
wenzelm@41471
   774
        | clause_to_lit_list (Prop_Logic.Not (Prop_Logic.BoolVar i)) =
wenzelm@22567
   775
        [~i]
wenzelm@22567
   776
        | clause_to_lit_list _ =
wenzelm@22567
   777
        raise INVALID_PROOF "Error: invalid clause in CNF formula."
wenzelm@41471
   778
      fun cnf_number_of_clauses (Prop_Logic.And (fm1, fm2)) =
wenzelm@22567
   779
        cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
wenzelm@22567
   780
        | cnf_number_of_clauses _ =
wenzelm@22567
   781
        1
wenzelm@22567
   782
      val number_of_clauses = cnf_number_of_clauses cnf
wenzelm@22567
   783
      (* int list array *)
wenzelm@22567
   784
      val clauses = Array.array (number_of_clauses, [])
wenzelm@22567
   785
      (* initialize the 'clauses' array *)
wenzelm@41471
   786
      fun init_array (Prop_Logic.And (fm1, fm2), n) =
wenzelm@22567
   787
        init_array (fm2, init_array (fm1, n))
wenzelm@22567
   788
        | init_array (fm, n) =
wenzelm@22567
   789
        (Array.update (clauses, n, clause_to_lit_list fm); n+1)
wenzelm@22567
   790
      val _ = init_array (cnf, 0)
wenzelm@22567
   791
      (* optimization for the common case where MiniSat "R"s clauses in their *)
wenzelm@22567
   792
      (* original order:                                                      *)
wenzelm@32740
   793
      val last_ref_clause = Unsynchronized.ref (number_of_clauses - 1)
wenzelm@22567
   794
      (* search the 'clauses' array for the given list of literals 'lits', *)
wenzelm@22567
   795
      (* starting at index '!last_ref_clause + 1'                          *)
wenzelm@22567
   796
      fun original_clause_id lits =
wenzelm@22567
   797
      let
wenzelm@22567
   798
        fun original_clause_id_from index =
wenzelm@22567
   799
          if index = number_of_clauses then
wenzelm@22567
   800
            (* search from beginning again *)
wenzelm@22567
   801
            original_clause_id_from 0
wenzelm@22567
   802
          (* both 'lits' and the list of literals used in 'clauses' are sorted, so *)
wenzelm@22567
   803
          (* testing for equality should suffice -- barring duplicate literals     *)
wenzelm@22567
   804
          else if Array.sub (clauses, index) = lits then (
wenzelm@22567
   805
            (* success *)
wenzelm@22567
   806
            last_ref_clause := index;
wenzelm@22567
   807
            SOME index
wenzelm@22567
   808
          ) else if index = !last_ref_clause then
wenzelm@22567
   809
            (* failure *)
wenzelm@22567
   810
            NONE
wenzelm@22567
   811
          else
wenzelm@22567
   812
            (* continue search *)
wenzelm@22567
   813
            original_clause_id_from (index + 1)
wenzelm@22567
   814
      in
wenzelm@22567
   815
        original_clause_id_from (!last_ref_clause + 1)
wenzelm@22567
   816
      end
wenzelm@55436
   817
      fun int_from_string s =
wenzelm@55436
   818
        (case Int.fromString s of
wenzelm@22567
   819
          SOME i => i
wenzelm@55436
   820
        | NONE   => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered)."))
wenzelm@22567
   821
      (* parse the proof file *)
wenzelm@32740
   822
      val clause_table  = Unsynchronized.ref (Inttab.empty : int list Inttab.table)
wenzelm@32740
   823
      val empty_id      = Unsynchronized.ref ~1
wenzelm@22567
   824
      (* contains a mapping from clause IDs as used by MiniSat to clause IDs in *)
wenzelm@22567
   825
      (* our proof format, where original clauses are numbered starting from 0  *)
wenzelm@32740
   826
      val clause_id_map = Unsynchronized.ref (Inttab.empty : int Inttab.table)
wenzelm@22567
   827
      fun sat_to_proof id = (
wenzelm@22567
   828
        case Inttab.lookup (!clause_id_map) id of
wenzelm@22567
   829
          SOME id' => id'
wenzelm@41491
   830
        | NONE     => raise INVALID_PROOF ("Clause ID " ^ string_of_int id ^ " used, but not defined.")
wenzelm@22567
   831
      )
wenzelm@32740
   832
      val next_id = Unsynchronized.ref (number_of_clauses - 1)
wenzelm@22567
   833
      fun process_tokens [] =
wenzelm@22567
   834
        ()
wenzelm@22567
   835
        | process_tokens (tok::toks) =
wenzelm@22567
   836
        if tok="R" then (
wenzelm@22567
   837
          case toks of
wenzelm@22567
   838
            id::sep::lits =>
wenzelm@22567
   839
            let
wenzelm@22567
   840
              val _        = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"R\" disallowed after \"X\"."
wenzelm@22567
   841
              val cid      = int_from_string id
wenzelm@22567
   842
              val _        = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
wenzelm@22567
   843
              val ls       = sort int_ord (map int_from_string lits)
wenzelm@22567
   844
              val proof_id = case original_clause_id ls of
wenzelm@22567
   845
                               SOME orig_id => orig_id
wenzelm@22567
   846
                             | NONE         => raise INVALID_PROOF ("Original clause (new ID is " ^ id ^ ") not found.")
wenzelm@22567
   847
            in
wenzelm@22567
   848
              (* extend the mapping of clause IDs with this newly defined ID *)
wenzelm@22567
   849
              clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map)
wenzelm@22567
   850
                handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"R\").")
wenzelm@22567
   851
              (* the proof itself doesn't change *)
wenzelm@22567
   852
            end
wenzelm@22567
   853
          | _ =>
wenzelm@22567
   854
            raise INVALID_PROOF "File format error: \"R\" followed by an insufficient number of tokens."
wenzelm@22567
   855
        ) else if tok="C" then (
wenzelm@22567
   856
          case toks of
wenzelm@22567
   857
            id::sep::ids =>
wenzelm@22567
   858
            let
wenzelm@22567
   859
              val _        = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"C\" disallowed after \"X\"."
wenzelm@22567
   860
              val cid      = int_from_string id
wenzelm@22567
   861
              val _        = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
wenzelm@22567
   862
              (* ignore the pivot literals in MiniSat's trace *)
wenzelm@22567
   863
              fun unevens []             = raise INVALID_PROOF "File format error: \"C\" followed by an even number of IDs."
wenzelm@22567
   864
                | unevens (x :: [])      = x :: []
wenzelm@22567
   865
                | unevens (x :: _ :: xs) = x :: unevens xs
wenzelm@22567
   866
              val rs       = (map sat_to_proof o unevens o map int_from_string) ids
wenzelm@22567
   867
              (* extend the mapping of clause IDs with this newly defined ID *)
wenzelm@32740
   868
              val proof_id = Unsynchronized.inc next_id
wenzelm@22567
   869
              val _        = clause_id_map := Inttab.update_new (cid, proof_id) (!clause_id_map)
wenzelm@22567
   870
                               handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once (in \"C\").")
wenzelm@22567
   871
            in
wenzelm@22567
   872
              (* update clause table *)
wenzelm@22567
   873
              clause_table := Inttab.update_new (proof_id, rs) (!clause_table)
wenzelm@22567
   874
                handle Inttab.DUP _ => raise INVALID_PROOF ("Error: internal ID for clause " ^ id ^ " already used.")
wenzelm@22567
   875
            end
wenzelm@22567
   876
          | _ =>
wenzelm@22567
   877
            raise INVALID_PROOF "File format error: \"C\" followed by an insufficient number of tokens."
wenzelm@22567
   878
        ) else if tok="D" then (
wenzelm@22567
   879
          case toks of
wenzelm@22567
   880
            [id] =>
wenzelm@22567
   881
            let
wenzelm@22567
   882
              val _ = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: \"D\" disallowed after \"X\"."
wenzelm@22567
   883
              val _ = sat_to_proof (int_from_string id)
wenzelm@22567
   884
            in
wenzelm@22567
   885
              (* simply ignore "D" *)
wenzelm@22567
   886
              ()
wenzelm@22567
   887
            end
wenzelm@22567
   888
          | _ =>
wenzelm@22567
   889
            raise INVALID_PROOF "File format error: \"D\" followed by an illegal number of tokens."
wenzelm@22567
   890
        ) else if tok="X" then (
wenzelm@22567
   891
          case toks of
wenzelm@22567
   892
            [id1, id2] =>
wenzelm@22567
   893
            let
wenzelm@22567
   894
              val _            = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one end-of-proof statement."
wenzelm@22567
   895
              val _            = sat_to_proof (int_from_string id1)
wenzelm@22567
   896
              val new_empty_id = sat_to_proof (int_from_string id2)
wenzelm@22567
   897
            in
wenzelm@22567
   898
              (* update conflict id *)
wenzelm@22567
   899
              empty_id := new_empty_id
wenzelm@22567
   900
            end
wenzelm@22567
   901
          | _ =>
wenzelm@22567
   902
            raise INVALID_PROOF "File format error: \"X\" followed by an illegal number of tokens."
wenzelm@22567
   903
        ) else
wenzelm@22567
   904
          raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.")
wenzelm@22567
   905
      fun process_lines [] =
wenzelm@22567
   906
        ()
wenzelm@22567
   907
        | process_lines (l::ls) = (
wenzelm@22567
   908
          process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l);
wenzelm@22567
   909
          process_lines ls
wenzelm@22567
   910
        )
wenzelm@22567
   911
      (* proof *)
wenzelm@22567
   912
      val _ = process_lines proof_lines
wenzelm@22567
   913
      val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
wenzelm@22567
   914
    in
wenzelm@22567
   915
      SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id))
wenzelm@22567
   916
    end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE))
wenzelm@22567
   917
  | result =>
wenzelm@22567
   918
    result
wenzelm@22567
   919
  end
webertj@20135
   920
in
wenzelm@22567
   921
  SatSolver.add_solver ("minisat_with_proofs", minisat_with_proofs)
webertj@20135
   922
end;
webertj@20135
   923
webertj@20033
   924
let
wenzelm@22567
   925
  fun minisat fm =
wenzelm@22567
   926
  let
wenzelm@35011
   927
    val _          = if getenv "MINISAT_HOME" = "" then raise SatSolver.NOT_CONFIGURED else ()
blanchet@29872
   928
    val serial_str = serial_string ()
blanchet@29872
   929
    val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
blanchet@29872
   930
    val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
wenzelm@35011
   931
    val cmd        = getenv "MINISAT_HOME" ^ "/minisat " ^ File.shell_path inpath ^ " -r " ^ File.shell_path outpath ^ " > /dev/null"
wenzelm@41471
   932
    fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
wenzelm@22567
   933
    fun readfn ()  = SatSolver.read_std_result_file outpath ("SAT", "", "UNSAT")
wenzelm@41944
   934
    val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
wenzelm@41944
   935
    val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else ()
wenzelm@22567
   936
    val result     = SatSolver.make_external_solver cmd writefn readfn fm
wenzelm@22567
   937
    val _          = try File.rm inpath
wenzelm@22567
   938
    val _          = try File.rm outpath
wenzelm@22567
   939
  in
wenzelm@22567
   940
    result
wenzelm@22567
   941
  end
webertj@20033
   942
in
wenzelm@22567
   943
  SatSolver.add_solver ("minisat", minisat)
webertj@20033
   944
end;
webertj@20033
   945
webertj@20033
   946
(* ------------------------------------------------------------------------- *)
webertj@15332
   947
(* zChaff (http://www.princeton.edu/~chaff/zchaff.html)                      *)
webertj@14453
   948
(* ------------------------------------------------------------------------- *)
webertj@14453
   949
webertj@17493
   950
(* ------------------------------------------------------------------------- *)
webertj@17493
   951
(* 'zchaff_with_proofs' applies the "zchaff" prover to a formula, and if     *)
webertj@17493
   952
(* zChaff finds that the formula is unsatisfiable, a proof of this is read   *)
webertj@17493
   953
(* from a file "resolve_trace" that was generated by zChaff.  See the code   *)
webertj@17493
   954
(* below for the expected format of the "resolve_trace" file.  Aside from    *)
webertj@17493
   955
(* some basic syntactic checks, no verification of the proof is performed.   *)
webertj@17493
   956
(* ------------------------------------------------------------------------- *)
webertj@17493
   957
webertj@17493
   958
(* add "zchaff_with_proofs" _before_ "zchaff" to the available solvers, so   *)
webertj@17493
   959
(* that the latter is preferred by the "auto" solver                         *)
webertj@17493
   960
webertj@17493
   961
let
wenzelm@22567
   962
  exception INVALID_PROOF of string
wenzelm@22567
   963
  fun zchaff_with_proofs fm =
wenzelm@22567
   964
  case SatSolver.invoke_solver "zchaff" fm of
wenzelm@22567
   965
    SatSolver.UNSATISFIABLE NONE =>
wenzelm@22567
   966
    (let
wenzelm@43701
   967
      (* FIXME File.tmp_path (!?) *)
wenzelm@22567
   968
      val proof_lines = ((split_lines o File.read) (Path.explode "resolve_trace"))
wenzelm@22567
   969
        handle IO.Io _ => raise INVALID_PROOF "Could not read file \"resolve_trace\""
wenzelm@41471
   970
      fun cnf_number_of_clauses (Prop_Logic.And (fm1, fm2)) =
wenzelm@41471
   971
            cnf_number_of_clauses fm1 + cnf_number_of_clauses fm2
wenzelm@41471
   972
        | cnf_number_of_clauses _ = 1
wenzelm@22567
   973
      fun int_from_string s = (
wenzelm@22567
   974
        case Int.fromString s of
wenzelm@22567
   975
          SOME i => i
wenzelm@22567
   976
        | NONE   => raise INVALID_PROOF ("File format error: number expected (" ^ quote s ^ " encountered).")
wenzelm@22567
   977
      )
wenzelm@22567
   978
      (* parse the "resolve_trace" file *)
wenzelm@32740
   979
      val clause_offset = Unsynchronized.ref ~1
wenzelm@32740
   980
      val clause_table  = Unsynchronized.ref (Inttab.empty : int list Inttab.table)
wenzelm@32740
   981
      val empty_id      = Unsynchronized.ref ~1
wenzelm@22567
   982
      fun process_tokens [] =
wenzelm@22567
   983
        ()
wenzelm@22567
   984
        | process_tokens (tok::toks) =
wenzelm@22567
   985
        if tok="CL:" then (
wenzelm@22567
   986
          case toks of
wenzelm@22567
   987
            id::sep::ids =>
wenzelm@22567
   988
            let
wenzelm@22567
   989
              val _   = if !clause_offset = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"VAR:\".")
wenzelm@22567
   990
              val _   = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"CL:\" disallowed after \"CONF:\".")
wenzelm@22567
   991
              val cid = int_from_string id
wenzelm@22567
   992
              val _   = if sep = "<=" then () else raise INVALID_PROOF ("File format error: \"<=\" expected (" ^ quote sep ^ " encountered).")
wenzelm@22567
   993
              val rs  = map int_from_string ids
wenzelm@22567
   994
            in
wenzelm@22567
   995
              (* update clause table *)
wenzelm@22567
   996
              clause_table := Inttab.update_new (cid, rs) (!clause_table)
wenzelm@22567
   997
                handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ id ^ " defined more than once.")
wenzelm@22567
   998
            end
wenzelm@22567
   999
          | _ =>
wenzelm@22567
  1000
            raise INVALID_PROOF "File format error: \"CL:\" followed by an insufficient number of tokens."
wenzelm@22567
  1001
        ) else if tok="VAR:" then (
wenzelm@22567
  1002
          case toks of
wenzelm@22567
  1003
            id::levsep::levid::valsep::valid::antesep::anteid::litsep::lits =>
wenzelm@22567
  1004
            let
wenzelm@22567
  1005
              val _   = if !empty_id = ~1 then () else raise INVALID_PROOF ("File format error: \"VAR:\" disallowed after \"CONF:\".")
wenzelm@22567
  1006
              (* set 'clause_offset' to the largest used clause ID *)
wenzelm@22567
  1007
              val _   = if !clause_offset = ~1 then clause_offset :=
wenzelm@52049
  1008
                (case Inttab.max (!clause_table) of
wenzelm@52049
  1009
                  SOME (id, _) => id
wenzelm@41471
  1010
                | NONE => cnf_number_of_clauses (Prop_Logic.defcnf fm) - 1  (* the first clause ID is 0, not 1 *))
wenzelm@22567
  1011
                else
wenzelm@22567
  1012
                  ()
wenzelm@22567
  1013
              val vid = int_from_string id
wenzelm@22567
  1014
              val _   = if levsep = "L:" then () else raise INVALID_PROOF ("File format error: \"L:\" expected (" ^ quote levsep ^ " encountered).")
wenzelm@22567
  1015
              val _   = int_from_string levid
wenzelm@22567
  1016
              val _   = if valsep = "V:" then () else raise INVALID_PROOF ("File format error: \"V:\" expected (" ^ quote valsep ^ " encountered).")
wenzelm@22567
  1017
              val _   = int_from_string valid
wenzelm@22567
  1018
              val _   = if antesep = "A:" then () else raise INVALID_PROOF ("File format error: \"A:\" expected (" ^ quote antesep ^ " encountered).")
wenzelm@22567
  1019
              val aid = int_from_string anteid
wenzelm@22567
  1020
              val _   = if litsep = "Lits:" then () else raise INVALID_PROOF ("File format error: \"Lits:\" expected (" ^ quote litsep ^ " encountered).")
wenzelm@22567
  1021
              val ls  = map int_from_string lits
wenzelm@22567
  1022
              (* convert the data provided by zChaff to our resolution-style proof format *)
wenzelm@22567
  1023
              (* each "VAR:" line defines a unit clause, the resolvents are implicitly    *)
wenzelm@22567
  1024
              (* given by the literals in the antecedent clause                           *)
wenzelm@22567
  1025
              (* we use the sum of '!clause_offset' and the variable ID as clause ID for the unit clause *)
wenzelm@22567
  1026
              val cid = !clause_offset + vid
wenzelm@22567
  1027
              (* the low bit of each literal gives its sign (positive/negative), therefore  *)
wenzelm@22567
  1028
              (* we have to divide each literal by 2 to obtain the proper variable ID; then *)
wenzelm@22567
  1029
              (* we add '!clause_offset' to obtain the ID of the corresponding unit clause  *)
wenzelm@22567
  1030
              val vids = filter (not_equal vid) (map (fn l => l div 2) ls)
wenzelm@22567
  1031
              val rs   = aid :: map (fn v => !clause_offset + v) vids
wenzelm@22567
  1032
            in
wenzelm@22567
  1033
              (* update clause table *)
wenzelm@22567
  1034
              clause_table := Inttab.update_new (cid, rs) (!clause_table)
wenzelm@22567
  1035
                handle Inttab.DUP _ => raise INVALID_PROOF ("File format error: clause " ^ string_of_int cid ^ " (derived from antecedent for variable " ^ id ^ ") already defined.")
wenzelm@22567
  1036
            end
wenzelm@22567
  1037
          | _ =>
wenzelm@22567
  1038
            raise INVALID_PROOF "File format error: \"VAR:\" followed by an insufficient number of tokens."
wenzelm@22567
  1039
        ) else if tok="CONF:" then (
wenzelm@22567
  1040
          case toks of
wenzelm@22567
  1041
            id::sep::ids =>
wenzelm@22567
  1042
            let
wenzelm@22567
  1043
              val _   = if !empty_id = ~1 then () else raise INVALID_PROOF "File format error: more than one conflicting clause specified."
wenzelm@22567
  1044
              val cid = int_from_string id
wenzelm@22567
  1045
              val _   = if sep = "==" then () else raise INVALID_PROOF ("File format error: \"==\" expected (" ^ quote sep ^ " encountered).")
wenzelm@22567
  1046
              val ls  = map int_from_string ids
wenzelm@22567
  1047
              (* the conflict clause must be resolved with the unit clauses *)
wenzelm@22567
  1048
              (* for its literals to obtain the empty clause                *)
wenzelm@22567
  1049
              val vids         = map (fn l => l div 2) ls
wenzelm@22567
  1050
              val rs           = cid :: map (fn v => !clause_offset + v) vids
wenzelm@52049
  1051
              val new_empty_id = the_default (!clause_offset) (Option.map fst (Inttab.max (!clause_table))) + 1
wenzelm@22567
  1052
            in
wenzelm@22567
  1053
              (* update clause table and conflict id *)
wenzelm@22567
  1054
              clause_table := Inttab.update_new (new_empty_id, rs) (!clause_table)
wenzelm@22567
  1055
                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
  1056
              empty_id     := new_empty_id
wenzelm@22567
  1057
            end
wenzelm@22567
  1058
          | _ =>
wenzelm@22567
  1059
            raise INVALID_PROOF "File format error: \"CONF:\" followed by an insufficient number of tokens."
wenzelm@22567
  1060
        ) else
wenzelm@22567
  1061
          raise INVALID_PROOF ("File format error: unknown token " ^ quote tok ^ " encountered.")
wenzelm@22567
  1062
      fun process_lines [] =
wenzelm@22567
  1063
        ()
wenzelm@22567
  1064
        | process_lines (l::ls) = (
wenzelm@22567
  1065
          process_tokens (String.tokens (fn c => c = #" " orelse c = #"\t") l);
wenzelm@22567
  1066
          process_lines ls
wenzelm@22567
  1067
        )
wenzelm@22567
  1068
      (* proof *)
wenzelm@22567
  1069
      val _ = process_lines proof_lines
wenzelm@22567
  1070
      val _ = if !empty_id <> ~1 then () else raise INVALID_PROOF "File format error: no conflicting clause specified."
wenzelm@22567
  1071
    in
wenzelm@22567
  1072
      SatSolver.UNSATISFIABLE (SOME (!clause_table, !empty_id))
wenzelm@22567
  1073
    end handle INVALID_PROOF reason => (warning reason; SatSolver.UNSATISFIABLE NONE))
wenzelm@22567
  1074
  | result =>
wenzelm@22567
  1075
    result
webertj@17493
  1076
in
wenzelm@22567
  1077
  SatSolver.add_solver ("zchaff_with_proofs", zchaff_with_proofs)
webertj@17493
  1078
end;
webertj@17493
  1079
webertj@14487
  1080
let
wenzelm@22567
  1081
  fun zchaff fm =
wenzelm@22567
  1082
  let
wenzelm@35011
  1083
    val _          = if getenv "ZCHAFF_HOME" = "" then raise SatSolver.NOT_CONFIGURED else ()
blanchet@29872
  1084
    val serial_str = serial_string ()
blanchet@29872
  1085
    val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
blanchet@29872
  1086
    val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
wenzelm@35011
  1087
    val cmd        = getenv "ZCHAFF_HOME" ^ "/zchaff " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath
wenzelm@41471
  1088
    fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
wenzelm@22567
  1089
    fun readfn ()  = SatSolver.read_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
wenzelm@41944
  1090
    val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
wenzelm@41944
  1091
    val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else ()
wenzelm@22567
  1092
    val result     = SatSolver.make_external_solver cmd writefn readfn fm
wenzelm@22567
  1093
    val _          = try File.rm inpath
wenzelm@22567
  1094
    val _          = try File.rm outpath
wenzelm@22567
  1095
  in
wenzelm@22567
  1096
    result
wenzelm@22567
  1097
  end
webertj@14487
  1098
in
wenzelm@22567
  1099
  SatSolver.add_solver ("zchaff", zchaff)
webertj@14965
  1100
end;
webertj@14965
  1101
webertj@14965
  1102
(* ------------------------------------------------------------------------- *)
webertj@14965
  1103
(* BerkMin 561 (http://eigold.tripod.com/BerkMin.html)                       *)
webertj@14965
  1104
(* ------------------------------------------------------------------------- *)
webertj@14965
  1105
webertj@14965
  1106
let
wenzelm@22567
  1107
  fun berkmin fm =
wenzelm@22567
  1108
  let
blanchet@30275
  1109
    val _          = if (getenv "BERKMIN_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
blanchet@29872
  1110
    val serial_str = serial_string ()
blanchet@29872
  1111
    val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
blanchet@29872
  1112
    val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
blanchet@30275
  1113
    val exec       = getenv "BERKMIN_EXE"
wenzelm@35011
  1114
    val cmd        = getenv "BERKMIN_HOME" ^ "/" ^ (if exec = "" then "BerkMin561" else exec) ^ " " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath
wenzelm@41471
  1115
    fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
wenzelm@22567
  1116
    fun readfn ()  = SatSolver.read_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
wenzelm@41944
  1117
    val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
wenzelm@41944
  1118
    val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else ()
wenzelm@22567
  1119
    val result     = SatSolver.make_external_solver cmd writefn readfn fm
wenzelm@22567
  1120
    val _          = try File.rm inpath
wenzelm@22567
  1121
    val _          = try File.rm outpath
wenzelm@22567
  1122
  in
wenzelm@22567
  1123
    result
wenzelm@22567
  1124
  end
webertj@14965
  1125
in
wenzelm@22567
  1126
  SatSolver.add_solver ("berkmin", berkmin)
webertj@14965
  1127
end;
webertj@14965
  1128
webertj@14965
  1129
(* ------------------------------------------------------------------------- *)
webertj@14965
  1130
(* Jerusat 1.3 (http://www.cs.tau.ac.il/~ale1/)                              *)
webertj@14965
  1131
(* ------------------------------------------------------------------------- *)
webertj@14965
  1132
webertj@14965
  1133
let
wenzelm@22567
  1134
  fun jerusat fm =
wenzelm@22567
  1135
  let
wenzelm@22567
  1136
    val _          = if (getenv "JERUSAT_HOME") = "" then raise SatSolver.NOT_CONFIGURED else ()
blanchet@29872
  1137
    val serial_str = serial_string ()
blanchet@29872
  1138
    val inpath     = File.tmp_path (Path.explode ("isabelle" ^ serial_str ^ ".cnf"))
blanchet@29872
  1139
    val outpath    = File.tmp_path (Path.explode ("result" ^ serial_str))
wenzelm@35011
  1140
    val cmd        = getenv "JERUSAT_HOME" ^ "/Jerusat1.3 " ^ File.shell_path inpath ^ " > " ^ File.shell_path outpath
wenzelm@41471
  1141
    fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (Prop_Logic.defcnf fm)
wenzelm@22567
  1142
    fun readfn ()  = SatSolver.read_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
wenzelm@41944
  1143
    val _ = if File.exists inpath then warning ("overwriting existing file " ^ Path.print inpath) else ()
wenzelm@41944
  1144
    val _ = if File.exists outpath then warning ("overwriting existing file " ^ Path.print outpath) else ()
wenzelm@22567
  1145
    val result     = SatSolver.make_external_solver cmd writefn readfn fm
wenzelm@22567
  1146
    val _          = try File.rm inpath
wenzelm@22567
  1147
    val _          = try File.rm outpath
wenzelm@22567
  1148
  in
wenzelm@22567
  1149
    result
wenzelm@22567
  1150
  end
webertj@14965
  1151
in
wenzelm@22567
  1152
  SatSolver.add_solver ("jerusat", jerusat)
webertj@14487
  1153
end;
webertj@14453
  1154