# HG changeset patch # User wenzelm # Date 1248731015 -7200 # Node ID a60f183eb63edd4a7dfca6116f97ff551ba81fb9 # Parent 6c394343360f382d21507acd567eac9d8197ec9e# Parent 2a3ffaf00de4ba1789c9a9c9cecddbedc4631627 merged diff -r 2a3ffaf00de4 -r a60f183eb63e src/HOL/SAT.thy --- a/src/HOL/SAT.thy Mon Jul 27 23:02:11 2009 +0200 +++ b/src/HOL/SAT.thy Mon Jul 27 23:43:35 2009 +0200 @@ -25,12 +25,12 @@ maxtime=60, satsolver="auto"] -ML {* structure sat = SATFunc(structure cnf = cnf); *} +ML {* structure sat = SATFunc(cnf) *} -method_setup sat = {* Scan.succeed (K (SIMPLE_METHOD' sat.sat_tac)) *} +method_setup sat = {* Scan.succeed (SIMPLE_METHOD' o sat.sat_tac) *} "SAT solver" -method_setup satx = {* Scan.succeed (K (SIMPLE_METHOD' sat.satx_tac)) *} +method_setup satx = {* Scan.succeed (SIMPLE_METHOD' o sat.satx_tac) *} "SAT solver (with definitional CNF)" end diff -r 2a3ffaf00de4 -r a60f183eb63e src/HOL/Tools/cnf_funcs.ML --- a/src/HOL/Tools/cnf_funcs.ML Mon Jul 27 23:02:11 2009 +0200 +++ b/src/HOL/Tools/cnf_funcs.ML Mon Jul 27 23:43:35 2009 +0200 @@ -33,19 +33,20 @@ signature CNF = sig - val is_atom : Term.term -> bool - val is_literal : Term.term -> bool - val is_clause : Term.term -> bool - val clause_is_trivial : Term.term -> bool + 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 -> Thm.thm + val clause2raw_thm: thm -> thm - val weakening_tac : int -> Tactical.tactic (* removes the first hypothesis of a subgoal *) + val weakening_tac: int -> tactic (* removes the first hypothesis of a subgoal *) - val make_cnf_thm : theory -> Term.term -> Thm.thm - val make_cnfx_thm : theory -> Term.term -> Thm.thm - val cnf_rewrite_tac : int -> Tactical.tactic (* converts all prems of a subgoal to CNF *) - val cnfx_rewrite_tac : int -> Tactical.tactic (* converts all prems of a subgoal to (almost) definitional CNF *) + val make_cnf_thm: theory -> term -> thm + val make_cnfx_thm: theory -> 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 = @@ -505,8 +506,6 @@ (* weakening_tac: removes the first hypothesis of the 'i'-th subgoal *) (* ------------------------------------------------------------------------- *) -(* int -> Tactical.tactic *) - fun weakening_tac i = dtac weakening_thm i THEN atac (i+1); @@ -516,17 +515,16 @@ (* premise) *) (* ------------------------------------------------------------------------- *) -(* int -> Tactical.tactic *) - -fun cnf_rewrite_tac i = +fun cnf_rewrite_tac ctxt i = (* cut the CNF formulas as new premises *) - OldGoals.METAHYPS (fn prems => + FOCUS (fn {prems, ...} => let - val cnf_thms = map (fn pr => make_cnf_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems + val thy = ProofContext.theory_of ctxt + val cnf_thms = map (make_cnf_thm thy 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) i + end) ctxt i (* remove the original premises *) THEN SELECT_GOAL (fn thm => let @@ -540,17 +538,16 @@ (* (possibly introducing new literals) *) (* ------------------------------------------------------------------------- *) -(* int -> Tactical.tactic *) - -fun cnfx_rewrite_tac i = +fun cnfx_rewrite_tac ctxt i = (* cut the CNF formulas as new premises *) - OldGoals.METAHYPS (fn prems => + FOCUS (fn {prems, ...} => let - val cnfx_thms = map (fn pr => make_cnfx_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems + val thy = ProofContext.theory_of ctxt; + val cnfx_thms = map (make_cnfx_thm thy 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) i + end) ctxt i (* remove the original premises *) THEN SELECT_GOAL (fn thm => let diff -r 2a3ffaf00de4 -r a60f183eb63e src/HOL/Tools/sat_funcs.ML --- a/src/HOL/Tools/sat_funcs.ML Mon Jul 27 23:02:11 2009 +0200 +++ b/src/HOL/Tools/sat_funcs.ML Mon Jul 27 23:43:35 2009 +0200 @@ -48,16 +48,16 @@ signature SAT = sig - val trace_sat : bool ref (* input: print trace messages *) - val solver : string ref (* input: name of SAT solver to be used *) - val counter : int ref (* output: number of resolution steps during last proof replay *) - val rawsat_thm : cterm list -> thm - val rawsat_tac : int -> Tactical.tactic - val sat_tac : int -> Tactical.tactic - val satx_tac : int -> Tactical.tactic + val trace_sat: bool ref (* input: print trace messages *) + val solver: string ref (* input: name of SAT solver to be used *) + val counter: int ref (* output: number of resolution steps during last proof replay *) + val rawsat_thm: 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 (structure cnf : CNF) : SAT = +functor SATFunc(cnf : CNF) : SAT = struct val trace_sat = ref false; @@ -410,7 +410,8 @@ (* or "True" *) (* ------------------------------------------------------------------------- *) -fun rawsat_tac i = OldGoals.METAHYPS (fn prems => rtac (rawsat_thm (map cprop_of prems)) 1) i; +fun rawsat_tac ctxt i = + FOCUS (fn {prems, ...} => rtac (rawsat_thm (map cprop_of prems)) 1) ctxt i; (* ------------------------------------------------------------------------- *) (* pre_cnf_tac: converts the i-th subgoal *) @@ -436,8 +437,8 @@ (* subgoal *) (* ------------------------------------------------------------------------- *) -fun cnfsat_tac i = - (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac i); +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 *) @@ -446,9 +447,9 @@ (* then applies 'rawsat_tac' to solve the subgoal *) (* ------------------------------------------------------------------------- *) -fun cnfxsat_tac i = +fun cnfxsat_tac ctxt i = (etac FalseE i) ORELSE - (REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac i); + (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 *) @@ -456,8 +457,8 @@ (* an exponential blowup. *) (* ------------------------------------------------------------------------- *) -fun sat_tac i = - pre_cnf_tac i THEN cnf.cnf_rewrite_tac i THEN cnfsat_tac i; +fun sat_tac ctxt i = + pre_cnf_tac 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 *) @@ -465,7 +466,7 @@ (* introducing new literals. *) (* ------------------------------------------------------------------------- *) -fun satx_tac i = - pre_cnf_tac i THEN cnf.cnfx_rewrite_tac i THEN cnfxsat_tac i; +fun satx_tac ctxt i = + pre_cnf_tac i THEN cnf.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i; end; diff -r 2a3ffaf00de4 -r a60f183eb63e src/HOL/ex/SAT_Examples.thy --- a/src/HOL/ex/SAT_Examples.thy Mon Jul 27 23:02:11 2009 +0200 +++ b/src/HOL/ex/SAT_Examples.thy Mon Jul 27 23:43:35 2009 +0200 @@ -83,7 +83,7 @@ ML {* reset quick_and_dirty; *} method_setup rawsat = - {* Scan.succeed (K (SIMPLE_METHOD' sat.rawsat_tac)) *} + {* Scan.succeed (SIMPLE_METHOD' o sat.rawsat_tac) *} "SAT solver (no preprocessing)" (* ML {* Toplevel.profiling := 1; *} *)