src/HOL/Tools/sat_funcs.ML
author webertj
Fri, 23 Sep 2005 22:58:50 +0200
changeset 17618 1330157e156a
child 17622 5d03a69481b6
permissions -rw-r--r--
new sat tactic imports resolution proofs from zChaff
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17618
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     1
(*  Title:      HOL/Tools/sat_funcs.ML
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     2
    ID:         $Id$
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     3
    Author:     Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     4
    Copyright   2005
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     5
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     6
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     7
Proof reconstruction from SAT solvers.
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     8
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
     9
  Description:
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    10
    This file defines several tactics to invoke a proof-producing
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    11
    SAT solver on a propositional goal in clausal form.
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    12
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    13
    We use a sequent presentation of clauses to speed up resolution
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    14
    proof reconstruction. 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    15
    We call such clauses as "raw clauses", which are of the form
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    16
          [| c1; c2; ...; ck |] ==> False
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    17
    where each clause ci is of the form
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    18
          [|l1,  l2,  ..., lm |] ==> False,
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    19
    where li is a literal  (see also comments in cnf_funcs.ML).
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    20
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    21
    -- observe that this is the "dualized" version of the standard
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    22
       clausal form
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    23
           l1' \/ l2' \/ ... \/ lm', where li is the negation normal
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    24
       form of ~li'.
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    25
       The tactic produces a clause representation of the given goal
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    26
       in DIMACS format and invokes a SAT solver, which should return
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    27
       a proof consisting of a sequence of resolution steps, indicating
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    28
       the two input clauses and the variable resolved upon, and resulting
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    29
       in new clauses, leading to the empty clause (i.e., False).
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    30
       The tactic replays this proof in Isabelle and thus solves the
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    31
       overall goal.
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    32
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    33
   There are two SAT tactics available. They differ in the CNF transformation
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    34
   used. The "sat_tac" uses naive CNF transformation to transform the theorem
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    35
   to be proved before giving it to SAT solver. The naive transformation in 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    36
   some worst case can lead to explonential blow up in formula size.
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    37
   The other tactic, the "satx_tac" uses the "definitional CNF transformation"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    38
   which produces formula of linear size increase compared to the input formula.
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    39
   This transformation introduces new variables. See also cnf_funcs.ML for
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    40
   more comments.
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    41
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    42
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    43
 Notes for the current revision:
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    44
   - The current version supports only zChaff prover.
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    45
   - The environment variable ZCHAFF_HOME must be set to point to
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    46
     the directory where zChaff executable resides
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    47
   - The environment variable ZCHAFF_VERSION must be set according to
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    48
     the version of zChaff used. Current supported version of zChaff:
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    49
     zChaff version 2004.11.15
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    50
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    51
*)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    52
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    53
(***************************************************************************)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    54
(** Array of clauses **)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    55
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    56
signature CLAUSEARR =
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    57
sig
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    58
   val init : int -> unit 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    59
   val register_at : int -> Thm.thm -> unit
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    60
   val register_list : Thm.thm list -> unit
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    61
   val getClause : int -> Thm.thm option
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    62
end
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    63
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    64
structure ClauseArr : CLAUSEARR =
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    65
struct
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    66
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    67
val clauses : ((Thm.thm option) array) ref = ref (Array.array(1, NONE));
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    68
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    69
fun init size = (clauses := Array.array(size, NONE))
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    70
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    71
fun register_at i c =  Array.update (!clauses, i, (SOME c))
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    72
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    73
fun reg_list n nil = ()
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    74
  | reg_list n (x::l) = 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    75
     (register_at n x; reg_list (n+1) l)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    76
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    77
fun register_list l = reg_list 0 l
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    78
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    79
fun getClause i = Array.sub (!clauses, i)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    80
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    81
end
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    82
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    83
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    84
(***************************************************************************)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    85
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    86
signature SAT =
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    87
sig
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    88
  val trace_sat : bool ref      (* trace tactic *)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    89
  val sat_tac : Tactical.tactic
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    90
  val satx_tac : Tactical.tactic
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    91
end
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    92
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    93
functor SATFunc (structure cnf_struct : CNF) : SAT =
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    94
struct
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    95
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    96
structure cnf = cnf_struct
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    97
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    98
val trace_sat = ref false;	(* debugging flag *)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
    99
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   100
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   101
(* Look up the Isabelle atom corresponding to a DIMACS index in the
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   102
   reverse dictionary. This entry should exist, otherwise an error
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   103
   is raised.
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   104
*)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   105
fun rev_lookup idx dictionary = 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   106
let
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   107
   fun rev_assoc [] = NONE
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   108
     | rev_assoc ((key, entry)::list) =
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   109
       if entry = idx then SOME key else rev_assoc list
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   110
in
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   111
   the (rev_assoc dictionary)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   112
