--- a/doc-src/Nitpick/nitpick.tex Mon Feb 21 17:43:23 2011 +0100
+++ b/doc-src/Nitpick/nitpick.tex Mon Feb 21 18:29:47 2011 +0100
@@ -2465,11 +2465,17 @@
{\small See also \textit{debug} (\S\ref{output-format}).}
-\optrue{peephole\_optim}{no\_peephole\_optim}
-Specifies whether Nitpick should simplify the generated Kodkod formulas using a
-peephole optimizer. These optimizations can make a significant difference.
-Unless you are tracking down a bug in Nitpick or distrust the peephole
-optimizer, you should leave this option enabled.
+\opargboolorsmart{preconstr}{term}{dont\_preconstr}
+Specifies whether a datatype value should be preconstructed, meaning Nitpick
+will reserve a Kodkod atom for it. If a value must necessarily belong to the
+subset of representable values that approximates a datatype, preconstructing
+it can speed up the search significantly, especially for high cardinalities. By
+default, Nitpick inspects the conjecture to infer terms that can be
+preconstructed.
+
+\opsmart{preconstr}{dont\_preconstr}
+Specifies the default preconstruction setting to use. This can be overridden on
+a per-term basis using the \textit{preconstr}~\qty{term} option described above.
\opdefault{datatype\_sym\_break}{int}{\upshape 5}
Specifies an upper bound on the number of datatypes for which Nitpick generates
@@ -2483,6 +2489,12 @@
considerably, especially for unsatisfiable problems, but too much of it can slow
it down.
+\optrue{peephole\_optim}{no\_peephole\_optim}
+Specifies whether Nitpick should simplify the generated Kodkod formulas using a
+peephole optimizer. These optimizations can make a significant difference.
+Unless you are tracking down a bug in Nitpick or distrust the peephole
+optimizer, you should leave this option enabled.
+
\opdefault{max\_threads}{int}{\upshape 0}
Specifies the maximum number of threads to use in Kodkod. If this option is set
to 0, Kodkod will compute an appropriate value based on the number of processor
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Mon Feb 21 17:43:23 2011 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Mon Feb 21 18:29:47 2011 +0100
@@ -38,7 +38,7 @@
{thy = thy, ctxt = ctxt, max_bisim_depth = ~1, boxes = [],
stds = stds, wfs = [], user_axioms = NONE, debug = false,
whacks = [], binary_ints = SOME false, destroy_constrs = true,
- specialize = false, star_linear_preds = false,
+ specialize = false, star_linear_preds = false, preconstrs = [],
tac_timeout = NONE, evals = [], case_names = case_names,
def_tables = def_tables, nondef_table = nondef_table,
user_nondefs = user_nondefs, simp_table = simp_table,
@@ -188,7 +188,7 @@
let
val t = th |> prop_of |> Type.legacy_freeze |> close_form
val neg_t = Logic.mk_implies (t, @{prop False})
- val (nondef_ts, def_ts, _, _, _) =
+ val (nondef_ts, def_ts, _, _, _, _) =
time_limit preproc_timeout (preprocess_formulas hol_ctxt []) neg_t
val res = name ^ ": " ^ check_formulas (nondef_ts, def_ts)
in File.append path (res ^ "\n"); writeln res end
--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Feb 21 17:43:23 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Feb 21 18:29:47 2011 +0100
@@ -34,6 +34,7 @@
destroy_constrs: bool,
specialize: bool,
star_linear_preds: bool,
+ preconstrs: (term option * bool option) list,
peephole_optim: bool,
datatype_sym_break: int,
kodkod_sym_break: int,
@@ -107,6 +108,7 @@
destroy_constrs: bool,
specialize: bool,
star_linear_preds: bool,
+ preconstrs: (term option * bool option) list,
peephole_optim: bool,
datatype_sym_break: int,
kodkod_sym_break: int,
@@ -209,10 +211,10 @@
boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
verbose, overlord, user_axioms, assms, whacks, merge_type_vars,
binary_ints, destroy_constrs, specialize, star_linear_preds,
- peephole_optim, datatype_sym_break, kodkod_sym_break, tac_timeout,
- max_threads, show_datatypes, show_consts, evals, formats, atomss,
- max_potential, max_genuine, check_potential, check_genuine, batch_size,
- ...} = params
+ preconstrs, peephole_optim, datatype_sym_break, kodkod_sym_break,
+ tac_timeout, max_threads, show_datatypes, show_consts, evals, formats,
+ atomss, max_potential, max_genuine, check_potential, check_genuine,
+ batch_size, ...} = params
val state_ref = Unsynchronized.ref state
val pprint =
if auto then
@@ -280,21 +282,23 @@
stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
whacks = whacks, binary_ints = binary_ints,
destroy_constrs = destroy_constrs, specialize = specialize,
- star_linear_preds = star_linear_preds, tac_timeout = tac_timeout,
- evals = evals, case_names = case_names, def_tables = def_tables,
- nondef_table = nondef_table, user_nondefs = user_nondefs,
- simp_table = simp_table, psimp_table = psimp_table,
- choice_spec_table = choice_spec_table, intro_table = intro_table,
- ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
- skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
+ star_linear_preds = star_linear_preds, preconstrs = preconstrs,
+ tac_timeout = tac_timeout, evals = evals, case_names = case_names,
+ def_tables = def_tables, nondef_table = nondef_table,
+ user_nondefs = user_nondefs, simp_table = simp_table,
+ psimp_table = psimp_table, choice_spec_table = choice_spec_table,
+ intro_table = intro_table, ground_thm_table = ground_thm_table,
+ ersatz_table = ersatz_table, skolems = Unsynchronized.ref [],
+ special_funs = Unsynchronized.ref [],
unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
constr_cache = Unsynchronized.ref []}
val pseudo_frees = []
val real_frees = fold Term.add_frees (neg_t :: assm_ts) []
val _ = null (fold Term.add_tvars (neg_t :: assm_ts) []) orelse
raise NOT_SUPPORTED "schematic type variables"
- val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms,
- binarize) = preprocess_formulas hol_ctxt assm_ts neg_t
+ val (nondef_ts, def_ts, preconstr_ts, got_all_mono_user_axioms,
+ no_poly_user_axioms, binarize) =
+ preprocess_formulas hol_ctxt assm_ts neg_t
val got_all_user_axioms =
got_all_mono_user_axioms andalso no_poly_user_axioms
@@ -320,8 +324,9 @@
handle TYPE (_, Ts, ts) =>
raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts)
- val nondef_us = map (nut_from_term hol_ctxt Eq) nondef_ts
- val def_us = map (nut_from_term hol_ctxt DefEq) def_ts
+ val nondef_us = nondef_ts |> map (nut_from_term hol_ctxt Eq)
+ val def_us = def_ts |> map (nut_from_term hol_ctxt DefEq)
+ val preconstr_us = preconstr_ts |> map (nut_from_term hol_ctxt Eq)
val (free_names, const_names) =
fold add_free_and_const_names (nondef_us @ def_us) ([], [])
val (sel_names, nonsel_names) =
@@ -506,10 +511,12 @@
(univ_card nat_card int_card main_j0 [] KK.True)
val _ = check_arity guiltiest_party min_univ_card min_highest_arity
- val def_us = map (choose_reps_in_nut scope unsound rep_table true)
- def_us
- val nondef_us = map (choose_reps_in_nut scope unsound rep_table false)
- nondef_us
+ val def_us =
+ def_us |> map (choose_reps_in_nut scope unsound rep_table true)
+ val nondef_us =
+ nondef_us |> map (choose_reps_in_nut scope unsound rep_table false)
+ val preconstr_us =
+ preconstr_us |> map (choose_reps_in_nut scope unsound rep_table false)
(*
val _ = List.app (print_g o string_for_nut ctxt)
(free_names @ sel_names @ nonsel_names @
@@ -521,8 +528,10 @@
rename_free_vars sel_names pool rel_table
val (other_rels, pool, rel_table) =
rename_free_vars nonsel_names pool rel_table
- val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us
- val def_us = map (rename_vars_in_nut pool rel_table) def_us
+ val nondef_us = nondef_us |> map (rename_vars_in_nut pool rel_table)
+ val def_us = def_us |> map (rename_vars_in_nut pool rel_table)
+ val preconstr_us =
+ preconstr_us |> map (rename_vars_in_nut pool rel_table)
val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us
val def_fs = map (kodkod_formula_from_nut ofs kk) def_us
val formula = fold (fold s_and) [def_fs, nondef_fs] KK.True
@@ -548,8 +557,8 @@
val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels
val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels
val dtype_axioms =
- declarative_axioms_for_datatypes hol_ctxt binarize datatype_sym_break
- bits ofs kk rel_table datatypes
+ declarative_axioms_for_datatypes hol_ctxt binarize preconstr_us
+ datatype_sym_break bits ofs kk rel_table datatypes
val declarative_axioms = plain_axioms @ dtype_axioms
val univ_card = Int.max (univ_card nat_card int_card main_j0
(plain_bounds @ sel_bounds) formula,
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 21 17:43:23 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Feb 21 18:29:47 2011 +0100
@@ -27,6 +27,7 @@
destroy_constrs: bool,
specialize: bool,
star_linear_preds: bool,
+ preconstrs: (term option * bool option) list,
tac_timeout: Time.time option,
evals: term list,
case_names: (string * int) list,
@@ -257,6 +258,7 @@
destroy_constrs: bool,
specialize: bool,
star_linear_preds: bool,
+ preconstrs: (term option * bool option) list,
tac_timeout: Time.time option,
evals: term list,
case_names: (string * int) list,
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Feb 21 17:43:23 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Feb 21 18:29:47 2011 +0100
@@ -58,6 +58,7 @@
("destroy_constrs", "true"),
("specialize", "true"),
("star_linear_preds", "true"),
+ ("preconstr", "smart"),
("peephole_optim", "true"),
("datatype_sym_break", "5"),
("kodkod_sym_break", "15"),
@@ -90,6 +91,7 @@
("dont_destroy_constrs", "destroy_constrs"),
("dont_specialize", "specialize"),
("dont_star_linear_preds", "star_linear_preds"),
+ ("dont_preconstr", "preconstr"),
("no_peephole_optim", "peephole_optim"),
("no_debug", "debug"),
("quiet", "verbose"),
@@ -102,11 +104,11 @@
fun is_known_raw_param s =
AList.defined (op =) default_default_params s orelse
AList.defined (op =) negated_params s orelse
- member (op =) ["max", "show_all", "whack", "atoms", "eval", "expect"] s orelse
+ member (op =) ["max", "show_all", "whack", "eval", "atoms", "expect"] s orelse
exists (fn p => String.isPrefix (p ^ " ") s)
["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
- "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format",
- "atoms"]
+ "mono", "non_mono", "std", "non_std", "wf", "non_wf", "preconstr",
+ "dont_preconstr", "format", "atoms"]
fun check_raw_param (s, _) =
if is_known_raw_param s then ()
@@ -251,6 +253,8 @@
val destroy_constrs = lookup_bool "destroy_constrs"
val specialize = lookup_bool "specialize"
val star_linear_preds = lookup_bool "star_linear_preds"
+ val preconstrs =
+ lookup_bool_option_assigns read_term_polymorphic "preconstr"
val peephole_optim = lookup_bool "peephole_optim"
val datatype_sym_break = lookup_int "datatype_sym_break"
val kodkod_sym_break = lookup_int "kodkod_sym_break"
@@ -259,9 +263,9 @@
val max_threads = if auto then 1 else Int.max (0, lookup_int "max_threads")
val show_datatypes = debug orelse lookup_bool "show_datatypes"
val show_consts = debug orelse lookup_bool "show_consts"
+ val evals = lookup_term_list_polymorphic "eval"
val formats = lookup_ints_assigns read_term_polymorphic "format" 0
val atomss = lookup_strings_assigns read_type_polymorphic "atoms"
- val evals = lookup_term_list_polymorphic "eval"
val max_potential =
if auto then 0 else Int.max (0, lookup_int "max_potential")
val max_genuine = Int.max (0, lookup_int "max_genuine")
@@ -281,12 +285,12 @@
user_axioms = user_axioms, assms = assms, whacks = whacks,
merge_type_vars = merge_type_vars, binary_ints = binary_ints,
destroy_constrs = destroy_constrs, specialize = specialize,
- star_linear_preds = star_linear_preds, peephole_optim = peephole_optim,
- datatype_sym_break = datatype_sym_break,
+ star_linear_preds = star_linear_preds, preconstrs = preconstrs,
+ peephole_optim = peephole_optim, datatype_sym_break = datatype_sym_break,
kodkod_sym_break = kodkod_sym_break, timeout = timeout,
tac_timeout = tac_timeout, max_threads = max_threads,
show_datatypes = show_datatypes, show_consts = show_consts,
- formats = formats, atomss = atomss, evals = evals,
+ evals = evals, formats = formats, atomss = atomss,
max_potential = max_potential, max_genuine = max_genuine,
check_potential = check_potential, check_genuine = check_genuine,
batch_size = batch_size, expect = expect}
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Feb 21 17:43:23 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Feb 21 18:29:47 2011 +0100
@@ -29,12 +29,13 @@
val bound_for_sel_rel :
Proof.context -> bool -> datatype_spec list -> nut -> Kodkod.bound
val merge_bounds : Kodkod.bound list -> Kodkod.bound list
+ val kodkod_formula_from_nut :
+ int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula
val declarative_axiom_for_plain_rel : kodkod_constrs -> nut -> Kodkod.formula
val declarative_axioms_for_datatypes :
- hol_context -> bool -> int -> int -> int Typtab.table -> kodkod_constrs
- -> nut NameTable.table -> datatype_spec list -> Kodkod.formula list
- val kodkod_formula_from_nut :
- int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula
+ hol_context -> bool -> nut list -> int -> int -> int Typtab.table
+ -> kodkod_constrs -> nut NameTable.table -> datatype_spec list
+ -> Kodkod.formula list
end;
structure Nitpick_Kodkod : NITPICK_KODKOD =
@@ -646,371 +647,6 @@
(kk_rel_eq (bit_set_from_atom kk T (KK.Var (1, ~1)))
(KK.Bits i))
-fun declarative_axiom_for_plain_rel kk (FreeRel (x, _, R as Func _, nick)) =
- kk_n_ary_function kk (R |> nick = @{const_name List.set} ? unopt_rep)
- (KK.Rel x)
- | declarative_axiom_for_plain_rel ({kk_lone, kk_one, ...} : kodkod_constrs)
- (FreeRel (x, _, R, _)) =
- if is_one_rep R then kk_one (KK.Rel x)
- else if is_lone_rep R andalso card_of_rep R > 1 then kk_lone (KK.Rel x)
- else KK.True
- | declarative_axiom_for_plain_rel _ u =
- raise NUT ("Nitpick_Kodkod.declarative_axiom_for_plain_rel", [u])
-
-fun const_triple rel_table (x as (s, T)) =
- case the_name rel_table (ConstName (s, T, Any)) of
- FreeRel ((n, j), _, R, _) => (KK.Rel (n, j), R, n)
- | _ => raise TERM ("Nitpick_Kodkod.const_triple", [Const x])
-
-fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr
-
-fun nfa_transitions_for_sel hol_ctxt binarize
- ({kk_project, ...} : kodkod_constrs) rel_table
- (dtypes : datatype_spec list) constr_x n =
- let
- val x as (_, T) =
- binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize constr_x n
- val (r, R, arity) = const_triple rel_table x
- val type_schema = type_schema_of_rep T R
- in
- map_filter (fn (j, T) =>
- if forall (not_equal T o #typ) dtypes then NONE
- else SOME ((x, kk_project r (map KK.Num [0, j])), T))
- (index_seq 1 (arity - 1) ~~ tl type_schema)
- end
-fun nfa_transitions_for_constr hol_ctxt binarize kk rel_table dtypes
- (x as (_, T)) =
- maps (nfa_transitions_for_sel hol_ctxt binarize kk rel_table dtypes x)
- (index_seq 0 (num_sels_for_constr_type T))
-fun nfa_entry_for_datatype _ _ _ _ _ ({co = true, ...} : datatype_spec) = NONE
- | nfa_entry_for_datatype _ _ _ _ _ {standard = false, ...} = NONE
- | nfa_entry_for_datatype _ _ _ _ _ {deep = false, ...} = NONE
- | nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes
- {typ, constrs, ...} =
- SOME (typ, maps (nfa_transitions_for_constr hol_ctxt binarize kk rel_table
- dtypes o #const) constrs)
-
-val empty_rel = KK.Product (KK.None, KK.None)
-
-fun direct_path_rel_exprs nfa start_T final_T =
- case AList.lookup (op =) nfa final_T of
- SOME trans => map (snd o fst) (filter (curry (op =) start_T o snd) trans)
- | NONE => []
-and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T
- final_T =
- fold kk_union (direct_path_rel_exprs nfa start_T final_T)
- (if start_T = final_T then KK.Iden else empty_rel)
- | any_path_rel_expr (kk as {kk_union, ...}) nfa (T :: Ts) start_T final_T =
- kk_union (any_path_rel_expr kk nfa Ts start_T final_T)
- (knot_path_rel_expr kk nfa Ts start_T T final_T)
-and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa Ts
- start_T knot_T final_T =
- kk_join (kk_join (any_path_rel_expr kk nfa Ts knot_T final_T)
- (kk_reflexive_closure (loop_path_rel_expr kk nfa Ts knot_T)))
- (any_path_rel_expr kk nfa Ts start_T knot_T)
-and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T =
- fold kk_union (direct_path_rel_exprs nfa start_T start_T) empty_rel
- | loop_path_rel_expr (kk as {kk_union, kk_closure, ...}) nfa (T :: Ts)
- start_T =
- if start_T = T then
- kk_closure (loop_path_rel_expr kk nfa Ts start_T)
- else
- kk_union (loop_path_rel_expr kk nfa Ts start_T)
- (knot_path_rel_expr kk nfa Ts start_T T start_T)
-
-fun add_nfa_to_graph [] = I
- | add_nfa_to_graph ((_, []) :: nfa) = add_nfa_to_graph nfa
- | add_nfa_to_graph ((T, ((_, T') :: transitions)) :: nfa) =
- add_nfa_to_graph ((T, transitions) :: nfa) o Typ_Graph.add_edge (T, T') o
- Typ_Graph.default_node (T', ()) o Typ_Graph.default_node (T, ())
-
-fun strongly_connected_sub_nfas nfa =
- add_nfa_to_graph nfa Typ_Graph.empty
- |> Typ_Graph.strong_conn
- |> map (fn keys => filter (member (op =) keys o fst) nfa)
-
-fun acyclicity_axiom_for_datatype (kk as {kk_no, kk_intersect, ...}) nfa
- start_T =
- kk_no (kk_intersect
- (loop_path_rel_expr kk nfa (pull start_T (map fst nfa)) start_T)
- KK.Iden)
-(* Cycle breaking in the bounds takes care of singly recursive datatypes, hence
- the first equation. *)
-fun acyclicity_axioms_for_datatypes _ [_] = []
- | acyclicity_axioms_for_datatypes kk nfas =
- maps (fn nfa => map (acyclicity_axiom_for_datatype kk nfa o fst) nfa) nfas
-
-fun all_ge ({kk_join, kk_reflexive_closure, ...} : kodkod_constrs) z r =
- kk_join r (kk_reflexive_closure (KK.Rel (suc_rel_for_atom_seq z)))
-fun gt ({kk_subset, kk_join, kk_closure, ...} : kodkod_constrs) z r1 r2 =
- kk_subset r1 (kk_join r2 (kk_closure (KK.Rel (suc_rel_for_atom_seq z))))
-
-fun constr_quadruple ({const = (s, T), delta, epsilon, ...} : constr_spec) =
- (delta, (epsilon, (num_binder_types T, s)))
-val constr_ord =
- prod_ord int_ord (prod_ord int_ord (prod_ord int_ord string_ord))
- o pairself constr_quadruple
-
-fun datatype_ord (({card = card1, self_rec = self_rec1, constrs = constr1, ...},
- {card = card2, self_rec = self_rec2, constrs = constr2, ...})
- : datatype_spec * datatype_spec) =
- prod_ord int_ord (prod_ord bool_ord int_ord)
- ((card1, (self_rec1, length constr1)),
- (card2, (self_rec2, length constr2)))
-
-(* We must absolutely tabulate "suc" for all datatypes whose selector bounds
- break cycles; otherwise, we may end up with two incompatible symmetry
- breaking orders, leading to spurious models. *)
-fun should_tabulate_suc_for_type dtypes T =
- is_asymmetric_nondatatype T orelse
- case datatype_spec dtypes T of
- SOME {self_rec, ...} => self_rec
- | NONE => false
-
-fun lex_order_rel_expr (kk as {kk_implies, kk_and, kk_subset, kk_join, ...})
- dtypes sel_quadruples =
- case sel_quadruples of
- [] => KK.True
- | ((r, Func (Atom _, Atom x), 2), (_, Type (_, [_, T]))) :: sel_quadruples' =>
- let val z = (x, should_tabulate_suc_for_type dtypes T) in
- if null sel_quadruples' then
- gt kk z (kk_join (KK.Var (1, 1)) r) (kk_join (KK.Var (1, 0)) r)
- else
- kk_and (kk_subset (kk_join (KK.Var (1, 1)) r)
- (all_ge kk z (kk_join (KK.Var (1, 0)) r)))
- (kk_implies (kk_subset (kk_join (KK.Var (1, 1)) r)
- (kk_join (KK.Var (1, 0)) r))
- (lex_order_rel_expr kk dtypes sel_quadruples'))
- end
- (* Skip constructors components that aren't atoms, since we cannot compare
- these easily. *)
- | _ :: sel_quadruples' => lex_order_rel_expr kk dtypes sel_quadruples'
-
-fun is_nil_like_constr_type dtypes T =
- case datatype_spec dtypes T of
- SOME {constrs, ...} =>
- (case filter_out (is_self_recursive_constr_type o snd o #const) constrs of
- [{const = (_, T'), ...}] => T = T'
- | _ => false)
- | NONE => false
-
-fun sym_break_axioms_for_constr_pair hol_ctxt binarize
- (kk as {kk_all, kk_or, kk_implies, kk_and, kk_some, kk_intersect,
- kk_join, ...}) rel_table nfas dtypes
- (constr_ord,
- ({const = const1 as (_, T1), delta = delta1, epsilon = epsilon1, ...},
- {const = const2 as (_, _), delta = delta2, epsilon = epsilon2, ...})
- : constr_spec * constr_spec) =
- let
- val dataT = body_type T1
- val nfa = nfas |> find_first (exists (curry (op =) dataT o fst)) |> these
- val rec_Ts = nfa |> map fst
- fun rec_and_nonrec_sels (x as (_, T)) =
- index_seq 0 (num_sels_for_constr_type T)
- |> map (binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize x)
- |> List.partition (member (op =) rec_Ts o range_type o snd)
- val sel_xs1 = rec_and_nonrec_sels const1 |> op @
- in
- if constr_ord = EQUAL andalso null sel_xs1 then
- []
- else
- let
- val z =
- (case #2 (const_triple rel_table (discr_for_constr const1)) of
- Func (Atom x, Formula _) => x
- | R => raise REP ("Nitpick_Kodkod.sym_break_axioms_for_constr_pair",
- [R]), should_tabulate_suc_for_type dtypes dataT)
- val (rec_sel_xs2, nonrec_sel_xs2) = rec_and_nonrec_sels const2
- val sel_xs2 = rec_sel_xs2 @ nonrec_sel_xs2
- fun sel_quadruples2 () = sel_xs2 |> map (`(const_triple rel_table))
- (* If the two constructors are the same, we drop the first selector
- because that one is always checked by the lexicographic order.
- We sometimes also filter out direct subterms, because those are
- already handled by the acyclicity breaking in the bound
- declarations. *)
- fun filter_out_sels no_direct sel_xs =
- apsnd (filter_out
- (fn ((x, _), T) =>
- (constr_ord = EQUAL andalso x = hd sel_xs) orelse
- (T = dataT andalso
- (no_direct orelse not (member (op =) sel_xs x)))))
- fun subterms_r no_direct sel_xs j =
- loop_path_rel_expr kk (map (filter_out_sels no_direct sel_xs) nfa)
- (filter_out (curry (op =) dataT) (map fst nfa)) dataT
- |> kk_join (KK.Var (1, j))
- in
- [kk_all [KK.DeclOne ((1, 0), discr_rel_expr rel_table const1),
- KK.DeclOne ((1, 1), discr_rel_expr rel_table const2)]
- (kk_implies
- (if delta2 >= epsilon1 then KK.True
- else if delta1 >= epsilon2 - 1 then KK.False
- else gt kk z (KK.Var (1, 1)) (KK.Var (1, 0)))
- (kk_or
- (if is_nil_like_constr_type dtypes T1 then
- KK.True
- else
- kk_some (kk_intersect (subterms_r false sel_xs2 1)
- (all_ge kk z (KK.Var (1, 0)))))
- (case constr_ord of
- EQUAL =>
- kk_and
- (lex_order_rel_expr kk dtypes (sel_quadruples2 ()))
- (kk_all [KK.DeclOne ((1, 2),
- subterms_r true sel_xs1 0)]
- (gt kk z (KK.Var (1, 1)) (KK.Var (1, 2))))
- | LESS =>
- kk_all [KK.DeclOne ((1, 2),
- subterms_r false sel_xs1 0)]
- (gt kk z (KK.Var (1, 1)) (KK.Var (1, 2)))
- | GREATER => KK.False)))]
- end
- end
-
-fun sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table nfas dtypes
- ({constrs, ...} : datatype_spec) =
- let
- val constrs = sort constr_ord constrs
- val constr_pairs = all_distinct_unordered_pairs_of constrs
- in
- map (pair EQUAL) (constrs ~~ constrs) @
- map (pair LESS) constr_pairs @
- map (pair GREATER) (map swap constr_pairs)
- |> maps (sym_break_axioms_for_constr_pair hol_ctxt binarize kk rel_table
- nfas dtypes)
- end
-
-val min_sym_break_card = 7
-
-fun sym_break_axioms_for_datatypes hol_ctxt binarize datatype_sym_break kk
- rel_table nfas dtypes =
- if datatype_sym_break = 0 then
- []
- else
- maps (sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table nfas
- dtypes)
- (dtypes |> filter is_datatype_acyclic
- |> filter (fn {constrs = [_], ...} => false
- | {card, constrs, ...} =>
- card >= min_sym_break_card andalso
- forall (forall (not o is_higher_order_type)
- o binder_types o snd o #const) constrs)
- |> (fn dtypes' =>
- dtypes'
- |> length dtypes' > datatype_sym_break
- ? (sort (datatype_ord o swap)
- #> take datatype_sym_break)))
-
-fun sel_axiom_for_sel hol_ctxt binarize j0
- (kk as {kk_all, kk_formula_if, kk_subset, kk_no, kk_join, ...})
- rel_table dom_r ({const, delta, epsilon, exclusive, ...} : constr_spec)
- n =
- let
- val x = binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const n
- val (r, R, _) = const_triple rel_table x
- val R2 = dest_Func R |> snd
- val z = (epsilon - delta, delta + j0)
- in
- if exclusive then
- kk_n_ary_function kk (Func (Atom z, R2)) r
- else
- let val r' = kk_join (KK.Var (1, 0)) r in
- kk_all [KK.DeclOne ((1, 0), KK.AtomSeq z)]
- (kk_formula_if (kk_subset (KK.Var (1, 0)) dom_r)
- (kk_n_ary_function kk R2 r') (kk_no r'))
- end
- end
-fun sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table
- (constr as {const, delta, epsilon, explicit_max, ...}) =
- let
- val honors_explicit_max =
- explicit_max < 0 orelse epsilon - delta <= explicit_max
- in
- if explicit_max = 0 then
- [formula_for_bool honors_explicit_max]
- else
- let
- val dom_r = discr_rel_expr rel_table const
- val max_axiom =
- if honors_explicit_max then
- KK.True
- else if bits = 0 orelse
- is_twos_complement_representable bits (epsilon - delta) then
- KK.LE (KK.Cardinality dom_r, KK.Num explicit_max)
- else
- raise TOO_SMALL ("Nitpick_Kodkod.sel_axioms_for_constr",
- "\"bits\" value " ^ string_of_int bits ^
- " too small for \"max\"")
- in
- max_axiom ::
- map (sel_axiom_for_sel hol_ctxt binarize j0 kk rel_table dom_r constr)
- (index_seq 0 (num_sels_for_constr_type (snd const)))
- end
- end
-fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table
- ({constrs, ...} : datatype_spec) =
- maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table) constrs
-
-fun uniqueness_axiom_for_constr hol_ctxt binarize
- ({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...}
- : kodkod_constrs) rel_table ({const, ...} : constr_spec) =
- let
- fun conjunct_for_sel r =
- kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r)
- val num_sels = num_sels_for_constr_type (snd const)
- val triples =
- map (const_triple rel_table
- o binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const)
- (~1 upto num_sels - 1)
- val set_r = triples |> hd |> #1
- in
- if num_sels = 0 then
- kk_lone set_r
- else
- kk_all (map (KK.DeclOne o rpair set_r o pair 1) [0, 1])
- (kk_implies
- (fold1 kk_and (map (conjunct_for_sel o #1) (tl triples)))
- (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))
- end
-fun uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table
- ({constrs, ...} : datatype_spec) =
- map (uniqueness_axiom_for_constr hol_ctxt binarize kk rel_table) constrs
-
-fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta
-fun partition_axioms_for_datatype j0 (kk as {kk_rel_eq, kk_union, ...})
- rel_table
- ({card, constrs, ...} : datatype_spec) =
- if forall #exclusive constrs then
- [Integer.sum (map effective_constr_max constrs) = card |> formula_for_bool]
- else
- let val rs = map (discr_rel_expr rel_table o #const) constrs in
- [kk_rel_eq (fold1 kk_union rs) (KK.AtomSeq (card, j0)),
- kk_disjoint_sets kk rs]
- end
-
-fun other_axioms_for_datatype _ _ _ _ _ _ {deep = false, ...} = []
- | other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table
- (dtype as {typ, ...}) =
- let val j0 = offset_of_type ofs typ in
- sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table dtype @
- uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table dtype @
- partition_axioms_for_datatype j0 kk rel_table dtype
- end
-
-fun declarative_axioms_for_datatypes hol_ctxt binarize datatype_sym_break bits
- ofs kk rel_table dtypes =
- let
- val nfas =
- dtypes |> map_filter (nfa_entry_for_datatype hol_ctxt binarize kk
- rel_table dtypes)
- |> strongly_connected_sub_nfas
- in
- acyclicity_axioms_for_datatypes kk nfas @
- sym_break_axioms_for_datatypes hol_ctxt binarize datatype_sym_break kk
- rel_table nfas dtypes @
- maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table)
- dtypes
- end
-
fun kodkod_formula_from_nut ofs
(kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not,
kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no,
@@ -1739,4 +1375,424 @@
r
in to_f_with_polarity Pos u end
+fun declarative_axiom_for_plain_rel kk (FreeRel (x, _, R as Func _, nick)) =
+ kk_n_ary_function kk (R |> nick = @{const_name List.set} ? unopt_rep)
+ (KK.Rel x)
+ | declarative_axiom_for_plain_rel ({kk_lone, kk_one, ...} : kodkod_constrs)
+ (FreeRel (x, _, R, _)) =
+ if is_one_rep R then kk_one (KK.Rel x)
+ else if is_lone_rep R andalso card_of_rep R > 1 then kk_lone (KK.Rel x)
+ else KK.True
+ | declarative_axiom_for_plain_rel _ u =
+ raise NUT ("Nitpick_Kodkod.declarative_axiom_for_plain_rel", [u])
+
+fun const_triple rel_table (x as (s, T)) =
+ case the_name rel_table (ConstName (s, T, Any)) of
+ FreeRel ((n, j), _, R, _) => (KK.Rel (n, j), R, n)
+ | _ => raise TERM ("Nitpick_Kodkod.const_triple", [Const x])
+
+fun discr_rel_expr rel_table = #1 o const_triple rel_table o discr_for_constr
+
+fun nfa_transitions_for_sel hol_ctxt binarize
+ ({kk_project, ...} : kodkod_constrs) rel_table
+ (dtypes : datatype_spec list) constr_x n =
+ let
+ val x as (_, T) =
+ binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize constr_x n
+ val (r, R, arity) = const_triple rel_table x
+ val type_schema = type_schema_of_rep T R
+ in
+ map_filter (fn (j, T) =>
+ if forall (not_equal T o #typ) dtypes then NONE
+ else SOME ((x, kk_project r (map KK.Num [0, j])), T))
+ (index_seq 1 (arity - 1) ~~ tl type_schema)
+ end
+fun nfa_transitions_for_constr hol_ctxt binarize kk rel_table dtypes
+ (x as (_, T)) =
+ maps (nfa_transitions_for_sel hol_ctxt binarize kk rel_table dtypes x)
+ (index_seq 0 (num_sels_for_constr_type T))
+fun nfa_entry_for_datatype _ _ _ _ _ ({co = true, ...} : datatype_spec) = NONE
+ | nfa_entry_for_datatype _ _ _ _ _ {standard = false, ...} = NONE
+ | nfa_entry_for_datatype _ _ _ _ _ {deep = false, ...} = NONE
+ | nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes
+ {typ, constrs, ...} =
+ SOME (typ, maps (nfa_transitions_for_constr hol_ctxt binarize kk rel_table
+ dtypes o #const) constrs)
+
+val empty_rel = KK.Product (KK.None, KK.None)
+
+fun direct_path_rel_exprs nfa start_T final_T =
+ case AList.lookup (op =) nfa final_T of
+ SOME trans => map (snd o fst) (filter (curry (op =) start_T o snd) trans)
+ | NONE => []
+and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T
+ final_T =
+ fold kk_union (direct_path_rel_exprs nfa start_T final_T)
+ (if start_T = final_T then KK.Iden else empty_rel)
+ | any_path_rel_expr (kk as {kk_union, ...}) nfa (T :: Ts) start_T final_T =
+ kk_union (any_path_rel_expr kk nfa Ts start_T final_T)
+ (knot_path_rel_expr kk nfa Ts start_T T final_T)
+and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa Ts
+ start_T knot_T final_T =
+ kk_join (kk_join (any_path_rel_expr kk nfa Ts knot_T final_T)
+ (kk_reflexive_closure (loop_path_rel_expr kk nfa Ts knot_T)))
+ (any_path_rel_expr kk nfa Ts start_T knot_T)
+and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T =
+ fold kk_union (direct_path_rel_exprs nfa start_T start_T) empty_rel
+ | loop_path_rel_expr (kk as {kk_union, kk_closure, ...}) nfa (T :: Ts)
+ start_T =
+ if start_T = T then
+ kk_closure (loop_path_rel_expr kk nfa Ts start_T)
+ else
+ kk_union (loop_path_rel_expr kk nfa Ts start_T)
+ (knot_path_rel_expr kk nfa Ts start_T T start_T)
+
+fun add_nfa_to_graph [] = I
+ | add_nfa_to_graph ((_, []) :: nfa) = add_nfa_to_graph nfa
+ | add_nfa_to_graph ((T, ((_, T') :: transitions)) :: nfa) =
+ add_nfa_to_graph ((T, transitions) :: nfa) o Typ_Graph.add_edge (T, T') o
+ Typ_Graph.default_node (T', ()) o Typ_Graph.default_node (T, ())
+
+fun strongly_connected_sub_nfas nfa =
+ add_nfa_to_graph nfa Typ_Graph.empty
+ |> Typ_Graph.strong_conn
+ |> map (fn keys => filter (member (op =) keys o fst) nfa)
+
+fun acyclicity_axiom_for_datatype (kk as {kk_no, kk_intersect, ...}) nfa
+ start_T =
+ kk_no (kk_intersect
+ (loop_path_rel_expr kk nfa (pull start_T (map fst nfa)) start_T)
+ KK.Iden)
+(* Cycle breaking in the bounds takes care of singly recursive datatypes, hence
+ the first equation. *)
+fun acyclicity_axioms_for_datatypes _ [_] = []
+ | acyclicity_axioms_for_datatypes kk nfas =
+ maps (fn nfa => map (acyclicity_axiom_for_datatype kk nfa o fst) nfa) nfas
+
+fun atom_equation_for_nut ofs kk (u, j) =
+ let val dummy_u = RelReg (0, type_of u, rep_of u) in
+ case Op2 (DefEq, bool_T, Formula Pos, dummy_u, u)
+ |> kodkod_formula_from_nut ofs kk of
+ KK.RelEq (KK.RelReg _, r) => KK.RelEq (KK.Atom j, r)
+ | _ => raise BAD ("Nitpick_Kodkod.atom_equation_for_nut",
+ "malformed Kodkod formula")
+ end
+
+fun preconstructed_value_axioms_for_datatype [] _ _ _ = []
+ | preconstructed_value_axioms_for_datatype preconstr_us ofs kk
+ ({typ, card, constrs, ...} : datatype_spec) =
+ let
+ fun aux (u as Construct (FreeRel (_, _, _, s) :: _, T, _, us)) =
+ fold aux us
+ #> (fn NONE => NONE
+ | accum as SOME (loose, fixed) =>
+ if T = typ then
+ case AList.lookup (op =) fixed u of
+ SOME _ => accum
+ | NONE =>
+ let
+ val constr_s = constr_name_for_sel_like s
+ val {delta, epsilon, ...} =
+ constrs
+ |> List.find (fn {const, ...} => fst const = constr_s)
+ |> the
+ val j0 = offset_of_type ofs T
+ in
+ case find_first (fn j => j >= delta andalso
+ j < delta + epsilon) loose of
+ SOME j =>
+ SOME (remove (op =) j loose, (u, j0 + j) :: fixed)
+ | NONE => NONE
+ end
+ else
+ accum)
+ | aux u =
+ raise NUT ("Nitpick_Kodkod.preconstructed_value_axioms_for_datatype\
+ \.aux", [u])
+ in
+ case SOME (index_seq 0 card, []) |> fold aux preconstr_us of
+ SOME (_, fixed) => fixed |> map (atom_equation_for_nut ofs kk)
+ | NONE => [KK.False]
+ end
+
+fun all_ge ({kk_join, kk_reflexive_closure, ...} : kodkod_constrs) z r =
+ kk_join r (kk_reflexive_closure (KK.Rel (suc_rel_for_atom_seq z)))
+fun gt ({kk_subset, kk_join, kk_closure, ...} : kodkod_constrs) z r1 r2 =
+ kk_subset r1 (kk_join r2 (kk_closure (KK.Rel (suc_rel_for_atom_seq z))))
+
+fun constr_quadruple ({const = (s, T), delta, epsilon, ...} : constr_spec) =
+ (delta, (epsilon, (num_binder_types T, s)))
+val constr_ord =
+ prod_ord int_ord (prod_ord int_ord (prod_ord int_ord string_ord))
+ o pairself constr_quadruple
+
+fun datatype_ord (({card = card1, self_rec = self_rec1, constrs = constr1, ...},
+ {card = card2, self_rec = self_rec2, constrs = constr2, ...})
+ : datatype_spec * datatype_spec) =
+ prod_ord int_ord (prod_ord bool_ord int_ord)
+ ((card1, (self_rec1, length constr1)),
+ (card2, (self_rec2, length constr2)))
+
+(* We must absolutely tabulate "suc" for all datatypes whose selector bounds
+ break cycles; otherwise, we may end up with two incompatible symmetry
+ breaking orders, leading to spurious models. *)
+fun should_tabulate_suc_for_type dtypes T =
+ is_asymmetric_nondatatype T orelse
+ case datatype_spec dtypes T of
+ SOME {self_rec, ...} => self_rec
+ | NONE => false
+
+fun lex_order_rel_expr (kk as {kk_implies, kk_and, kk_subset, kk_join, ...})
+ dtypes sel_quadruples =
+ case sel_quadruples of
+ [] => KK.True
+ | ((r, Func (Atom _, Atom x), 2), (_, Type (_, [_, T]))) :: sel_quadruples' =>
+ let val z = (x, should_tabulate_suc_for_type dtypes T) in
+ if null sel_quadruples' then
+ gt kk z (kk_join (KK.Var (1, 1)) r) (kk_join (KK.Var (1, 0)) r)
+ else
+ kk_and (kk_subset (kk_join (KK.Var (1, 1)) r)
+ (all_ge kk z (kk_join (KK.Var (1, 0)) r)))
+ (kk_implies (kk_subset (kk_join (KK.Var (1, 1)) r)
+ (kk_join (KK.Var (1, 0)) r))
+ (lex_order_rel_expr kk dtypes sel_quadruples'))
+ end
+ (* Skip constructors components that aren't atoms, since we cannot compare
+ these easily. *)
+ | _ :: sel_quadruples' => lex_order_rel_expr kk dtypes sel_quadruples'
+
+fun is_nil_like_constr_type dtypes T =
+ case datatype_spec dtypes T of
+ SOME {constrs, ...} =>
+ (case filter_out (is_self_recursive_constr_type o snd o #const) constrs of
+ [{const = (_, T'), ...}] => T = T'
+ | _ => false)
+ | NONE => false
+
+fun sym_break_axioms_for_constr_pair hol_ctxt binarize
+ (kk as {kk_all, kk_or, kk_implies, kk_and, kk_some, kk_intersect,
+ kk_join, ...}) rel_table nfas dtypes
+ (constr_ord,
+ ({const = const1 as (_, T1), delta = delta1, epsilon = epsilon1, ...},
+ {const = const2 as (_, _), delta = delta2, epsilon = epsilon2, ...})
+ : constr_spec * constr_spec) =
+ let
+ val dataT = body_type T1
+ val nfa = nfas |> find_first (exists (curry (op =) dataT o fst)) |> these
+ val rec_Ts = nfa |> map fst
+ fun rec_and_nonrec_sels (x as (_, T)) =
+ index_seq 0 (num_sels_for_constr_type T)
+ |> map (binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize x)
+ |> List.partition (member (op =) rec_Ts o range_type o snd)
+ val sel_xs1 = rec_and_nonrec_sels const1 |> op @
+ in
+ if constr_ord = EQUAL andalso null sel_xs1 then
+ []
+ else
+ let
+ val z =
+ (case #2 (const_triple rel_table (discr_for_constr const1)) of
+ Func (Atom x, Formula _) => x
+ | R => raise REP ("Nitpick_Kodkod.sym_break_axioms_for_constr_pair",
+ [R]), should_tabulate_suc_for_type dtypes dataT)
+ val (rec_sel_xs2, nonrec_sel_xs2) = rec_and_nonrec_sels const2
+ val sel_xs2 = rec_sel_xs2 @ nonrec_sel_xs2
+ fun sel_quadruples2 () = sel_xs2 |> map (`(const_triple rel_table))
+ (* If the two constructors are the same, we drop the first selector
+ because that one is always checked by the lexicographic order.
+ We sometimes also filter out direct subterms, because those are
+ already handled by the acyclicity breaking in the bound
+ declarations. *)
+ fun filter_out_sels no_direct sel_xs =
+ apsnd (filter_out
+ (fn ((x, _), T) =>
+ (constr_ord = EQUAL andalso x = hd sel_xs) orelse
+ (T = dataT andalso
+ (no_direct orelse not (member (op =) sel_xs x)))))
+ fun subterms_r no_direct sel_xs j =
+ loop_path_rel_expr kk (map (filter_out_sels no_direct sel_xs) nfa)
+ (filter_out (curry (op =) dataT) (map fst nfa)) dataT
+ |> kk_join (KK.Var (1, j))
+ in
+ [kk_all [KK.DeclOne ((1, 0), discr_rel_expr rel_table const1),
+ KK.DeclOne ((1, 1), discr_rel_expr rel_table const2)]
+ (kk_implies
+ (if delta2 >= epsilon1 then KK.True
+ else if delta1 >= epsilon2 - 1 then KK.False
+ else gt kk z (KK.Var (1, 1)) (KK.Var (1, 0)))
+ (kk_or
+ (if is_nil_like_constr_type dtypes T1 then
+ KK.True
+ else
+ kk_some (kk_intersect (subterms_r false sel_xs2 1)
+ (all_ge kk z (KK.Var (1, 0)))))
+ (case constr_ord of
+ EQUAL =>
+ kk_and
+ (lex_order_rel_expr kk dtypes (sel_quadruples2 ()))
+ (kk_all [KK.DeclOne ((1, 2),
+ subterms_r true sel_xs1 0)]
+ (gt kk z (KK.Var (1, 1)) (KK.Var (1, 2))))
+ | LESS =>
+ kk_all [KK.DeclOne ((1, 2),
+ subterms_r false sel_xs1 0)]
+ (gt kk z (KK.Var (1, 1)) (KK.Var (1, 2)))
+ | GREATER => KK.False)))]
+ end
+ end
+
+fun sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table nfas dtypes
+ ({constrs, ...} : datatype_spec) =
+ let
+ val constrs = sort constr_ord constrs
+ val constr_pairs = all_distinct_unordered_pairs_of constrs
+ in
+ map (pair EQUAL) (constrs ~~ constrs) @
+ map (pair LESS) constr_pairs @
+ map (pair GREATER) (map swap constr_pairs)
+ |> maps (sym_break_axioms_for_constr_pair hol_ctxt binarize kk rel_table
+ nfas dtypes)
+ end
+
+fun is_datatype_in_preconstructed_value T (Construct (_, T', _, us)) =
+ T = T' orelse exists (is_datatype_in_preconstructed_value T) us
+ | is_datatype_in_preconstructed_value _ _ = false
+
+val min_sym_break_card = 7
+
+fun sym_break_axioms_for_datatypes hol_ctxt binarize preconstr_us
+ datatype_sym_break kk rel_table nfas dtypes =
+ if datatype_sym_break = 0 then
+ []
+ else
+ dtypes |> filter is_datatype_acyclic
+ |> filter (fn {constrs = [_], ...} => false
+ | {card, constrs, ...} =>
+ card >= min_sym_break_card andalso
+ forall (forall (not o is_higher_order_type)
+ o binder_types o snd o #const) constrs)
+ |> filter_out
+ (fn {typ, ...} =>
+ exists (is_datatype_in_preconstructed_value typ)
+ preconstr_us)
+ |> (fn dtypes' =>
+ dtypes' |> length dtypes' > datatype_sym_break
+ ? (sort (datatype_ord o swap)
+ #> take datatype_sym_break))
+ |> maps (sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table
+ nfas dtypes)
+
+
+fun sel_axiom_for_sel hol_ctxt binarize j0
+ (kk as {kk_all, kk_formula_if, kk_subset, kk_no, kk_join, ...})
+ rel_table dom_r ({const, delta, epsilon, exclusive, ...} : constr_spec)
+ n =
+ let
+ val x = binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const n
+ val (r, R, _) = const_triple rel_table x
+ val R2 = dest_Func R |> snd
+ val z = (epsilon - delta, delta + j0)
+ in
+ if exclusive then
+ kk_n_ary_function kk (Func (Atom z, R2)) r
+ else
+ let val r' = kk_join (KK.Var (1, 0)) r in
+ kk_all [KK.DeclOne ((1, 0), KK.AtomSeq z)]
+ (kk_formula_if (kk_subset (KK.Var (1, 0)) dom_r)
+ (kk_n_ary_function kk R2 r') (kk_no r'))
+ end
+ end
+fun sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table
+ (constr as {const, delta, epsilon, explicit_max, ...}) =
+ let
+ val honors_explicit_max =
+ explicit_max < 0 orelse epsilon - delta <= explicit_max
+ in
+ if explicit_max = 0 then
+ [formula_for_bool honors_explicit_max]
+ else
+ let
+ val dom_r = discr_rel_expr rel_table const
+ val max_axiom =
+ if honors_explicit_max then
+ KK.True
+ else if bits = 0 orelse
+ is_twos_complement_representable bits (epsilon - delta) then
+ KK.LE (KK.Cardinality dom_r, KK.Num explicit_max)
+ else
+ raise TOO_SMALL ("Nitpick_Kodkod.sel_axioms_for_constr",
+ "\"bits\" value " ^ string_of_int bits ^
+ " too small for \"max\"")
+ in
+ max_axiom ::
+ map (sel_axiom_for_sel hol_ctxt binarize j0 kk rel_table dom_r constr)
+ (index_seq 0 (num_sels_for_constr_type (snd const)))
+ end
+ end
+fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table
+ ({constrs, ...} : datatype_spec) =
+ maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table) constrs
+
+fun uniqueness_axiom_for_constr hol_ctxt binarize
+ ({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...}
+ : kodkod_constrs) rel_table ({const, ...} : constr_spec) =
+ let
+ fun conjunct_for_sel r =
+ kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r)
+ val num_sels = num_sels_for_constr_type (snd const)
+ val triples =
+ map (const_triple rel_table
+ o binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const)
+ (~1 upto num_sels - 1)
+ val set_r = triples |> hd |> #1
+ in
+ if num_sels = 0 then
+ kk_lone set_r
+ else
+ kk_all (map (KK.DeclOne o rpair set_r o pair 1) [0, 1])
+ (kk_implies
+ (fold1 kk_and (map (conjunct_for_sel o #1) (tl triples)))
+ (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))
+ end
+fun uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table
+ ({constrs, ...} : datatype_spec) =
+ map (uniqueness_axiom_for_constr hol_ctxt binarize kk rel_table) constrs
+
+fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta
+fun partition_axioms_for_datatype j0 (kk as {kk_rel_eq, kk_union, ...})
+ rel_table
+ ({card, constrs, ...} : datatype_spec) =
+ if forall #exclusive constrs then
+ [Integer.sum (map effective_constr_max constrs) = card |> formula_for_bool]
+ else
+ let val rs = map (discr_rel_expr rel_table o #const) constrs in
+ [kk_rel_eq (fold1 kk_union rs) (KK.AtomSeq (card, j0)),
+ kk_disjoint_sets kk rs]
+ end
+
+fun other_axioms_for_datatype _ _ _ _ _ _ {deep = false, ...} = []
+ | other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table
+ (dtype as {typ, ...}) =
+ let val j0 = offset_of_type ofs typ in
+ sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table dtype @
+ uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table dtype @
+ partition_axioms_for_datatype j0 kk rel_table dtype
+ end
+
+fun declarative_axioms_for_datatypes hol_ctxt binarize preconstr_us
+ datatype_sym_break bits ofs kk rel_table dtypes =
+ let
+ val nfas =
+ dtypes |> map_filter (nfa_entry_for_datatype hol_ctxt binarize kk
+ rel_table dtypes)
+ |> strongly_connected_sub_nfas
+ in
+ acyclicity_axioms_for_datatypes kk nfas @
+ maps (preconstructed_value_axioms_for_datatype preconstr_us ofs kk) dtypes @
+ sym_break_axioms_for_datatypes hol_ctxt binarize preconstr_us
+ datatype_sym_break kk rel_table nfas dtypes @
+ maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table)
+ dtypes
+ end
+
end;
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Feb 21 17:43:23 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Feb 21 18:29:47 2011 +0100
@@ -862,12 +862,12 @@
fun reconstruct_hol_model {show_datatypes, show_consts}
({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
debug, whacks, binary_ints, destroy_constrs, specialize,
- star_linear_preds, tac_timeout, evals, case_names,
- def_tables, nondef_table, user_nondefs, simp_table,
- psimp_table, choice_spec_table, intro_table,
+ star_linear_preds, preconstrs, tac_timeout, evals,
+ case_names, def_tables, nondef_table, user_nondefs,
+ simp_table, psimp_table, choice_spec_table, intro_table,
ground_thm_table, ersatz_table, skolems, special_funs,
- unrolled_preds, wf_cache, constr_cache},
- binarize, card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
+ unrolled_preds, wf_cache, constr_cache}, binarize,
+ card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
formats atomss real_frees pseudo_frees free_names sel_names nonsel_names
rel_table bounds =
let
@@ -879,15 +879,15 @@
stds = stds, wfs = wfs, user_axioms = user_axioms, debug = debug,
whacks = whacks, binary_ints = binary_ints,
destroy_constrs = destroy_constrs, specialize = specialize,
- star_linear_preds = star_linear_preds, tac_timeout = tac_timeout,
- evals = evals, case_names = case_names, def_tables = def_tables,
- nondef_table = nondef_table, user_nondefs = user_nondefs,
- simp_table = simp_table, psimp_table = psimp_table,
- choice_spec_table = choice_spec_table, intro_table = intro_table,
- ground_thm_table = ground_thm_table, ersatz_table = ersatz_table,
- skolems = skolems, special_funs = special_funs,
- unrolled_preds = unrolled_preds, wf_cache = wf_cache,
- constr_cache = constr_cache}
+ star_linear_preds = star_linear_preds, preconstrs = preconstrs,
+ tac_timeout = tac_timeout, evals = evals, case_names = case_names,
+ def_tables = def_tables, nondef_table = nondef_table,
+ user_nondefs = user_nondefs, simp_table = simp_table,
+ psimp_table = psimp_table, choice_spec_table = choice_spec_table,
+ intro_table = intro_table, ground_thm_table = ground_thm_table,
+ ersatz_table = ersatz_table, skolems = skolems,
+ special_funs = special_funs, unrolled_preds = unrolled_preds,
+ wf_cache = wf_cache, constr_cache = constr_cache}
val scope =
{hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Feb 21 17:43:23 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Mon Feb 21 18:29:47 2011 +0100
@@ -10,7 +10,7 @@
type hol_context = Nitpick_HOL.hol_context
val preprocess_formulas :
hol_context -> term list -> term
- -> term list * term list * bool * bool * bool
+ -> term list * term list * term list * bool * bool * bool
end;
structure Nitpick_Preproc : NITPICK_PREPROC =
@@ -1246,7 +1246,7 @@
fun preprocess_formulas
(hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs, boxes,
- ...}) assm_ts neg_t =
+ preconstrs, ...}) assm_ts neg_t =
let
val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
neg_t |> unfold_defs_in_term hol_ctxt
@@ -1266,13 +1266,14 @@
val table =
Termtab.empty
|> box ? fold (add_to_uncurry_table ctxt) (nondef_ts @ def_ts)
- fun do_rest def =
+ fun do_middle def =
binarize ? binarize_nat_and_int_in_term
#> box ? uncurry_term table
#> box ? box_fun_and_pair_in_term hol_ctxt def
- #> destroy_constrs ? (pull_out_universal_constrs hol_ctxt def
- #> pull_out_existential_constrs hol_ctxt
- #> destroy_pulled_out_constrs hol_ctxt def)
+ fun do_tail def =
+ destroy_constrs ? (pull_out_universal_constrs hol_ctxt def
+ #> pull_out_existential_constrs hol_ctxt
+ #> destroy_pulled_out_constrs hol_ctxt def)
#> curry_assms
#> destroy_universal_equalities
#> destroy_existential_equalities hol_ctxt
@@ -1281,10 +1282,17 @@
#> push_quantifiers_inward
#> close_form
#> Term.map_abs_vars shortest_name
- val nondef_ts = map (do_rest false) nondef_ts
- val def_ts = map (do_rest true) def_ts
+ val nondef_ts = nondef_ts |> map (do_middle false)
+ val preconstr_ts =
+ (* FIXME: Implement preconstruction inference. *)
+ preconstrs
+ |> map_filter (fn (SOME t, SOME true) => SOME (t |> do_middle false)
+ | _ => NONE)
+ val nondef_ts = nondef_ts |> map (do_tail false)
+ val def_ts = def_ts |> map (do_middle true #> do_tail true)
in
- (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms, binarize)
+ (nondef_ts, def_ts, preconstr_ts, got_all_mono_user_axioms,
+ no_poly_user_axioms, binarize)
end
end;
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML Mon Feb 21 17:43:23 2011 +0100
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML Mon Feb 21 18:29:47 2011 +0100
@@ -62,7 +62,7 @@
avail = make_avail is_remote "CVC3",
command = make_command is_remote "CVC3",
options = cvc3_options,
- default_max_relevant = 200 (* FUDGE *),
+ default_max_relevant = 150 (* FUDGE *),
supports_filter = false,
outcome =
on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
@@ -86,7 +86,7 @@
options = (fn ctxt => [
"--rand-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
"--smtlib"]),
- default_max_relevant = 200 (* FUDGE *),
+ default_max_relevant = 150 (* FUDGE *),
supports_filter = false,
outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
cex_parser = NONE,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Feb 21 17:43:23 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Feb 21 18:29:47 2011 +0100
@@ -478,8 +478,6 @@
(* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until
these are sorted out properly in the SMT module, we have to interpret these
ourselves. *)
-val perl_failures =
- [(127, NoPerl)]
val remote_smt_failures =
[(22, CantConnect),
(2, NoLibwwwPerl)]
@@ -495,8 +493,7 @@
val unix_failures =
[(139, Crashed)]
val smt_failures =
- perl_failures @ remote_smt_failures @ z3_wrapper_failures @ z3_failures @
- unix_failures
+ remote_smt_failures @ z3_wrapper_failures @ z3_failures @ unix_failures
val internal_error_prefix = "Internal error: "