summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | webertj |

Thu, 20 Jul 2006 14:34:57 +0200 | |

changeset 20170 | 6ff853f82d73 |

parent 20169 | 52173f7687fd |

child 20171 | 424739228123 |

comments fixed, member function renamed

--- a/src/HOL/Tools/sat_funcs.ML Wed Jul 19 23:22:22 2006 +0200 +++ b/src/HOL/Tools/sat_funcs.ML Thu Jul 20 14:34:57 2006 +0200 @@ -43,16 +43,6 @@ dependent) configuration settings. To replay SAT proofs in Isabelle, you must of course use a proof-producing SAT solver in the first place. - Notes for the current revision: - - Currently zChaff is the only proof-producing SAT solver that is supported. - - The environment variable ZCHAFF_HOME must be set to point to the directory - where the zChaff executable resides. - - The environment variable ZCHAFF_VERSION must be set according to the - version of zChaff used. Current supported version of zChaff: - zChaff version 2004.11.15 - - zChaff must have been compiled with proof generation enabled - (#define VERIFY_ON). - 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. @@ -72,7 +62,7 @@ val trace_sat = ref false; -val solver = ref "zchaff_with_proofs"; +val solver = ref "zchaff_with_proofs"; (* see HOL/Tools/sat_solver.ML for possible values *) val counter = ref 0; @@ -101,8 +91,7 @@ (* and then perform resolution with *) (* [| ?P ==> False; ~?P ==> False |] ==> False *) (* to produce *) -(* [| y1; ...; x1; ...; xn; ...; yn |] ==> False *) -(* amd finally remove duplicate literals. *) +(* x1; ...; xn; y1; ...; ym |- False *) (* ------------------------------------------------------------------------- *) (* Thm.thm list -> Thm.thm *) @@ -119,14 +108,14 @@ (* see the comments on the term order below for why this implementation is sound *) (* (Term.term * Term.term -> order) -> Thm.cterm list -> Term.term -> Thm.cterm option *) - fun member _ [] _ = NONE - | member ord (y::ys) x = (case term_of y of (* "un-certifying" y is faster than certifying x *) + fun member' _ [] _ = NONE + | member' ord (y::ys) x = (case term_of y of (* "un-certifying" y is faster than certifying x *) Const ("Trueprop", _) $ y' => (* compare the order *) (case ord (x, y') of LESS => NONE | EQUAL => SOME y - | GREATER => member ord ys x) + | GREATER => member' ord ys x) | _ => (* no need to continue in this case *) NONE) @@ -142,7 +131,7 @@ Const ("Trueprop", _) $ lit => (* hyps are implemented as ordered list in the kernel, and *) (* stripping 'Trueprop' should not change the order *) - (case member Term.fast_term_ord ys (dual lit) of + (case member' Term.fast_term_ord ys (dual lit) of SOME y => (x, y) | NONE => res_hyps xs ys) | _ =>