# HG changeset patch # User blanchet # Date 1298309387 -3600 # Node ID 173e1b50d5c5b54317dd7872aad4b9f2951a38d3 # Parent c3aa3c87ef218bc3023926d9498ec1d11ab7a2e5# Parent a96684499e854879a944a13c713e7ce835ad1fb3 merged diff -r c3aa3c87ef21 -r 173e1b50d5c5 doc-src/Nitpick/nitpick.tex --- 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 diff -r c3aa3c87ef21 -r 173e1b50d5c5 src/HOL/Nitpick_Examples/Mono_Nits.thy --- 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 diff -r c3aa3c87ef21 -r 173e1b50d5c5 src/HOL/Tools/Nitpick/nitpick.ML --- 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, diff -r c3aa3c87ef21 -r 173e1b50d5c5 src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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, diff -r c3aa3c87ef21 -r 173e1b50d5c5 src/HOL/Tools/Nitpick/nitpick_isar.ML --- 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} diff -r c3aa3c87ef21 -r 173e1b50d5c5 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- 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; diff -r c3aa3c87ef21 -r 173e1b50d5c5 src/HOL/Tools/Nitpick/nitpick_model.ML --- 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} diff -r c3aa3c87ef21 -r 173e1b50d5c5 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- 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; diff -r c3aa3c87ef21 -r 173e1b50d5c5 src/HOL/Tools/SMT/smt_setup_solvers.ML --- 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, diff -r c3aa3c87ef21 -r 173e1b50d5c5 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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: "