--- a/src/HOL/HOL.thy Sat Feb 01 20:46:19 2014 +0100
+++ b/src/HOL/HOL.thy Sat Feb 01 21:09:53 2014 +0100
@@ -1690,7 +1690,8 @@
val trans = @{thm trans}
*}
-ML_file "Tools/cnf_funcs.ML"
+ML_file "Tools/cnf.ML"
+
subsection {* Code generator setup *}
--- a/src/HOL/SAT.thy Sat Feb 01 20:46:19 2014 +0100
+++ b/src/HOL/SAT.thy Sat Feb 01 21:09:53 2014 +0100
@@ -13,14 +13,12 @@
ML_file "Tools/prop_logic.ML"
ML_file "Tools/sat_solver.ML"
-ML_file "Tools/sat_funcs.ML"
+ML_file "Tools/sat.ML"
-ML {* structure sat = SATFunc(cnf) *}
-
-method_setup sat = {* Scan.succeed (SIMPLE_METHOD' o sat.sat_tac) *}
+method_setup sat = {* Scan.succeed (SIMPLE_METHOD' o SAT.sat_tac) *}
"SAT solver"
-method_setup satx = {* Scan.succeed (SIMPLE_METHOD' o sat.satx_tac) *}
+method_setup satx = {* Scan.succeed (SIMPLE_METHOD' o SAT.satx_tac) *}
"SAT solver (with definitional CNF)"
end
--- a/src/HOL/Tools/Meson/meson_clausify.ML Sat Feb 01 20:46:19 2014 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Sat Feb 01 21:09:53 2014 +0100
@@ -222,7 +222,7 @@
fun to_definitional_cnf_with_quantifiers ctxt th =
let
- val eqth = cnf.make_cnfx_thm ctxt (HOLogic.dest_Trueprop (prop_of th))
+ val eqth = CNF.make_cnfx_thm ctxt (HOLogic.dest_Trueprop (prop_of th))
val eqth = eqth RS @{thm eq_reflection}
val eqth = eqth RS @{thm TruepropI}
in Thm.equal_elim eqth th end
--- a/src/HOL/Tools/Metis/metis_tactic.ML Sat Feb 01 20:46:19 2014 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Sat Feb 01 21:09:53 2014 +0100
@@ -245,7 +245,7 @@
(if exists (Meson.has_too_many_clauses ctxt)
(Logic.prems_of_goal (prop_of st0) 1) then
Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex} ctxt) 1
- THEN cnf.cnfx_rewrite_tac ctxt 1
+ THEN CNF.cnfx_rewrite_tac ctxt 1
else
all_tac) st0
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/cnf.ML Sat Feb 01 21:09:53 2014 +0100
@@ -0,0 +1,579 @@
+(* Title: HOL/Tools/cnf.ML
+ Author: Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
+ Author: Tjark Weber, TU Muenchen
+
+FIXME: major overlaps with the code in meson.ML
+
+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)
+ False
+ True
+
+where each xij is a literal (a positive or negative atomic Boolean
+term), i.e. the formula is a conjunction of disjunctions of literals,
+or "False", or "True".
+
+A (non-empty) disjunction of literals is referred to as "clause".
+
+For the purpose of SAT proof reconstruction, we also make use of
+another representation of clauses, which we call the "raw clauses".
+Raw clauses are of the form
+
+ [..., x1', x2', ..., xn'] |- False ,
+
+where each xi is a literal, and each xi' is the negation normal form
+of ~xi.
+
+Literals are successively removed from the hyps of raw clauses by
+resolution during SAT proof reconstruction.
+*)
+
+signature CNF =
+sig
+ val is_atom: term -> bool
+ val is_literal: term -> bool
+ val is_clause: term -> bool
+ val clause_is_trivial: term -> bool
+
+ val clause2raw_thm: thm -> thm
+ val make_nnf_thm: theory -> term -> thm
+
+ val weakening_tac: int -> tactic (* removes the first hypothesis of a subgoal *)
+
+ val make_cnf_thm: Proof.context -> term -> thm
+ val make_cnfx_thm: Proof.context -> term -> thm
+ val cnf_rewrite_tac: Proof.context -> int -> tactic (* converts all prems of a subgoal to CNF *)
+ val cnfx_rewrite_tac: Proof.context -> int -> tactic
+ (* converts all prems of a subgoal to (almost) definitional CNF *)
+end;
+
+structure CNF : CNF =
+struct
+
+val clause2raw_notE = @{lemma "[| P; ~P |] ==> False" by auto};
+val clause2raw_not_disj = @{lemma "[| ~P; ~Q |] ==> ~(P | Q)" by auto};
+val clause2raw_not_not = @{lemma "P ==> ~~P" by auto};
+
+val iff_refl = @{lemma "(P::bool) = P" by auto};
+val iff_trans = @{lemma "[| (P::bool) = Q; Q = R |] ==> P = R" by auto};
+val conj_cong = @{lemma "[| P = P'; Q = Q' |] ==> (P & Q) = (P' & Q')" by auto};
+val disj_cong = @{lemma "[| P = P'; Q = Q' |] ==> (P | Q) = (P' | Q')" by auto};
+
+val make_nnf_imp = @{lemma "[| (~P) = P'; Q = Q' |] ==> (P --> Q) = (P' | Q')" by auto};
+val make_nnf_iff = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (P = Q) = ((P' | NQ) & (NP | Q'))" by auto};
+val make_nnf_not_false = @{lemma "(~False) = True" by auto};
+val make_nnf_not_true = @{lemma "(~True) = False" by auto};
+val make_nnf_not_conj = @{lemma "[| (~P) = P'; (~Q) = Q' |] ==> (~(P & Q)) = (P' | Q')" by auto};
+val make_nnf_not_disj = @{lemma "[| (~P) = P'; (~Q) = Q' |] ==> (~(P | Q)) = (P' & Q')" by auto};
+val make_nnf_not_imp = @{lemma "[| P = P'; (~Q) = Q' |] ==> (~(P --> Q)) = (P' & Q')" by auto};
+val make_nnf_not_iff = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (~(P = Q)) = ((P' | Q') & (NP | NQ))" by auto};
+val make_nnf_not_not = @{lemma "P = P' ==> (~~P) = P'" by auto};
+
+val simp_TF_conj_True_l = @{lemma "[| P = True; Q = Q' |] ==> (P & Q) = Q'" by auto};
+val simp_TF_conj_True_r = @{lemma "[| P = P'; Q = True |] ==> (P & Q) = P'" by auto};
+val simp_TF_conj_False_l = @{lemma "P = False ==> (P & Q) = False" by auto};
+val simp_TF_conj_False_r = @{lemma "Q = False ==> (P & Q) = False" by auto};
+val simp_TF_disj_True_l = @{lemma "P = True ==> (P | Q) = True" by auto};
+val simp_TF_disj_True_r = @{lemma "Q = True ==> (P | Q) = True" by auto};
+val simp_TF_disj_False_l = @{lemma "[| P = False; Q = Q' |] ==> (P | Q) = Q'" by auto};
+val simp_TF_disj_False_r = @{lemma "[| P = P'; Q = False |] ==> (P | Q) = P'" by auto};
+
+val make_cnf_disj_conj_l = @{lemma "[| (P | R) = PR; (Q | R) = QR |] ==> ((P & Q) | R) = (PR & QR)" by auto};
+val make_cnf_disj_conj_r = @{lemma "[| (P | Q) = PQ; (P | R) = PR |] ==> (P | (Q & R)) = (PQ & PR)" by auto};
+
+val make_cnfx_disj_ex_l = @{lemma "((EX (x::bool). P x) | Q) = (EX x. P x | Q)" by auto};
+val make_cnfx_disj_ex_r = @{lemma "(P | (EX (x::bool). Q x)) = (EX x. P | Q x)" by auto};
+val make_cnfx_newlit = @{lemma "(P | Q) = (EX x. (P | x) & (Q | ~x))" by auto};
+val make_cnfx_ex_cong = @{lemma "(ALL (x::bool). P x = Q x) ==> (EX x. P x) = (EX x. Q x)" by auto};
+
+val weakening_thm = @{lemma "[| P; Q |] ==> Q" by auto};
+
+val cnftac_eq_imp = @{lemma "[| P = Q; P |] ==> Q" by auto};
+
+fun is_atom (Const (@{const_name False}, _)) = false
+ | is_atom (Const (@{const_name True}, _)) = false
+ | is_atom (Const (@{const_name HOL.conj}, _) $ _ $ _) = false
+ | is_atom (Const (@{const_name HOL.disj}, _) $ _ $ _) = false
+ | is_atom (Const (@{const_name HOL.implies}, _) $ _ $ _) = false
+ | is_atom (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ _ $ _) = false
+ | is_atom (Const (@{const_name Not}, _) $ _) = false
+ | is_atom _ = true;
+
+fun is_literal (Const (@{const_name Not}, _) $ x) = is_atom x
+ | is_literal x = is_atom x;
+
+fun is_clause (Const (@{const_name HOL.disj}, _) $ x $ y) = is_clause x andalso is_clause y
+ | is_clause x = is_literal x;
+
+(* ------------------------------------------------------------------------- *)
+(* clause_is_trivial: a clause is trivially true if it contains both an atom *)
+(* and the atom's negation *)
+(* ------------------------------------------------------------------------- *)
+
+fun clause_is_trivial c =
+ let
+ fun dual (Const (@{const_name Not}, _) $ x) = x
+ | dual x = HOLogic.Not $ x
+ fun has_duals [] = false
+ | has_duals (x::xs) = member (op =) xs (dual x) orelse has_duals xs
+ in
+ has_duals (HOLogic.disjuncts c)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* clause2raw_thm: translates a clause into a raw clause, i.e. *)
+(* [...] |- x1 | ... | xn *)
+(* (where each xi is a literal) is translated to *)
+(* [..., x1', ..., xn'] |- False , *)
+(* where each xi' is the negation normal form of ~xi *)
+(* ------------------------------------------------------------------------- *)
+
+fun clause2raw_thm clause =
+ let
+ (* eliminates negated disjunctions from the i-th premise, possibly *)
+ (* adding new premises, then continues with the (i+1)-th premise *)
+ (* int -> Thm.thm -> Thm.thm *)
+ fun not_disj_to_prem i thm =
+ if i > nprems_of thm then
+ thm
+ else
+ not_disj_to_prem (i+1) (Seq.hd (REPEAT_DETERM (rtac clause2raw_not_disj i) thm))
+ (* moves all premises to hyps, i.e. "[...] |- A1 ==> ... ==> An ==> B" *)
+ (* becomes "[..., A1, ..., An] |- B" *)
+ (* Thm.thm -> Thm.thm *)
+ fun prems_to_hyps thm =
+ fold (fn cprem => fn thm' =>
+ Thm.implies_elim thm' (Thm.assume cprem)) (cprems_of thm) thm
+ in
+ (* [...] |- ~(x1 | ... | xn) ==> False *)
+ (clause2raw_notE OF [clause])
+ (* [...] |- ~x1 ==> ... ==> ~xn ==> False *)
+ |> not_disj_to_prem 1
+ (* [...] |- x1' ==> ... ==> xn' ==> False *)
+ |> Seq.hd o TRYALL (rtac clause2raw_not_not)
+ (* [..., x1', ..., xn'] |- False *)
+ |> prems_to_hyps
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* inst_thm: instantiates a theorem with a list of terms *)
+(* ------------------------------------------------------------------------- *)
+
+fun inst_thm thy ts thm =
+ instantiate' [] (map (SOME o cterm_of thy) ts) thm;
+
+(* ------------------------------------------------------------------------- *)
+(* Naive CNF transformation *)
+(* ------------------------------------------------------------------------- *)
+
+(* ------------------------------------------------------------------------- *)
+(* make_nnf_thm: produces a theorem of the form t = t', where t' is the *)
+(* negation normal form (i.e. negation only occurs in front of atoms) *)
+(* of t; implications ("-->") and equivalences ("=" on bool) are *)
+(* eliminated (possibly causing an exponential blowup) *)
+(* ------------------------------------------------------------------------- *)
+
+fun make_nnf_thm thy (Const (@{const_name HOL.conj}, _) $ x $ y) =
+ let
+ val thm1 = make_nnf_thm thy x
+ val thm2 = make_nnf_thm thy y
+ in
+ conj_cong OF [thm1, thm2]
+ end
+ | make_nnf_thm thy (Const (@{const_name HOL.disj}, _) $ x $ y) =
+ let
+ val thm1 = make_nnf_thm thy x
+ val thm2 = make_nnf_thm thy y
+ in
+ disj_cong OF [thm1, thm2]
+ end
+ | make_nnf_thm thy (Const (@{const_name HOL.implies}, _) $ x $ y) =
+ let
+ val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
+ val thm2 = make_nnf_thm thy y
+ in
+ make_nnf_imp OF [thm1, thm2]
+ end
+ | make_nnf_thm thy (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y) =
+ let
+ val thm1 = make_nnf_thm thy x
+ val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
+ val thm3 = make_nnf_thm thy y
+ val thm4 = make_nnf_thm thy (HOLogic.Not $ y)
+ in
+ make_nnf_iff OF [thm1, thm2, thm3, thm4]
+ end
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name False}, _)) =
+ make_nnf_not_false
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name True}, _)) =
+ make_nnf_not_true
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.conj}, _) $ x $ y)) =
+ let
+ val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
+ val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
+ in
+ make_nnf_not_conj OF [thm1, thm2]
+ end
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.disj}, _) $ x $ y)) =
+ let
+ val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
+ val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
+ in
+ make_nnf_not_disj OF [thm1, thm2]
+ end
+ | make_nnf_thm thy
+ (Const (@{const_name Not}, _) $
+ (Const (@{const_name HOL.implies}, _) $ x $ y)) =
+ let
+ val thm1 = make_nnf_thm thy x
+ val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
+ in
+ make_nnf_not_imp OF [thm1, thm2]
+ end
+ | make_nnf_thm thy
+ (Const (@{const_name Not}, _) $
+ (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
+ let
+ val thm1 = make_nnf_thm thy x
+ val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
+ val thm3 = make_nnf_thm thy y
+ val thm4 = make_nnf_thm thy (HOLogic.Not $ y)
+ in
+ make_nnf_not_iff OF [thm1, thm2, thm3, thm4]
+ end
+ | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name Not}, _) $ x)) =
+ let
+ val thm1 = make_nnf_thm thy x
+ in
+ make_nnf_not_not OF [thm1]
+ end
+ | make_nnf_thm thy t = inst_thm thy [t] iff_refl;
+
+val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq}
+val eq_reflection = @{thm eq_reflection}
+
+fun make_under_quantifiers ctxt make t =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ fun conv ctxt ct =
+ case term_of ct of
+ Const _ $ Abs _ => Conv.comb_conv (conv ctxt) ct
+ | Abs _ => Conv.abs_conv (conv o snd) ctxt ct
+ | Const _ => Conv.all_conv ct
+ | t => make t RS eq_reflection
+ in conv ctxt (cterm_of thy t) RS meta_eq_to_obj_eq end
+
+fun make_nnf_thm_under_quantifiers ctxt =
+ make_under_quantifiers ctxt (make_nnf_thm (Proof_Context.theory_of ctxt))
+
+(* ------------------------------------------------------------------------- *)
+(* simp_True_False_thm: produces a theorem t = t', where t' is equivalent to *)
+(* t, but simplified wrt. the following theorems: *)
+(* (True & x) = x *)
+(* (x & True) = x *)
+(* (False & x) = False *)
+(* (x & False) = False *)
+(* (True | x) = True *)
+(* (x | True) = True *)
+(* (False | x) = x *)
+(* (x | False) = x *)
+(* No simplification is performed below connectives other than & and |. *)
+(* Optimization: The right-hand side of a conjunction (disjunction) is *)
+(* simplified only if the left-hand side does not simplify to False *)
+(* (True, respectively). *)
+(* ------------------------------------------------------------------------- *)
+
+(* Theory.theory -> Term.term -> Thm.thm *)
+
+fun simp_True_False_thm thy (Const (@{const_name HOL.conj}, _) $ x $ y) =
+ let
+ val thm1 = simp_True_False_thm thy x
+ val x'= (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
+ in
+ if x' = @{term False} then
+ simp_TF_conj_False_l OF [thm1] (* (x & y) = False *)
+ else
+ let
+ val thm2 = simp_True_False_thm thy y
+ val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
+ in
+ if x' = @{term True} then
+ simp_TF_conj_True_l OF [thm1, thm2] (* (x & y) = y' *)
+ else if y' = @{term False} then
+ simp_TF_conj_False_r OF [thm2] (* (x & y) = False *)
+ else if y' = @{term True} then
+ simp_TF_conj_True_r OF [thm1, thm2] (* (x & y) = x' *)
+ else
+ conj_cong OF [thm1, thm2] (* (x & y) = (x' & y') *)
+ end
+ end
+ | simp_True_False_thm thy (Const (@{const_name HOL.disj}, _) $ x $ y) =
+ let
+ val thm1 = simp_True_False_thm thy x
+ val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
+ in
+ if x' = @{term True} then
+ simp_TF_disj_True_l OF [thm1] (* (x | y) = True *)
+ else
+ let
+ val thm2 = simp_True_False_thm thy y
+ val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
+ in
+ if x' = @{term False} then
+ simp_TF_disj_False_l OF [thm1, thm2] (* (x | y) = y' *)
+ else if y' = @{term True} then
+ simp_TF_disj_True_r OF [thm2] (* (x | y) = True *)
+ else if y' = @{term False} then
+ simp_TF_disj_False_r OF [thm1, thm2] (* (x | y) = x' *)
+ else
+ disj_cong OF [thm1, thm2] (* (x | y) = (x' | y') *)
+ end
+ end
+ | simp_True_False_thm thy t = inst_thm thy [t] iff_refl; (* t = t *)
+
+(* ------------------------------------------------------------------------- *)
+(* make_cnf_thm: given any HOL term 't', produces a theorem t = t', where t' *)
+(* is in conjunction normal form. May cause an exponential blowup *)
+(* in the length of the term. *)
+(* ------------------------------------------------------------------------- *)
+
+fun make_cnf_thm ctxt t =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ fun make_cnf_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) =
+ let
+ val thm1 = make_cnf_thm_from_nnf x
+ val thm2 = make_cnf_thm_from_nnf y
+ in
+ conj_cong OF [thm1, thm2]
+ end
+ | make_cnf_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) =
+ let
+ (* produces a theorem "(x' | y') = t'", where x', y', and t' are in CNF *)
+ fun make_cnf_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' =
+ let
+ val thm1 = make_cnf_disj_thm x1 y'
+ val thm2 = make_cnf_disj_thm x2 y'
+ in
+ make_cnf_disj_conj_l OF [thm1, thm2] (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
+ end
+ | make_cnf_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) =
+ let
+ val thm1 = make_cnf_disj_thm x' y1
+ val thm2 = make_cnf_disj_thm x' y2
+ in
+ make_cnf_disj_conj_r OF [thm1, thm2] (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
+ end
+ | make_cnf_disj_thm x' y' =
+ inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl (* (x' | y') = (x' | y') *)
+ val thm1 = make_cnf_thm_from_nnf x
+ val thm2 = make_cnf_thm_from_nnf y
+ val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
+ val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
+ val disj_thm = disj_cong OF [thm1, thm2] (* (x | y) = (x' | y') *)
+ in
+ iff_trans OF [disj_thm, make_cnf_disj_thm x' y']
+ end
+ | make_cnf_thm_from_nnf t = inst_thm thy [t] iff_refl
+ (* convert 't' to NNF first *)
+ val nnf_thm = make_nnf_thm_under_quantifiers ctxt t
+(*###
+ val nnf_thm = make_nnf_thm thy t
+*)
+ val nnf = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm
+ (* then simplify wrt. True/False (this should preserve NNF) *)
+ val simp_thm = simp_True_False_thm thy nnf
+ val simp = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm
+ (* finally, convert to CNF (this should preserve the simplification) *)
+ val cnf_thm = make_under_quantifiers ctxt make_cnf_thm_from_nnf simp
+(* ###
+ val cnf_thm = make_cnf_thm_from_nnf simp
+*)
+ in
+ iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnf_thm]
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* CNF transformation by introducing new literals *)
+(* ------------------------------------------------------------------------- *)
+
+(* ------------------------------------------------------------------------- *)
+(* make_cnfx_thm: given any HOL term 't', produces a theorem t = t', where *)
+(* t' is almost in conjunction normal form, except that conjunctions *)
+(* and existential quantifiers may be nested. (Use e.g. 'REPEAT_DETERM *)
+(* (etac exE i ORELSE etac conjE i)' afterwards to normalize.) May *)
+(* introduce new (existentially bound) literals. Note: the current *)
+(* implementation calls 'make_nnf_thm', causing an exponential blowup *)
+(* in the case of nested equivalences. *)
+(* ------------------------------------------------------------------------- *)
+
+fun make_cnfx_thm ctxt t =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val var_id = Unsynchronized.ref 0 (* properly initialized below *)
+ fun new_free () =
+ Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT)
+ fun make_cnfx_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) : thm =
+ let
+ val thm1 = make_cnfx_thm_from_nnf x
+ val thm2 = make_cnfx_thm_from_nnf y
+ in
+ conj_cong OF [thm1, thm2]
+ end
+ | make_cnfx_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) =
+ if is_clause x andalso is_clause y then
+ inst_thm thy [HOLogic.mk_disj (x, y)] iff_refl
+ else if is_literal y orelse is_literal x then
+ let
+ (* produces a theorem "(x' | y') = t'", where x', y', and t' are *)
+ (* almost in CNF, and x' or y' is a literal *)
+ fun make_cnfx_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' =
+ let
+ val thm1 = make_cnfx_disj_thm x1 y'
+ val thm2 = make_cnfx_disj_thm x2 y'
+ in
+ make_cnf_disj_conj_l OF [thm1, thm2] (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
+ end
+ | make_cnfx_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) =
+ let
+ val thm1 = make_cnfx_disj_thm x' y1
+ val thm2 = make_cnfx_disj_thm x' y2
+ in
+ make_cnf_disj_conj_r OF [thm1, thm2] (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
+ end
+ | make_cnfx_disj_thm (@{term "Ex::(bool => bool) => bool"} $ x') y' =
+ let
+ val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l (* ((Ex x') | y') = (Ex (x' | y')) *)
+ val var = new_free ()
+ val thm2 = make_cnfx_disj_thm (betapply (x', var)) y' (* (x' | y') = body' *)
+ val thm3 = Thm.forall_intr (cterm_of thy var) thm2 (* !!v. (x' | y') = body' *)
+ val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *)
+ val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
+ in
+ iff_trans OF [thm1, thm5] (* ((Ex x') | y') = (Ex v. body') *)
+ end
+ | make_cnfx_disj_thm x' (@{term "Ex::(bool => bool) => bool"} $ y') =
+ let
+ val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r (* (x' | (Ex y')) = (Ex (x' | y')) *)
+ val var = new_free ()
+ val thm2 = make_cnfx_disj_thm x' (betapply (y', var)) (* (x' | y') = body' *)
+ val thm3 = Thm.forall_intr (cterm_of thy var) thm2 (* !!v. (x' | y') = body' *)
+ val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *)
+ val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
+ in
+ iff_trans OF [thm1, thm5] (* (x' | (Ex y')) = (EX v. body') *)
+ end
+ | make_cnfx_disj_thm x' y' =
+ inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl (* (x' | y') = (x' | y') *)
+ val thm1 = make_cnfx_thm_from_nnf x
+ val thm2 = make_cnfx_thm_from_nnf y
+ val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
+ val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
+ val disj_thm = disj_cong OF [thm1, thm2] (* (x | y) = (x' | y') *)
+ in
+ iff_trans OF [disj_thm, make_cnfx_disj_thm x' y']
+ end
+ else
+ let (* neither 'x' nor 'y' is a literal: introduce a fresh variable *)
+ val thm1 = inst_thm thy [x, y] make_cnfx_newlit (* (x | y) = EX v. (x | v) & (y | ~v) *)
+ val var = new_free ()
+ val body = HOLogic.mk_conj (HOLogic.mk_disj (x, var), HOLogic.mk_disj (y, HOLogic.Not $ var))
+ val thm2 = make_cnfx_thm_from_nnf body (* (x | v) & (y | ~v) = body' *)
+ val thm3 = Thm.forall_intr (cterm_of thy var) thm2 (* !!v. (x | v) & (y | ~v) = body' *)
+ val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x | v) & (y | ~v) = body' *)
+ val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *)
+ in
+ iff_trans OF [thm1, thm5]
+ end
+ | make_cnfx_thm_from_nnf t = inst_thm thy [t] iff_refl
+ (* convert 't' to NNF first *)
+ val nnf_thm = make_nnf_thm_under_quantifiers ctxt t
+(* ###
+ val nnf_thm = make_nnf_thm thy t
+*)
+ val nnf = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm
+ (* then simplify wrt. True/False (this should preserve NNF) *)
+ val simp_thm = simp_True_False_thm thy nnf
+ val simp = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm
+ (* initialize var_id, in case the term already contains variables of the form "cnfx_<int>" *)
+ val _ = (var_id := fold (fn free => fn max =>
+ let
+ val (name, _) = dest_Free free
+ val idx =
+ if String.isPrefix "cnfx_" name then
+ (Int.fromString o String.extract) (name, String.size "cnfx_", NONE)
+ else
+ NONE
+ in
+ Int.max (max, the_default 0 idx)
+ end) (Misc_Legacy.term_frees simp) 0)
+ (* finally, convert to definitional CNF (this should preserve the simplification) *)
+ val cnfx_thm = make_under_quantifiers ctxt make_cnfx_thm_from_nnf simp
+(*###
+ val cnfx_thm = make_cnfx_thm_from_nnf simp
+*)
+ in
+ iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnfx_thm]
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Tactics *)
+(* ------------------------------------------------------------------------- *)
+
+(* ------------------------------------------------------------------------- *)
+(* weakening_tac: removes the first hypothesis of the 'i'-th subgoal *)
+(* ------------------------------------------------------------------------- *)
+
+fun weakening_tac i =
+ dtac weakening_thm i THEN atac (i+1);
+
+(* ------------------------------------------------------------------------- *)
+(* cnf_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF *)
+(* (possibly causing an exponential blowup in the length of each *)
+(* premise) *)
+(* ------------------------------------------------------------------------- *)
+
+fun cnf_rewrite_tac ctxt i =
+ (* cut the CNF formulas as new premises *)
+ Subgoal.FOCUS (fn {prems, ...} =>
+ let
+ val cnf_thms = map (make_cnf_thm ctxt o HOLogic.dest_Trueprop o Thm.prop_of) prems
+ val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems)
+ in
+ cut_facts_tac cut_thms 1
+ end) ctxt i
+ (* remove the original premises *)
+ THEN SELECT_GOAL (fn thm =>
+ let
+ val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm)
+ in
+ PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
+ end) i;
+
+(* ------------------------------------------------------------------------- *)
+(* cnfx_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF *)
+(* (possibly introducing new literals) *)
+(* ------------------------------------------------------------------------- *)
+
+fun cnfx_rewrite_tac ctxt i =
+ (* cut the CNF formulas as new premises *)
+ Subgoal.FOCUS (fn {prems, ...} =>
+ let
+ val cnfx_thms = map (make_cnfx_thm ctxt o HOLogic.dest_Trueprop o prop_of) prems
+ val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems)
+ in
+ cut_facts_tac cut_thms 1
+ end) ctxt i
+ (* remove the original premises *)
+ THEN SELECT_GOAL (fn thm =>
+ let
+ val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm)
+ in
+ PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
+ end) i;
+
+end;
--- a/src/HOL/Tools/cnf_funcs.ML Sat Feb 01 20:46:19 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,579 +0,0 @@
-(* Title: HOL/Tools/cnf_funcs.ML
- Author: Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
- Author: Tjark Weber, TU Muenchen
-
-FIXME: major overlaps with the code in meson.ML
-
-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)
- False
- True
-
-where each xij is a literal (a positive or negative atomic Boolean
-term), i.e. the formula is a conjunction of disjunctions of literals,
-or "False", or "True".
-
-A (non-empty) disjunction of literals is referred to as "clause".
-
-For the purpose of SAT proof reconstruction, we also make use of
-another representation of clauses, which we call the "raw clauses".
-Raw clauses are of the form
-
- [..., x1', x2', ..., xn'] |- False ,
-
-where each xi is a literal, and each xi' is the negation normal form
-of ~xi.
-
-Literals are successively removed from the hyps of raw clauses by
-resolution during SAT proof reconstruction.
-*)
-
-signature CNF =
-sig
- val is_atom: term -> bool
- val is_literal: term -> bool
- val is_clause: term -> bool
- val clause_is_trivial: term -> bool
-
- val clause2raw_thm: thm -> thm
- val make_nnf_thm: theory -> term -> thm
-
- val weakening_tac: int -> tactic (* removes the first hypothesis of a subgoal *)
-
- val make_cnf_thm: Proof.context -> term -> thm
- val make_cnfx_thm: Proof.context -> term -> thm
- val cnf_rewrite_tac: Proof.context -> int -> tactic (* converts all prems of a subgoal to CNF *)
- val cnfx_rewrite_tac: Proof.context -> int -> tactic
- (* converts all prems of a subgoal to (almost) definitional CNF *)
-end;
-
-structure cnf : CNF =
-struct
-
-val clause2raw_notE = @{lemma "[| P; ~P |] ==> False" by auto};
-val clause2raw_not_disj = @{lemma "[| ~P; ~Q |] ==> ~(P | Q)" by auto};
-val clause2raw_not_not = @{lemma "P ==> ~~P" by auto};
-
-val iff_refl = @{lemma "(P::bool) = P" by auto};
-val iff_trans = @{lemma "[| (P::bool) = Q; Q = R |] ==> P = R" by auto};
-val conj_cong = @{lemma "[| P = P'; Q = Q' |] ==> (P & Q) = (P' & Q')" by auto};
-val disj_cong = @{lemma "[| P = P'; Q = Q' |] ==> (P | Q) = (P' | Q')" by auto};
-
-val make_nnf_imp = @{lemma "[| (~P) = P'; Q = Q' |] ==> (P --> Q) = (P' | Q')" by auto};
-val make_nnf_iff = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (P = Q) = ((P' | NQ) & (NP | Q'))" by auto};
-val make_nnf_not_false = @{lemma "(~False) = True" by auto};
-val make_nnf_not_true = @{lemma "(~True) = False" by auto};
-val make_nnf_not_conj = @{lemma "[| (~P) = P'; (~Q) = Q' |] ==> (~(P & Q)) = (P' | Q')" by auto};
-val make_nnf_not_disj = @{lemma "[| (~P) = P'; (~Q) = Q' |] ==> (~(P | Q)) = (P' & Q')" by auto};
-val make_nnf_not_imp = @{lemma "[| P = P'; (~Q) = Q' |] ==> (~(P --> Q)) = (P' & Q')" by auto};
-val make_nnf_not_iff = @{lemma "[| P = P'; (~P) = NP; Q = Q'; (~Q) = NQ |] ==> (~(P = Q)) = ((P' | Q') & (NP | NQ))" by auto};
-val make_nnf_not_not = @{lemma "P = P' ==> (~~P) = P'" by auto};
-
-val simp_TF_conj_True_l = @{lemma "[| P = True; Q = Q' |] ==> (P & Q) = Q'" by auto};
-val simp_TF_conj_True_r = @{lemma "[| P = P'; Q = True |] ==> (P & Q) = P'" by auto};
-val simp_TF_conj_False_l = @{lemma "P = False ==> (P & Q) = False" by auto};
-val simp_TF_conj_False_r = @{lemma "Q = False ==> (P & Q) = False" by auto};
-val simp_TF_disj_True_l = @{lemma "P = True ==> (P | Q) = True" by auto};
-val simp_TF_disj_True_r = @{lemma "Q = True ==> (P | Q) = True" by auto};
-val simp_TF_disj_False_l = @{lemma "[| P = False; Q = Q' |] ==> (P | Q) = Q'" by auto};
-val simp_TF_disj_False_r = @{lemma "[| P = P'; Q = False |] ==> (P | Q) = P'" by auto};
-
-val make_cnf_disj_conj_l = @{lemma "[| (P | R) = PR; (Q | R) = QR |] ==> ((P & Q) | R) = (PR & QR)" by auto};
-val make_cnf_disj_conj_r = @{lemma "[| (P | Q) = PQ; (P | R) = PR |] ==> (P | (Q & R)) = (PQ & PR)" by auto};
-
-val make_cnfx_disj_ex_l = @{lemma "((EX (x::bool). P x) | Q) = (EX x. P x | Q)" by auto};
-val make_cnfx_disj_ex_r = @{lemma "(P | (EX (x::bool). Q x)) = (EX x. P | Q x)" by auto};
-val make_cnfx_newlit = @{lemma "(P | Q) = (EX x. (P | x) & (Q | ~x))" by auto};
-val make_cnfx_ex_cong = @{lemma "(ALL (x::bool). P x = Q x) ==> (EX x. P x) = (EX x. Q x)" by auto};
-
-val weakening_thm = @{lemma "[| P; Q |] ==> Q" by auto};
-
-val cnftac_eq_imp = @{lemma "[| P = Q; P |] ==> Q" by auto};
-
-fun is_atom (Const (@{const_name False}, _)) = false
- | is_atom (Const (@{const_name True}, _)) = false
- | is_atom (Const (@{const_name HOL.conj}, _) $ _ $ _) = false
- | is_atom (Const (@{const_name HOL.disj}, _) $ _ $ _) = false
- | is_atom (Const (@{const_name HOL.implies}, _) $ _ $ _) = false
- | is_atom (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ _ $ _) = false
- | is_atom (Const (@{const_name Not}, _) $ _) = false
- | is_atom _ = true;
-
-fun is_literal (Const (@{const_name Not}, _) $ x) = is_atom x
- | is_literal x = is_atom x;
-
-fun is_clause (Const (@{const_name HOL.disj}, _) $ x $ y) = is_clause x andalso is_clause y
- | is_clause x = is_literal x;
-
-(* ------------------------------------------------------------------------- *)
-(* clause_is_trivial: a clause is trivially true if it contains both an atom *)
-(* and the atom's negation *)
-(* ------------------------------------------------------------------------- *)
-
-fun clause_is_trivial c =
- let
- fun dual (Const (@{const_name Not}, _) $ x) = x
- | dual x = HOLogic.Not $ x
- fun has_duals [] = false
- | has_duals (x::xs) = member (op =) xs (dual x) orelse has_duals xs
- in
- has_duals (HOLogic.disjuncts c)
- end;
-
-(* ------------------------------------------------------------------------- *)
-(* clause2raw_thm: translates a clause into a raw clause, i.e. *)
-(* [...] |- x1 | ... | xn *)
-(* (where each xi is a literal) is translated to *)
-(* [..., x1', ..., xn'] |- False , *)
-(* where each xi' is the negation normal form of ~xi *)
-(* ------------------------------------------------------------------------- *)
-
-fun clause2raw_thm clause =
- let
- (* eliminates negated disjunctions from the i-th premise, possibly *)
- (* adding new premises, then continues with the (i+1)-th premise *)
- (* int -> Thm.thm -> Thm.thm *)
- fun not_disj_to_prem i thm =
- if i > nprems_of thm then
- thm
- else
- not_disj_to_prem (i+1) (Seq.hd (REPEAT_DETERM (rtac clause2raw_not_disj i) thm))
- (* moves all premises to hyps, i.e. "[...] |- A1 ==> ... ==> An ==> B" *)
- (* becomes "[..., A1, ..., An] |- B" *)
- (* Thm.thm -> Thm.thm *)
- fun prems_to_hyps thm =
- fold (fn cprem => fn thm' =>
- Thm.implies_elim thm' (Thm.assume cprem)) (cprems_of thm) thm
- in
- (* [...] |- ~(x1 | ... | xn) ==> False *)
- (clause2raw_notE OF [clause])
- (* [...] |- ~x1 ==> ... ==> ~xn ==> False *)
- |> not_disj_to_prem 1
- (* [...] |- x1' ==> ... ==> xn' ==> False *)
- |> Seq.hd o TRYALL (rtac clause2raw_not_not)
- (* [..., x1', ..., xn'] |- False *)
- |> prems_to_hyps
- end;
-
-(* ------------------------------------------------------------------------- *)
-(* inst_thm: instantiates a theorem with a list of terms *)
-(* ------------------------------------------------------------------------- *)
-
-fun inst_thm thy ts thm =
- instantiate' [] (map (SOME o cterm_of thy) ts) thm;
-
-(* ------------------------------------------------------------------------- *)
-(* Naive CNF transformation *)
-(* ------------------------------------------------------------------------- *)
-
-(* ------------------------------------------------------------------------- *)
-(* make_nnf_thm: produces a theorem of the form t = t', where t' is the *)
-(* negation normal form (i.e. negation only occurs in front of atoms) *)
-(* of t; implications ("-->") and equivalences ("=" on bool) are *)
-(* eliminated (possibly causing an exponential blowup) *)
-(* ------------------------------------------------------------------------- *)
-
-fun make_nnf_thm thy (Const (@{const_name HOL.conj}, _) $ x $ y) =
- let
- val thm1 = make_nnf_thm thy x
- val thm2 = make_nnf_thm thy y
- in
- conj_cong OF [thm1, thm2]
- end
- | make_nnf_thm thy (Const (@{const_name HOL.disj}, _) $ x $ y) =
- let
- val thm1 = make_nnf_thm thy x
- val thm2 = make_nnf_thm thy y
- in
- disj_cong OF [thm1, thm2]
- end
- | make_nnf_thm thy (Const (@{const_name HOL.implies}, _) $ x $ y) =
- let
- val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
- val thm2 = make_nnf_thm thy y
- in
- make_nnf_imp OF [thm1, thm2]
- end
- | make_nnf_thm thy (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y) =
- let
- val thm1 = make_nnf_thm thy x
- val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
- val thm3 = make_nnf_thm thy y
- val thm4 = make_nnf_thm thy (HOLogic.Not $ y)
- in
- make_nnf_iff OF [thm1, thm2, thm3, thm4]
- end
- | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name False}, _)) =
- make_nnf_not_false
- | make_nnf_thm thy (Const (@{const_name Not}, _) $ Const (@{const_name True}, _)) =
- make_nnf_not_true
- | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.conj}, _) $ x $ y)) =
- let
- val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
- val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
- in
- make_nnf_not_conj OF [thm1, thm2]
- end
- | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.disj}, _) $ x $ y)) =
- let
- val thm1 = make_nnf_thm thy (HOLogic.Not $ x)
- val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
- in
- make_nnf_not_disj OF [thm1, thm2]
- end
- | make_nnf_thm thy
- (Const (@{const_name Not}, _) $
- (Const (@{const_name HOL.implies}, _) $ x $ y)) =
- let
- val thm1 = make_nnf_thm thy x
- val thm2 = make_nnf_thm thy (HOLogic.Not $ y)
- in
- make_nnf_not_imp OF [thm1, thm2]
- end
- | make_nnf_thm thy
- (Const (@{const_name Not}, _) $
- (Const (@{const_name HOL.eq}, Type ("fun", @{typ bool} :: _)) $ x $ y)) =
- let
- val thm1 = make_nnf_thm thy x
- val thm2 = make_nnf_thm thy (HOLogic.Not $ x)
- val thm3 = make_nnf_thm thy y
- val thm4 = make_nnf_thm thy (HOLogic.Not $ y)
- in
- make_nnf_not_iff OF [thm1, thm2, thm3, thm4]
- end
- | make_nnf_thm thy (Const (@{const_name Not}, _) $ (Const (@{const_name Not}, _) $ x)) =
- let
- val thm1 = make_nnf_thm thy x
- in
- make_nnf_not_not OF [thm1]
- end
- | make_nnf_thm thy t = inst_thm thy [t] iff_refl;
-
-val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq}
-val eq_reflection = @{thm eq_reflection}
-
-fun make_under_quantifiers ctxt make t =
- let
- val thy = Proof_Context.theory_of ctxt
- fun conv ctxt ct =
- case term_of ct of
- Const _ $ Abs _ => Conv.comb_conv (conv ctxt) ct
- | Abs _ => Conv.abs_conv (conv o snd) ctxt ct
- | Const _ => Conv.all_conv ct
- | t => make t RS eq_reflection
- in conv ctxt (cterm_of thy t) RS meta_eq_to_obj_eq end
-
-fun make_nnf_thm_under_quantifiers ctxt =
- make_under_quantifiers ctxt (make_nnf_thm (Proof_Context.theory_of ctxt))
-
-(* ------------------------------------------------------------------------- *)
-(* simp_True_False_thm: produces a theorem t = t', where t' is equivalent to *)
-(* t, but simplified wrt. the following theorems: *)
-(* (True & x) = x *)
-(* (x & True) = x *)
-(* (False & x) = False *)
-(* (x & False) = False *)
-(* (True | x) = True *)
-(* (x | True) = True *)
-(* (False | x) = x *)
-(* (x | False) = x *)
-(* No simplification is performed below connectives other than & and |. *)
-(* Optimization: The right-hand side of a conjunction (disjunction) is *)
-(* simplified only if the left-hand side does not simplify to False *)
-(* (True, respectively). *)
-(* ------------------------------------------------------------------------- *)
-
-(* Theory.theory -> Term.term -> Thm.thm *)
-
-fun simp_True_False_thm thy (Const (@{const_name HOL.conj}, _) $ x $ y) =
- let
- val thm1 = simp_True_False_thm thy x
- val x'= (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
- in
- if x' = @{term False} then
- simp_TF_conj_False_l OF [thm1] (* (x & y) = False *)
- else
- let
- val thm2 = simp_True_False_thm thy y
- val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
- in
- if x' = @{term True} then
- simp_TF_conj_True_l OF [thm1, thm2] (* (x & y) = y' *)
- else if y' = @{term False} then
- simp_TF_conj_False_r OF [thm2] (* (x & y) = False *)
- else if y' = @{term True} then
- simp_TF_conj_True_r OF [thm1, thm2] (* (x & y) = x' *)
- else
- conj_cong OF [thm1, thm2] (* (x & y) = (x' & y') *)
- end
- end
- | simp_True_False_thm thy (Const (@{const_name HOL.disj}, _) $ x $ y) =
- let
- val thm1 = simp_True_False_thm thy x
- val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
- in
- if x' = @{term True} then
- simp_TF_disj_True_l OF [thm1] (* (x | y) = True *)
- else
- let
- val thm2 = simp_True_False_thm thy y
- val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
- in
- if x' = @{term False} then
- simp_TF_disj_False_l OF [thm1, thm2] (* (x | y) = y' *)
- else if y' = @{term True} then
- simp_TF_disj_True_r OF [thm2] (* (x | y) = True *)
- else if y' = @{term False} then
- simp_TF_disj_False_r OF [thm1, thm2] (* (x | y) = x' *)
- else
- disj_cong OF [thm1, thm2] (* (x | y) = (x' | y') *)
- end
- end
- | simp_True_False_thm thy t = inst_thm thy [t] iff_refl; (* t = t *)
-
-(* ------------------------------------------------------------------------- *)
-(* make_cnf_thm: given any HOL term 't', produces a theorem t = t', where t' *)
-(* is in conjunction normal form. May cause an exponential blowup *)
-(* in the length of the term. *)
-(* ------------------------------------------------------------------------- *)
-
-fun make_cnf_thm ctxt t =
- let
- val thy = Proof_Context.theory_of ctxt
- fun make_cnf_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) =
- let
- val thm1 = make_cnf_thm_from_nnf x
- val thm2 = make_cnf_thm_from_nnf y
- in
- conj_cong OF [thm1, thm2]
- end
- | make_cnf_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) =
- let
- (* produces a theorem "(x' | y') = t'", where x', y', and t' are in CNF *)
- fun make_cnf_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' =
- let
- val thm1 = make_cnf_disj_thm x1 y'
- val thm2 = make_cnf_disj_thm x2 y'
- in
- make_cnf_disj_conj_l OF [thm1, thm2] (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
- end
- | make_cnf_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) =
- let
- val thm1 = make_cnf_disj_thm x' y1
- val thm2 = make_cnf_disj_thm x' y2
- in
- make_cnf_disj_conj_r OF [thm1, thm2] (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
- end
- | make_cnf_disj_thm x' y' =
- inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl (* (x' | y') = (x' | y') *)
- val thm1 = make_cnf_thm_from_nnf x
- val thm2 = make_cnf_thm_from_nnf y
- val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
- val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
- val disj_thm = disj_cong OF [thm1, thm2] (* (x | y) = (x' | y') *)
- in
- iff_trans OF [disj_thm, make_cnf_disj_thm x' y']
- end
- | make_cnf_thm_from_nnf t = inst_thm thy [t] iff_refl
- (* convert 't' to NNF first *)
- val nnf_thm = make_nnf_thm_under_quantifiers ctxt t
-(*###
- val nnf_thm = make_nnf_thm thy t
-*)
- val nnf = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm
- (* then simplify wrt. True/False (this should preserve NNF) *)
- val simp_thm = simp_True_False_thm thy nnf
- val simp = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm
- (* finally, convert to CNF (this should preserve the simplification) *)
- val cnf_thm = make_under_quantifiers ctxt make_cnf_thm_from_nnf simp
-(* ###
- val cnf_thm = make_cnf_thm_from_nnf simp
-*)
- in
- iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnf_thm]
- end;
-
-(* ------------------------------------------------------------------------- *)
-(* CNF transformation by introducing new literals *)
-(* ------------------------------------------------------------------------- *)
-
-(* ------------------------------------------------------------------------- *)
-(* make_cnfx_thm: given any HOL term 't', produces a theorem t = t', where *)
-(* t' is almost in conjunction normal form, except that conjunctions *)
-(* and existential quantifiers may be nested. (Use e.g. 'REPEAT_DETERM *)
-(* (etac exE i ORELSE etac conjE i)' afterwards to normalize.) May *)
-(* introduce new (existentially bound) literals. Note: the current *)
-(* implementation calls 'make_nnf_thm', causing an exponential blowup *)
-(* in the case of nested equivalences. *)
-(* ------------------------------------------------------------------------- *)
-
-fun make_cnfx_thm ctxt t =
- let
- val thy = Proof_Context.theory_of ctxt
- val var_id = Unsynchronized.ref 0 (* properly initialized below *)
- fun new_free () =
- Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT)
- fun make_cnfx_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) : thm =
- let
- val thm1 = make_cnfx_thm_from_nnf x
- val thm2 = make_cnfx_thm_from_nnf y
- in
- conj_cong OF [thm1, thm2]
- end
- | make_cnfx_thm_from_nnf (Const (@{const_name HOL.disj}, _) $ x $ y) =
- if is_clause x andalso is_clause y then
- inst_thm thy [HOLogic.mk_disj (x, y)] iff_refl
- else if is_literal y orelse is_literal x then
- let
- (* produces a theorem "(x' | y') = t'", where x', y', and t' are *)
- (* almost in CNF, and x' or y' is a literal *)
- fun make_cnfx_disj_thm (Const (@{const_name HOL.conj}, _) $ x1 $ x2) y' =
- let
- val thm1 = make_cnfx_disj_thm x1 y'
- val thm2 = make_cnfx_disj_thm x2 y'
- in
- make_cnf_disj_conj_l OF [thm1, thm2] (* ((x1 & x2) | y') = ((x1 | y')' & (x2 | y')') *)
- end
- | make_cnfx_disj_thm x' (Const (@{const_name HOL.conj}, _) $ y1 $ y2) =
- let
- val thm1 = make_cnfx_disj_thm x' y1
- val thm2 = make_cnfx_disj_thm x' y2
- in
- make_cnf_disj_conj_r OF [thm1, thm2] (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
- end
- | make_cnfx_disj_thm (@{term "Ex::(bool => bool) => bool"} $ x') y' =
- let
- val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l (* ((Ex x') | y') = (Ex (x' | y')) *)
- val var = new_free ()
- val thm2 = make_cnfx_disj_thm (betapply (x', var)) y' (* (x' | y') = body' *)
- val thm3 = Thm.forall_intr (cterm_of thy var) thm2 (* !!v. (x' | y') = body' *)
- val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *)
- val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
- in
- iff_trans OF [thm1, thm5] (* ((Ex x') | y') = (Ex v. body') *)
- end
- | make_cnfx_disj_thm x' (@{term "Ex::(bool => bool) => bool"} $ y') =
- let
- val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r (* (x' | (Ex y')) = (Ex (x' | y')) *)
- val var = new_free ()
- val thm2 = make_cnfx_disj_thm x' (betapply (y', var)) (* (x' | y') = body' *)
- val thm3 = Thm.forall_intr (cterm_of thy var) thm2 (* !!v. (x' | y') = body' *)
- val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x' | y') = body' *)
- val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x' | y')) = (EX v. body') *)
- in
- iff_trans OF [thm1, thm5] (* (x' | (Ex y')) = (EX v. body') *)
- end
- | make_cnfx_disj_thm x' y' =
- inst_thm thy [HOLogic.mk_disj (x', y')] iff_refl (* (x' | y') = (x' | y') *)
- val thm1 = make_cnfx_thm_from_nnf x
- val thm2 = make_cnfx_thm_from_nnf y
- val x' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm1
- val y' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) thm2
- val disj_thm = disj_cong OF [thm1, thm2] (* (x | y) = (x' | y') *)
- in
- iff_trans OF [disj_thm, make_cnfx_disj_thm x' y']
- end
- else
- let (* neither 'x' nor 'y' is a literal: introduce a fresh variable *)
- val thm1 = inst_thm thy [x, y] make_cnfx_newlit (* (x | y) = EX v. (x | v) & (y | ~v) *)
- val var = new_free ()
- val body = HOLogic.mk_conj (HOLogic.mk_disj (x, var), HOLogic.mk_disj (y, HOLogic.Not $ var))
- val thm2 = make_cnfx_thm_from_nnf body (* (x | v) & (y | ~v) = body' *)
- val thm3 = Thm.forall_intr (cterm_of thy var) thm2 (* !!v. (x | v) & (y | ~v) = body' *)
- val thm4 = Thm.strip_shyps (thm3 COMP allI) (* ALL v. (x | v) & (y | ~v) = body' *)
- val thm5 = Thm.strip_shyps (thm4 RS make_cnfx_ex_cong) (* (EX v. (x | v) & (y | ~v)) = (EX v. body') *)
- in
- iff_trans OF [thm1, thm5]
- end
- | make_cnfx_thm_from_nnf t = inst_thm thy [t] iff_refl
- (* convert 't' to NNF first *)
- val nnf_thm = make_nnf_thm_under_quantifiers ctxt t
-(* ###
- val nnf_thm = make_nnf_thm thy t
-*)
- val nnf = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm
- (* then simplify wrt. True/False (this should preserve NNF) *)
- val simp_thm = simp_True_False_thm thy nnf
- val simp = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm
- (* initialize var_id, in case the term already contains variables of the form "cnfx_<int>" *)
- val _ = (var_id := fold (fn free => fn max =>
- let
- val (name, _) = dest_Free free
- val idx =
- if String.isPrefix "cnfx_" name then
- (Int.fromString o String.extract) (name, String.size "cnfx_", NONE)
- else
- NONE
- in
- Int.max (max, the_default 0 idx)
- end) (Misc_Legacy.term_frees simp) 0)
- (* finally, convert to definitional CNF (this should preserve the simplification) *)
- val cnfx_thm = make_under_quantifiers ctxt make_cnfx_thm_from_nnf simp
-(*###
- val cnfx_thm = make_cnfx_thm_from_nnf simp
-*)
- in
- iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnfx_thm]
- end;
-
-(* ------------------------------------------------------------------------- *)
-(* Tactics *)
-(* ------------------------------------------------------------------------- *)
-
-(* ------------------------------------------------------------------------- *)
-(* weakening_tac: removes the first hypothesis of the 'i'-th subgoal *)
-(* ------------------------------------------------------------------------- *)
-
-fun weakening_tac i =
- dtac weakening_thm i THEN atac (i+1);
-
-(* ------------------------------------------------------------------------- *)
-(* cnf_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF *)
-(* (possibly causing an exponential blowup in the length of each *)
-(* premise) *)
-(* ------------------------------------------------------------------------- *)
-
-fun cnf_rewrite_tac ctxt i =
- (* cut the CNF formulas as new premises *)
- Subgoal.FOCUS (fn {prems, ...} =>
- let
- val cnf_thms = map (make_cnf_thm ctxt o HOLogic.dest_Trueprop o Thm.prop_of) prems
- val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems)
- in
- cut_facts_tac cut_thms 1
- end) ctxt i
- (* remove the original premises *)
- THEN SELECT_GOAL (fn thm =>
- let
- val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm)
- in
- PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
- end) i;
-
-(* ------------------------------------------------------------------------- *)
-(* cnfx_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF *)
-(* (possibly introducing new literals) *)
-(* ------------------------------------------------------------------------- *)
-
-fun cnfx_rewrite_tac ctxt i =
- (* cut the CNF formulas as new premises *)
- Subgoal.FOCUS (fn {prems, ...} =>
- let
- val cnfx_thms = map (make_cnfx_thm ctxt o HOLogic.dest_Trueprop o prop_of) prems
- val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems)
- in
- cut_facts_tac cut_thms 1
- end) ctxt i
- (* remove the original premises *)
- THEN SELECT_GOAL (fn thm =>
- let
- val n = Logic.count_prems ((Term.strip_all_body o fst o Logic.dest_implies o prop_of) thm)
- in
- PRIMITIVE (funpow (n div 2) (Seq.hd o weakening_tac 1)) thm
- end) i;
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/sat.ML Sat Feb 01 21:09:53 2014 +0100
@@ -0,0 +1,474 @@
+(* Title: HOL/Tools/sat.ML
+ Author: Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
+ Author: Tjark Weber, TU Muenchen
+
+Proof reconstruction from SAT solvers.
+
+ Description:
+ This file defines several tactics to invoke a proof-producing
+ SAT solver on a propositional goal in clausal form.
+
+ We use a sequent presentation of clauses to speed up resolution
+ proof reconstruction.
+ We call such clauses "raw clauses", which are of the form
+ [x1, ..., xn, P] |- False
+ (note the use of |- instead of ==>, i.e. of Isabelle's (meta-)hyps here),
+ where each xi is a literal (see also comments in cnf.ML).
+
+ 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
+ the two input clauses, and resulting in new clauses, leading to
+ the empty clause (i.e. "False"). The tactic replays this proof
+ in Isabelle and thus solves the overall goal.
+
+ There are three SAT tactics available. They differ in the CNF transformation
+ used. "sat_tac" uses naive CNF transformation to transform the theorem to be
+ proved before giving it to the SAT solver. The naive transformation in the
+ worst case can lead to an exponential blow up in formula size. Another
+ tactic, "satx_tac", uses "definitional CNF transformation" which attempts to
+ produce a formula of linear size increase compared to the input formula, at
+ the cost of possibly introducing new variables. See cnf.ML for more
+ comments on the CNF transformation. "rawsat_tac" should be used with
+ caution: no CNF transformation is performed, and the tactic's behavior is
+ undefined if the subgoal is not already given as [| C1; ...; Cn |] ==> False,
+ where each Ci is a disjunction.
+
+ The SAT solver to be used can be set via the "solver" reference. See
+ sat_solvers.ML for possible values, and etc/settings for required (solver-
+ dependent) configuration settings. To replay SAT proofs in Isabelle, you
+ must of course use a proof-producing SAT solver in the first place.
+
+ Proofs are replayed only if "quick_and_dirty" is false. If
+ "quick_and_dirty" is true, the theorem (in case the SAT solver claims its
+ negation to be unsatisfiable) is proved via an oracle.
+*)
+
+signature SAT =
+sig
+ val trace_sat: bool Unsynchronized.ref (* input: print trace messages *)
+ val solver: string Unsynchronized.ref (* input: name of SAT solver to be used *)
+ val counter: int Unsynchronized.ref (* output: number of resolution steps during last proof replay *)
+ val rawsat_thm: Proof.context -> cterm list -> thm
+ val rawsat_tac: Proof.context -> int -> tactic
+ val sat_tac: Proof.context -> int -> tactic
+ val satx_tac: Proof.context -> int -> tactic
+end
+
+structure SAT : SAT =
+struct
+
+val trace_sat = Unsynchronized.ref false;
+
+val solver = Unsynchronized.ref "zchaff_with_proofs";
+ (*see HOL/Tools/sat_solver.ML for possible values*)
+
+val counter = Unsynchronized.ref 0;
+
+val resolution_thm =
+ @{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)}
+
+val cP = cterm_of @{theory} (Var (("P", 0), HOLogic.boolT));
+
+(* ------------------------------------------------------------------------- *)
+(* lit_ord: an order on integers that considers their absolute values only, *)
+(* thereby treating integers that represent the same atom (positively *)
+(* or negatively) as equal *)
+(* ------------------------------------------------------------------------- *)
+
+fun lit_ord (i, j) = int_ord (abs i, abs j);
+
+(* ------------------------------------------------------------------------- *)
+(* CLAUSE: during proof reconstruction, three kinds of clauses are *)
+(* distinguished: *)
+(* 1. NO_CLAUSE: clause not proved (yet) *)
+(* 2. ORIG_CLAUSE: a clause as it occurs in the original problem *)
+(* 3. RAW_CLAUSE: a raw clause, with additional precomputed information *)
+(* (a mapping from int's to its literals) for faster proof *)
+(* reconstruction *)
+(* ------------------------------------------------------------------------- *)
+
+datatype CLAUSE =
+ NO_CLAUSE
+ | ORIG_CLAUSE of thm
+ | RAW_CLAUSE of thm * (int * cterm) list;
+
+(* ------------------------------------------------------------------------- *)
+(* resolve_raw_clauses: given a non-empty list of raw clauses, we fold *)
+(* resolution over the list (starting with its head), i.e. with two raw *)
+(* clauses *)
+(* [P, x1, ..., a, ..., xn] |- False *)
+(* and *)
+(* [Q, y1, ..., a', ..., ym] |- False *)
+(* (where a and a' are dual to each other), we convert the first clause *)
+(* to *)
+(* [P, x1, ..., xn] |- a ==> False , *)
+(* the second clause to *)
+(* [Q, y1, ..., ym] |- a' ==> False *)
+(* and then perform resolution with *)
+(* [| ?P ==> False; ~?P ==> False |] ==> False *)
+(* to produce *)
+(* [P, Q, x1, ..., xn, y1, ..., ym] |- False *)
+(* Each clause is accompanied with an association list mapping integers *)
+(* (positive for positive literals, negative for negative literals, and *)
+(* the same absolute value for dual literals) to the actual literals as *)
+(* cterms. *)
+(* ------------------------------------------------------------------------- *)
+
+fun resolve_raw_clauses _ [] =
+ raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
+ | resolve_raw_clauses ctxt (c::cs) =
+ let
+ (* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *)
+ fun merge xs [] = xs
+ | merge [] ys = ys
+ | merge (x :: xs) (y :: ys) =
+ (case (lit_ord o pairself fst) (x, y) of
+ LESS => x :: merge xs (y :: ys)
+ | EQUAL => x :: merge xs ys
+ | GREATER => y :: merge (x :: xs) ys)
+
+ (* find out which two hyps are used in the resolution *)
+ fun find_res_hyps ([], _) _ =
+ raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
+ | find_res_hyps (_, []) _ =
+ raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
+ | find_res_hyps (h1 :: hyps1, h2 :: hyps2) acc =
+ (case (lit_ord o pairself fst) (h1, h2) of
+ LESS => find_res_hyps (hyps1, h2 :: hyps2) (h1 :: acc)
+ | EQUAL =>
+ let
+ val (i1, chyp1) = h1
+ val (i2, chyp2) = h2
+ in
+ if i1 = ~ i2 then
+ (i1 < 0, chyp1, chyp2, rev acc @ merge hyps1 hyps2)
+ else (* i1 = i2 *)
+ find_res_hyps (hyps1, hyps2) (h1 :: acc)
+ end
+ | GREATER => find_res_hyps (h1 :: hyps1, hyps2) (h2 :: acc))
+
+ fun resolution (c1, hyps1) (c2, hyps2) =
+ let
+ val _ =
+ if ! trace_sat then (* FIXME !? *)
+ tracing ("Resolving clause: " ^ Display.string_of_thm ctxt c1 ^
+ " (hyps: " ^ ML_Syntax.print_list
+ (Syntax.string_of_term_global (theory_of_thm c1)) (Thm.hyps_of c1)
+ ^ ")\nwith clause: " ^ Display.string_of_thm ctxt c2 ^
+ " (hyps: " ^ ML_Syntax.print_list
+ (Syntax.string_of_term_global (theory_of_thm c2)) (Thm.hyps_of c2) ^ ")")
+ else ()
+
+ (* the two literals used for resolution *)
+ val (hyp1_is_neg, hyp1, hyp2, new_hyps) = find_res_hyps (hyps1, hyps2) []
+
+ val c1' = Thm.implies_intr hyp1 c1 (* Gamma1 |- hyp1 ==> False *)
+ val c2' = Thm.implies_intr hyp2 c2 (* Gamma2 |- hyp2 ==> False *)
+
+ val res_thm = (* |- (lit ==> False) ==> (~lit ==> False) ==> False *)
+ let
+ val cLit =
+ snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1)) (* strip Trueprop *)
+ in
+ Thm.instantiate ([], [(cP, cLit)]) resolution_thm
+ end
+
+ val _ =
+ if !trace_sat then
+ tracing ("Resolution theorem: " ^ Display.string_of_thm ctxt res_thm)
+ else ()
+
+ (* Gamma1, Gamma2 |- False *)
+ val c_new =
+ Thm.implies_elim
+ (Thm.implies_elim res_thm (if hyp1_is_neg then c2' else c1'))
+ (if hyp1_is_neg then c1' else c2')
+
+ val _ =
+ if !trace_sat then
+ tracing ("Resulting clause: " ^ Display.string_of_thm ctxt c_new ^
+ " (hyps: " ^ ML_Syntax.print_list
+ (Syntax.string_of_term_global (theory_of_thm c_new)) (Thm.hyps_of c_new) ^ ")")
+ else ()
+ val _ = Unsynchronized.inc counter
+ in
+ (c_new, new_hyps)
+ end
+ in
+ fold resolution cs c
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* replay_proof: replays the resolution proof returned by the SAT solver; *)
+(* cf. SatSolver.proof for details of the proof format. Updates the *)
+(* 'clauses' array with derived clauses, and returns the derived clause *)
+(* at index 'empty_id' (which should just be "False" if proof *)
+(* reconstruction was successful, with the used clauses as hyps). *)
+(* 'atom_table' must contain an injective mapping from all atoms that *)
+(* occur (as part of a literal) in 'clauses' to positive integers. *)
+(* ------------------------------------------------------------------------- *)
+
+fun replay_proof ctxt atom_table clauses (clause_table, empty_id) =
+ let
+ fun index_of_literal chyp =
+ (case (HOLogic.dest_Trueprop o Thm.term_of) chyp of
+ (Const (@{const_name Not}, _) $ atom) =>
+ SOME (~ (the (Termtab.lookup atom_table atom)))
+ | atom => SOME (the (Termtab.lookup atom_table atom)))
+ handle TERM _ => NONE; (* 'chyp' is not a literal *)
+
+ fun prove_clause id =
+ (case Array.sub (clauses, id) of
+ RAW_CLAUSE clause => clause
+ | ORIG_CLAUSE thm =>
+ (* convert the original clause *)
+ let
+ val _ =
+ if !trace_sat then tracing ("Using original clause #" ^ string_of_int id) else ()
+ val raw = CNF.clause2raw_thm thm
+ val hyps = sort (lit_ord o pairself fst) (map_filter (fn chyp =>
+ Option.map (rpair chyp) (index_of_literal chyp)) (#hyps (Thm.crep_thm raw)))
+ val clause = (raw, hyps)
+ val _ = Array.update (clauses, id, RAW_CLAUSE clause)
+ in
+ clause
+ end
+ | NO_CLAUSE =>
+ (* prove the clause, using information from 'clause_table' *)
+ let
+ val _ =
+ if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else ()
+ val ids = the (Inttab.lookup clause_table id)
+ val clause = resolve_raw_clauses ctxt (map prove_clause ids)
+ val _ = Array.update (clauses, id, RAW_CLAUSE clause)
+ val _ =
+ if !trace_sat then
+ tracing ("Replay chain successful; clause stored at #" ^ string_of_int id)
+ else ()
+ in
+ clause
+ end)
+
+ val _ = counter := 0
+ val empty_clause = fst (prove_clause empty_id)
+ val _ =
+ if !trace_sat then
+ tracing ("Proof reconstruction successful; " ^
+ string_of_int (!counter) ^ " resolution step(s) total.")
+ else ()
+ in
+ empty_clause
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* string_of_prop_formula: return a human-readable string representation of *)
+(* a 'prop_formula' (just for tracing) *)
+(* ------------------------------------------------------------------------- *)
+
+fun string_of_prop_formula Prop_Logic.True = "True"
+ | string_of_prop_formula Prop_Logic.False = "False"
+ | string_of_prop_formula (Prop_Logic.BoolVar i) = "x" ^ string_of_int i
+ | string_of_prop_formula (Prop_Logic.Not fm) = "~" ^ string_of_prop_formula fm
+ | string_of_prop_formula (Prop_Logic.Or (fm1, fm2)) =
+ "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")"
+ | string_of_prop_formula (Prop_Logic.And (fm1, fm2)) =
+ "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")";
+
+(* ------------------------------------------------------------------------- *)
+(* rawsat_thm: run external SAT solver with the given clauses. Reconstructs *)
+(* a proof from the resulting proof trace of the SAT solver. The *)
+(* theorem returned is just "False" (with some of the given clauses as *)
+(* hyps). *)
+(* ------------------------------------------------------------------------- *)
+
+fun rawsat_thm ctxt clauses =
+ let
+ (* remove premises that equal "True" *)
+ val clauses' = filter (fn clause =>
+ (not_equal @{term True} o HOLogic.dest_Trueprop o Thm.term_of) clause
+ handle TERM ("dest_Trueprop", _) => true) clauses
+ (* remove non-clausal premises -- of course this shouldn't actually *)
+ (* remove anything as long as 'rawsat_tac' is only called after the *)
+ (* premises have been converted to clauses *)
+ val clauses'' = filter (fn clause =>
+ ((CNF.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause
+ handle TERM ("dest_Trueprop", _) => false)
+ orelse (
+ warning ("Ignoring non-clausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of clause));
+ false)) clauses'
+ (* remove trivial clauses -- this is necessary because zChaff removes *)
+ (* trivial clauses during preprocessing, and otherwise our clause *)
+ (* numbering would be off *)
+ val nontrivial_clauses =
+ filter (not o CNF.clause_is_trivial o HOLogic.dest_Trueprop o Thm.term_of) clauses''
+ (* sort clauses according to the term order -- an optimization, *)
+ (* useful because forming the union of hypotheses, as done by *)
+ (* Conjunction.intr_balanced and fold Thm.weaken below, is quadratic for *)
+ (* terms sorted in descending order, while only linear for terms *)
+ (* sorted in ascending order *)
+ val sorted_clauses = sort (Term_Ord.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
+ val _ =
+ if !trace_sat then
+ tracing ("Sorted non-trivial clauses:\n" ^
+ cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses))
+ else ()
+ (* translate clauses from HOL terms to Prop_Logic.prop_formula *)
+ val (fms, atom_table) =
+ fold_map (Prop_Logic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of)
+ sorted_clauses Termtab.empty
+ val _ =
+ if !trace_sat then
+ tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms))
+ else ()
+ val fm = Prop_Logic.all fms
+ fun make_quick_and_dirty_thm () =
+ let
+ val _ =
+ if !trace_sat then
+ tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead."
+ else ()
+ val False_thm = Skip_Proof.make_thm_cterm @{cprop False}
+ in
+ (* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold *)
+ (* Thm.weaken sorted_clauses' would be quadratic, since we sorted *)
+ (* clauses in ascending order (which is linear for *)
+ (* 'Conjunction.intr_balanced', used below) *)
+ fold Thm.weaken (rev sorted_clauses) False_thm
+ end
+ in
+ case
+ let val the_solver = ! solver
+ in (tracing ("Invoking solver " ^ the_solver); SatSolver.invoke_solver the_solver fm) end
+ of
+ SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) =>
+ (if !trace_sat then
+ tracing ("Proof trace from SAT solver:\n" ^
+ "clauses: " ^ ML_Syntax.print_list
+ (ML_Syntax.print_pair ML_Syntax.print_int (ML_Syntax.print_list ML_Syntax.print_int))
+ (Inttab.dest clause_table) ^ "\n" ^
+ "empty clause: " ^ string_of_int empty_id)
+ else ();
+ if Config.get ctxt quick_and_dirty then
+ make_quick_and_dirty_thm ()
+ else
+ let
+ (* optimization: convert the given clauses to "[c_1 && ... && c_n] |- c_i"; *)
+ (* this avoids accumulation of hypotheses during resolution *)
+ (* [c_1, ..., c_n] |- c_1 && ... && c_n *)
+ val clauses_thm = Conjunction.intr_balanced (map Thm.assume sorted_clauses)
+ (* [c_1 && ... && c_n] |- c_1 && ... && c_n *)
+ val cnf_cterm = cprop_of clauses_thm
+ val cnf_thm = Thm.assume cnf_cterm
+ (* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *)
+ val cnf_clauses = Conjunction.elim_balanced (length sorted_clauses) cnf_thm
+ (* initialize the clause array with the given clauses *)
+ val max_idx = fst (the (Inttab.max clause_table))
+ val clause_arr = Array.array (max_idx + 1, NO_CLAUSE)
+ val _ =
+ fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1))
+ cnf_clauses 0
+ (* replay the proof to derive the empty clause *)
+ (* [c_1 && ... && c_n] |- False *)
+ val raw_thm = replay_proof ctxt atom_table clause_arr (clause_table, empty_id)
+ in
+ (* [c_1, ..., c_n] |- False *)
+ Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm
+ end)
+ | SatSolver.UNSATISFIABLE NONE =>
+ if Config.get ctxt quick_and_dirty then
+ (warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof";
+ make_quick_and_dirty_thm ())
+ else
+ raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, [])
+ | SatSolver.SATISFIABLE assignment =>
+ let
+ val msg =
+ "SAT solver found a countermodel:\n" ^
+ (commas o map (fn (term, idx) =>
+ Syntax.string_of_term_global @{theory} term ^ ": " ^
+ (case assignment idx of NONE => "arbitrary"
+ | SOME true => "true" | SOME false => "false")))
+ (Termtab.dest atom_table)
+ in
+ raise THM (msg, 0, [])
+ end
+ | SatSolver.UNKNOWN =>
+ raise THM ("SAT solver failed to decide the formula", 0, [])
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Tactics *)
+(* ------------------------------------------------------------------------- *)
+
+(* ------------------------------------------------------------------------- *)
+(* rawsat_tac: solves the i-th subgoal of the proof state; this subgoal *)
+(* should be of the form *)
+(* [| c1; c2; ...; ck |] ==> False *)
+(* where each cj is a non-empty clause (i.e. a disjunction of literals) *)
+(* or "True" *)
+(* ------------------------------------------------------------------------- *)
+
+fun rawsat_tac ctxt i =
+ Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
+ rtac (rawsat_thm ctxt' (map cprop_of prems)) 1) ctxt i;
+
+(* ------------------------------------------------------------------------- *)
+(* pre_cnf_tac: converts the i-th subgoal *)
+(* [| A1 ; ... ; An |] ==> B *)
+(* to *)
+(* [| A1; ... ; An ; ~B |] ==> False *)
+(* (handling meta-logical connectives in B properly before negating), *)
+(* then replaces meta-logical connectives in the premises (i.e. "==>", *)
+(* "!!" and "==") by connectives of the HOL object-logic (i.e. by *)
+(* "-->", "!", and "="), then performs beta-eta-normalization on the *)
+(* subgoal *)
+(* ------------------------------------------------------------------------- *)
+
+fun pre_cnf_tac ctxt =
+ rtac ccontr THEN'
+ Object_Logic.atomize_prems_tac ctxt THEN'
+ CONVERSION Drule.beta_eta_conversion;
+
+(* ------------------------------------------------------------------------- *)
+(* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *)
+(* if not, eliminates conjunctions (i.e. each clause of the CNF formula *)
+(* becomes a separate premise), then applies 'rawsat_tac' to solve the *)
+(* subgoal *)
+(* ------------------------------------------------------------------------- *)
+
+fun cnfsat_tac ctxt i =
+ (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac ctxt i);
+
+(* ------------------------------------------------------------------------- *)
+(* cnfxsat_tac: checks if the empty clause "False" occurs among the *)
+(* premises; if not, eliminates conjunctions (i.e. each clause of the *)
+(* CNF formula becomes a separate premise) and existential quantifiers, *)
+(* then applies 'rawsat_tac' to solve the subgoal *)
+(* ------------------------------------------------------------------------- *)
+
+fun cnfxsat_tac ctxt i =
+ (etac FalseE i) ORELSE
+ (REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac ctxt i);
+
+(* ------------------------------------------------------------------------- *)
+(* sat_tac: tactic for calling an external SAT solver, taking as input an *)
+(* arbitrary formula. The input is translated to CNF, possibly causing *)
+(* an exponential blowup. *)
+(* ------------------------------------------------------------------------- *)
+
+fun sat_tac ctxt i =
+ pre_cnf_tac ctxt i THEN CNF.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i;
+
+(* ------------------------------------------------------------------------- *)
+(* satx_tac: tactic for calling an external SAT solver, taking as input an *)
+(* arbitrary formula. The input is translated to CNF, possibly *)
+(* introducing new literals. *)
+(* ------------------------------------------------------------------------- *)
+
+fun satx_tac ctxt i =
+ pre_cnf_tac ctxt i THEN CNF.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i;
+
+end;
--- a/src/HOL/Tools/sat_funcs.ML Sat Feb 01 20:46:19 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,474 +0,0 @@
-(* Title: HOL/Tools/sat_funcs.ML
- Author: Stephan Merz and Alwen Tiu, QSL Team, LORIA (http://qsl.loria.fr)
- Author: Tjark Weber, TU Muenchen
-
-Proof reconstruction from SAT solvers.
-
- Description:
- This file defines several tactics to invoke a proof-producing
- SAT solver on a propositional goal in clausal form.
-
- We use a sequent presentation of clauses to speed up resolution
- proof reconstruction.
- We call such clauses "raw clauses", which are of the form
- [x1, ..., xn, P] |- False
- (note the use of |- instead of ==>, i.e. of Isabelle's (meta-)hyps here),
- where each xi is a literal (see also comments in cnf_funcs.ML).
-
- 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
- the two input clauses, and resulting in new clauses, leading to
- the empty clause (i.e. "False"). The tactic replays this proof
- in Isabelle and thus solves the overall goal.
-
- There are three SAT tactics available. They differ in the CNF transformation
- used. "sat_tac" uses naive CNF transformation to transform the theorem to be
- proved before giving it to the SAT solver. The naive transformation in the
- worst case can lead to an exponential blow up in formula size. Another
- tactic, "satx_tac", uses "definitional CNF transformation" which attempts to
- produce a formula of linear size increase compared to the input formula, at
- the cost of possibly introducing new variables. See cnf_funcs.ML for more
- comments on the CNF transformation. "rawsat_tac" should be used with
- caution: no CNF transformation is performed, and the tactic's behavior is
- undefined if the subgoal is not already given as [| C1; ...; Cn |] ==> False,
- where each Ci is a disjunction.
-
- The SAT solver to be used can be set via the "solver" reference. See
- sat_solvers.ML for possible values, and etc/settings for required (solver-
- dependent) configuration settings. To replay SAT proofs in Isabelle, you
- must of course use a proof-producing SAT solver in the first place.
-
- Proofs are replayed only if "quick_and_dirty" is false. If
- "quick_and_dirty" is true, the theorem (in case the SAT solver claims its
- negation to be unsatisfiable) is proved via an oracle.
-*)
-
-signature SAT =
-sig
- val trace_sat: bool Unsynchronized.ref (* input: print trace messages *)
- val solver: string Unsynchronized.ref (* input: name of SAT solver to be used *)
- val counter: int Unsynchronized.ref (* output: number of resolution steps during last proof replay *)
- val rawsat_thm: Proof.context -> cterm list -> thm
- val rawsat_tac: Proof.context -> int -> tactic
- val sat_tac: Proof.context -> int -> tactic
- val satx_tac: Proof.context -> int -> tactic
-end
-
-functor SATFunc(cnf : CNF) : SAT =
-struct
-
-val trace_sat = Unsynchronized.ref false;
-
-val solver = Unsynchronized.ref "zchaff_with_proofs";
- (*see HOL/Tools/sat_solver.ML for possible values*)
-
-val counter = Unsynchronized.ref 0;
-
-val resolution_thm =
- @{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)}
-
-val cP = cterm_of @{theory} (Var (("P", 0), HOLogic.boolT));
-
-(* ------------------------------------------------------------------------- *)
-(* lit_ord: an order on integers that considers their absolute values only, *)
-(* thereby treating integers that represent the same atom (positively *)
-(* or negatively) as equal *)
-(* ------------------------------------------------------------------------- *)
-
-fun lit_ord (i, j) = int_ord (abs i, abs j);
-
-(* ------------------------------------------------------------------------- *)
-(* CLAUSE: during proof reconstruction, three kinds of clauses are *)
-(* distinguished: *)
-(* 1. NO_CLAUSE: clause not proved (yet) *)
-(* 2. ORIG_CLAUSE: a clause as it occurs in the original problem *)
-(* 3. RAW_CLAUSE: a raw clause, with additional precomputed information *)
-(* (a mapping from int's to its literals) for faster proof *)
-(* reconstruction *)
-(* ------------------------------------------------------------------------- *)
-
-datatype CLAUSE =
- NO_CLAUSE
- | ORIG_CLAUSE of thm
- | RAW_CLAUSE of thm * (int * cterm) list;
-
-(* ------------------------------------------------------------------------- *)
-(* resolve_raw_clauses: given a non-empty list of raw clauses, we fold *)
-(* resolution over the list (starting with its head), i.e. with two raw *)
-(* clauses *)
-(* [P, x1, ..., a, ..., xn] |- False *)
-(* and *)
-(* [Q, y1, ..., a', ..., ym] |- False *)
-(* (where a and a' are dual to each other), we convert the first clause *)
-(* to *)
-(* [P, x1, ..., xn] |- a ==> False , *)
-(* the second clause to *)
-(* [Q, y1, ..., ym] |- a' ==> False *)
-(* and then perform resolution with *)
-(* [| ?P ==> False; ~?P ==> False |] ==> False *)
-(* to produce *)
-(* [P, Q, x1, ..., xn, y1, ..., ym] |- False *)
-(* Each clause is accompanied with an association list mapping integers *)
-(* (positive for positive literals, negative for negative literals, and *)
-(* the same absolute value for dual literals) to the actual literals as *)
-(* cterms. *)
-(* ------------------------------------------------------------------------- *)
-
-fun resolve_raw_clauses _ [] =
- raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
- | resolve_raw_clauses ctxt (c::cs) =
- let
- (* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *)
- fun merge xs [] = xs
- | merge [] ys = ys
- | merge (x :: xs) (y :: ys) =
- (case (lit_ord o pairself fst) (x, y) of
- LESS => x :: merge xs (y :: ys)
- | EQUAL => x :: merge xs ys
- | GREATER => y :: merge (x :: xs) ys)
-
- (* find out which two hyps are used in the resolution *)
- fun find_res_hyps ([], _) _ =
- raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
- | find_res_hyps (_, []) _ =
- raise THM ("Proof reconstruction failed (no literal for resolution)!", 0, [])
- | find_res_hyps (h1 :: hyps1, h2 :: hyps2) acc =
- (case (lit_ord o pairself fst) (h1, h2) of
- LESS => find_res_hyps (hyps1, h2 :: hyps2) (h1 :: acc)
- | EQUAL =>
- let
- val (i1, chyp1) = h1
- val (i2, chyp2) = h2
- in
- if i1 = ~ i2 then
- (i1 < 0, chyp1, chyp2, rev acc @ merge hyps1 hyps2)
- else (* i1 = i2 *)
- find_res_hyps (hyps1, hyps2) (h1 :: acc)
- end
- | GREATER => find_res_hyps (h1 :: hyps1, hyps2) (h2 :: acc))
-
- fun resolution (c1, hyps1) (c2, hyps2) =
- let
- val _ =
- if ! trace_sat then (* FIXME !? *)
- tracing ("Resolving clause: " ^ Display.string_of_thm ctxt c1 ^
- " (hyps: " ^ ML_Syntax.print_list
- (Syntax.string_of_term_global (theory_of_thm c1)) (Thm.hyps_of c1)
- ^ ")\nwith clause: " ^ Display.string_of_thm ctxt c2 ^
- " (hyps: " ^ ML_Syntax.print_list
- (Syntax.string_of_term_global (theory_of_thm c2)) (Thm.hyps_of c2) ^ ")")
- else ()
-
- (* the two literals used for resolution *)
- val (hyp1_is_neg, hyp1, hyp2, new_hyps) = find_res_hyps (hyps1, hyps2) []
-
- val c1' = Thm.implies_intr hyp1 c1 (* Gamma1 |- hyp1 ==> False *)
- val c2' = Thm.implies_intr hyp2 c2 (* Gamma2 |- hyp2 ==> False *)
-
- val res_thm = (* |- (lit ==> False) ==> (~lit ==> False) ==> False *)
- let
- val cLit =
- snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1)) (* strip Trueprop *)
- in
- Thm.instantiate ([], [(cP, cLit)]) resolution_thm
- end
-
- val _ =
- if !trace_sat then
- tracing ("Resolution theorem: " ^ Display.string_of_thm ctxt res_thm)
- else ()
-
- (* Gamma1, Gamma2 |- False *)
- val c_new =
- Thm.implies_elim
- (Thm.implies_elim res_thm (if hyp1_is_neg then c2' else c1'))
- (if hyp1_is_neg then c1' else c2')
-
- val _ =
- if !trace_sat then
- tracing ("Resulting clause: " ^ Display.string_of_thm ctxt c_new ^
- " (hyps: " ^ ML_Syntax.print_list
- (Syntax.string_of_term_global (theory_of_thm c_new)) (Thm.hyps_of c_new) ^ ")")
- else ()
- val _ = Unsynchronized.inc counter
- in
- (c_new, new_hyps)
- end
- in
- fold resolution cs c
- end;
-
-(* ------------------------------------------------------------------------- *)
-(* replay_proof: replays the resolution proof returned by the SAT solver; *)
-(* cf. SatSolver.proof for details of the proof format. Updates the *)
-(* 'clauses' array with derived clauses, and returns the derived clause *)
-(* at index 'empty_id' (which should just be "False" if proof *)
-(* reconstruction was successful, with the used clauses as hyps). *)
-(* 'atom_table' must contain an injective mapping from all atoms that *)
-(* occur (as part of a literal) in 'clauses' to positive integers. *)
-(* ------------------------------------------------------------------------- *)
-
-fun replay_proof ctxt atom_table clauses (clause_table, empty_id) =
- let
- fun index_of_literal chyp =
- (case (HOLogic.dest_Trueprop o Thm.term_of) chyp of
- (Const (@{const_name Not}, _) $ atom) =>
- SOME (~ (the (Termtab.lookup atom_table atom)))
- | atom => SOME (the (Termtab.lookup atom_table atom)))
- handle TERM _ => NONE; (* 'chyp' is not a literal *)
-
- fun prove_clause id =
- (case Array.sub (clauses, id) of
- RAW_CLAUSE clause => clause
- | ORIG_CLAUSE thm =>
- (* convert the original clause *)
- let
- val _ =
- if !trace_sat then tracing ("Using original clause #" ^ string_of_int id) else ()
- val raw = cnf.clause2raw_thm thm
- val hyps = sort (lit_ord o pairself fst) (map_filter (fn chyp =>
- Option.map (rpair chyp) (index_of_literal chyp)) (#hyps (Thm.crep_thm raw)))
- val clause = (raw, hyps)
- val _ = Array.update (clauses, id, RAW_CLAUSE clause)
- in
- clause
- end
- | NO_CLAUSE =>
- (* prove the clause, using information from 'clause_table' *)
- let
- val _ =
- if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else ()
- val ids = the (Inttab.lookup clause_table id)
- val clause = resolve_raw_clauses ctxt (map prove_clause ids)
- val _ = Array.update (clauses, id, RAW_CLAUSE clause)
- val _ =
- if !trace_sat then
- tracing ("Replay chain successful; clause stored at #" ^ string_of_int id)
- else ()
- in
- clause
- end)
-
- val _ = counter := 0
- val empty_clause = fst (prove_clause empty_id)
- val _ =
- if !trace_sat then
- tracing ("Proof reconstruction successful; " ^
- string_of_int (!counter) ^ " resolution step(s) total.")
- else ()
- in
- empty_clause
- end;
-
-(* ------------------------------------------------------------------------- *)
-(* string_of_prop_formula: return a human-readable string representation of *)
-(* a 'prop_formula' (just for tracing) *)
-(* ------------------------------------------------------------------------- *)
-
-fun string_of_prop_formula Prop_Logic.True = "True"
- | string_of_prop_formula Prop_Logic.False = "False"
- | string_of_prop_formula (Prop_Logic.BoolVar i) = "x" ^ string_of_int i
- | string_of_prop_formula (Prop_Logic.Not fm) = "~" ^ string_of_prop_formula fm
- | string_of_prop_formula (Prop_Logic.Or (fm1, fm2)) =
- "(" ^ string_of_prop_formula fm1 ^ " v " ^ string_of_prop_formula fm2 ^ ")"
- | string_of_prop_formula (Prop_Logic.And (fm1, fm2)) =
- "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")";
-
-(* ------------------------------------------------------------------------- *)
-(* rawsat_thm: run external SAT solver with the given clauses. Reconstructs *)
-(* a proof from the resulting proof trace of the SAT solver. The *)
-(* theorem returned is just "False" (with some of the given clauses as *)
-(* hyps). *)
-(* ------------------------------------------------------------------------- *)
-
-fun rawsat_thm ctxt clauses =
- let
- (* remove premises that equal "True" *)
- val clauses' = filter (fn clause =>
- (not_equal @{term True} o HOLogic.dest_Trueprop o Thm.term_of) clause
- handle TERM ("dest_Trueprop", _) => true) clauses
- (* remove non-clausal premises -- of course this shouldn't actually *)
- (* remove anything as long as 'rawsat_tac' is only called after the *)
- (* premises have been converted to clauses *)
- val clauses'' = filter (fn clause =>
- ((cnf.is_clause o HOLogic.dest_Trueprop o Thm.term_of) clause
- handle TERM ("dest_Trueprop", _) => false)
- orelse (
- warning ("Ignoring non-clausal premise " ^ Syntax.string_of_term ctxt (Thm.term_of clause));
- false)) clauses'
- (* remove trivial clauses -- this is necessary because zChaff removes *)
- (* trivial clauses during preprocessing, and otherwise our clause *)
- (* numbering would be off *)
- val nontrivial_clauses =
- filter (not o cnf.clause_is_trivial o HOLogic.dest_Trueprop o Thm.term_of) clauses''
- (* sort clauses according to the term order -- an optimization, *)
- (* useful because forming the union of hypotheses, as done by *)
- (* Conjunction.intr_balanced and fold Thm.weaken below, is quadratic for *)
- (* terms sorted in descending order, while only linear for terms *)
- (* sorted in ascending order *)
- val sorted_clauses = sort (Term_Ord.fast_term_ord o pairself Thm.term_of) nontrivial_clauses
- val _ =
- if !trace_sat then
- tracing ("Sorted non-trivial clauses:\n" ^
- cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses))
- else ()
- (* translate clauses from HOL terms to Prop_Logic.prop_formula *)
- val (fms, atom_table) =
- fold_map (Prop_Logic.prop_formula_of_term o HOLogic.dest_Trueprop o Thm.term_of)
- sorted_clauses Termtab.empty
- val _ =
- if !trace_sat then
- tracing ("Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms))
- else ()
- val fm = Prop_Logic.all fms
- fun make_quick_and_dirty_thm () =
- let
- val _ =
- if !trace_sat then
- tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead."
- else ()
- val False_thm = Skip_Proof.make_thm_cterm @{cprop False}
- in
- (* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold *)
- (* Thm.weaken sorted_clauses' would be quadratic, since we sorted *)
- (* clauses in ascending order (which is linear for *)
- (* 'Conjunction.intr_balanced', used below) *)
- fold Thm.weaken (rev sorted_clauses) False_thm
- end
- in
- case
- let val the_solver = ! solver
- in (tracing ("Invoking solver " ^ the_solver); SatSolver.invoke_solver the_solver fm) end
- of
- SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) =>
- (if !trace_sat then
- tracing ("Proof trace from SAT solver:\n" ^
- "clauses: " ^ ML_Syntax.print_list
- (ML_Syntax.print_pair ML_Syntax.print_int (ML_Syntax.print_list ML_Syntax.print_int))
- (Inttab.dest clause_table) ^ "\n" ^
- "empty clause: " ^ string_of_int empty_id)
- else ();
- if Config.get ctxt quick_and_dirty then
- make_quick_and_dirty_thm ()
- else
- let
- (* optimization: convert the given clauses to "[c_1 && ... && c_n] |- c_i"; *)
- (* this avoids accumulation of hypotheses during resolution *)
- (* [c_1, ..., c_n] |- c_1 && ... && c_n *)
- val clauses_thm = Conjunction.intr_balanced (map Thm.assume sorted_clauses)
- (* [c_1 && ... && c_n] |- c_1 && ... && c_n *)
- val cnf_cterm = cprop_of clauses_thm
- val cnf_thm = Thm.assume cnf_cterm
- (* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *)
- val cnf_clauses = Conjunction.elim_balanced (length sorted_clauses) cnf_thm
- (* initialize the clause array with the given clauses *)
- val max_idx = fst (the (Inttab.max clause_table))
- val clause_arr = Array.array (max_idx + 1, NO_CLAUSE)
- val _ =
- fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1))
- cnf_clauses 0
- (* replay the proof to derive the empty clause *)
- (* [c_1 && ... && c_n] |- False *)
- val raw_thm = replay_proof ctxt atom_table clause_arr (clause_table, empty_id)
- in
- (* [c_1, ..., c_n] |- False *)
- Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm
- end)
- | SatSolver.UNSATISFIABLE NONE =>
- if Config.get ctxt quick_and_dirty then
- (warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof";
- make_quick_and_dirty_thm ())
- else
- raise THM ("SAT solver claims the formula to be unsatisfiable, but did not provide a proof", 0, [])
- | SatSolver.SATISFIABLE assignment =>
- let
- val msg =
- "SAT solver found a countermodel:\n" ^
- (commas o map (fn (term, idx) =>
- Syntax.string_of_term_global @{theory} term ^ ": " ^
- (case assignment idx of NONE => "arbitrary"
- | SOME true => "true" | SOME false => "false")))
- (Termtab.dest atom_table)
- in
- raise THM (msg, 0, [])
- end
- | SatSolver.UNKNOWN =>
- raise THM ("SAT solver failed to decide the formula", 0, [])
- end;
-
-(* ------------------------------------------------------------------------- *)
-(* Tactics *)
-(* ------------------------------------------------------------------------- *)
-
-(* ------------------------------------------------------------------------- *)
-(* rawsat_tac: solves the i-th subgoal of the proof state; this subgoal *)
-(* should be of the form *)
-(* [| c1; c2; ...; ck |] ==> False *)
-(* where each cj is a non-empty clause (i.e. a disjunction of literals) *)
-(* or "True" *)
-(* ------------------------------------------------------------------------- *)
-
-fun rawsat_tac ctxt i =
- Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
- rtac (rawsat_thm ctxt' (map cprop_of prems)) 1) ctxt i;
-
-(* ------------------------------------------------------------------------- *)
-(* pre_cnf_tac: converts the i-th subgoal *)
-(* [| A1 ; ... ; An |] ==> B *)
-(* to *)
-(* [| A1; ... ; An ; ~B |] ==> False *)
-(* (handling meta-logical connectives in B properly before negating), *)
-(* then replaces meta-logical connectives in the premises (i.e. "==>", *)
-(* "!!" and "==") by connectives of the HOL object-logic (i.e. by *)
-(* "-->", "!", and "="), then performs beta-eta-normalization on the *)
-(* subgoal *)
-(* ------------------------------------------------------------------------- *)
-
-fun pre_cnf_tac ctxt =
- rtac ccontr THEN'
- Object_Logic.atomize_prems_tac ctxt THEN'
- CONVERSION Drule.beta_eta_conversion;
-
-(* ------------------------------------------------------------------------- *)
-(* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *)
-(* if not, eliminates conjunctions (i.e. each clause of the CNF formula *)
-(* becomes a separate premise), then applies 'rawsat_tac' to solve the *)
-(* subgoal *)
-(* ------------------------------------------------------------------------- *)
-
-fun cnfsat_tac ctxt i =
- (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac ctxt i);
-
-(* ------------------------------------------------------------------------- *)
-(* cnfxsat_tac: checks if the empty clause "False" occurs among the *)
-(* premises; if not, eliminates conjunctions (i.e. each clause of the *)
-(* CNF formula becomes a separate premise) and existential quantifiers, *)
-(* then applies 'rawsat_tac' to solve the subgoal *)
-(* ------------------------------------------------------------------------- *)
-
-fun cnfxsat_tac ctxt i =
- (etac FalseE i) ORELSE
- (REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac ctxt i);
-
-(* ------------------------------------------------------------------------- *)
-(* sat_tac: tactic for calling an external SAT solver, taking as input an *)
-(* arbitrary formula. The input is translated to CNF, possibly causing *)
-(* an exponential blowup. *)
-(* ------------------------------------------------------------------------- *)
-
-fun sat_tac ctxt i =
- pre_cnf_tac ctxt i THEN cnf.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i;
-
-(* ------------------------------------------------------------------------- *)
-(* satx_tac: tactic for calling an external SAT solver, taking as input an *)
-(* arbitrary formula. The input is translated to CNF, possibly *)
-(* introducing new literals. *)
-(* ------------------------------------------------------------------------- *)
-
-fun satx_tac ctxt i =
- pre_cnf_tac ctxt i THEN cnf.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i;
-
-end;
--- a/src/HOL/ex/SAT_Examples.thy Sat Feb 01 20:46:19 2014 +0100
+++ b/src/HOL/ex/SAT_Examples.thy Sat Feb 01 21:09:53 2014 +0100
@@ -8,9 +8,9 @@
theory SAT_Examples imports Main
begin
-(* ML {* sat.solver := "zchaff_with_proofs"; *} *)
-(* ML {* sat.solver := "minisat_with_proofs"; *} *)
-ML {* sat.trace_sat := true; *}
+(* ML {* SAT.solver := "zchaff_with_proofs"; *} *)
+(* ML {* SAT.solver := "minisat_with_proofs"; *} *)
+ML {* SAT.trace_sat := true; *}
declare [[quick_and_dirty]]
lemma "True"
@@ -24,13 +24,13 @@
lemma "(a & b) | (c & d) \<Longrightarrow> (a & b) | (c & d)"
(*
-apply (tactic {* cnf.cnf_rewrite_tac 1 *})
+apply (tactic {* CNF.cnf_rewrite_tac 1 *})
*)
by sat
lemma "(a & b) | (c & d) \<Longrightarrow> (a & b) | (c & d)"
(*
-apply (tactic {* cnf.cnfx_rewrite_tac 1 *})
+apply (tactic {* CNF.cnfx_rewrite_tac 1 *})
apply (erule exE | erule conjE)+
*)
by satx
@@ -38,14 +38,14 @@
lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)
\<Longrightarrow> (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)"
(*
-apply (tactic {* cnf.cnf_rewrite_tac 1 *})
+apply (tactic {* CNF.cnf_rewrite_tac 1 *})
*)
by sat
lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)
\<Longrightarrow> (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)"
(*
-apply (tactic {* cnf.cnfx_rewrite_tac 1 *})
+apply (tactic {* CNF.cnfx_rewrite_tac 1 *})
apply (erule exE | erule conjE)+
*)
by satx
@@ -77,11 +77,11 @@
lemma "(ALL x. P x) | ~ All P"
by sat
-ML {* sat.trace_sat := false; *}
+ML {* SAT.trace_sat := false; *}
declare [[quick_and_dirty = false]]
method_setup rawsat = {*
- Scan.succeed (SIMPLE_METHOD' o sat.rawsat_tac)
+ Scan.succeed (SIMPLE_METHOD' o SAT.rawsat_tac)
*} "SAT solver (no preprocessing)"
(* Translated from TPTP problem library: PUZ015-2.006.dimacs *)
@@ -520,26 +520,26 @@
*}
(* ML {*
-sat.solver := "zchaff_with_proofs";
-sat.trace_sat := false;
+SAT.solver := "zchaff_with_proofs";
+SAT.trace_sat := false;
*}
declare [[quick_and_dirty = false]]
*)
ML {*
-fun benchmark dimacsfile =
-let
- val prop_fm = SatSolver.read_dimacs_cnf_file (Path.explode dimacsfile)
- fun and_to_list (Prop_Logic.And (fm1, fm2)) acc = and_to_list fm2 (fm1 :: acc)
- | and_to_list fm acc = rev (fm :: acc)
- val clauses = and_to_list prop_fm []
- val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) clauses
- val cterms = map (Thm.cterm_of @{theory}) terms
- val start = Timing.start ()
- val _ = sat.rawsat_thm @{context} cterms
-in
- (Timing.result start, ! sat.counter)
-end;
+ fun benchmark dimacsfile =
+ let
+ val prop_fm = SatSolver.read_dimacs_cnf_file (Path.explode dimacsfile)
+ fun and_to_list (Prop_Logic.And (fm1, fm2)) acc = and_to_list fm2 (fm1 :: acc)
+ | and_to_list fm acc = rev (fm :: acc)
+ val clauses = and_to_list prop_fm []
+ val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) clauses
+ val cterms = map (Thm.cterm_of @{theory}) terms
+ val start = Timing.start ()
+ val _ = SAT.rawsat_thm @{context} cterms
+ in
+ (Timing.result start, ! SAT.counter)
+ end;
*}
end