author | webertj |

Thu Jul 20 14:34:57 2006 +0200 (2006-07-20) | |

changeset 20170 | 6ff853f82d73 |

parent 20169 | 52173f7687fd |

child 20171 | 424739228123 |

comments fixed, member function renamed

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 | _ =>