# HG changeset patch # User blanchet # Date 1279739818 -7200 # Node ID 24785fa2416cf2a33d8ee45b31738198e56eafda # Parent 29cacb2c2184741c2f8c687c09bdb1b1be58d6ee do a better job at Skolemizing in Nitpick, for TPTP FOF diff -r 29cacb2c2184 -r 24785fa2416c src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Jul 21 21:15:49 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Jul 21 21:16:58 2010 +0200 @@ -492,7 +492,6 @@ else 0 val settings = [("solver", commas_quote kodkod_sat_solver), - ("skolem_depth", "-1"), ("bit_width", string_of_int bit_width), ("symmetry_breaking", "20"), ("sharing", "3"), diff -r 29cacb2c2184 -r 24785fa2416c src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Wed Jul 21 21:15:49 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Wed Jul 21 21:16:58 2010 +0200 @@ -547,59 +547,74 @@ skolem_depth = let val incrs = map (Integer.add 1) - fun aux ss Ts js depth polar t = + fun aux ss Ts js skolemizable polar t = let fun do_quantifier quant_s quant_T abs_s abs_T t = - if not (loose_bvar1 (t, 0)) then - aux ss Ts js depth polar (incr_boundvars ~1 t) - else if depth <= skolem_depth andalso - is_positive_existential polar quant_s then - let - val j = length (!skolems) + 1 - val sko_s = skolem_prefix_for (length js) j ^ abs_s - val _ = Unsynchronized.change skolems (cons (sko_s, ss)) - val sko_t = list_comb (Const (sko_s, rev Ts ---> abs_T), - map Bound (rev js)) - val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t) - in - if null js then s_betapply Ts (abs_t, sko_t) - else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t - end - else - Const (quant_s, quant_T) - $ Abs (abs_s, abs_T, - if is_higher_order_type abs_T then - t + (if not (loose_bvar1 (t, 0)) then + aux ss Ts js skolemizable polar (incr_boundvars ~1 t) + else if is_positive_existential polar quant_s then + let + val j = length (!skolems) + 1 + val (js', (ss', Ts')) = + js ~~ (ss ~~ Ts) + |> filter (fn (j, _) => loose_bvar1 (t, j + 1)) + |> ListPair.unzip ||> ListPair.unzip + in + if skolemizable andalso length js' <= skolem_depth then + let + val sko_s = skolem_prefix_for (length js') j ^ abs_s + val _ = Unsynchronized.change skolems (cons (sko_s, ss')) + val sko_t = list_comb (Const (sko_s, rev Ts' ---> abs_T), + map Bound (rev js')) + val abs_t = Abs (abs_s, abs_T, + aux ss Ts (incrs js) skolemizable polar t) + in + if null js' then + s_betapply Ts (abs_t, sko_t) else - aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js) - (depth + 1) polar t) + Const (@{const_name Let}, abs_T --> quant_T) $ sko_t + $ abs_t + end + else + raise SAME () + end + else + raise SAME ()) + handle SAME () => + Const (quant_s, quant_T) + $ Abs (abs_s, abs_T, + if is_higher_order_type abs_T then + t + else + aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js) + skolemizable polar t) in case t of Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) => do_quantifier s0 T0 s1 T1 t1 | @{const "==>"} $ t1 $ t2 => - @{const "==>"} $ aux ss Ts js depth (flip_polarity polar) t1 - $ aux ss Ts js depth polar t2 + @{const "==>"} $ aux ss Ts js skolemizable (flip_polarity polar) t1 + $ aux ss Ts js skolemizable polar t2 | @{const Pure.conjunction} $ t1 $ t2 => - @{const Pure.conjunction} $ aux ss Ts js depth polar t1 - $ aux ss Ts js depth polar t2 + @{const Pure.conjunction} $ aux ss Ts js skolemizable polar t1 + $ aux ss Ts js skolemizable polar t2 | @{const Trueprop} $ t1 => - @{const Trueprop} $ aux ss Ts js depth polar t1 + @{const Trueprop} $ aux ss Ts js skolemizable polar t1 | @{const Not} $ t1 => - @{const Not} $ aux ss Ts js depth (flip_polarity polar) t1 + @{const Not} $ aux ss Ts js skolemizable (flip_polarity polar) t1 | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) => do_quantifier s0 T0 s1 T1 t1 | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) => do_quantifier s0 T0 s1 T1 t1 | @{const "op &"} $ t1 $ t2 => - s_conj (pairself (aux ss Ts js depth polar) (t1, t2)) + s_conj (pairself (aux ss Ts js skolemizable polar) (t1, t2)) | @{const "op |"} $ t1 $ t2 => - s_disj (pairself (aux ss Ts js depth polar) (t1, t2)) + s_disj (pairself (aux ss Ts js skolemizable polar) (t1, t2)) | @{const "op -->"} $ t1 $ t2 => - @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1 - $ aux ss Ts js depth polar t2 + @{const "op -->"} $ aux ss Ts js skolemizable (flip_polarity polar) t1 + $ aux ss Ts js skolemizable polar t2 | (t0 as Const (@{const_name Let}, _)) $ t1 $ t2 => - t0 $ t1 $ aux ss Ts js depth polar t2 + t0 $ t1 $ aux ss Ts js skolemizable polar t2 | Const (x as (s, T)) => if is_inductive_pred hol_ctxt x andalso not (is_well_founded_inductive_pred hol_ctxt x) then @@ -609,7 +624,7 @@ if gfp then (lbfp_prefix, @{const "op |"}) else (ubfp_prefix, @{const "op &"}) fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x - |> aux ss Ts js depth polar + |> aux ss Ts js skolemizable polar fun neg () = Const (pref ^ s, T) in case polar |> gfp ? flip_polarity of @@ -627,12 +642,13 @@ else Const x | t1 $ t2 => - s_betapply Ts (aux ss Ts [] (skolem_depth + 1) polar t1, - aux ss Ts [] depth Neut t2) - | Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1) + s_betapply Ts (aux ss Ts [] false polar t1, + aux ss Ts [] skolemizable Neut t2) + | Abs (s, T, t1) => + Abs (s, T, aux ss Ts (incrs js) skolemizable polar t1) | _ => t end - in aux [] [] [] 0 Pos end + in aux [] [] [] true Pos end (** Function specialization **) @@ -1216,7 +1232,7 @@ (** Preprocessor entry point **) -val max_skolem_depth = 4 +val max_skolem_depth = 3 fun preprocess_term (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs, boxes, ...}) finitizes monos t =