comments fixed, member function renamed
authorwebertj
Thu Jul 20 14:34:57 2006 +0200 (2006-07-20)
changeset 201706ff853f82d73
parent 20169 52173f7687fd
child 20171 424739228123
comments fixed, member function renamed
src/HOL/Tools/sat_funcs.ML
     1.1 --- a/src/HOL/Tools/sat_funcs.ML	Wed Jul 19 23:22:22 2006 +0200
     1.2 +++ b/src/HOL/Tools/sat_funcs.ML	Thu Jul 20 14:34:57 2006 +0200
     1.3 @@ -43,16 +43,6 @@
     1.4    dependent) configuration settings.  To replay SAT proofs in Isabelle, you
     1.5    must of course use a proof-producing SAT solver in the first place.
     1.6  
     1.7 -  Notes for the current revision:
     1.8 -   - Currently zChaff is the only proof-producing SAT solver that is supported.
     1.9 -   - The environment variable ZCHAFF_HOME must be set to point to the directory
    1.10 -     where the zChaff executable resides.
    1.11 -   - The environment variable ZCHAFF_VERSION must be set according to the
    1.12 -     version of zChaff used.  Current supported version of zChaff:
    1.13 -     zChaff version 2004.11.15
    1.14 -   - zChaff must have been compiled with proof generation enabled
    1.15 -     (#define VERIFY_ON).
    1.16 -
    1.17    Proofs are replayed only if "!quick_and_dirty" is false.  If
    1.18    "!quick_and_dirty" is true, the theorem (in case the SAT solver claims its
    1.19    negation to be unsatisfiable) is proved via an oracle.
    1.20 @@ -72,7 +62,7 @@
    1.21  
    1.22  val trace_sat = ref false;
    1.23  
    1.24 -val solver = ref "zchaff_with_proofs";
    1.25 +val solver = ref "zchaff_with_proofs";  (* see HOL/Tools/sat_solver.ML for possible values *)
    1.26  
    1.27  val counter = ref 0;
    1.28  
    1.29 @@ -101,8 +91,7 @@
    1.30  (*      and then perform resolution with                                     *)
    1.31  (*        [| ?P ==> False; ~?P ==> False |] ==> False                        *)
    1.32  (*      to produce                                                           *)
    1.33 -(*        [| y1; ...; x1; ...; xn; ...; yn |] ==> False                      *)
    1.34 -(*      amd finally remove duplicate literals.                               *)
    1.35 +(*        x1; ...; xn; y1; ...; ym |- False                                  *)
    1.36  (* ------------------------------------------------------------------------- *)
    1.37  
    1.38  (* Thm.thm list -> Thm.thm *)
    1.39 @@ -119,14 +108,14 @@
    1.40  
    1.41  		(* see the comments on the term order below for why this implementation is sound *)
    1.42  		(* (Term.term * Term.term -> order) -> Thm.cterm list -> Term.term -> Thm.cterm option *)
    1.43 -		fun member _   []      _ = NONE
    1.44 -		  | member ord (y::ys) x = (case term_of y of  (* "un-certifying" y is faster than certifying x *)
    1.45 +		fun member' _   []      _ = NONE
    1.46 +		  | member' ord (y::ys) x = (case term_of y of  (* "un-certifying" y is faster than certifying x *)
    1.47  			  Const ("Trueprop", _) $ y' =>
    1.48  				(* compare the order *)
    1.49  				(case ord (x, y') of
    1.50  				  LESS    => NONE
    1.51  				| EQUAL   => SOME y
    1.52 -				| GREATER => member ord ys x)
    1.53 +				| GREATER => member' ord ys x)
    1.54  			| _                         =>
    1.55  				(* no need to continue in this case *)
    1.56  				NONE)
    1.57 @@ -142,7 +131,7 @@
    1.58  			  Const ("Trueprop", _) $ lit =>
    1.59  				(* hyps are implemented as ordered list in the kernel, and *)
    1.60  				(* stripping 'Trueprop' should not change the order        *)
    1.61 -				(case member Term.fast_term_ord ys (dual lit) of
    1.62 +				(case member' Term.fast_term_ord ys (dual lit) of
    1.63  				  SOME y => (x, y)
    1.64  				| NONE   => res_hyps xs ys)
    1.65  			| _ =>