--- a/src/HOL/Tools/cnf_funcs.ML Fri Mar 10 16:21:49 2006 +0100
+++ b/src/HOL/Tools/cnf_funcs.ML Fri Mar 10 16:31:50 2006 +0100
@@ -2,14 +2,14 @@
ID: $Id$
Author: Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
Author: Tjark Weber
- Copyright 2005
+ Copyright 2005-2006
Description:
This file contains functions and tactics to transform a formula into
Conjunctive Normal Form (CNF).
A formula in CNF is of the following form:
- (x11 | x12 | .. x1n) & ... & (xm1 | xm2 | ... | xmk)
+ (x11 | x12 | ... | x1n) & ... & (xm1 | xm2 | ... | xmk)
False
True
@@ -23,11 +23,13 @@
representation of clauses, which we call the "raw clauses".
Raw clauses are of the form
- x1 ==> x2 ==> .. ==> xn ==> False ,
+ x1', x2', ..., xn', ~ (x1 | x2 | ... | xn) ==> False |- False ,
+
+ where each xi is a literal, and each xi' is the negation normal form of ~xi.
- where each xi is a literal. Note that the above raw clause corresponds
- to the clause (x1' | ... | xn'), where each xi' is the negation normal
- form of ~xi.
+ Raw clauses may contain further hyps of the form "~ clause ==> False".
+ Literals are successively removed from the hyps of raw clauses by resolution
+ during SAT proof reconstruction.
*)
signature CNF =
@@ -37,8 +39,8 @@
val is_clause : Term.term -> bool
val clause_is_trivial : Term.term -> bool
- val is_raw_clause : Term.term -> bool
- val clause2raw_thm : Thm.thm -> Thm.thm
+ val clause2raw_thm : Thm.thm -> Thm.thm
+ val rawhyps2clausehyps_thm : Thm.thm -> Thm.thm
val weakening_tac : int -> Tactical.tactic (* removes the first hypothesis of a subgoal *)
@@ -137,24 +139,10 @@
end;
(* ------------------------------------------------------------------------- *)
-(* is_raw_clause: returns true iff the term is of the form *)
-(* x1 ==> ... ==> xn ==> False , *)
-(* with n >= 1, where each xi is a literal *)
-(* ------------------------------------------------------------------------- *)
-
-(* Term.term -> bool *)
-
-fun is_raw_clause (Const ("==>", _) $ x $ y) =
- is_literal x andalso
- (y = HOLogic.mk_Trueprop HOLogic.false_const orelse is_raw_clause y)
- | is_raw_clause _ =
- false;
-
-(* ------------------------------------------------------------------------- *)
(* clause2raw_thm: translates a clause into a raw clause, i.e. *)
-(* x1 | ... | xn *)
+(* ... |- x1 | ... | xn *)
(* (where each xi is a literal) is translated to *)
-(* x1' ==> ... ==> xn' ==> False , *)
+(* ~(x1 | ... | xn) ==> False, x1', ..., xn' |- False , *)
(* where each xi' is the negation normal form of ~xi. *)
(* ------------------------------------------------------------------------- *)
@@ -162,7 +150,9 @@
fun clause2raw_thm c =
let
- val thm1 = c RS clause2raw_notE (* ~(x1 | ... | xn) ==> False *)
+ val disj = HOLogic.dest_Trueprop (prop_of c)
+ val not_disj_imp_false = Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_not disj), HOLogic.mk_Trueprop HOLogic.false_const)
+ val thm1 = Thm.assume (cterm_of (theory_of_thm c) not_disj_imp_false) (* ~(x1 | ... | xn) ==> False |- ~(x1 | ... | xn) ==> False *)
(* eliminates negated disjunctions from the i-th premise, possibly *)
(* adding new premises, then continues with the (i+1)-th premise *)
(* Thm.thm -> int -> Thm.thm *)
@@ -171,13 +161,38 @@
thm
else
not_disj_to_prem (Seq.hd (REPEAT_DETERM (rtac clause2raw_not_disj i) thm)) (i+1)
- val thm2 = not_disj_to_prem thm1 1 (* ~x1 ==> ... ==> ~xn ==> False *)
- val thm3 = Seq.hd (TRYALL (rtac clause2raw_not_not) thm2) (* x1' ==> ... ==> xn' ==> False *)
+ val thm2 = not_disj_to_prem thm1 1 (* ~(x1 | ... | xn) ==> False |- ~x1 ==> ... ==> ~xn ==> False *)
+ val thm3 = Seq.hd (TRYALL (rtac clause2raw_not_not) thm2) (* ~(x1 | ... | xn) ==> False |- x1' ==> ... ==> xn' ==> False *)
+ val thy3 = theory_of_thm thm3
+ val thm4 = fold (fn prem => fn thm => Thm.implies_elim thm (Thm.assume (cterm_of thy3 prem))) (prems_of thm3) thm3 (* ~(x1 | ... | xn) ==> False, x1', ..., xn' |- False *)
in
- thm3
+ thm4
end;
(* ------------------------------------------------------------------------- *)
+(* rawhyps2clausehyps_thm: translates all hyps of the form "~P ==> False" to *)
+(* hyps of the form "P" *)
+(* ------------------------------------------------------------------------- *)
+
+(* Thm.thm -> Thm.thm *)
+
+fun rawhyps2clausehyps_thm c =
+ fold (fn hyp => fn thm =>
+ case hyp of Const ("==>", _) $ (Const ("Trueprop", _) $ (Const ("Not", _) $ P)) $ (Const ("Trueprop", _) $ Const ("False", _)) =>
+ let
+ val cterm = cterm_of (theory_of_thm thm)
+ val thm1 = Thm.implies_intr (cterm hyp) thm (* hyps |- (~P ==> False) ==> goal *)
+ val varP = Var (("P", 0), HOLogic.boolT)
+ val notE = Thm.instantiate ([], [(cterm varP, cterm P)]) clause2raw_notE (* P ==> ~P ==> False *)
+ val notE' = Thm.implies_elim notE (Thm.assume (cterm (HOLogic.mk_Trueprop P))) (* P |- ~P ==> False *)
+ val thm2 = Thm.implies_elim thm1 notE' (* hyps, P |- goal *)
+ in
+ thm2
+ end
+ | _ =>
+ thm) (#hyps (rep_thm c)) c;
+
+(* ------------------------------------------------------------------------- *)
(* inst_thm: instantiates a theorem with a list of terms *)
(* ------------------------------------------------------------------------- *)
--- a/src/HOL/Tools/sat_funcs.ML Fri Mar 10 16:21:49 2006 +0100
+++ b/src/HOL/Tools/sat_funcs.ML Fri Mar 10 16:31:50 2006 +0100
@@ -2,7 +2,7 @@
ID: $Id$
Author: Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
Author: Tjark Weber
- Copyright 2005
+ Copyright 2005-2006
Proof reconstruction from SAT solvers.
@@ -14,15 +14,14 @@
We use a sequent presentation of clauses to speed up resolution
proof reconstruction.
We call such clauses "raw clauses", which are of the form
- [| c1; c2; ...; ck |] ==> False
+ x1; ...; xn; c1; c2; ...; ck |- False
+ (note the use of |- instead of ==>, i.e. of Isabelle's (meta-)hyps here),
where each clause ci is of the form
- [| l1; l2; ...; lm |] ==> False,
- where each li is a literal (see also comments in cnf_funcs.ML).
+ ~ (l1 | l2 | ... | lm) ==> False,
+ where each xi and each li is a literal (see also comments in cnf_funcs.ML).
- -- Observe that this is the "dualized" version of the standard
- clausal form
- l1' \/ l2' \/ ... \/ lm', where li is the negation normal
- form of ~li'.
+ This does not work for goals containing schematic variables!
+
The tactic produces a clause representation of the given goal
in DIMACS format and invokes a SAT solver, which should return
a proof consisting of a sequence of resolution steps, indicating
@@ -65,21 +64,15 @@
val counter = ref 0;
-(* ------------------------------------------------------------------------- *)
-(* swap_prem: convert raw clauses of the form *)
-(* [| l1; l2; ...; li; ... |] ==> False *)
-(* to *)
-(* [| l1; l2; ... |] ==> ~li . *)
-(* Note that ~li may be equal to ~~a for some atom a. *)
-(* ------------------------------------------------------------------------- *)
-
-(* Thm.thm -> int -> Thm.thm *)
-
-fun swap_prem raw_cl i =
- Seq.hd ((metacut_tac raw_cl 1 (* [| [| ?P; False |] ==> False; ?P ==> l1; ...; ?P ==> li; ... |] ==> ~ ?P *)
- THEN atac (i+1) (* [| [| li; False |] ==> False; li ==> l1; ... |] ==> ~ li *)
- THEN atac 1 (* [| li ==> l1; ... |] ==> ~ li *)
- THEN ALLGOALS cnf.weakening_tac) notI);
+(* Thm.thm *)
+val resolution_thm = (* "[| P ==> False; ~P ==> False |] ==> False" *)
+ let
+ val cterm = cterm_of (the_context ())
+ val Q = Var (("Q", 0), HOLogic.boolT)
+ val False = HOLogic.false_const
+ in
+ Thm.instantiate ([], [(cterm Q, cterm False)]) case_split_thm
+ end;
(* ------------------------------------------------------------------------- *)
(* resolve_raw_clauses: given a non-empty list of raw clauses, we fold *)
@@ -109,35 +102,70 @@
fun is_neg (Const ("Not", _) $ _) = true
| is_neg _ = false
- (* find out which premises are used in the resolution *)
- (* Term.term list -> Term.term list -> int -> (int * int * bool) *)
- fun res_prems [] _ _ =
+ (* find out which two hyps are used in the resolution *)
+ (* Term.term list -> Term.term list -> Term.term * Term.term *)
+ fun res_hyps [] _ =
+ raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
+ | res_hyps _ [] =
raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
- | res_prems (x::xs) ys idx1 =
- let
- val x' = HOLogic.dest_Trueprop x
- val idx2 = find_index_eq (dual x') ys
- in
- if idx2 = (~1) then
- res_prems xs ys (idx1+1)
+ | res_hyps ((Const ("Trueprop", _) $ x) :: xs) ys =
+ let val dx = dual x in
+ (* hyps are implemented as ordered list in the kernel, and *)
+ (* stripping 'Trueprop' should not change the order *)
+ if OrdList.member Term.fast_term_ord ys dx then
+ (x, dx)
else
- (idx1, idx2, is_neg x')
+ res_hyps xs ys
end
+ | res_hyps (_ :: xs) ys =
+ (* hyps are implemented as ordered list in the kernel, all hyps are of *)
+ (* the form 'Trueprop $ lit' or 'implies $ (negated clause) $ False', *)
+ (* and the former are LESS than the latter according to the order -- *)
+ (* therefore there is no need to continue the search via *)
+ (* 'res_hyps xs ys' here *)
+ raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
(* Thm.thm -> Thm.thm -> Thm.thm *)
fun resolution c1 c2 =
let
val _ = if !trace_sat then
- tracing ("Resolving clause: " ^ string_of_thm c1 ^ "\nwith clause: " ^ string_of_thm c2)
+ tracing ("Resolving clause: " ^ string_of_thm c1 ^ " (hyps: " ^ space_implode ", " (map (Sign.string_of_term (theory_of_thm c1)) (#hyps (rep_thm c1)))
+ ^ ")\nwith clause: " ^ string_of_thm c2 ^ " (hyps: " ^ space_implode ", " (map (Sign.string_of_term (theory_of_thm c2)) (#hyps (rep_thm c2))) ^ ")")
else ()
- val prems2 = map HOLogic.dest_Trueprop (prems_of c2)
- val (idx1, idx2, is_neg_lit) = res_prems (prems_of c1) prems2 0
- val swap_c1 = swap_prem c1 (idx1+1)
- val swap_c1_nnf = if is_neg_lit then Seq.hd (rtac swap_c1 1 notnotD) else swap_c1 (* deal with double-negation *)
- val c_new = Seq.hd ((rtac swap_c1_nnf (idx2+1) THEN distinct_subgoals_tac) c2)
+ (* Term.term list -> Term.term list *)
+ fun dest_filter_Trueprop [] = []
+ | dest_filter_Trueprop ((Const ("Trueprop", _) $ x) :: xs) = x :: dest_filter_Trueprop xs
+ | dest_filter_Trueprop (_ :: xs) = dest_filter_Trueprop xs
+
+ val hyps1 = (#hyps o rep_thm) c1
+ (* minor optimization: dest/filter over the second list outside 'res_hyps' to do it only once *)
+ val hyps2 = (dest_filter_Trueprop o #hyps o rep_thm) c2
+
+ val (l1, l2) = res_hyps hyps1 hyps2 (* the two literals used for resolution, with 'Trueprop' stripped *)
+ val is_neg = is_neg l1
+
+ val c1' = Thm.implies_intr (cterm_of (theory_of_thm c1) (HOLogic.mk_Trueprop l1)) c1 (* Gamma1 |- l1 ==> False *)
+ val c2' = Thm.implies_intr (cterm_of (theory_of_thm c2) (HOLogic.mk_Trueprop l2)) c2 (* Gamma2 |- l2 ==> False *)
- val _ = if !trace_sat then tracing ("Resulting clause: " ^ string_of_thm c_new) else ()
+ val res_thm = (* |- (lit ==> False) ==> (~lit ==> False) ==> False *)
+ let
+ val P = Var (("P", 0), HOLogic.boolT)
+ val (lit, thy) = if is_neg then (l2, theory_of_thm c2') else (l1, theory_of_thm c1')
+ val cterm = cterm_of thy
+ in
+ Thm.instantiate ([], [(cterm P, cterm lit)]) resolution_thm
+ end
+
+ val _ = if !trace_sat then
+ tracing ("Resolution theorem: " ^ string_of_thm res_thm)
+ else ()
+
+ val c_new = Thm.implies_elim (Thm.implies_elim res_thm (if is_neg then c2' else c1')) (if is_neg then c1' else c2') (* Gamma1, Gamma2 |- False *)
+
+ val _ = if !trace_sat then
+ tracing ("Resulting clause: " ^ string_of_thm c_new ^ " (hyps: " ^ space_implode ", " (map (Sign.string_of_term (theory_of_thm c_new)) (#hyps (rep_thm c_new))) ^ ")")
+ else ()
val _ = inc counter
in
c_new
@@ -248,11 +276,17 @@
(* but converted to raw clause format *)
val max_idx = valOf (Inttab.max_key clause_table)
val clause_arr = Array.array (max_idx + 1, NONE)
- val raw_clauses = map (Seq.hd o distinct_subgoals_tac o cnf.clause2raw_thm) non_triv_clauses
+ val raw_clauses = map cnf.clause2raw_thm non_triv_clauses
+ (* Every raw clause has only its literals and itself as hyp, and hyps are *)
+ (* accumulated during resolution steps. Experimental results indicate *)
+ (* that it is NOT faster to weaken all raw_clauses to contain every *)
+ (* clause in the hyps beforehand. *)
val _ = fold (fn thm => fn idx => (Array.update (clause_arr, idx, SOME thm); idx+1)) raw_clauses 0
+ (* replay the proof to derive the empty clause *)
+ val FalseThm = replay_proof clause_arr (clause_table, empty_id)
in
- (* replay the proof to derive the empty clause *)
- replay_proof clause_arr (clause_table, empty_id)
+ (* convert the hyps back to the original format *)
+ cnf.rawhyps2clausehyps_thm FalseThm
end)
| SatSolver.UNSATISFIABLE NONE =>
if !quick_and_dirty then (
--- a/src/HOL/ex/SAT_Examples.thy Fri Mar 10 16:21:49 2006 +0100
+++ b/src/HOL/ex/SAT_Examples.thy Fri Mar 10 16:31:50 2006 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/ex/SAT_Examples.thy
ID: $Id$
Author: Alwen Tiu, Tjark Weber
- Copyright 2005
+ Copyright 2005-2006
*)
header {* Examples for the 'sat' and 'satx' tactic *}
@@ -11,6 +11,7 @@
begin
ML {* set sat.trace_sat; *}
+ML {* set quick_and_dirty; *}
lemma "True"
by sat
@@ -64,10 +65,9 @@
by satx
ML {* reset sat.trace_sat; *}
+ML {* reset quick_and_dirty; *}
-(*
ML {* Toplevel.profiling := 1; *}
-*)
(* Translated from TPTP problem library: PUZ015-2.006.dimacs *)
@@ -488,8 +488,6 @@
200 201 202 203 204
by sat
-(*
ML {* Toplevel.profiling := 0; *}
-*)
end