# HG changeset patch # User blanchet # Date 1325611998 -3600 # Node ID a00685a18e556cc0ac2fe5e96a7daa35b996e69a # Parent cd5c72462bca86f36f64d4c4e08c54682ac6c901 tuned Refute diff -r cd5c72462bca -r a00685a18e55 src/HOL/SAT.thy --- a/src/HOL/SAT.thy Tue Jan 03 18:33:18 2012 +0100 +++ b/src/HOL/SAT.thy Tue Jan 03 18:33:18 2012 +0100 @@ -13,18 +13,6 @@ "Tools/sat_funcs.ML" begin -text {* \medskip Late package setup: default values for refute, see - also theory @{theory Refute}. *} - -refute_params - ["itself"=1, - minsize=1, - maxsize=8, - maxvars=10000, - maxtime=60, - satsolver="auto", - no_assms="false"] - ML {* structure sat = SATFunc(cnf) *} method_setup sat = {* Scan.succeed (SIMPLE_METHOD' o sat.sat_tac) *} diff -r cd5c72462bca -r a00685a18e55 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Tue Jan 03 18:33:18 2012 +0100 +++ b/src/HOL/Tools/refute.ML Tue Jan 03 18:33:18 2012 +0100 @@ -204,6 +204,15 @@ wellformed: prop_formula }; +val default_parameters = + [("itself", "1"), + ("minsize", "1"), + ("maxsize", "8"), + ("maxvars", "10000"), + ("maxtime", "60"), + ("satsolver", "auto"), + ("no_assms", "false")] + |> Symtab.make structure Data = Theory_Data ( @@ -213,7 +222,8 @@ printers: (string * (Proof.context -> model -> typ -> interpretation -> (int -> bool) -> term option)) list, parameters: string Symtab.table}; - val empty = {interpreters = [], printers = [], parameters = Symtab.empty}; + val empty = + {interpreters = [], printers = [], parameters = default_parameters}; val extend = I; fun merge ({interpreters = in1, printers = pr1, parameters = pa1}, @@ -417,7 +427,7 @@ (* denotes membership to an axiomatic type class *) (* ------------------------------------------------------------------------- *) -fun is_const_of_class thy (s, T) = +fun is_const_of_class thy (s, _) = let val class_const_names = map Logic.const_of_class (Sign.all_classes thy) in @@ -446,7 +456,7 @@ (* operator of an inductive datatype in 'thy' *) (* ------------------------------------------------------------------------- *) -fun is_IDT_recursor thy (s, T) = +fun is_IDT_recursor thy (s, _) = let val rec_names = Symtab.fold (append o #rec_names o snd) (Datatype.get_all thy) [] @@ -625,7 +635,7 @@ (* unfold the constant if there is a defining equation *) else case get_def thy (s, T) of - SOME (axname, rhs) => + SOME ((*axname*) _, rhs) => (* Note: if the term to be unfolded (i.e. 'Const (s, T)') *) (* occurs on the right-hand side of the equation, i.e. in *) (* 'rhs', we must not use this equation to unfold, because *) @@ -721,7 +731,7 @@ | Type ("itself", [T1]) => collect_type_axioms T1 axs | Type (s, Ts) => (case Datatype.get_info thy s of - SOME info => (* inductive datatype *) + SOME _ => (* inductive datatype *) (* only collect relevant type axioms for the argument types *) fold collect_type_axioms Ts axs | NONE => @@ -972,7 +982,7 @@ (* enumerates all int lists with a fixed length, where 0<=x<='max' for *) (* all list elements x (unless 'max'<0) *) (* int -> int -> int -> int list -> int list option *) - fun next max len sum [] = + fun next _ _ _ [] = NONE | next max len sum [x] = (* we've reached the last list element, so there's no shift possible *) @@ -1243,7 +1253,7 @@ strip_all_vars t | strip_all_vars (Const (@{const_name All}, _) $ Abs (a, T, t)) = (a, T) :: strip_all_vars t - | strip_all_vars t = [] : (string * typ) list + | strip_all_vars _ = [] : (string * typ) list val strip_t = strip_all_body ex_closure val frees = Term.rename_wrt_term strip_t (strip_all_vars ex_closure) val subst_t = Term.subst_bounds (map Free frees, strip_t) @@ -1470,10 +1480,6 @@ prop_formula_list_dot_product_interpretation_list (fms,trees)) | prop_formula_list_dot_product_interpretation_list (_,_) = raise REFUTE ("interpretation_apply", "empty list (in dot product)") - (* concatenates 'x' with every list in 'xss', returning a new list of *) - (* lists *) - (* 'a -> 'a list list -> 'a list list *) - fun cons_list x xss = map (cons x) xss (* returns a list of lists, each one consisting of one element from each *) (* element of 'xss' *) (* 'a list list -> 'a list list *) @@ -1535,7 +1541,6 @@ fun stlc_interpreter ctxt model args t = let - val thy = Proof_Context.theory_of ctxt val (typs, terms) = model val {maxvars, def_eq, next_idx, bounds, wellformed} = args (* Term.typ -> (interpretation * model * arguments) option *) @@ -1616,7 +1621,7 @@ | Free (_, T) => interpret_groundterm T | Var (_, T) => interpret_groundterm T | Bound i => SOME (nth (#bounds args) i, model, args) - | Abs (x, T, body) => + | Abs (_, T, body) => let (* create all constants of type 'T' *) val constants = make_constants ctxt model T @@ -1679,7 +1684,7 @@ SOME ((if #def_eq args then make_def_equality else make_equality) (i1, i2), m2, a2) end - | Const (@{const_name "=="}, _) $ t1 => + | Const (@{const_name "=="}, _) $ _ => SOME (interpret ctxt model args (eta_expand t 1)) | Const (@{const_name "=="}, _) => SOME (interpret ctxt model args (eta_expand t 2)) @@ -1693,7 +1698,7 @@ in SOME (Leaf [fmTrue, fmFalse], m2, a2) end - | Const (@{const_name "==>"}, _) $ t1 => + | Const (@{const_name "==>"}, _) $ _ => SOME (interpret ctxt model args (eta_expand t 1)) | Const (@{const_name "==>"}, _) => SOME (interpret ctxt model args (eta_expand t 2)) @@ -1759,7 +1764,7 @@ in SOME (make_equality (i1, i2), m2, a2) end - | Const (@{const_name HOL.eq}, _) $ t1 => + | Const (@{const_name HOL.eq}, _) $ _ => SOME (interpret ctxt model args (eta_expand t 1)) | Const (@{const_name HOL.eq}, _) => SOME (interpret ctxt model args (eta_expand t 2)) @@ -1773,7 +1778,7 @@ in SOME (Leaf [fmTrue, fmFalse], m2, a2) end - | Const (@{const_name HOL.conj}, _) $ t1 => + | Const (@{const_name HOL.conj}, _) $ _ => SOME (interpret ctxt model args (eta_expand t 1)) | Const (@{const_name HOL.conj}, _) => SOME (interpret ctxt model args (eta_expand t 2)) @@ -1790,7 +1795,7 @@ in SOME (Leaf [fmTrue, fmFalse], m2, a2) end - | Const (@{const_name HOL.disj}, _) $ t1 => + | Const (@{const_name HOL.disj}, _) $ _ => SOME (interpret ctxt model args (eta_expand t 1)) | Const (@{const_name HOL.disj}, _) => SOME (interpret ctxt model args (eta_expand t 2)) @@ -1807,7 +1812,7 @@ in SOME (Leaf [fmTrue, fmFalse], m2, a2) end - | Const (@{const_name HOL.implies}, _) $ t1 => + | Const (@{const_name HOL.implies}, _) $ _ => SOME (interpret ctxt model args (eta_expand t 1)) | Const (@{const_name HOL.implies}, _) => SOME (interpret ctxt model args (eta_expand t 2)) @@ -2053,7 +2058,7 @@ [] => (* 'Const (s, T)' is not a constructor of this datatype *) NONE - | (_, ctypes)::cs => + | (_, ctypes)::_ => let (* int option -- only /recursive/ IDTs have an associated *) (* depth *) @@ -2144,7 +2149,7 @@ let fun search (x::xs) (y::ys) = if x = y then search xs ys else search (x::xs) ys - | search (x::xs) [] = + | search (_::_) [] = raise REFUTE ("IDT_constructor_interpreter", "element order not preserved") | search [] _ = () @@ -2471,7 +2476,7 @@ | rec_intr (Datatype.DtRec _) (Node _) = raise REFUTE ("IDT_recursion_interpreter", "interpretation for IDT is a node") - | rec_intr (Datatype.DtType ("fun", [dt1, dt2])) (Node xs) = + | rec_intr (Datatype.DtType ("fun", [_, dt2])) (Node xs) = (* recursive argument is something like *) (* "\x::dt1. rec_? params (elem x)" *) Node (map (rec_intr dt2) xs) @@ -2518,7 +2523,7 @@ fun set_interpreter ctxt model args t = let - val (typs, terms) = model + val (_, terms) = model in case AList.lookup (op =) terms t of SOME intr => @@ -2534,7 +2539,7 @@ (* 'op :' == application *) | Const (@{const_name Set.member}, _) $ t1 $ t2 => SOME (interpret ctxt model args (t2 $ t1)) - | Const (@{const_name Set.member}, _) $ t1 => + | Const (@{const_name Set.member}, _) $ _ => SOME (interpret ctxt model args (eta_expand t 1)) | Const (@{const_name Set.member}, _) => SOME (interpret ctxt model args (eta_expand t 2)) @@ -2592,7 +2597,7 @@ fun Finite_Set_finite_interpreter ctxt model args t = case t of Const (@{const_name Finite_Set.finite}, - Type ("fun", [Type ("fun", [T, @{typ bool}]), + Type ("fun", [Type ("fun", [_, @{typ bool}]), @{typ bool}])) $ _ => (* we only consider finite models anyway, hence EVERY set is *) (* "finite" *)