src/HOL/Tools/sat_funcs.ML
changeset 32232 6c394343360f
parent 32231 95b8afcbb0ed
child 32283 3bebc195c124
     1.1 --- a/src/HOL/Tools/sat_funcs.ML	Mon Jul 27 20:45:40 2009 +0200
     1.2 +++ b/src/HOL/Tools/sat_funcs.ML	Mon Jul 27 23:17:40 2009 +0200
     1.3 @@ -48,16 +48,16 @@
     1.4  
     1.5  signature SAT =
     1.6  sig
     1.7 -	val trace_sat  : bool ref    (* input: print trace messages *)
     1.8 -	val solver     : string ref  (* input: name of SAT solver to be used *)
     1.9 -	val counter    : int ref     (* output: number of resolution steps during last proof replay *)
    1.10 -	val rawsat_thm : cterm list -> thm
    1.11 -	val rawsat_tac : int -> Tactical.tactic
    1.12 -	val sat_tac    : int -> Tactical.tactic
    1.13 -	val satx_tac   : int -> Tactical.tactic
    1.14 +	val trace_sat: bool ref    (* input: print trace messages *)
    1.15 +	val solver: string ref  (* input: name of SAT solver to be used *)
    1.16 +	val counter: int ref     (* output: number of resolution steps during last proof replay *)
    1.17 +	val rawsat_thm: cterm list -> thm
    1.18 +	val rawsat_tac: Proof.context -> int -> tactic
    1.19 +	val sat_tac: Proof.context -> int -> tactic
    1.20 +	val satx_tac: Proof.context -> int -> tactic
    1.21  end
    1.22  
    1.23 -functor SATFunc (structure cnf : CNF) : SAT =
    1.24 +functor SATFunc(cnf : CNF) : SAT =
    1.25  struct
    1.26  
    1.27  val trace_sat = ref false;
    1.28 @@ -410,7 +410,8 @@
    1.29  (*      or "True"                                                            *)
    1.30  (* ------------------------------------------------------------------------- *)
    1.31  
    1.32 -fun rawsat_tac i = OldGoals.METAHYPS (fn prems => rtac (rawsat_thm (map cprop_of prems)) 1) i;
    1.33 +fun rawsat_tac ctxt i =
    1.34 +  FOCUS (fn {prems, ...} => rtac (rawsat_thm (map cprop_of prems)) 1) ctxt i;
    1.35  
    1.36  (* ------------------------------------------------------------------------- *)
    1.37  (* pre_cnf_tac: converts the i-th subgoal                                    *)
    1.38 @@ -436,8 +437,8 @@
    1.39  (*      subgoal                                                              *)
    1.40  (* ------------------------------------------------------------------------- *)
    1.41  
    1.42 -fun cnfsat_tac i =
    1.43 -	(etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac i);
    1.44 +fun cnfsat_tac ctxt i =
    1.45 +	(etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac ctxt i);
    1.46  
    1.47  (* ------------------------------------------------------------------------- *)
    1.48  (* cnfxsat_tac: checks if the empty clause "False" occurs among the          *)
    1.49 @@ -446,9 +447,9 @@
    1.50  (*      then applies 'rawsat_tac' to solve the subgoal                       *)
    1.51  (* ------------------------------------------------------------------------- *)
    1.52  
    1.53 -fun cnfxsat_tac i =
    1.54 +fun cnfxsat_tac ctxt i =
    1.55  	(etac FalseE i) ORELSE
    1.56 -		(REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac i);
    1.57 +		(REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac ctxt i);
    1.58  
    1.59  (* ------------------------------------------------------------------------- *)
    1.60  (* sat_tac: tactic for calling an external SAT solver, taking as input an    *)
    1.61 @@ -456,8 +457,8 @@
    1.62  (*      an exponential blowup.                                               *)
    1.63  (* ------------------------------------------------------------------------- *)
    1.64  
    1.65 -fun sat_tac i =
    1.66 -	pre_cnf_tac i THEN cnf.cnf_rewrite_tac i THEN cnfsat_tac i;
    1.67 +fun sat_tac ctxt i =
    1.68 +	pre_cnf_tac i THEN cnf.cnf_rewrite_tac ctxt i THEN cnfsat_tac ctxt i;
    1.69  
    1.70  (* ------------------------------------------------------------------------- *)
    1.71  (* satx_tac: tactic for calling an external SAT solver, taking as input an   *)
    1.72 @@ -465,7 +466,7 @@
    1.73  (*      introducing new literals.                                            *)
    1.74  (* ------------------------------------------------------------------------- *)
    1.75  
    1.76 -fun satx_tac i =
    1.77 -	pre_cnf_tac i THEN cnf.cnfx_rewrite_tac i THEN cnfxsat_tac i;
    1.78 +fun satx_tac ctxt i =
    1.79 +	pre_cnf_tac i THEN cnf.cnfx_rewrite_tac ctxt i THEN cnfxsat_tac ctxt i;
    1.80  
    1.81  end;