# HG changeset patch # User wenzelm # Date 1391288540 -3600 # Node ID ef601c60ccbea92851750b3c7a3283aa17b98d65 # Parent 7ddb889e23bd1bb24a4d9e29afdce79a9aeb9da5# Parent efc4c0e0e14adf928532bc1c0e534b85269ac364 merged diff -r 7ddb889e23bd -r ef601c60ccbe src/HOL/HOL.thy --- a/src/HOL/HOL.thy Sat Feb 01 20:38:29 2014 +0000 +++ b/src/HOL/HOL.thy Sat Feb 01 22:02:20 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 *} diff -r 7ddb889e23bd -r ef601c60ccbe src/HOL/ROOT --- a/src/HOL/ROOT Sat Feb 01 20:38:29 2014 +0000 +++ b/src/HOL/ROOT Sat Feb 01 22:02:20 2014 +0100 @@ -572,8 +572,7 @@ Sudoku (* FIXME (*requires a proof-generating SAT solver (zChaff or MiniSAT)*) -(*global side-effects ahead!*) -try use_thy "SAT_Examples"; (* FIXME try!? (not really a proper test) *) + SAT_Examples *) files "document/root.bib" "document/root.tex" diff -r 7ddb889e23bd -r ef601c60ccbe src/HOL/SAT.thy --- a/src/HOL/SAT.thy Sat Feb 01 20:38:29 2014 +0000 +++ b/src/HOL/SAT.thy Sat Feb 01 22:02:20 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 diff -r 7ddb889e23bd -r ef601c60ccbe src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Sat Feb 01 20:38:29 2014 +0000 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Sat Feb 01 22:02:20 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 diff -r 7ddb889e23bd -r ef601c60ccbe src/HOL/Tools/Metis/metis_tactic.ML --- a/src/HOL/Tools/Metis/metis_tactic.ML Sat Feb 01 20:38:29 2014 +0000 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Sat Feb 01 22:02:20 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 diff -r 7ddb889e23bd -r ef601c60ccbe src/HOL/Tools/cnf.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/cnf.ML Sat Feb 01 22:02:20 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_" *) + 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; diff -r 7ddb889e23bd -r ef601c60ccbe src/HOL/Tools/cnf_funcs.ML --- a/src/HOL/Tools/cnf_funcs.ML Sat Feb 01 20:38:29 2014 +0000 +++ /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_" *) - 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; diff -r 7ddb889e23bd -r ef601c60ccbe src/HOL/Tools/sat.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/sat.ML Sat Feb 01 22:02:20 2014 +0100 @@ -0,0 +1,465 @@ +(* 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: bool Config.T (* print trace messages *) + val solver: string Config.T (* 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 = Attrib.setup_config_bool @{binding sat_trace} (K false); + +fun cond_tracing ctxt msg = + if Config.get ctxt trace then tracing (msg ()) else (); + +val solver = Attrib.setup_config_string @{binding sat_solver} (K "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 _ = + cond_tracing ctxt (fn () => + "Resolving clause: " ^ Display.string_of_thm ctxt c1 ^ + " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c1) ^ + ")\nwith clause: " ^ Display.string_of_thm ctxt c2 ^ + " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c2) ^ ")") + + (* 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 _ = + cond_tracing ctxt + (fn () => "Resolution theorem: " ^ Display.string_of_thm ctxt res_thm) + + (* 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 _ = + cond_tracing ctxt (fn () => + "Resulting clause: " ^ Display.string_of_thm ctxt c_new ^ + " (hyps: " ^ + ML_Syntax.print_list (Syntax.string_of_term ctxt) (Thm.hyps_of c_new) ^ ")") + + 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 _ = cond_tracing ctxt (fn () => "Using original clause #" ^ string_of_int id) + 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 _ = cond_tracing ctxt (fn () => "Proving clause #" ^ string_of_int id ^ " ...") + 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 _ = + cond_tracing ctxt + (fn () => "Replay chain successful; clause stored at #" ^ string_of_int id) + in + clause + end) + + val _ = counter := 0 + val empty_clause = fst (prove_clause empty_id) + val _ = + cond_tracing ctxt (fn () => + "Proof reconstruction successful; " ^ + string_of_int (!counter) ^ " resolution step(s) total.") + 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 _ = + cond_tracing ctxt (fn () => + "Sorted non-trivial clauses:\n" ^ + cat_lines (map (Syntax.string_of_term ctxt o Thm.term_of) sorted_clauses)) + (* 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 _ = + cond_tracing ctxt + (fn () => "Invoking SAT solver on clauses:\n" ^ cat_lines (map string_of_prop_formula fms)) + val fm = Prop_Logic.all fms + fun make_quick_and_dirty_thm () = + let + val _ = + cond_tracing ctxt + (fn () => "quick_and_dirty is set: proof reconstruction skipped, using oracle instead") + 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 = Config.get ctxt solver + in (tracing ("Invoking solver " ^ the_solver); SatSolver.invoke_solver the_solver fm) end + of + SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => + (cond_tracing ctxt (fn () => + "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); + 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; diff -r 7ddb889e23bd -r ef601c60ccbe src/HOL/Tools/sat_funcs.ML --- a/src/HOL/Tools/sat_funcs.ML Sat Feb 01 20:38:29 2014 +0000 +++ /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; diff -r 7ddb889e23bd -r ef601c60ccbe src/HOL/ex/SAT_Examples.thy --- a/src/HOL/ex/SAT_Examples.thy Sat Feb 01 20:38:29 2014 +0000 +++ b/src/HOL/ex/SAT_Examples.thy Sat Feb 01 22:02:20 2014 +0100 @@ -3,14 +3,17 @@ Copyright 2005-2009 *) -header {* Examples for the 'sat' and 'satx' tactic *} +header {* Examples for proof methods "sat" and "satx" *} theory SAT_Examples imports Main begin -(* ML {* sat.solver := "zchaff_with_proofs"; *} *) -(* ML {* sat.solver := "minisat_with_proofs"; *} *) -ML {* sat.trace_sat := true; *} +(* +declare [[sat_solver = zchaff_with_proofs]] +declare [[sat_solver = minisat_with_proofs]] +*) + +declare [[sat_trace]] declare [[quick_and_dirty]] lemma "True" @@ -24,13 +27,13 @@ lemma "(a & b) | (c & d) \ (a & b) | (c & d)" (* -apply (tactic {* cnf.cnf_rewrite_tac 1 *}) +apply (tactic {* CNF.cnf_rewrite_tac @{context} 1 *}) *) by sat lemma "(a & b) | (c & d) \ (a & b) | (c & d)" (* -apply (tactic {* cnf.cnfx_rewrite_tac 1 *}) +apply (tactic {* CNF.cnfx_rewrite_tac @{context} 1 *}) apply (erule exE | erule conjE)+ *) by satx @@ -38,14 +41,14 @@ lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q) \ (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 @{context} 1 *}) *) by sat lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q) \ (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 @{context} 1 *}) apply (erule exE | erule conjE)+ *) by satx @@ -77,11 +80,11 @@ lemma "(ALL x. P x) | ~ All P" by sat -ML {* sat.trace_sat := false; *} +declare [[sat_trace = 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 *) @@ -519,27 +522,25 @@ the number of resolution steps in the proof. *} -(* ML {* -sat.solver := "zchaff_with_proofs"; -sat.trace_sat := false; -*} +(* +declare [[sat_solver = zchaff_with_proofs]] +declare [[sat_trace = 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