new sat tactic imports resolution proofs from zChaff
authorwebertj
Fri Sep 23 22:58:50 2005 +0200 (2005-09-23)
changeset 176181330157e156a
parent 17617 73397145d58a
child 17619 026f7bbc8a0f
new sat tactic imports resolution proofs from zChaff
src/HOL/IsaMakefile
src/HOL/Main.thy
src/HOL/SAT.thy
src/HOL/Tools/cnf_funcs.ML
src/HOL/Tools/sat_funcs.ML
src/HOL/ex/ROOT.ML
src/HOL/ex/SAT_Examples.thy
     1.1 --- a/src/HOL/IsaMakefile	Fri Sep 23 22:49:25 2005 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Sep 23 22:58:50 2005 +0200
     1.3 @@ -91,12 +91,13 @@
     1.4    Nat.ML Nat.thy NatArith.thy OrderedGroup.ML OrderedGroup.thy			\
     1.5    Orderings.ML Orderings.thy Power.thy PreList.thy Product_Type.thy		\
     1.6    ROOT.ML Recdef.thy Reconstruction.thy Record.thy Refute.thy			\
     1.7 -  Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy Set.ML		\
     1.8 +  Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy SAT.thy Set.ML		\
     1.9    Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/AtpCommunication.ML		\
    1.10    Tools/ATP/recon_order_clauses.ML Tools/ATP/recon_parse.ML			\
    1.11    Tools/ATP/recon_transfer_proof.ML			\
    1.12    Tools/ATP/recon_translate_proof.ML Tools/ATP/res_clasimpset.ML		\
    1.13    Tools/ATP/watcher.ML 					\
    1.14 +  Tools/cnf_funcs.ML					\
    1.15    Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML				\
    1.16    Tools/datatype_codegen.ML Tools/datatype_package.ML				\
    1.17    Tools/datatype_prop.ML Tools/datatype_realizer.ML				\
    1.18 @@ -108,6 +109,7 @@
    1.19    Tools/refute_isar.ML Tools/res_atp.ML Tools/res_axioms.ML			\
    1.20    Tools/res_clause.ML Tools/res_lib.ML Tools/res_skolem_function.ML		\
    1.21    Tools/res_types_sorts.ML Tools/rewrite_hol_proof.ML				\
    1.22 +  Tools/sat_funcs.ML					\
    1.23    Tools/sat_solver.ML Tools/specification_package.ML Tools/split_rule.ML	\
    1.24    Tools/typedef_package.ML Transitive_Closure.ML Transitive_Closure.thy		\
    1.25    Typedef.thy Wellfounded_Recursion.thy Wellfounded_Relations.thy		\
    1.26 @@ -598,7 +600,7 @@
    1.27    ex/NatSum.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy		\
    1.28    ex/Puzzle.thy ex/Qsort.thy ex/Quickcheck_Examples.thy ex/ROOT.ML	\
    1.29    ex/Recdefs.thy ex/Records.thy ex/Reflected_Presburger.thy		\
    1.30 -  ex/Refute_Examples.thy ex/SVC_Oracle.ML ex/SVC_Oracle.thy		\
    1.31 +  ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.ML ex/SVC_Oracle.thy		\
    1.32    ex/StringEx.thy ex/Tarski.thy ex/Tuple.thy ex/document/root.bib	\
    1.33    ex/document/root.tex ex/mesontest2.ML ex/mesontest2.thy ex/set.thy	\
    1.34    ex/svc_funcs.ML ex/svc_test.ML ex/svc_test.thy
     2.1 --- a/src/HOL/Main.thy	Fri Sep 23 22:49:25 2005 +0200
     2.2 +++ b/src/HOL/Main.thy	Fri Sep 23 22:58:50 2005 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4  header {* Main HOL *}
     2.5  
     2.6  theory Main
     2.7 -imports Refute Reconstruction
     2.8 +imports Refute Reconstruction SAT
     2.9  begin
    2.10  
    2.11  text {*
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/SAT.thy	Fri Sep 23 22:58:50 2005 +0200
     3.3 @@ -0,0 +1,41 @@
     3.4 +(*  Title:      HOL/SAT.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Alwen Tiu, Tjark Weber
     3.7 +    Copyright   2005
     3.8 +
     3.9 +Basic setup for the 'sat' tactic.
    3.10 +*)
    3.11 +
    3.12 +header {* Reconstructing external resolution proofs for propositional logic *}
    3.13 +
    3.14 +theory SAT imports HOL
    3.15 +
    3.16 +uses "Tools/sat_solver.ML"
    3.17 +     "Tools/cnf_funcs.ML"
    3.18 +     "Tools/sat_funcs.ML"
    3.19 +
    3.20 +begin
    3.21 +
    3.22 +ML {* structure sat = SATFunc(structure cnf_struct = cnf); *}
    3.23 +
    3.24 +method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD sat.sat_tac) *}
    3.25 +  "SAT solver"
    3.26 +
    3.27 +method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD sat.satx_tac) *}
    3.28 +  "SAT solver (with definitional CNF)"
    3.29 +
    3.30 +(*
    3.31 +method_setup cnf = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_tac) *}
    3.32 +  "Transforming hypotheses in a goal into CNF"
    3.33 +
    3.34 +method_setup cnf_concl = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_concl_tac) *}
    3.35 +  "Transforming the conclusion of a goal to CNF"
    3.36 +
    3.37 +method_setup cnf_thin = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnf_thin_tac) *}
    3.38 +  "Same as cnf, but remove the original hypotheses"
    3.39 +
    3.40 +method_setup cnfx_thin = {* Method.no_args (Method.SIMPLE_METHOD cnf.cnfx_thin_tac) *}
    3.41 +  "Same as cnf_thin, but may introduce extra variables"
    3.42 +*)
    3.43 +
    3.44 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Fri Sep 23 22:58:50 2005 +0200
     4.3 @@ -0,0 +1,660 @@
     4.4 +(*  Title:      HOL/Tools/cnf_funcs.ML
     4.5 +    ID:         $Id$
     4.6 +    Author:     Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
     4.7 +    Copyright   2005
     4.8 +
     4.9 +  Description:
    4.10 +  This file contains functions and tactics to transform a formula into 
    4.11 +  Conjunctive Normal Forms (CNF). 
    4.12 +  A formula in CNF is of the following form:
    4.13 +
    4.14 +      (x11 | x12 | .. x1m) & ... & (xm1 | xm2 | ... | xmn)
    4.15 +
    4.16 +  where each xij is a literal (i.e., positive or negative propositional
    4.17 +  variables).
    4.18 +  This kind of formula will simply be referred to as CNF.
    4.19 +  A disjunction of literals is referred to as "clause".
    4.20 +
    4.21 +  For the purpose of SAT proof reconstruction, we also make use of another
    4.22 +  representation of clauses, which we call the "raw clauses".
    4.23 +  Raw clauses are of the form
    4.24 +
    4.25 +      (x1 ==> x2 ==> .. ==> xn ==> False)
    4.26 +
    4.27 +  where each xi is a literal. Note that the above raw clause corresponds
    4.28 +  to the clause (x1' | ... | xn'), where each xi' is the negation normal
    4.29 +  form of ~xi.
    4.30 +
    4.31 +  Notes for current revision:
    4.32 +  - the "definitional CNF transformation" (anything with prefix cnfx_ )
    4.33 +    introduces new literals of the form (lit_i) where i is an integer.
    4.34 +    For these functions to work, it is necessary that no free variables
    4.35 +    which names are of the form lit_i appears in the formula being
    4.36 +    transformed.
    4.37 +*)
    4.38 +
    4.39 +
    4.40 +(***************************************************************************)
    4.41 +
    4.42 +signature CNF =
    4.43 +sig
    4.44 +  val cnf_tac : Tactical.tactic
    4.45 +  val cnf_thin_tac : Tactical.tactic
    4.46 +  val cnfx_thin_tac : Tactical.tactic
    4.47 +  val cnf_concl_tac : Tactical.tactic
    4.48 +  val weakening_tac : int -> Tactical.tactic
    4.49 +  val mk_cnf_thm : Sign.sg -> Term.term -> Thm.thm
    4.50 +  val mk_cnfx_thm : Sign.sg -> Term.term ->  Thm.thm
    4.51 +  val is_atm : Term.term -> bool
    4.52 +  val is_lit : Term.term -> bool
    4.53 +  val is_clause : Term.term -> bool
    4.54 +  val is_raw_clause : Term.term -> bool
    4.55 +  val cnf2raw_thm : Thm.thm -> Thm.thm
    4.56 +  val cnf2raw_thms : Thm.thm list -> Thm.thm list
    4.57 +  val cnf2prop : Thm.thm list -> (PropLogic.prop_formula * ((Term.term * int) list))
    4.58 +end
    4.59 +
    4.60 +
    4.61 +(***************************************************************************)
    4.62 +
    4.63 +structure cnf : CNF =
    4.64 +struct
    4.65 +
    4.66 +val cur_thy = the_context();
    4.67 +val mk_disj = HOLogic.mk_disj;
    4.68 +val mk_conj = HOLogic.mk_conj;
    4.69 +val mk_imp  = HOLogic.mk_imp;
    4.70 +val Not = HOLogic.Not;
    4.71 +val false_const = HOLogic.false_const;
    4.72 +val true_const = HOLogic.true_const;
    4.73 +
    4.74 +
    4.75 +(* Index for new literals *)
    4.76 +val lit_id = ref 0;
    4.77 +
    4.78 +fun thm_by_auto G =
    4.79 +    prove_goal cur_thy G (fn prems => [cut_facts_tac prems 1, Auto_tac]);
    4.80 +
    4.81 +(***************************************************************************)
    4.82 +
    4.83 +
    4.84 +val cnf_eq_id = thm_by_auto "(P :: bool) = P";
    4.85 +
    4.86 +val cnf_eq_sym = thm_by_auto "(P :: bool) = Q ==> Q = P";
    4.87 +
    4.88 +val cnf_not_true_false = thm_by_auto "~True = False";
    4.89 +
    4.90 +val cnf_not_false_true = thm_by_auto "~False = True";
    4.91 +
    4.92 +val cnf_imp2disj = thm_by_auto "(P --> Q) = (~P | Q)";
    4.93 +
    4.94 +val cnf_neg_conj = thm_by_auto "(~(P & Q)) = (~P | ~Q)";
    4.95 +
    4.96 +val cnf_neg_disj = thm_by_auto "(~(P | Q)) = (~P & ~Q)";
    4.97 +
    4.98 +val cnf_neg_imp = thm_by_auto "(~(P --> Q)) = (P & ~Q)";
    4.99 +
   4.100 +val cnf_double_neg = thm_by_auto "(~~P) = P";
   4.101 + 
   4.102 +val cnf_disj_conj = thm_by_auto "((P & Q) | R) = ((P | R) & (Q | R))";
   4.103 +
   4.104 +val cnf_disj_imp = thm_by_auto "((P --> Q) | R) = (~P | (Q | R))";
   4.105 +
   4.106 +val cnf_disj_disj = thm_by_auto "((P | Q) | R) = (P | (Q | R))";
   4.107 +
   4.108 +val cnf_disj_false = thm_by_auto "(False | P) = P";
   4.109 +
   4.110 +val cnf_disj_true = thm_by_auto "(True | P) = True";
   4.111 +
   4.112 +val cnf_disj_not_false = thm_by_auto "(~False | P) = True";
   4.113 +
   4.114 +val cnf_disj_not_true = thm_by_auto "(~True | P) = P";
   4.115 +
   4.116 +val cnf_eq_trans = thm_by_auto "[| ( (P::bool) = Q) ; Q = R |] ==> (P = R)";
   4.117 +
   4.118 +val cnf_comb2eq = thm_by_auto "[| P = Q ; R = T |] ==> (P & R) = (Q & T)";
   4.119 +
   4.120 +val cnf_disj_sym = thm_by_auto "(P | Q) = (Q | P)";
   4.121 +
   4.122 +val cnf_cong_disj = thm_by_auto "(P = Q) ==> (P | R) = (Q | R)";
   4.123 +
   4.124 +val icnf_elim_disj1 = thm_by_auto "Q = R  ==> (~P | Q) = (P --> R)";
   4.125 +
   4.126 +val icnf_elim_disj2 = thm_by_auto "Q = R ==> (P | Q) = (~P --> R)";
   4.127 +
   4.128 +val icnf_neg_false1 = thm_by_auto "(~P) = (P --> False)";
   4.129 +
   4.130 +val icnf_neg_false2 = thm_by_auto "P = (~P --> False)";
   4.131 +
   4.132 +val weakening_thm = thm_by_auto "[| P ; Q |] ==> Q";
   4.133 +
   4.134 +val cnf_newlit = thm_by_auto 
   4.135 +    "((P & Q) | R) = (EX (x :: bool). (~x | P) & (~x | Q) & (x | ~P | ~ Q) & (x | R))";
   4.136 +
   4.137 +val cnf_all_ex = thm_by_auto 
   4.138 +    "(ALL (x :: bool). (P x = Q x)) ==> (EX x. P x) = (EX x. Q x)";
   4.139 +
   4.140 +(* [| P ; ~P |] ==> False *)
   4.141 +val cnf_notE = read_instantiate [("R", "False")] (rotate_prems 1 notE);
   4.142 +
   4.143 +val cnf_dneg = thm_by_auto "P ==> ~~P";
   4.144 +
   4.145 +val cnf_neg_disjI = thm_by_auto "[| ~P ; ~Q |] ==> ~(P | Q)";
   4.146 +
   4.147 +val cnf_eq_imp = thm_by_auto "[|((P::bool) = Q) ; P |] ==> Q";
   4.148 +
   4.149 +(***************************************************************************)
   4.150 +
   4.151 +fun is_atm (Const("Trueprop",_) $ x) = is_atm x
   4.152 +  | is_atm (Const("==>",_) $ x $ y) = false
   4.153 +  | is_atm (Const("False",_)) = false
   4.154 +  | is_atm (Const("True", _)) = false
   4.155 +  | is_atm (Const("op &",_) $ x $ y) = false
   4.156 +  | is_atm (Const("op |",_) $ x $ y) = false
   4.157 +  | is_atm (Const("op -->",_) $ x $ y) = false
   4.158 +  | is_atm (Const("Not",_) $ x) = false
   4.159 +  | is_atm t = true
   4.160 +
   4.161 +
   4.162 +fun is_lit (Const("Trueprop",_) $ x) = is_lit x
   4.163 +  | is_lit (Const("Not", _) $ x) = is_atm x
   4.164 +  | is_lit t = is_atm t
   4.165 +
   4.166 +fun is_clause (Const("Trueprop",_) $ x) = is_clause x
   4.167 +  | is_clause (Const("op |", _) $ x $ y) = 
   4.168 +          (is_clause x) andalso (is_clause y)
   4.169 +  | is_clause t = is_lit t
   4.170 +
   4.171 +fun is_cnf (Const("Trueprop", _) $ x) = is_cnf x
   4.172 +  | is_cnf (Const("op &",_) $ x $ y) = (is_cnf x) andalso (is_cnf y)
   4.173 +  | is_cnf t = is_clause t
   4.174 +
   4.175 +
   4.176 +(* Checking for raw clauses *)
   4.177 +fun is_raw_clause (Const("Trueprop",_) $ x) = is_raw_clause x
   4.178 +  | is_raw_clause (Const("==>",_) $ x $ 
   4.179 +                   (Const("Trueprop",_) $ Const("False",_))) = is_lit x
   4.180 +  | is_raw_clause (Const("==>",_) $ x $ y) = 
   4.181 +        (is_lit x) andalso (is_raw_clause y)
   4.182 +  | is_raw_clause t = false
   4.183 +
   4.184 +
   4.185 +
   4.186 +(* Translate a CNF clause into a raw clause *)
   4.187 +fun cnf2raw_thm c =
   4.188 +let val nc = c RS cnf_notE
   4.189 +in
   4.190 +rule_by_tactic (REPEAT_SOME (fn i => 
   4.191 +               rtac cnf_dneg i 
   4.192 +               ORELSE rtac cnf_neg_disjI i)) nc
   4.193 +handle THM _ => nc
   4.194 +end
   4.195 +
   4.196 +fun cnf2raw_thms nil = nil
   4.197 +  | cnf2raw_thms (c::l) =
   4.198 +    let val t = term_of (cprop_of c)
   4.199 +    in
   4.200 +       if (is_clause t) then (cnf2raw_thm c) :: cnf2raw_thms l
   4.201 +       else cnf2raw_thms l
   4.202 +    end
   4.203 +
   4.204 +
   4.205 +(* Translating HOL formula (in CNF) to PropLogic formula. Returns also an
   4.206 +   association list, relating literals to their indices *)
   4.207 +
   4.208 +local
   4.209 +  (* maps atomic formulas to variable numbers *)
   4.210 +  val dictionary : ((Term.term * int) list) ref = ref nil;
   4.211 +  val var_count = ref 0;
   4.212 +  val pAnd = PropLogic.And;
   4.213 +  val pOr = PropLogic.Or;
   4.214 +  val pNot = PropLogic.Not;
   4.215 +  val pFalse = PropLogic.False;
   4.216 +  val pTrue = PropLogic.True;
   4.217 +  val pVar = PropLogic.BoolVar;
   4.218 +
   4.219 +  fun mk_clause (Const("Trueprop",_) $ x) = mk_clause x
   4.220 +    | mk_clause (Const("op |",_) $ x $ y) = pOr(mk_clause x, mk_clause y)
   4.221 +    | mk_clause (Const("Not", _) $ x) = pNot (mk_clause x)
   4.222 +    | mk_clause (Const("True",_)) = pTrue
   4.223 +    | mk_clause (Const("False",_)) = pFalse
   4.224 +    | mk_clause t =
   4.225 +      let
   4.226 +         val idx = AList.lookup op= (!dictionary) t
   4.227 +      in
   4.228 +         case idx of
   4.229 +            (SOME x) => pVar x
   4.230 +           | NONE =>
   4.231 +             let
   4.232 +                val new_var = inc var_count
   4.233 +             in
   4.234 +                dictionary := (t, new_var) :: (!dictionary);
   4.235 +                pVar new_var
   4.236 +             end
   4.237 +      end
   4.238 +
   4.239 +   fun mk_clauses nil = pTrue
   4.240 +     | mk_clauses (x::nil) = mk_clause x
   4.241 +     | mk_clauses (x::l) = pAnd(mk_clause x, mk_clauses l)
   4.242 +
   4.243 +in
   4.244 +   fun cnf2prop thms =
   4.245 +   (
   4.246 +     var_count := 0;
   4.247 +     dictionary := nil;
   4.248 +     (mk_clauses (map (fn x => term_of (cprop_of x)) thms), !dictionary)
   4.249 +   )
   4.250 +end
   4.251 +
   4.252 +
   4.253 +
   4.254 +(* Instantiate a theorem with a list of terms *)
   4.255 +fun inst_thm sign l thm = 
   4.256 +  instantiate' [] (map (fn x => SOME (cterm_of sign x)) l) thm
   4.257 +
   4.258 +(* Tactic to remove the first hypothesis of the first subgoal. *) 
   4.259 +fun weakening_tac i = (dtac weakening_thm i) THEN (atac (i+1));
   4.260 +
   4.261 +(* Tactic for removing the n first hypotheses of the first subgoal. *)
   4.262 +fun weakenings_tac 0 state = all_tac state
   4.263 +  | weakenings_tac n state = ((weakening_tac  1) THEN (weakenings_tac (n-1))) state
   4.264 +
   4.265 +
   4.266 +(* 
   4.267 +  Transform a formula into a "head" negation normal form, that is, 
   4.268 +  the top level connective is not a negation, with the exception
   4.269 +  of negative literals. Returns the pair of the head normal term with
   4.270 +  the theorem corresponding to the transformation.
   4.271 +*)
   4.272 +fun head_nnf sign (Const("Not",_)  $ (Const("op &",_) $ x $ y)) =
   4.273 +    let val t = mk_disj(Not $ x, Not $ y)
   4.274 +        val neg_thm = inst_thm sign [x, y] cnf_neg_conj 
   4.275 +    in
   4.276 +        (t, neg_thm)
   4.277 +    end
   4.278 +
   4.279 +  | head_nnf sign (Const("Not", _) $ (Const("op |",_) $ x $ y)) =
   4.280 +    let val t = mk_conj(Not $ x, Not $ y)
   4.281 +        val neg_thm =  inst_thm sign [x, y] cnf_neg_disj; 
   4.282 +    in
   4.283 +        (t, neg_thm)
   4.284 +    end
   4.285 +
   4.286 +  | head_nnf sign (Const("Not", _) $ (Const("op -->",_) $ x $ y)) = 
   4.287 +    let val t = mk_conj(x, Not $ y)
   4.288 +        val neg_thm = inst_thm sign [x, y] cnf_neg_imp
   4.289 +    in
   4.290 +        (t, neg_thm)
   4.291 +    end
   4.292 +
   4.293 +  | head_nnf sign (Const("Not",_) $ (Const("Not",_) $ x)) =
   4.294 +    (x, inst_thm sign [x] cnf_double_neg)
   4.295 +
   4.296 +  | head_nnf sign (Const("Not",_) $ Const("True",_)) = 
   4.297 +      (false_const, cnf_not_true_false)
   4.298 +
   4.299 +  | head_nnf sign (Const("Not",_) $ Const("False",_)) = 
   4.300 +      (true_const, cnf_not_false_true)  
   4.301 +
   4.302 +  | head_nnf sign t = 
   4.303 +    (t, inst_thm sign [t] cnf_eq_id)
   4.304 +
   4.305 +
   4.306 +(***************************************************************************)
   4.307 +(*                  Tactics for simple CNF transformation                  *)
   4.308 +
   4.309 +(* A naive procedure for CNF transformation:
   4.310 +   Given any t, produce a theorem t = t', where t' is in
   4.311 +   conjunction normal form 
   4.312 +*)
   4.313 +fun mk_cnf_thm sign (Const("Trueprop",_) $ x) = mk_cnf_thm sign x
   4.314 +  | mk_cnf_thm sign (t as (Const(_,_))) = inst_thm sign [t] cnf_eq_id
   4.315 +  | mk_cnf_thm sign (t as (Free(_,_))) =  inst_thm sign [t] cnf_eq_id
   4.316 + 
   4.317 +  | mk_cnf_thm sign (Const("op -->", _) $ x $ y) =
   4.318 +       let val thm1 = inst_thm sign [x, y] cnf_imp2disj;
   4.319 +           val thm2 = mk_cnf_thm sign (mk_disj(Not $ x, y));
   4.320 +       in
   4.321 +           cnf_eq_trans OF [thm1, thm2]
   4.322 +       end
   4.323 +
   4.324 +  | mk_cnf_thm sign (Const("op &", _) $ x $ y) = 
   4.325 +       let val cnf1 = mk_cnf_thm sign x;
   4.326 +           val cnf2 = mk_cnf_thm sign y;
   4.327 +       in
   4.328 +           cnf_comb2eq OF [cnf1, cnf2]
   4.329 +       end
   4.330 +
   4.331 +  | mk_cnf_thm sign (Const("Not",_) $ Const("True",_)) = 
   4.332 +        cnf_not_true_false
   4.333 +
   4.334 +  | mk_cnf_thm sign (Const("Not",_) $ Const("False",_)) = 
   4.335 +        cnf_not_false_true
   4.336 +
   4.337 +  | mk_cnf_thm sign (t as (Const("Not", _) $ x)) =
   4.338 +      ( 
   4.339 +       if (is_atm x) then inst_thm sign [t] cnf_eq_id
   4.340 +       else
   4.341 +         let val (t1, hn_thm) = head_nnf sign t
   4.342 +             val cnf_thm = mk_cnf_thm sign t1
   4.343 +         in
   4.344 +             cnf_eq_trans OF [hn_thm, cnf_thm]
   4.345 +         end
   4.346 +       ) 
   4.347 +
   4.348 +  | mk_cnf_thm sign (Const("op |",_) $ (Const("op &", _) $ p $ q) $ r) =
   4.349 +       let val thm1 = inst_thm sign [p, q, r] cnf_disj_conj;
   4.350 +           val thm2 = mk_cnf_thm sign (mk_conj(mk_disj(p, r), mk_disj(q,r)));
   4.351 +       in
   4.352 +          cnf_eq_trans OF [thm1, thm2]
   4.353 +       end
   4.354 +
   4.355 +  | mk_cnf_thm sign (Const("op |",_) $ (Const("op |", _) $ p $ q) $ r) =
   4.356 +       let val thm1 = inst_thm sign [p,q,r] cnf_disj_disj;
   4.357 +           val thm2 = mk_cnf_thm sign (mk_disj(p, mk_disj(q,r)));
   4.358 +       in
   4.359 +          cnf_eq_trans OF [thm1, thm2]
   4.360 +       end
   4.361 +
   4.362 +  | mk_cnf_thm sign (Const("op |",_) $ (Const("op -->", _) $ p $ q) $ r) =                       
   4.363 +       let val thm1 = inst_thm sign [p,q,r] cnf_disj_imp;
   4.364 +           val thm2 = mk_cnf_thm sign (mk_disj(Not $ p, mk_disj(q, r)));
   4.365 +       in
   4.366 +           cnf_eq_trans OF [thm1, thm2]
   4.367 +       end
   4.368 +
   4.369 +  | mk_cnf_thm sign (Const("op |",_) $ Const("False",_) $ p) =
   4.370 +       let val thm1 = inst_thm sign [p] cnf_disj_false;
   4.371 +           val thm2 = mk_cnf_thm sign p
   4.372 +       in
   4.373 +           cnf_eq_trans OF [thm1, thm2]
   4.374 +       end
   4.375 +
   4.376 +  | mk_cnf_thm sign (Const("op |",_) $ Const("True",_) $ p) =
   4.377 +       inst_thm sign [p] cnf_disj_true
   4.378 +
   4.379 +  | mk_cnf_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("True",_)) $ p) =
   4.380 +       let val thm1 = inst_thm sign [p] cnf_disj_not_true;
   4.381 +           val thm2 = mk_cnf_thm sign p
   4.382 +       in
   4.383 +           cnf_eq_trans OF [thm1, thm2]
   4.384 +       end
   4.385 +
   4.386 +  | mk_cnf_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("False",_)) $ p) =
   4.387 +       inst_thm sign [p] cnf_disj_not_false
   4.388 +
   4.389 +  | mk_cnf_thm sign (t as (Const("op |",_) $ p $ q)) = 
   4.390 +       if (is_lit p) then
   4.391 +          (
   4.392 +            if (is_clause t) then inst_thm sign [t] cnf_eq_id
   4.393 +            else 
   4.394 +             let val thm1 = inst_thm sign [p, q] cnf_disj_sym;
   4.395 +                 val thm2 = mk_cnf_thm sign (mk_disj(q, p))
   4.396 +             in
   4.397 +                cnf_eq_trans OF [thm1, thm2]
   4.398 +             end
   4.399 +          )
   4.400 +       else 
   4.401 +            let val (u, thm1) = head_nnf sign p;
   4.402 +                val thm2 = inst_thm sign [p,u,q] cnf_cong_disj;
   4.403 +                val thm3 = mk_cnf_thm sign (mk_disj(u, q))
   4.404 +            in
   4.405 +                cnf_eq_trans OF [(thm1 RS thm2), thm3]
   4.406 +            end
   4.407 +
   4.408 + | mk_cnf_thm sign t = inst_thm sign [t] cnf_eq_id
   4.409 +    (* error ("I don't know how to handle the formula " ^ 
   4.410 +                          (Sign.string_of_term sign t))
   4.411 +    *)
   4.412 +
   4.413 +fun term_of_thm c = term_of (cprop_of c)
   4.414 +
   4.415 +
   4.416 +(* Transform a given list of theorems (thms) into CNF *)
   4.417 +
   4.418 +fun mk_cnf_thms sg nil = nil
   4.419 +  | mk_cnf_thms sg (x::l) = 
   4.420 +    let val t = term_of_thm x
   4.421 +    in
   4.422 +      if (is_clause t) then x :: mk_cnf_thms sg l
   4.423 +      else 
   4.424 +       let val thm1 = mk_cnf_thm sg t
   4.425 +           val thm2 = cnf_eq_imp OF [thm1, x]
   4.426 +       in 
   4.427 +           thm2 :: mk_cnf_thms sg l
   4.428 +       end
   4.429 +    end
   4.430 +
   4.431 +
   4.432 +(* Count the number of hypotheses in a formula *)
   4.433 +fun num_of_hyps (Const("Trueprop", _) $ x) = num_of_hyps x
   4.434 +  | num_of_hyps (Const("==>",_) $ x $ y) = 1 + (num_of_hyps y)
   4.435 +  | num_of_hyps t = 0
   4.436 +
   4.437 +(* Tactic for converting to CNF (in primitive form): 
   4.438 +   it takes the first subgoal of the proof state, transform all its
   4.439 +   hypotheses into CNF (in primivite form) and remove the original 
   4.440 +   hypotheses.
   4.441 +*)
   4.442 +fun cnf_thin_tac state =
   4.443 +let val sg = Thm.sign_of_thm state
   4.444 +in
   4.445 +case (prems_of state) of 
   4.446 +  [] => Seq.empty
   4.447 +| (subgoal::_) => 
   4.448 +  let 
   4.449 +    val n = num_of_hyps (strip_all_body subgoal);
   4.450 +    val tac1 = METAHYPS (fn l => cut_facts_tac (mk_cnf_thms sg l) 1) 1
   4.451 +  in
   4.452 +    (tac1 THEN weakenings_tac n THEN (REPEAT (etac conjE 1)) ) state
   4.453 +  end
   4.454 +end
   4.455 +
   4.456 +(* Tactic for converting to CNF (in primitive form), keeping 
   4.457 +   the original hypotheses. *)
   4.458 +
   4.459 +fun cnf_tac state =
   4.460 +let val sg = Thm.sign_of_thm state
   4.461 +in
   4.462 +case (prems_of state) of 
   4.463 +  [] => Seq.empty
   4.464 +| (subgoal::_) => 
   4.465 +   METAHYPS (fn l => cut_facts_tac (mk_cnf_thms sg l) 1 
   4.466 +                    THEN (REPEAT (etac conjE 1)) ) 1 state
   4.467 +end
   4.468 +
   4.469 +
   4.470 +(***************************************************************************)
   4.471 +(*            CNF transformation by introducing new literals               *)
   4.472 +
   4.473 +(*** IMPORTANT: 
   4.474 +  This transformation uses variables of the form "lit_i", where i is a natural
   4.475 +  number. For the transformation to work, these variables must not already
   4.476 +  occur freely in the formula being transformed.
   4.477 +***)
   4.478 +
   4.479 +fun ext_conj x p q r =
   4.480 +   mk_conj(
   4.481 +    mk_disj(Not $ x, p),
   4.482 +    mk_conj(
   4.483 +      mk_disj(Not $ x, q),
   4.484 +      mk_conj(
   4.485 +        mk_disj(x, mk_disj(Not $ p, Not $ q)),
   4.486 +        mk_disj(x, r)
   4.487 +      )
   4.488 +    )
   4.489 +   )
   4.490 +
   4.491 +
   4.492 +(* Transform to CNF in primitive forms, possibly introduce extra variables *)
   4.493 +fun mk_cnfx_thm sign (Const("Trueprop",_) $ x) = mk_cnfx_thm sign x 
   4.494 +  | mk_cnfx_thm sign (t as (Const(_,_)))  = inst_thm sign [t] cnf_eq_id
   4.495 +  | mk_cnfx_thm sign (t as (Free(_,_)))  = inst_thm sign [t] cnf_eq_id
   4.496 +  | mk_cnfx_thm sign (Const("op -->", _) $ x $ y)  =
   4.497 +       let val thm1 = inst_thm sign [x, y] cnf_imp2disj;
   4.498 +           val thm2 = mk_cnfx_thm sign (mk_disj(Not $ x, y)) 
   4.499 +       in
   4.500 +           cnf_eq_trans OF [thm1, thm2]
   4.501 +       end
   4.502 +
   4.503 +  | mk_cnfx_thm sign (Const("op &", _) $ x $ y)  = 
   4.504 +       let val cnf1 = mk_cnfx_thm sign x
   4.505 +           val cnf2 = mk_cnfx_thm sign y
   4.506 +       in
   4.507 +           cnf_comb2eq OF [cnf1, cnf2]
   4.508 +       end
   4.509 +
   4.510 +  | mk_cnfx_thm sign (Const("Not",_) $ Const("True",_)) = 
   4.511 +        cnf_not_true_false
   4.512 +
   4.513 +  | mk_cnfx_thm sign (Const("Not",_) $ Const("False",_))  = 
   4.514 +        cnf_not_false_true
   4.515 +
   4.516 +  | mk_cnfx_thm sign (t as (Const("Not", _) $ x))  =
   4.517 +      ( 
   4.518 +       if (is_atm x) then inst_thm sign [t] cnf_eq_id
   4.519 +       else
   4.520 +         let val (t1, hn_thm) = head_nnf sign t
   4.521 +             val cnf_thm = mk_cnfx_thm sign t1 
   4.522 +         in
   4.523 +             cnf_eq_trans OF [hn_thm, cnf_thm]
   4.524 +         end
   4.525 +       ) 
   4.526 +
   4.527 +  | mk_cnfx_thm sign (Const("op |",_) $ (Const("op &", _) $ p $ q) $ r)  =
   4.528 +      if (is_lit r) then
   4.529 +        let val thm1 = inst_thm sign [p, q, r] cnf_disj_conj
   4.530 +            val thm2 = mk_cnfx_thm sign (mk_conj(mk_disj(p, r), mk_disj(q,r)))
   4.531 +        in
   4.532 +           cnf_eq_trans OF [thm1, thm2]
   4.533 +        end
   4.534 +      else cnfx_newlit sign p q r 
   4.535 +
   4.536 +  | mk_cnfx_thm sign (Const("op |",_) $ (Const("op |", _) $ p $ q) $ r)  =
   4.537 +       let val thm1 = inst_thm sign [p,q,r] cnf_disj_disj
   4.538 +           val thm2 = mk_cnfx_thm sign (mk_disj(p, mk_disj(q,r))) 
   4.539 +       in
   4.540 +          cnf_eq_trans OF [thm1, thm2]
   4.541 +       end
   4.542 +
   4.543 +  | mk_cnfx_thm sign (Const("op |",_) $ (Const("op -->", _) $ p $ q) $ r) =                       
   4.544 +       let val thm1 = inst_thm sign [p,q,r] cnf_disj_imp
   4.545 +           val thm2 = mk_cnfx_thm sign (mk_disj(Not $ p, mk_disj(q, r))) 
   4.546 +       in
   4.547 +           cnf_eq_trans OF [thm1, thm2]
   4.548 +       end
   4.549 +
   4.550 +  | mk_cnfx_thm sign (Const("op |",_) $ Const("False",_) $ p)  =
   4.551 +       let val thm1 = inst_thm sign [p] cnf_disj_false;
   4.552 +           val thm2 = mk_cnfx_thm sign p 
   4.553 +       in
   4.554 +           cnf_eq_trans OF [thm1, thm2]
   4.555 +       end
   4.556 +
   4.557 +  | mk_cnfx_thm sign (Const("op |",_) $ Const("True",_) $ p)  =
   4.558 +       inst_thm sign [p] cnf_disj_true
   4.559 +
   4.560 +  | mk_cnfx_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("True",_)) $ p)  =
   4.561 +       let val thm1 = inst_thm sign [p] cnf_disj_not_true;
   4.562 +           val thm2 = mk_cnfx_thm sign p 
   4.563 +       in
   4.564 +           cnf_eq_trans OF [thm1, thm2]
   4.565 +       end
   4.566 +
   4.567 +  | mk_cnfx_thm sign (Const("op |",_) $ (Const("Not",_) $ Const("False",_)) $ p)  =
   4.568 +       inst_thm sign [p] cnf_disj_not_false
   4.569 +
   4.570 +  | mk_cnfx_thm sign (t as (Const("op |",_) $ p $ q))  = 
   4.571 +       if (is_lit p) then
   4.572 +          (
   4.573 +            if (is_clause t) then inst_thm sign [t] cnf_eq_id
   4.574 +            else 
   4.575 +             let val thm1 = inst_thm sign [p, q] cnf_disj_sym
   4.576 +                 val thm2 = mk_cnfx_thm sign (mk_disj(q, p)) 
   4.577 +             in
   4.578 +                cnf_eq_trans OF [thm1, thm2]
   4.579 +             end
   4.580 +          )
   4.581 +       else 
   4.582 +            let val (u, thm1) = head_nnf sign p
   4.583 +                val thm2 = inst_thm sign [p,u,q] cnf_cong_disj
   4.584 +                val thm3 = mk_cnfx_thm sign (mk_disj(u, q)) 
   4.585 +            in
   4.586 +                cnf_eq_trans OF [(thm1 RS thm2), thm3]
   4.587 +            end
   4.588 +
   4.589 + | mk_cnfx_thm sign t  = error ("I don't know how to handle the formula " ^ 
   4.590 +                          (Sign.string_of_term sign t))
   4.591 +
   4.592 +and cnfx_newlit sign p q r  = 
   4.593 +   let val lit = read ("lit_" ^ (Int.toString (!lit_id)) ^ " :: bool")
   4.594 +       val _ = (lit_id := !lit_id + 1)
   4.595 +       val ct_lit = cterm_of sign lit
   4.596 +       val x_conj = ext_conj lit p q r
   4.597 +       val thm1 = inst_thm sign [p,q,r] cnf_newlit
   4.598 +       val thm2 = mk_cnfx_thm sign x_conj 
   4.599 +       val thm3 = forall_intr ct_lit thm2
   4.600 +       val thm4 = strip_shyps (thm3 COMP allI)
   4.601 +       val thm5 = strip_shyps (thm4 RS cnf_all_ex)
   4.602 +   in
   4.603 +       cnf_eq_trans OF [thm1, thm5]
   4.604 +   end
   4.605 +
   4.606 +
   4.607 +(* Theorems for converting formula into CNF (in primitive form), with 
   4.608 +   new extra variables *)
   4.609 +
   4.610 +
   4.611 +fun mk_cnfx_thms sg nil = nil
   4.612 +  | mk_cnfx_thms sg (x::l) = 
   4.613 +    let val t = term_of_thm x
   4.614 +    in
   4.615 +      if (is_clause t) then x :: mk_cnfx_thms sg l
   4.616 +      else 
   4.617 +       let val thm1 = mk_cnfx_thm sg t
   4.618 +           val thm2 = cnf_eq_imp OF [thm1,x]
   4.619 +       in 
   4.620 +           thm2 :: mk_cnfx_thms sg l
   4.621 +       end
   4.622 +    end
   4.623 +
   4.624 +
   4.625 +(* Tactic for converting hypotheses into CNF, possibly
   4.626 +   introducing new variables *)
   4.627 +
   4.628 +fun cnfx_thin_tac state =
   4.629 +let val sg = Thm.sign_of_thm state
   4.630 +in
   4.631 +case (prems_of state) of 
   4.632 +  [] => Seq.empty
   4.633 +| (subgoal::_) => 
   4.634 +   let val n = num_of_hyps (strip_all_body subgoal);
   4.635 +       val tac1 =  METAHYPS (fn l => cut_facts_tac (mk_cnfx_thms sg l) 1) 1
   4.636 +   in
   4.637 +      EVERY [tac1, weakenings_tac n, 
   4.638 +             REPEAT (etac conjE 1 ORELSE etac exE 1)] state
   4.639 +   end
   4.640 +end
   4.641 +
   4.642 +(* Tactic for converting the conclusion of a goal into CNF *)
   4.643 +
   4.644 +fun get_concl (Const("Trueprop", _) $ x) = get_concl x
   4.645 +  | get_concl (Const("==>",_) $ x $ y) = get_concl y
   4.646 +  | get_concl t = t
   4.647 +
   4.648 +fun cnf_concl_tac' state =
   4.649 +case (prems_of state) of 
   4.650 +  [] => Seq.empty
   4.651 +| (subgoal::_) =>
   4.652 +  let val sg = Thm.sign_of_thm state
   4.653 +      val c = get_concl subgoal
   4.654 +      val thm1 = (mk_cnf_thm sg c) RS cnf_eq_sym
   4.655 +      val thm2 = thm1 RS subst
   4.656 +  in
   4.657 +    rtac thm2 1 state
   4.658 +  end
   4.659 +
   4.660 +val cnf_concl_tac  = METAHYPS (fn l => cnf_concl_tac') 1 
   4.661 +
   4.662 +
   4.663 +end (*of structure*)
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/sat_funcs.ML	Fri Sep 23 22:58:50 2005 +0200
     5.3 @@ -0,0 +1,328 @@
     5.4 +(*  Title:      HOL/Tools/sat_funcs.ML
     5.5 +    ID:         $Id$
     5.6 +    Author:     Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
     5.7 +    Copyright   2005
     5.8 +
     5.9 +
    5.10 +Proof reconstruction from SAT solvers.
    5.11 +
    5.12 +  Description:
    5.13 +    This file defines several tactics to invoke a proof-producing
    5.14 +    SAT solver on a propositional goal in clausal form.
    5.15 +
    5.16 +    We use a sequent presentation of clauses to speed up resolution
    5.17 +    proof reconstruction. 
    5.18 +    We call such clauses as "raw clauses", which are of the form
    5.19 +          [| c1; c2; ...; ck |] ==> False
    5.20 +    where each clause ci is of the form
    5.21 +          [|l1,  l2,  ..., lm |] ==> False,
    5.22 +    where li is a literal  (see also comments in cnf_funcs.ML).
    5.23 +
    5.24 +    -- observe that this is the "dualized" version of the standard
    5.25 +       clausal form
    5.26 +           l1' \/ l2' \/ ... \/ lm', where li is the negation normal
    5.27 +       form of ~li'.
    5.28 +       The tactic produces a clause representation of the given goal
    5.29 +       in DIMACS format and invokes a SAT solver, which should return
    5.30 +       a proof consisting of a sequence of resolution steps, indicating
    5.31 +       the two input clauses and the variable resolved upon, and resulting
    5.32 +       in new clauses, leading to the empty clause (i.e., False).
    5.33 +       The tactic replays this proof in Isabelle and thus solves the
    5.34 +       overall goal.
    5.35 +
    5.36 +   There are two SAT tactics available. They differ in the CNF transformation
    5.37 +   used. The "sat_tac" uses naive CNF transformation to transform the theorem
    5.38 +   to be proved before giving it to SAT solver. The naive transformation in 
    5.39 +   some worst case can lead to explonential blow up in formula size.
    5.40 +   The other tactic, the "satx_tac" uses the "definitional CNF transformation"
    5.41 +   which produces formula of linear size increase compared to the input formula.
    5.42 +   This transformation introduces new variables. See also cnf_funcs.ML for
    5.43 +   more comments.
    5.44 +
    5.45 +
    5.46 + Notes for the current revision:
    5.47 +   - The current version supports only zChaff prover.
    5.48 +   - The environment variable ZCHAFF_HOME must be set to point to
    5.49 +     the directory where zChaff executable resides
    5.50 +   - The environment variable ZCHAFF_VERSION must be set according to
    5.51 +     the version of zChaff used. Current supported version of zChaff:
    5.52 +     zChaff version 2004.11.15
    5.53 +
    5.54 +*)
    5.55 +
    5.56 +(***************************************************************************)
    5.57 +(** Array of clauses **)
    5.58 +
    5.59 +signature CLAUSEARR =
    5.60 +sig
    5.61 +   val init : int -> unit 
    5.62 +   val register_at : int -> Thm.thm -> unit
    5.63 +   val register_list : Thm.thm list -> unit
    5.64 +   val getClause : int -> Thm.thm option
    5.65 +end
    5.66 +
    5.67 +structure ClauseArr : CLAUSEARR =
    5.68 +struct
    5.69 +
    5.70 +val clauses : ((Thm.thm option) array) ref = ref (Array.array(1, NONE));
    5.71 +
    5.72 +fun init size = (clauses := Array.array(size, NONE))
    5.73 +
    5.74 +fun register_at i c =  Array.update (!clauses, i, (SOME c))
    5.75 +
    5.76 +fun reg_list n nil = ()
    5.77 +  | reg_list n (x::l) = 
    5.78 +     (register_at n x; reg_list (n+1) l)
    5.79 +
    5.80 +fun register_list l = reg_list 0 l
    5.81 +
    5.82 +fun getClause i = Array.sub (!clauses, i)
    5.83 +
    5.84 +end
    5.85 +
    5.86 +
    5.87 +(***************************************************************************)
    5.88 +
    5.89 +signature SAT =
    5.90 +sig
    5.91 +  val trace_sat : bool ref      (* trace tactic *)
    5.92 +  val sat_tac : Tactical.tactic
    5.93 +  val satx_tac : Tactical.tactic
    5.94 +end
    5.95 +
    5.96 +functor SATFunc (structure cnf_struct : CNF) : SAT =
    5.97 +struct
    5.98 +
    5.99 +structure cnf = cnf_struct
   5.100 +
   5.101 +val trace_sat = ref false;	(* debugging flag *)
   5.102 +
   5.103 +
   5.104 +(* Look up the Isabelle atom corresponding to a DIMACS index in the
   5.105 +   reverse dictionary. This entry should exist, otherwise an error
   5.106 +   is raised.
   5.107 +*)
   5.108 +fun rev_lookup idx dictionary = 
   5.109 +let
   5.110 +   fun rev_assoc [] = NONE
   5.111 +     | rev_assoc ((key, entry)::list) =
   5.112 +       if entry = idx then SOME key else rev_assoc list
   5.113 +in
   5.114 +   the (rev_assoc dictionary)
   5.115 +end;
   5.116 +
   5.117 +
   5.118 +(* Convert rules of the form
   5.119 +   l1 ==> l2 ==> .. ==> li ==> .. ==> False
   5.120 +    to
   5.121 +   l1 ==> l2 ==> .... ==> ~li
   5.122 +*)
   5.123 +fun swap_prem rslv c = 
   5.124 +let 
   5.125 +    val thm1 = rule_by_tactic (metacut_tac c 1  THEN 
   5.126 +                  (atac 1) THEN (REPEAT_SOME atac)) rslv
   5.127 +in
   5.128 +    rule_by_tactic (ALLGOALS (cnf.weakening_tac)) thm1
   5.129 +end
   5.130 +
   5.131 +(*** Proof reconstruction: given two clauses
   5.132 +   [| x1 ; .. ; a ; .. ; xn |] ==> False
   5.133 +   and 
   5.134 +   [| y1 ; .. ; ~a ; .. ; ym |] ==> False , 
   5.135 +
   5.136 +   we firt convert the first clause into
   5.137 +
   5.138 +   [| x1 ; ... ; xn |] ==> ~a     (using swap_prem)
   5.139 +
   5.140 +   and do a resolution with the second clause to produce
   5.141 +   [| y1 ; ... ; x1 ; ... ; xn ; ... ; yn |] ==> False
   5.142 +
   5.143 +***)
   5.144 +
   5.145 +fun dual (Const("Trueprop",_) $ x) (Const("Trueprop",_) $ y) = dual x y
   5.146 +  | dual (Const("Not",_) $ x) y = (x = y)
   5.147 +  | dual x (Const("Not",_) $ y) = (x = y)
   5.148 +  | dual x y = false
   5.149 +
   5.150 +(* Check if an atom has a dual in a list of atoms *)
   5.151 +
   5.152 +fun dual_mem x nil = false
   5.153 +  | dual_mem x (y::l) = if (dual x y) then true else dual_mem x l
   5.154 +
   5.155 +
   5.156 +fun replay_chain sg idx (c::cs) =
   5.157 +let
   5.158 +   val (SOME fc) = ClauseArr.getClause c;
   5.159 +
   5.160 +   fun strip_neg (Const("Trueprop", _) $ x) = strip_neg x
   5.161 +     | strip_neg (Const("Not",_) $ x) = x
   5.162 +     | strip_neg x = x
   5.163 +
   5.164 +   (* Find out which atom (literal) is used in the resolution *)
   5.165 +   fun res_atom nil l = raise THM ("Proof reconstruction failed!", 0, [])
   5.166 +     | res_atom (x::l1) l2 = 
   5.167 +        if (dual_mem x l2) then strip_neg x
   5.168 +        else res_atom l1 l2
   5.169 +
   5.170 +   fun replay old [] = old
   5.171 +     | replay old (cls :: clss) =
   5.172 +       let
   5.173 +          val (SOME icls) = ClauseArr.getClause cls;
   5.174 +          val var = res_atom (prems_of old) (prems_of icls);
   5.175 +          val atom = cterm_of sg var;
   5.176 +          val rslv = instantiate' [] [SOME atom] notI;
   5.177 +
   5.178 +          val _ = if (!trace_sat) then
   5.179 +            (
   5.180 +              writeln "-- resolving clause:";
   5.181 +              print_thm old;
   5.182 +              writeln "-- with clause: ";
   5.183 +              print_thm icls;
   5.184 +              writeln "-- using ";
   5.185 +              writeln (string_of_cterm atom)
   5.186 +            ) else ();
   5.187 +
   5.188 +          val thm1 = (
   5.189 +              rule_by_tactic (REPEAT_SOME (rtac (swap_prem rslv old))) icls
   5.190 +              handle THM _ =>
   5.191 +              rule_by_tactic (REPEAT_SOME (rtac (swap_prem rslv icls))) old );
   5.192 +
   5.193 +          val new = rule_by_tactic distinct_subgoals_tac thm1;
   5.194 +          val _ = if (!trace_sat) then (writeln "-- resulting clause:"; print_thm new)
   5.195 +                  else ()
   5.196 +       in
   5.197 +          replay new clss 
   5.198 +       end
   5.199 +in
   5.200 +   ClauseArr.register_at idx (replay fc cs);
   5.201 +   if (!trace_sat) then (
   5.202 +      writeln ("-- Replay chain successful. " ^ 
   5.203 +               "The resulting clause stored at #" ^ (Int.toString idx))
   5.204 +   ) else ()
   5.205 +end
   5.206 +
   5.207 +
   5.208 +(* Replay the resolution proof from file prf_file with hypotheses hyps.
   5.209 +   Returns the theorem established by the proof (which is just False).
   5.210 +*)
   5.211 +fun replay_prf sg tab size =
   5.212 +  let
   5.213 +     val prf = Inttab.dest tab;
   5.214 +
   5.215 +     fun complete nil = true
   5.216 +       | complete (x::l) = (
   5.217 +           case ClauseArr.getClause x of 
   5.218 +             NONE => false
   5.219 +           | (SOME _) => complete l)
   5.220 +
   5.221 +     fun do_chains [] = ()
   5.222 +       | do_chains (pr :: rs) = 
   5.223 +         let val (idx, cls) = pr
   5.224 +         in
   5.225 +            if (complete cls) then  
   5.226 +               (replay_chain sg idx cls; do_chains rs)
   5.227 +            else do_chains (rs @ [pr])
   5.228 +         end
   5.229 +  in
   5.230 +    if (!trace_sat) then (
   5.231 +        writeln "Proof trace from SAT solver: ";
   5.232 +        print prf ; ()
   5.233 +     ) else () ;
   5.234 +     do_chains prf;
   5.235 +     ClauseArr.getClause size
   5.236 +  end;
   5.237 +
   5.238 +
   5.239 +(***************************************************************************)
   5.240 +(***                  Functions to build the sat tactic                  ***)
   5.241 +
   5.242 +(* A trivial tactic, used in preprocessing before calling the main 
   5.243 +   tactic *)
   5.244 +
   5.245 +val pre_sat_tac  = (REPEAT (etac conjE 1)) THEN 
   5.246 +                   (REPEAT ((atac 1) ORELSE (etac FalseE 1)))
   5.247 +
   5.248 +fun collect_atoms (Const("Trueprop",_) $ x) l = collect_atoms x l
   5.249 +  | collect_atoms (Const("op |", _) $ x $ y) l = 
   5.250 +        collect_atoms x (collect_atoms y l) 
   5.251 +  | collect_atoms x l = if (x mem l) then l else (x::l) 
   5.252 +
   5.253 +fun has_duals nil = false
   5.254 +  | has_duals (x::l) = if (dual_mem x l) then true else has_duals l
   5.255 +
   5.256 +fun trivial_clause (Const("True",_)) = true
   5.257 +  | trivial_clause c = has_duals (collect_atoms c nil)
   5.258 +
   5.259 +(* Remove trivial clauses *)
   5.260 +fun filter_clauses nil = nil
   5.261 +  | filter_clauses (x::l) =
   5.262 +    if (trivial_clause (term_of (cprop_of x))) then filter_clauses l
   5.263 +    else (x:: filter_clauses l)
   5.264 +
   5.265 +fun is_true assignment x =
   5.266 +    case (assignment x) of 
   5.267 +      NONE => false
   5.268 +    | SOME b => b
   5.269 +
   5.270 +fun get_model dict assignment = 
   5.271 +    map (fn (x,y) => x) (List.filter (fn (x,y) => is_true assignment y) dict)
   5.272 +
   5.273 +fun string_of_model sg nil = ""
   5.274 +  | string_of_model sg [x] = Sign.string_of_term sg x
   5.275 +  | string_of_model sg (x::l) = (Sign.string_of_term sg x) ^ ", " ^ (string_of_model sg l)
   5.276 +
   5.277 +(* Run external SAT solver with the given clauses. Reconstruct a proof from
   5.278 +   the resulting proof trace of the SAT solver. 
   5.279 +*)
   5.280 +
   5.281 +fun rawsat_thm sg prems =
   5.282 +let val thms = filter_clauses prems 
   5.283 +    val (fm, dict) = cnf.cnf2prop thms
   5.284 +    val raw_thms = cnf.cnf2raw_thms thms
   5.285 +in
   5.286 +   let
   5.287 +       val result = SatSolver.invoke_solver "zchaff_with_proofs" fm;
   5.288 +   in
   5.289 +     case result of
   5.290 +       (SatSolver.UNSATISFIABLE (SOME (table, size))) => 
   5.291 +          let val _ = ClauseArr.init (size + 1);
   5.292 +              val _ = ClauseArr.register_list 
   5.293 +                      (map (fn x => (rule_by_tactic distinct_subgoals_tac x)) raw_thms);
   5.294 +              val (SOME thm1) = replay_prf sg table size
   5.295 +          in 
   5.296 +              thm1
   5.297 +          end
   5.298 +      | (SatSolver.SATISFIABLE model) => 
   5.299 +          let val msg = "\nSAT solver found a countermodel:\n{ " ^ 
   5.300 +                        (string_of_model sg (get_model dict model)) ^ " }\n"
   5.301 +          in
   5.302 +                raise THM (msg, 0, [])
   5.303 +          end    
   5.304 +      | _ => raise THM ("SAT solver failed!\n", 0, [])
   5.305 +
   5.306 +  end
   5.307 +end
   5.308 +
   5.309 +fun cnfsat_basic_tac state = 
   5.310 +let val sg = Thm.sign_of_thm state
   5.311 +in 
   5.312 +  METAHYPS (fn prems => rtac (rawsat_thm sg prems) 1) 1 state
   5.313 +end
   5.314 +
   5.315 +(* Tactic for calling external SAT solver, taking as input CNF clauses *)
   5.316 +val cnfsat_tac = pre_sat_tac THEN (IF_UNSOLVED cnfsat_basic_tac)
   5.317 +
   5.318 +
   5.319 +(* 
   5.320 +   Tactic for calling external SAT solver, taking as input arbitrary formula. 
   5.321 +*)
   5.322 +val sat_tac = cnf.cnf_thin_tac THEN cnfsat_tac;
   5.323 +
   5.324 +(* 
   5.325 +  Tactic for calling external SAT solver, taking as input arbitratry formula.
   5.326 +  The input is translated to CNF (in primitive form), possibly introducing
   5.327 +  new literals. 
   5.328 +*)
   5.329 +val satx_tac = cnf.cnfx_thin_tac THEN cnfsat_tac;
   5.330 +
   5.331 +end (*of structure*)
     6.1 --- a/src/HOL/ex/ROOT.ML	Fri Sep 23 22:49:25 2005 +0200
     6.2 +++ b/src/HOL/ex/ROOT.ML	Fri Sep 23 22:58:50 2005 +0200
     6.3 @@ -45,6 +45,9 @@
     6.4  time_use_thy "SVC_Oracle";
     6.5  if_svc_enabled time_use_thy "svc_test";
     6.6  
     6.7 +(* requires zChaff with proof generation to be installed: *)
     6.8 +time_use_thy "SAT_Examples" handle ERROR => ();
     6.9 +
    6.10  time_use_thy "Refute_Examples";
    6.11  time_use_thy "Quickcheck_Examples";
    6.12  
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/ex/SAT_Examples.thy	Fri Sep 23 22:58:50 2005 +0200
     7.3 @@ -0,0 +1,212 @@
     7.4 +(*  Title:      HOL/ex/SAT_Examples.thy
     7.5 +    ID:         $Id$
     7.6 +    Author:     Alwen Tiu, Tjark Weber
     7.7 +    Copyright   2005
     7.8 +*)
     7.9 +
    7.10 +header {* Examples for the 'sat' command *}
    7.11 +
    7.12 +theory SAT_Examples imports Main
    7.13 +
    7.14 +begin
    7.15 +
    7.16 +(* Translated from TPTP problem library: PUZ015-2.006.dimacs *)
    7.17 +
    7.18 +lemma assumes 1: "~x0"
    7.19 +and 2: "~x30"
    7.20 +and 3: "~x29"
    7.21 +and 4: "~x59"
    7.22 +and 5: "x1 | x31 | x0"
    7.23 +and 6: "x2 | x32 | x1"
    7.24 +and 7: "x3 | x33 | x2"
    7.25 +and 8: "x4 | x34 | x3"
    7.26 +and 9: "x35 | x4"
    7.27 +and 10: "x5 | x36 | x30"
    7.28 +and 11: "x6 | x37 | x5 | x31"
    7.29 +and 12: "x7 | x38 | x6 | x32"
    7.30 +and 13: "x8 | x39 | x7 | x33"
    7.31 +and 14: "x9 | x40 | x8 | x34"
    7.32 +and 15: "x41 | x9 | x35"
    7.33 +and 16: "x10 | x42 | x36"
    7.34 +and 17: "x11 | x43 | x10 | x37"
    7.35 +and 18: "x12 | x44 | x11 | x38"
    7.36 +and 19: "x13 | x45 | x12 | x39"
    7.37 +and 20: "x14 | x46 | x13 | x40"
    7.38 +and 21: "x47 | x14 | x41"
    7.39 +and 22: "x15 | x48 | x42"
    7.40 +and 23: "x16 | x49 | x15 | x43"
    7.41 +and 24: "x17 | x50 | x16 | x44"
    7.42 +and 25: "x18 | x51 | x17 | x45"
    7.43 +and 26: "x19 | x52 | x18 | x46"
    7.44 +and 27: "x53 | x19 | x47"
    7.45 +and 28: "x20 | x54 | x48"
    7.46 +and 29: "x21 | x55 | x20 | x49"
    7.47 +and 30: "x22 | x56 | x21 | x50"
    7.48 +and 31: "x23 | x57 | x22 | x51"
    7.49 +and 32: "x24 | x58 | x23 | x52"
    7.50 +and 33: "x59 | x24 | x53"
    7.51 +and 34: "x25 | x54"
    7.52 +and 35: "x26 | x25 | x55"
    7.53 +and 36: "x27 | x26 | x56"
    7.54 +and 37: "x28 | x27 | x57"
    7.55 +and 38: "x29 | x28 | x58"
    7.56 +and 39: "~x1 | ~x31"
    7.57 +and 40: "~x1 | ~x0"
    7.58 +and 41: "~x31 | ~x0"
    7.59 +and 42: "~x2 | ~x32"
    7.60 +and 43: "~x2 | ~x1"
    7.61 +and 44: "~x32 | ~x1"
    7.62 +and 45: "~x3 | ~x33"
    7.63 +and 46: "~x3 | ~x2"
    7.64 +and 47: "~x33 | ~x2"
    7.65 +and 48: "~x4 | ~x34"
    7.66 +and 49: "~x4 | ~x3"
    7.67 +and 50: "~x34 | ~x3"
    7.68 +and 51: "~x35 | ~x4"
    7.69 +and 52: "~x5 | ~x36"
    7.70 +and 53: "~x5 | ~x30"
    7.71 +and 54: "~x36 | ~x30"
    7.72 +and 55: "~x6 | ~x37"
    7.73 +and 56: "~x6 | ~x5"
    7.74 +and 57: "~x6 | ~x31"
    7.75 +and 58: "~x37 | ~x5"
    7.76 +and 59: "~x37 | ~x31"
    7.77 +and 60: "~x5 | ~x31"
    7.78 +and 61: "~x7 | ~x38"
    7.79 +and 62: "~x7 | ~x6"
    7.80 +and 63: "~x7 | ~x32"
    7.81 +and 64: "~x38 | ~x6"
    7.82 +and 65: "~x38 | ~x32"
    7.83 +and 66: "~x6 | ~x32"
    7.84 +and 67: "~x8 | ~x39"
    7.85 +and 68: "~x8 | ~x7"
    7.86 +and 69: "~x8 | ~x33"
    7.87 +and 70: "~x39 | ~x7"
    7.88 +and 71: "~x39 | ~x33"
    7.89 +and 72: "~x7 | ~x33"
    7.90 +and 73: "~x9 | ~x40"
    7.91 +and 74: "~x9 | ~x8"
    7.92 +and 75: "~x9 | ~x34"
    7.93 +and 76: "~x40 | ~x8"
    7.94 +and 77: "~x40 | ~x34"
    7.95 +and 78: "~x8 | ~x34"
    7.96 +and 79: "~x41 | ~x9"
    7.97 +and 80: "~x41 | ~x35"
    7.98 +and 81: "~x9 | ~x35"
    7.99 +and 82: "~x10 | ~x42"
   7.100 +and 83: "~x10 | ~x36"
   7.101 +and 84: "~x42 | ~x36"
   7.102 +and 85: "~x11 | ~x43"
   7.103 +and 86: "~x11 | ~x10"
   7.104 +and 87: "~x11 | ~x37"
   7.105 +and 88: "~x43 | ~x10"
   7.106 +and 89: "~x43 | ~x37"
   7.107 +and 90: "~x10 | ~x37"
   7.108 +and 91: "~x12 | ~x44"
   7.109 +and 92: "~x12 | ~x11"
   7.110 +and 93: "~x12 | ~x38"
   7.111 +and 94: "~x44 | ~x11"
   7.112 +and 95: "~x44 | ~x38"
   7.113 +and 96: "~x11 | ~x38"
   7.114 +and 97: "~x13 | ~x45"
   7.115 +and 98: "~x13 | ~x12"
   7.116 +and 99: "~x13 | ~x39"
   7.117 +and 100: "~x45 | ~x12"
   7.118 +and 101: "~x45 | ~x39"
   7.119 +and 102: "~x12 | ~x39"
   7.120 +and 103: "~x14 | ~x46"
   7.121 +and 104: "~x14 | ~x13"
   7.122 +and 105: "~x14 | ~x40"
   7.123 +and 106: "~x46 | ~x13"
   7.124 +and 107: "~x46 | ~x40"
   7.125 +and 108: "~x13 | ~x40"
   7.126 +and 109: "~x47 | ~x14"
   7.127 +and 110: "~x47 | ~x41"
   7.128 +and 111: "~x14 | ~x41"
   7.129 +and 112: "~x15 | ~x48"
   7.130 +and 113: "~x15 | ~x42"
   7.131 +and 114: "~x48 | ~x42"
   7.132 +and 115: "~x16 | ~x49"
   7.133 +and 116: "~x16 | ~x15"
   7.134 +and 117: "~x16 | ~x43"
   7.135 +and 118: "~x49 | ~x15"
   7.136 +and 119: "~x49 | ~x43"
   7.137 +and 120: "~x15 | ~x43"
   7.138 +and 121: "~x17 | ~x50"
   7.139 +and 122: "~x17 | ~x16"
   7.140 +and 123: "~x17 | ~x44"
   7.141 +and 124: "~x50 | ~x16"
   7.142 +and 125: "~x50 | ~x44"
   7.143 +and 126: "~x16 | ~x44"
   7.144 +and 127: "~x18 | ~x51"
   7.145 +and 128: "~x18 | ~x17"
   7.146 +and 129: "~x18 | ~x45"
   7.147 +and 130: "~x51 | ~x17"
   7.148 +and 131: "~x51 | ~x45"
   7.149 +and 132: "~x17 | ~x45"
   7.150 +and 133: "~x19 | ~x52"
   7.151 +and 134: "~x19 | ~x18"
   7.152 +and 135: "~x19 | ~x46"
   7.153 +and 136: "~x52 | ~x18"
   7.154 +and 137: "~x52 | ~x46"
   7.155 +and 138: "~x18 | ~x46"
   7.156 +and 139: "~x53 | ~x19"
   7.157 +and 140: "~x53 | ~x47"
   7.158 +and 141: "~x19 | ~x47"
   7.159 +and 142: "~x20 | ~x54"
   7.160 +and 143: "~x20 | ~x48"
   7.161 +and 144: "~x54 | ~x48"
   7.162 +and 145: "~x21 | ~x55"
   7.163 +and 146: "~x21 | ~x20"
   7.164 +and 147: "~x21 | ~x49"
   7.165 +and 148: "~x55 | ~x20"
   7.166 +and 149: "~x55 | ~x49"
   7.167 +and 150: "~x20 | ~x49"
   7.168 +and 151: "~x22 | ~x56"
   7.169 +and 152: "~x22 | ~x21"
   7.170 +and 153: "~x22 | ~x50"
   7.171 +and 154: "~x56 | ~x21"
   7.172 +and 155: "~x56 | ~x50"
   7.173 +and 156: "~x21 | ~x50"
   7.174 +and 157: "~x23 | ~x57"
   7.175 +and 158: "~x23 | ~x22"
   7.176 +and 159: "~x23 | ~x51"
   7.177 +and 160: "~x57 | ~x22"
   7.178 +and 161: "~x57 | ~x51"
   7.179 +and 162: "~x22 | ~x51"
   7.180 +and 163: "~x24 | ~x58"
   7.181 +and 164: "~x24 | ~x23"
   7.182 +and 165: "~x24 | ~x52"
   7.183 +and 166: "~x58 | ~x23"
   7.184 +and 167: "~x58 | ~x52"
   7.185 +and 168: "~x23 | ~x52"
   7.186 +and 169: "~x59 | ~x24"
   7.187 +and 170: "~x59 | ~x53"
   7.188 +and 171: "~x24 | ~x53"
   7.189 +and 172: "~x25 | ~x54"
   7.190 +and 173: "~x26 | ~x25"
   7.191 +and 174: "~x26 | ~x55"
   7.192 +and 175: "~x25 | ~x55"
   7.193 +and 176: "~x27 | ~x26"
   7.194 +and 177: "~x27 | ~x56"
   7.195 +and 178: "~x26 | ~x56"
   7.196 +and 179: "~x28 | ~x27"
   7.197 +and 180: "~x28 | ~x57"
   7.198 +and 181: "~x27 | ~x57"
   7.199 +and 182: "~x29 | ~x28"
   7.200 +and 183: "~x29 | ~x58"
   7.201 +and 184: "~x28 | ~x58"
   7.202 +shows "False"
   7.203 +using 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 
   7.204 +20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 
   7.205 +40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 
   7.206 +60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 
   7.207 +80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 
   7.208 +100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 
   7.209 +120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 
   7.210 +140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 
   7.211 +160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 
   7.212 +180 181 182 183 184 
   7.213 +by sat
   7.214 +
   7.215 +end