end;
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   113
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   114
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   115
(* Convert rules of the form
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   116
   l1 ==> l2 ==> .. ==> li ==> .. ==> False
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   117
    to
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   118
   l1 ==> l2 ==> .... ==> ~li
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   119
*)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   120
fun swap_prem rslv c = 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   121
let 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   122
    val thm1 = rule_by_tactic (metacut_tac c 1  THEN 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   123
                  (atac 1) THEN (REPEAT_SOME atac)) rslv
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   124
in
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   125
    rule_by_tactic (ALLGOALS (cnf.weakening_tac)) thm1
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   126
end
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   127
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   128
(*** Proof reconstruction: given two clauses
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   129
   [| x1 ; .. ; a ; .. ; xn |] ==> False
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   130
   and 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   131
   [| y1 ; .. ; ~a ; .. ; ym |] ==> False , 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   132
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   133
   we firt convert the first clause into
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   134
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   135
   [| x1 ; ... ; xn |] ==> ~a     (using swap_prem)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   136
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   137
   and do a resolution with the second clause to produce
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   138
   [| y1 ; ... ; x1 ; ... ; xn ; ... ; yn |] ==> False
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   139
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   140
***)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   141
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   142
fun dual (Const("Trueprop",_) $ x) (Const("Trueprop",_) $ y) = dual x y
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   143
  | dual (Const("Not",_) $ x) y = (x = y)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   144
  | dual x (Const("Not",_) $ y) = (x = y)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   145
  | dual x y = false
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   146
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   147
(* Check if an atom has a dual in a list of atoms *)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   148
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   149
fun dual_mem x nil = false
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   150
  | dual_mem x (y::l) = if (dual x y) then true else dual_mem x l
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   151
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   152
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   153
fun replay_chain sg idx (c::cs) =
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   154
let
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   155
   val (SOME fc) = ClauseArr.getClause c;
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   156
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   157
   fun strip_neg (Const("Trueprop", _) $ x) = strip_neg x
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   158
     | strip_neg (Const("Not",_) $ x) = x
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   159
     | strip_neg x = x
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   160
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   161
   (* Find out which atom (literal) is used in the resolution *)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   162
   fun res_atom nil l = raise THM ("Proof reconstruction failed!", 0, [])
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   163
     | res_atom (x::l1) l2 = 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   164
        if (dual_mem x l2) then strip_neg x
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   165
        else res_atom l1 l2
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   166
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   167
   fun replay old [] = old
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   168
     | replay old (cls :: clss) =
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   169
       let
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   170
          val (SOME icls) = ClauseArr.getClause cls;
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   171
          val var = res_atom (prems_of old) (prems_of icls);
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   172
          val atom = cterm_of sg var;
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   173
          val rslv = instantiate' [] [SOME atom] notI;
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   174
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   175
          val _ = if (!trace_sat) then
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   176
            (
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   177
              writeln "-- resolving clause:";
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   178
              print_thm old;
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   179
              writeln "-- with clause: ";
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   180
              print_thm icls;
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   181
              writeln "-- using ";
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   182
              writeln (string_of_cterm atom)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   183
            ) else ();
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   184
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   185
          val thm1 = (
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   186
              rule_by_tactic (REPEAT_SOME (rtac (swap_prem rslv old))) icls
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   187
              handle THM _ =>
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   188
              rule_by_tactic (REPEAT_SOME (rtac (swap_prem rslv icls))) old );
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   189
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   190
          val new = rule_by_tactic distinct_subgoals_tac thm1;
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   191
          val _ = if (!trace_sat) then (writeln "-- resulting clause:"; print_thm new)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   192
                  else ()
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   193
       in
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   194
          replay new clss 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   195
       end
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   196
in
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   197
   ClauseArr.register_at idx (replay fc cs);
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   198
   if (!trace_sat) then (
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   199
      writeln ("-- Replay chain successful. " ^ 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   200
               "The resulting clause stored at #" ^ (Int.toString idx))
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   201
   ) else ()
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   202
end
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   203
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   204
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   205
(* Replay the resolution proof from file prf_file with hypotheses hyps.
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   206
   Returns the theorem established by the proof (which is just False).
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   207
*)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   208
fun replay_prf sg tab size =
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   209
  let
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   210
     val prf = Inttab.dest tab;
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   211
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   212
     fun complete nil = true
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   213
       | complete (x::l) = (
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   214
           case ClauseArr.getClause x of 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   215
             NONE => false
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   216
           | (SOME _) => complete l)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   217
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   218
     fun do_chains [] = ()
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   219
       | do_chains (pr :: rs) = 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   220
         let val (idx, cls) = pr
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   221
         in
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   222
            if (complete cls) then  
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   223
               (replay_chain sg idx cls; do_chains rs)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   224
            else do_chains (rs @ [pr])
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   225
         end
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   226
  in
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   227
    if (!trace_sat) then (
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   228
        writeln "Proof trace from SAT solver: ";
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   229
        print prf ; ()
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   230
     ) else () ;
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   231
     do_chains prf;
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   232
     ClauseArr.getClause size
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   233
  end;
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   234
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   235
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   236
(***************************************************************************)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   237
(***                  Functions to build the sat tactic                  ***)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   238
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   239
(* A trivial tactic, used in preprocessing before calling the main 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   240
   tactic *)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   241
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   242
val pre_sat_tac  = (REPEAT (etac conjE 1)) THEN 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   243
                   (REPEAT ((atac 1) ORELSE (etac FalseE 1)))
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   244
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   245
fun collect_atoms (Const("Trueprop",_) $ x) l = collect_atoms x l
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   246
  | collect_atoms (Const("op |", _) $ x $ y) l = 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   247
        collect_atoms x (collect_atoms y l) 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   248
  | collect_atoms x l = if (x mem l) then l else (x::l) 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   249
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   250
fun has_duals nil = false
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   251
  | has_duals (x::l) = if (dual_mem x l) then true else has_duals l
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   252
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   253
fun trivial_clause (Const("True",_)) = true
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   254
  | trivial_clause c = has_duals (collect_atoms c nil)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   255
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   256
(* Remove trivial clauses *)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   257
fun filter_clauses nil = nil
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   258
  | filter_clauses (x::l) =
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   259
    if (trivial_clause (term_of (cprop_of x))) then filter_clauses l
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   260
    else (x:: filter_clauses l)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   261
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   262
fun is_true assignment x =
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   263
    case (assignment x) of 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   264
      NONE => false
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   265
    | SOME b => b
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   266
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   267
fun get_model dict assignment = 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   268
    map (fn (x,y) => x) (List.filter (fn (x,y) => is_true assignment y) dict)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   269
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   270
fun string_of_model sg nil = ""
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   271
  | string_of_model sg [x] = Sign.string_of_term sg x
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   272
  | string_of_model sg (x::l) = (Sign.string_of_term sg x) ^ ", " ^ (string_of_model sg l)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   273
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   274
(* Run external SAT solver with the given clauses. Reconstruct a proof from
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   275
   the resulting proof trace of the SAT solver. 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   276
*)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   277
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   278
fun rawsat_thm sg prems =
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   279
let val thms = filter_clauses prems 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   280
    val (fm, dict) = cnf.cnf2prop thms
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   281
    val raw_thms = cnf.cnf2raw_thms thms
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   282
in
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   283
   let
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   284
       val result = SatSolver.invoke_solver "zchaff_with_proofs" fm;
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   285
   in
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   286
     case result of
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   287
       (SatSolver.UNSATISFIABLE (SOME (table, size))) => 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   288
          let val _ = ClauseArr.init (size + 1);
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   289
              val _ = ClauseArr.register_list 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   290
                      (map (fn x => (rule_by_tactic distinct_subgoals_tac x)) raw_thms);
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   291
              val (SOME thm1) = replay_prf sg table size
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   292
          in 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   293
              thm1
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   294
          end
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   295
      | (SatSolver.SATISFIABLE model) => 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   296
          let val msg = "\nSAT solver found a countermodel:\n{ " ^ 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   297
                        (string_of_model sg (get_model dict model)) ^ " }\n"
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   298
          in
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   299
                raise THM (msg, 0, [])
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   300
          end    
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   301
      | _ => raise THM ("SAT solver failed!\n", 0, [])
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   302
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   303
  end
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   304
end
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   305
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   306
fun cnfsat_basic_tac state = 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   307
let val sg = Thm.sign_of_thm state
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   308
in 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   309
  METAHYPS (fn prems => rtac (rawsat_thm sg prems) 1) 1 state
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   310
end
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   311
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   312
(* Tactic for calling external SAT solver, taking as input CNF clauses *)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   313
val cnfsat_tac = pre_sat_tac THEN (IF_UNSOLVED cnfsat_basic_tac)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   314
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   315
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   316
(* 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   317
   Tactic for calling external SAT solver, taking as input arbitrary formula. 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   318
*)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   319
val sat_tac = cnf.cnf_thin_tac THEN cnfsat_tac;
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   320
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   321
(* 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   322
  Tactic for calling external SAT solver, taking as input arbitratry formula.
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   323
  The input is translated to CNF (in primitive form), possibly introducing
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   324
  new literals. 
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   325
*)
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   326
val satx_tac = cnf.cnfx_thin_tac THEN cnfsat_tac;
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   327
1330157e156a new sat tactic imports resolution proofs from zChaff
webertj
parents:
diff changeset
   328
end (*of structure*)