--- a/doc-src/Nitpick/nitpick.tex Sun Aug 01 10:26:55 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex Sun Aug 01 17:43:51 2010 +0200
@@ -818,7 +818,7 @@
\hbox{}\qquad \textit{card nat}~= 50. \\[2\smallskipamount]
Nitpick found a potential counterexample for \textit{card nat}~= 50: \\[2\smallskipamount]
\hbox{}\qquad Empty assignment \\[2\smallskipamount]
-Nitpick could not find a better counterexample. \\[2\smallskipamount]
+Nitpick could not find a better counterexample. It checked 1 of 1 scope. \\[2\smallskipamount]
Total time: 2274 ms.
\postw
@@ -2371,6 +2371,15 @@
which you will find on Kodkod's web site \cite{kodkod-2009}. Unlike the standard
version of MiniSat, the JNI version can be used incrementally.
+\item[$\bullet$] \textbf{\textit{CryptoMiniSat}:} CryptoMiniSat is the winner of
+the 2010 SAT Race. To use CryptoMiniSat, set the environment variable
+\texttt{CRYPTO\-MINISAT\_}\discretionary{}{}{}\texttt{HOME} to the directory that contains the \texttt{crypto\-minisat}
+executable.%
+\footref{cygwin-paths}
+The \cpp{} sources and executables for Crypto\-Mini\-Sat are available at
+\url{http://planete.inrialpes.fr/~soos/}\allowbreak\url{CryptoMiniSat2/index.php}.
+Nitpick has been tested with version 2.51.
+
\item[$\bullet$] \textbf{\textit{PicoSAT}:} PicoSAT is an efficient solver
written in C. You can install a standard version of
PicoSAT and set the environment variable \texttt{PICOSAT\_HOME} to the directory
@@ -2433,11 +2442,9 @@
optimized for small problems. It can also be used incrementally.
\item[$\bullet$] \textbf{\textit{smart}:} If \textit{sat\_solver} is set to
-\textit{smart}, Nitpick selects the first solver among MiniSat,
-PicoSAT, zChaff, RSat, BerkMin, BerkMin\_Alloy, Jerusat, MiniSat\_JNI, and zChaff\_JNI
-that is recognized by Isabelle. If none is found, it falls back on SAT4J, which
-should always be available. If \textit{verbose} (\S\ref{output-format}) is
-enabled, Nitpick displays which SAT solver was chosen.
+\textit{smart}, Nitpick selects the first solver among the above that is
+recognized by Isabelle. If \textit{verbose} (\S\ref{output-format}) is enabled,
+Nitpick displays which SAT solver was chosen.
\end{enum}
\fussy
@@ -2493,6 +2500,18 @@
Unless you are tracking down a bug in Nitpick or distrust the peephole
optimizer, you should leave this option enabled.
+\opdefault{datatype\_sym\_break}{int}{5}
+Specifies an upper bound on the number of datatypes for which Nitpick generates
+symmetry breaking predicates. Symmetry breaking can speed up the SAT solver
+considerably, especially for unsatisfiable problems, but too much of it can slow
+it down.
+
+\opdefault{kodkod\_sym\_break}{int}{15}
+Specifies an upper bound on the number of relations for which Kodkod generates
+symmetry breaking predicates. Symmetry breaking can speed up the SAT solver
+considerably, especially for unsatisfiable problems, but too much of it can slow
+it down.
+
\opdefault{max\_threads}{int}{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/Tools/Nitpick/kodkod.ML Sun Aug 01 10:26:55 2010 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Sun Aug 01 17:43:51 2010 +0200
@@ -47,7 +47,7 @@
Acyclic of n_ary_index |
Function of n_ary_index * rel_expr * rel_expr |
Functional of n_ary_index * rel_expr * rel_expr |
- TotalOrdering of n_ary_index * n_ary_index * n_ary_index * n_ary_index |
+ TotalOrdering of n_ary_index * rel_expr * rel_expr * rel_expr |
Subset of rel_expr * rel_expr |
RelEq of rel_expr * rel_expr |
IntEq of int_expr * int_expr |
@@ -216,7 +216,7 @@
Acyclic of n_ary_index |
Function of n_ary_index * rel_expr * rel_expr |
Functional of n_ary_index * rel_expr * rel_expr |
- TotalOrdering of n_ary_index * n_ary_index * n_ary_index * n_ary_index |
+ TotalOrdering of n_ary_index * rel_expr * rel_expr * rel_expr |
Subset of rel_expr * rel_expr |
RelEq of rel_expr * rel_expr |
IntEq of int_expr * int_expr |
@@ -316,7 +316,15 @@
rel_expr_func: rel_expr -> 'a -> 'a,
int_expr_func: int_expr -> 'a -> 'a}
-(** Auxiliary functions on ML representation of Kodkod problems **)
+fun is_new_kodkodi_version () =
+ case getenv "KODKODI_VERSION" of
+ "" => false
+ | s => dict_ord int_ord (s |> space_explode "."
+ |> map (the o Int.fromString),
+ [1, 2, 13]) = GREATER
+ handle Option.Option => false
+
+(** Auxiliary functions on Kodkod problems **)
fun fold_formula (F : 'a fold_expr_funcs) formula =
case formula of
@@ -335,9 +343,9 @@
fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2
| Functional (x, r1, r2) =>
fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2
- | TotalOrdering (x1, x2, x3, x4) =>
- fold_rel_expr F (Rel x1) #> fold_rel_expr F (Rel x2)
- #> fold_rel_expr F (Rel x3) #> fold_rel_expr F (Rel x4)
+ | TotalOrdering (x, r1, r2, r3) =>
+ fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2
+ #> fold_rel_expr F r3
| Subset (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
| RelEq (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
| IntEq (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
@@ -518,7 +526,10 @@
fun int_reg_name j = "$i" ^ base_name j
fun tuple_name x = n_ary_name x "A" "P" "T"
-fun rel_name x = n_ary_name x "s" "r" "m"
+fun rel_name new_kodkodi (n, j) =
+ n_ary_name (n, if new_kodkodi then j
+ else if j >= 0 then 2 * j
+ else 2 * ~j - 1) "s" "r" "m"
fun var_name x = n_ary_name x "S" "R" "M"
fun tuple_reg_name x = n_ary_name x "$A" "$P" "$T"
fun tuple_set_reg_name x = n_ary_name x "$a" "$p" "$t"
@@ -530,7 +541,8 @@
fun block_comment "" = ""
| block_comment comment = prefix_lines "// " comment ^ "\n"
-fun commented_rel_name (x, s) = rel_name x ^ inline_comment s
+fun commented_rel_name new_kodkodi (x, s) =
+ rel_name new_kodkodi x ^ inline_comment s
fun string_for_tuple (Tuple js) = "[" ^ commas (map atom_name js) ^ "]"
| string_for_tuple (TupleIndex x) = tuple_name x
@@ -581,8 +593,8 @@
| string_for_tuple_assign (AssignTupleSet (x, ts)) =
tuple_set_reg_name x ^ " := " ^ string_for_tuple_set ts ^ "\n"
-fun string_for_bound (zs, tss) =
- "bounds " ^ commas (map commented_rel_name zs) ^ ": " ^
+fun string_for_bound new_kodkodi (zs, tss) =
+ "bounds " ^ commas (map (commented_rel_name new_kodkodi) zs) ^ ": " ^
(if length tss = 1 then "" else "[") ^ commas (map string_for_tuple_set tss) ^
(if length tss = 1 then "" else "]") ^ "\n"
@@ -685,6 +697,8 @@
fun write_problem_file out problems =
let
+ val new_kodkodi = is_new_kodkodi_version ()
+ val rel_name = rel_name new_kodkodi
fun out_outmost_f (And (f1, f2)) =
(out_outmost_f f1; out "\n && "; out_outmost_f f2)
| out_outmost_f f = out_f f prec_And
@@ -715,9 +729,9 @@
| Functional (x, r1, r2) =>
(out ("FUNCTION(" ^ rel_name x ^ ", "); out_r r1 0; out " -> lone ";
out_r r2 0; out ")")
- | TotalOrdering (x1, x2, x3, x4) =>
- out ("TOTAL_ORDERING(" ^ rel_name x1 ^ ", " ^ rel_name x2 ^ ", "
- ^ rel_name x3 ^ ", " ^ rel_name x4 ^ ")")
+ | TotalOrdering (x, r1, r2, r3) =>
+ (out ("TOTAL_ORDERING(" ^ rel_name x ^ ", "); out_r r1 0; out ", ";
+ out_r r2 0; out ", "; out_r r3 0; out ")")
| Subset (r1, r2) => (out_r r1 prec; out " in "; out_r r2 prec)
| RelEq (r1, r2) => (out_r r1 prec; out " = "; out_r r2 prec)
| IntEq (i1, i2) => (out_i i1 prec; out " = "; out_i i2 prec)
@@ -837,7 +851,7 @@
settings) ^
"univ: " ^ atom_seq_name (univ_card, 0) ^ "\n" ^
implode (map string_for_tuple_assign tuple_assigns) ^
- implode (map string_for_bound bounds) ^
+ implode (map (string_for_bound new_kodkodi) bounds) ^
(if int_bounds = [] then
""
else
@@ -871,22 +885,29 @@
fun scan_list scan = scan_non_empty_list scan || Scan.succeed []
val scan_nat = Scan.repeat1 (Scan.one Symbol.is_ascii_digit)
>> (the o Int.fromString o space_implode "")
-val scan_rel_name = $$ "s" |-- scan_nat >> pair 1
- || $$ "r" |-- scan_nat >> pair 2
- || ($$ "m" |-- scan_nat --| $$ "_") -- scan_nat
+fun scan_rel_name new_kodkodi =
+ ($$ "s" |-- scan_nat >> pair 1
+ || $$ "r" |-- scan_nat >> pair 2
+ || ($$ "m" |-- scan_nat --| $$ "_") -- scan_nat) -- Scan.option ($$ "'")
+ >> (fn ((n, j), SOME _) => (n, ~j - 1)
+ | ((n, j), NONE) => (n, if new_kodkodi then j
+ else if j mod 2 = 0 then j div 2
+ else ~(j - 1) div 2))
val scan_atom = $$ "A" |-- scan_nat
val scan_tuple = $$ "[" |-- scan_list scan_atom --| $$ "]"
val scan_tuple_set = $$ "[" |-- scan_list scan_tuple --| $$ "]"
-val scan_assignment = (scan_rel_name --| $$ "=") -- scan_tuple_set
-val scan_instance = Scan.this_string "relations:" |--
- $$ "{" |-- scan_list scan_assignment --| $$ "}"
+fun scan_assignment new_kodkodi =
+ (scan_rel_name new_kodkodi --| $$ "=") -- scan_tuple_set
+fun scan_instance new_kodkodi =
+ Scan.this_string "relations:"
+ |-- $$ "{" |-- scan_list (scan_assignment new_kodkodi) --| $$ "}"
-val parse_instance =
+fun parse_instance new_kodkodi =
fst o Scan.finite Symbol.stopper
(Scan.error (!! (fn _ =>
raise SYNTAX ("Kodkod.parse_instance",
"ill-formed Kodkodi output"))
- scan_instance))
+ (scan_instance new_kodkodi)))
o strip_blanks o explode
val problem_marker = "*** PROBLEM "
@@ -897,15 +918,15 @@
Substring.string o fst o Substring.position "\n\n"
o Substring.triml (size marker)
-fun read_next_instance s =
+fun read_next_instance new_kodkodi s =
let val s = Substring.position instance_marker s |> snd in
if Substring.isEmpty s then
raise SYNTAX ("Kodkod.read_next_instance", "expected \"INSTANCE\" marker")
else
- read_section_body instance_marker s |> parse_instance
+ read_section_body instance_marker s |> parse_instance new_kodkodi
end
-fun read_next_outcomes j (s, ps, js) =
+fun read_next_outcomes new_kodkodi j (s, ps, js) =
let val (s1, s2) = Substring.position outcome_marker s in
if Substring.isEmpty s2 orelse
not (Substring.isEmpty (Substring.position problem_marker s1
@@ -917,16 +938,17 @@
val s = Substring.triml (size outcome_marker) s2
in
if String.isSuffix "UNSATISFIABLE" outcome then
- read_next_outcomes j (s, ps, j :: js)
+ read_next_outcomes new_kodkodi j (s, ps, j :: js)
else if String.isSuffix "SATISFIABLE" outcome then
- read_next_outcomes j (s, (j, read_next_instance s2) :: ps, js)
+ read_next_outcomes new_kodkodi j
+ (s, (j, read_next_instance new_kodkodi s2) :: ps, js)
else
raise SYNTAX ("Kodkod.read_next_outcomes",
"unknown outcome " ^ quote outcome)
end
end
-fun read_next_problems (s, ps, js) =
+fun read_next_problems new_kodkodi (s, ps, js) =
let val s = Substring.position problem_marker s |> snd in
if Substring.isEmpty s then
(ps, js)
@@ -936,14 +958,18 @@
val j_plus_1 = s |> Substring.takel (not_equal #" ") |> Substring.string
|> Int.fromString |> the
val j = j_plus_1 - 1
- in read_next_problems (read_next_outcomes j (s, ps, js)) end
+ in
+ read_next_problems new_kodkodi
+ (read_next_outcomes new_kodkodi j (s, ps, js))
+ end
end
handle Option.Option => raise SYNTAX ("Kodkod.read_next_problems",
"expected number after \"PROBLEM\"")
-fun read_output_file path =
- (false, read_next_problems (Substring.full (File.read path), [], [])
- |>> rev ||> rev)
+fun read_output_file new_kodkodi path =
+ (false,
+ read_next_problems new_kodkodi (Substring.full (File.read path), [], [])
+ |>> rev ||> rev)
handle IO.Io _ => (true, ([], [])) | OS.SysErr _ => (true, ([], []))
(** Main Kodkod entry point **)
@@ -973,6 +999,7 @@
fun uncached_solve_any_problem overlord deadline max_threads max_solutions
problems =
let
+ val new_kodkodi = is_new_kodkodi_version ()
val j = find_index (curry (op =) True o #formula) problems
val indexed_problems = if j >= 0 then
[(j, nth problems j)]
@@ -1026,7 +1053,7 @@
" > " ^ File.shell_path out_path ^
" 2> " ^ File.shell_path err_path)
val (io_error, (ps, nontriv_js)) =
- read_output_file out_path
+ read_output_file new_kodkodi out_path
||> apfst (map (apfst reindex)) ||> apsnd (map reindex)
val js = triv_js @ nontriv_js
val first_error =
@@ -1063,7 +1090,8 @@
handle Exn.Interrupt =>
let
val nontriv_js =
- read_output_file out_path |> snd |> snd |> map reindex
+ read_output_file new_kodkodi out_path
+ |> snd |> snd |> map reindex
in
(remove_temporary_files ();
Interrupted (SOME (triv_js @ nontriv_js)))
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Sun Aug 01 10:26:55 2010 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Sun Aug 01 17:43:51 2010 +0200
@@ -26,16 +26,21 @@
External of sink * string * string * string list |
ExternalV2 of sink * string * string * string list * string * string * string
+(* for compatibility with "SatSolver" *)
val berkmin_exec = getenv "BERKMIN_EXE"
(* (string * sat_solver_info) list *)
val static_list =
[("MiniSat", ExternalV2 (ToFile, "MINISAT_HOME", "minisat", [], "SAT", "",
"UNSAT")),
+ ("MiniSat_JNI", Internal (JNI, Incremental, ["MiniSat"])),
+ ("CryptoMiniSat", External (ToStdout, "CRYPTOMINISAT_HOME", "cryptominisat",
+ [])),
("PicoSAT", External (ToStdout, "PICOSAT_HOME", "picosat", [])),
("zChaff", ExternalV2 (ToStdout, "ZCHAFF_HOME", "zchaff", [],
"Instance Satisfiable", "",
"Instance Unsatisfiable")),
+ ("zChaff_JNI", Internal (JNI, Batch, ["zChaff"])),
("RSat", ExternalV2 (ToStdout, "RSAT_HOME", "rsat", ["-s"],
"s SATISFIABLE", "v ", "s UNSATISFIABLE")),
("BerkMin", ExternalV2 (ToStdout, "BERKMIN_HOME",
@@ -44,8 +49,6 @@
"solution =", "UNSATISFIABLE !!")),
("BerkMin_Alloy", External (ToStdout, "BERKMINALLOY_HOME", "berkmin", [])),
("Jerusat", External (ToStdout, "JERUSAT_HOME", "Jerusat1.3", [])),
- ("MiniSat_JNI", Internal (JNI, Incremental, ["MiniSat"])),
- ("zChaff_JNI", Internal (JNI, Batch, ["zChaff"])),
("SAT4J", Internal (Java, Incremental, ["DefaultSAT4J"])),
("SAT4J_Light", Internal (Java, Incremental, ["LightSAT4J"]))]
--- a/src/HOL/Tools/Nitpick/nitpick.ML Sun Aug 01 10:26:55 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Sun Aug 01 17:43:51 2010 +0200
@@ -35,6 +35,8 @@
star_linear_preds: bool,
fast_descrs: bool,
peephole_optim: bool,
+ datatype_sym_break: int,
+ kodkod_sym_break: int,
timeout: Time.time option,
tac_timeout: Time.time option,
max_threads: int,
@@ -106,6 +108,8 @@
star_linear_preds: bool,
fast_descrs: bool,
peephole_optim: bool,
+ datatype_sym_break: int,
+ kodkod_sym_break: int,
timeout: Time.time option,
tac_timeout: Time.time option,
max_threads: int,
@@ -191,9 +195,10 @@
boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints,
destroy_constrs, specialize, star_linear_preds, fast_descrs,
- peephole_optim, tac_timeout, max_threads, show_datatypes, show_consts,
- evals, formats, atomss, max_potential, max_genuine, check_potential,
- check_genuine, batch_size, ...} = params
+ 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
@@ -493,7 +498,7 @@
0
val settings = [("solver", commas_quote kodkod_sat_solver),
("bit_width", string_of_int bit_width),
- ("symmetry_breaking", "20"),
+ ("symmetry_breaking", string_of_int kodkod_sym_break),
("sharing", "3"),
("flatten", "false"),
("delay", signed_string_of_int delay)]
@@ -502,19 +507,22 @@
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 bits ofs kk
- rel_table datatypes
+ declarative_axioms_for_datatypes hol_ctxt binarize 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,
main_j0 |> bits > 0 ? Integer.add (bits + 1))
- val built_in_bounds = bounds_for_built_in_rels_in_formula debug
- univ_card nat_card int_card main_j0 formula
+ val (built_in_bounds, built_in_axioms) =
+ bounds_and_axioms_for_built_in_rels_in_formulas debug ofs
+ univ_card nat_card int_card main_j0
+ (formula :: declarative_axioms)
val bounds = built_in_bounds @ plain_bounds @ sel_bounds
|> not debug ? merge_bounds
+ val axioms = built_in_axioms @ declarative_axioms
val highest_arity =
fold Integer.max (map (fst o fst) (maps fst bounds)) 0
- val formula = fold_rev s_and declarative_axioms formula
+ val formula = fold_rev s_and axioms formula
val _ = if bits = 0 then () else check_bits bits formula
val _ = if formula = KK.False then ()
else check_arity univ_card highest_arity
@@ -904,9 +912,13 @@
"")); if skipped > 0 then "unknown" else "none")
else
(print_m (fn () =>
- "Nitpick could not find a" ^
- (if max_genuine = 1 then " better " ^ das_wort_model ^ "."
- else "ny better " ^ das_wort_model ^ "s.")); "potential")
+ excipit ("could not find a" ^
+ (if max_genuine = 1 then
+ " better " ^ das_wort_model ^ "."
+ else
+ "ny better " ^ das_wort_model ^ "s.") ^
+ " It checked"));
+ "potential")
else if found_really_genuine then
"genuine"
else
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Sun Aug 01 10:26:55 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Sun Aug 01 17:43:51 2010 +0200
@@ -56,6 +56,8 @@
("star_linear_preds", "true"),
("fast_descrs", "true"),
("peephole_optim", "true"),
+ ("datatype_sym_break", "5"),
+ ("kodkod_sym_break", "15"),
("timeout", "30 s"),
("tac_timeout", "500 ms"),
("max_threads", "0"),
@@ -245,6 +247,8 @@
val star_linear_preds = lookup_bool "star_linear_preds"
val fast_descrs = lookup_bool "fast_descrs"
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"
val timeout = if auto then NONE else lookup_time "timeout"
val tac_timeout = lookup_time "tac_timeout"
val max_threads = Int.max (0, lookup_int "max_threads")
@@ -273,7 +277,8 @@
merge_type_vars = merge_type_vars, binary_ints = binary_ints,
destroy_constrs = destroy_constrs, specialize = specialize,
star_linear_preds = star_linear_preds, fast_descrs = fast_descrs,
- peephole_optim = peephole_optim, timeout = timeout,
+ 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,
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Sun Aug 01 10:26:55 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Sun Aug 01 17:43:51 2010 +0200
@@ -8,12 +8,9 @@
signature NITPICK_KODKOD =
sig
type hol_context = Nitpick_HOL.hol_context
- type dtype_spec = Nitpick_Scope.dtype_spec
+ type datatype_spec = Nitpick_Scope.datatype_spec
type kodkod_constrs = Nitpick_Peephole.kodkod_constrs
type nut = Nitpick_Nut.nut
- type nfa_transition = Kodkod.rel_expr * typ
- type nfa_entry = typ * nfa_transition list
- type nfa_table = nfa_entry list
structure NameTable : TABLE
@@ -25,16 +22,17 @@
val tuple_set_from_atom_schema : (int * int) list -> Kodkod.tuple_set
val sequential_int_bounds : int -> Kodkod.int_bound list
val pow_of_two_int_bounds : int -> int -> Kodkod.int_bound list
- val bounds_for_built_in_rels_in_formula :
- bool -> int -> int -> int -> int -> Kodkod.formula -> Kodkod.bound list
+ val bounds_and_axioms_for_built_in_rels_in_formulas :
+ bool -> int Typtab.table -> int -> int -> int -> int -> Kodkod.formula list
+ -> Kodkod.bound list * Kodkod.formula list
val bound_for_plain_rel : Proof.context -> bool -> nut -> Kodkod.bound
val bound_for_sel_rel :
- Proof.context -> bool -> dtype_spec list -> nut -> Kodkod.bound
+ Proof.context -> bool -> datatype_spec list -> nut -> Kodkod.bound
val merge_bounds : Kodkod.bound list -> Kodkod.bound list
val declarative_axiom_for_plain_rel : kodkod_constrs -> nut -> Kodkod.formula
val declarative_axioms_for_datatypes :
- hol_context -> bool -> int -> int Typtab.table -> kodkod_constrs
- -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list
+ 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
end;
@@ -51,11 +49,13 @@
structure KK = Kodkod
-type nfa_transition = KK.rel_expr * typ
-type nfa_entry = typ * nfa_transition list
-type nfa_table = nfa_entry list
+structure NfaGraph = Typ_Graph
+
+fun pull x xs = x :: filter_out (curry (op =) x) xs
-structure NfaGraph = Typ_Graph
+fun is_datatype_good_and_old ({co = false, standard = true, deep = true, ...}
+ : datatype_spec) = true
+ | is_datatype_good_and_old _ = false
fun flip_nums n = index_seq 1 n @ [0] |> map KK.Num
@@ -122,19 +122,16 @@
aux (iter - 1) (2 * pow_of_two) (j + 1)
in aux (bits + 1) 1 j0 end
-fun built_in_rels_in_formula formula =
+fun built_in_rels_in_formulas formulas =
let
fun rel_expr_func (KK.Rel (x as (n, j))) =
- if x = unsigned_bit_word_sel_rel orelse x = signed_bit_word_sel_rel then
- I
- else
- (case AList.lookup (op =) (#rels initial_pool) n of
- SOME k => j < k ? insert (op =) x
- | NONE => I)
+ (j < 0 andalso x <> unsigned_bit_word_sel_rel andalso
+ x <> signed_bit_word_sel_rel)
+ ? insert (op =) x
| rel_expr_func _ = I
val expr_F = {formula_func = K I, rel_expr_func = rel_expr_func,
int_expr_func = K I}
- in KK.fold_formula expr_F formula [] end
+ in fold (KK.fold_formula expr_F) formulas [] end
val max_table_size = 65536
@@ -201,7 +198,8 @@
else if m = 0 orelse n = 0 then (0, 1)
else let val p = isa_zgcd (m, n) in (isa_div (m, p), isa_div (n, p)) end
-fun tabulate_built_in_rel debug univ_card nat_card int_card j0 (x as (n, _)) =
+fun tabulate_built_in_rel debug ofs univ_card nat_card int_card j0
+ (x as (n, _)) =
(check_arity univ_card n;
if x = not3_rel then
("not3", tabulate_func1 debug univ_card (2, j0) (curry (op -) 1))
@@ -241,15 +239,40 @@
else
raise ARG ("Nitpick_Kodkod.tabulate_built_in_rel", "unknown relation"))
-fun bound_for_built_in_rel debug univ_card nat_card int_card j0 x =
- let
- val (nick, ts) = tabulate_built_in_rel debug univ_card nat_card int_card
- j0 x
- in ([(x, nick)], [KK.TupleSet ts]) end
+fun bound_for_built_in_rel debug ofs univ_card nat_card int_card main_j0
+ (x as (n, j)) =
+ if n = 2 andalso j <= suc_rels_base then
+ let val (y as (k, j0), tabulate) = atom_seq_for_suc_rel x in
+ ([(x, "suc")],
+ if tabulate then
+ [KK.TupleSet (tabulate_func1 debug univ_card (k - 1, j0)
+ (Integer.add 1))]
+ else
+ [KK.TupleSet [], tuple_set_from_atom_schema [y, y]])
+ end
+ else
+ let
+ val (nick, ts) = tabulate_built_in_rel debug ofs univ_card nat_card
+ int_card main_j0 x
+ in ([(x, nick)], [KK.TupleSet ts]) end
-fun bounds_for_built_in_rels_in_formula debug univ_card nat_card int_card j0 =
- map (bound_for_built_in_rel debug univ_card nat_card int_card j0)
- o built_in_rels_in_formula
+fun axiom_for_built_in_rel (x as (n, j)) =
+ if n = 2 andalso j <= suc_rels_base then
+ let val (y as (k, j0), tabulate) = atom_seq_for_suc_rel x in
+ if tabulate orelse k < 2 then
+ NONE
+ else
+ SOME (KK.TotalOrdering (x, KK.AtomSeq y, KK.Atom j0, KK.Atom (j0 + 1)))
+ end
+ else
+ NONE
+fun bounds_and_axioms_for_built_in_rels_in_formulas debug ofs univ_card nat_card
+ int_card main_j0 formulas =
+ let val rels = built_in_rels_in_formulas formulas in
+ (map (bound_for_built_in_rel debug ofs univ_card nat_card int_card main_j0)
+ rels,
+ map_filter axiom_for_built_in_rel rels)
+ end
fun bound_comment ctxt debug nick T R =
short_name nick ^
@@ -284,11 +307,10 @@
else
[KK.TupleSet [],
if T1 = T2 andalso epsilon > delta andalso
- (datatype_spec dtypes T1 |> the |> pairf #co #standard)
- = (false, true) then
+ is_datatype_good_and_old (the (datatype_spec dtypes T1)) then
index_seq delta (epsilon - delta)
|> map (fn j =>
- KK.TupleProduct (KK.TupleSet [Kodkod.Tuple [j + j0]],
+ KK.TupleProduct (KK.TupleSet [KK.Tuple [j + j0]],
KK.TupleAtomSeq (j, j0)))
|> foldl1 KK.TupleUnion
else
@@ -334,8 +356,6 @@
map2 (fn j => fn x => KK.DeclOne ((1, j), KK.AtomSeq x))
(index_seq j0 (length schema)) schema
-(* The type constraint below is a workaround for a Poly/ML bug. *)
-
fun d_n_ary_function ({kk_all, kk_join, kk_lone, kk_one, ...} : kodkod_constrs)
R r =
let val body_R = body_rep R in
@@ -670,7 +690,7 @@
fun nfa_transitions_for_sel hol_ctxt binarize
({kk_project, ...} : kodkod_constrs) rel_table
- (dtypes : dtype_spec list) constr_x n =
+ (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
@@ -679,14 +699,14 @@
in
map_filter (fn (j, T) =>
if forall (not_equal T o #typ) dtypes then NONE
- else SOME (kk_project r (map KK.Num [0, j]), T))
+ 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, ...} : dtype_spec) = NONE
+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
@@ -698,7 +718,7 @@
fun direct_path_rel_exprs nfa start_T final_T =
case AList.lookup (op =) nfa final_T of
- SOME trans => map fst (filter (curry (op =) start_T o snd) trans)
+ 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 =
@@ -736,14 +756,168 @@
nfa |> graph_for_nfa |> NfaGraph.strong_conn
|> map (fn keys => filter (member (op =) keys o fst) nfa)
-fun acyclicity_axiom_for_datatype kk nfa start_T =
- #kk_no kk (#kk_intersect kk
- (loop_path_rel_expr kk nfa (map fst nfa) start_T) KK.Iden)
-fun acyclicity_axioms_for_datatypes hol_ctxt binarize kk rel_table dtypes =
- map_filter (nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes)
- dtypes
- |> strongly_connected_sub_nfas
- |> maps (fn nfa => map (acyclicity_axiom_for_datatype kk nfa 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)
+fun 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_ord (({const = (s1, _), delta = delta1, epsilon = epsilon1, ...},
+ {const = (s2, _), delta = delta2, epsilon = epsilon2, ...})
+ : constr_spec * constr_spec) =
+ prod_ord int_ord (prod_ord int_ord string_ord)
+ ((delta1, (epsilon2, s1)), (delta2, (epsilon2, s2)))
+
+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 has_nil_like_constr dtypes T =
+ case #constrs (the (datatype_spec dtypes T))
+ |> filter_out (is_self_recursive_constr_type o snd o #const) of
+ [{const = (_, T'), ...}] => T = T'
+ | _ => false
+
+fun sym_break_axioms_for_constr_pair hol_ctxt binarize
+ (kk as {kk_all, kk_or, kk_iff, kk_implies, kk_and, kk_some, kk_subset,
+ kk_intersect, kk_join, kk_project, ...}) rel_table nfas dtypes
+ (constr1 as {const = const1 as (_, T1), delta = delta1,
+ epsilon = epsilon1, ...},
+ constr2 as {const = const2 as (_, T2), delta = delta2,
+ epsilon = epsilon2, ...}) =
+ let
+ val dataT = body_type T1
+ val nfa = nfas |> find_first (exists (curry (op =) dataT o fst)) |> these
+ val rec_Ts = nfa |> map fst
+ val same_constr = (const1 = const2)
+ 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 same_constr 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) =>
+ (same_constr 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)]
+ ((if same_constr then kk_implies else kk_iff)
+ (if delta2 >= epsilon1 then KK.True
+ else gt kk z (KK.Var (1, 1)) (KK.Var (1, 0)))
+ (kk_or
+ (if has_nil_like_constr dtypes dataT andalso
+ T1 = dataT then
+ KK.True
+ else
+ kk_some (kk_intersect (subterms_r false sel_xs2 1)
+ (all_ge kk z (KK.Var (1, 0)))))
+ (if same_constr then
+ kk_and
+ (lex_order_rel_expr kk dtypes (sel_quadruples2 ()))
+ (if length rec_sel_xs2 > 1 then
+ kk_all [KK.DeclOne ((1, 2),
+ subterms_r true sel_xs1 0)]
+ (gt kk z (KK.Var (1, 1)) (KK.Var (1, 2)))
+ else
+ KK.True)
+ else
+ kk_all [KK.DeclOne ((1, 2),
+ subterms_r false sel_xs1 0)]
+ (gt kk z (KK.Var (1, 1)) (KK.Var (1, 2))))))]
+ 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 in
+ maps (sym_break_axioms_for_constr_pair hol_ctxt binarize kk rel_table nfas
+ dtypes)
+ ((constrs ~~ constrs) @ all_distinct_unordered_pairs_of constrs)
+ 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_good_and_old
+ |> 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 (rev_order o datatype_ord)
+ #> 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, ...})
@@ -778,7 +952,8 @@
val max_axiom =
if honors_explicit_max then
KK.True
- else if is_twos_complement_representable bits (epsilon - delta) then
+ 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",
@@ -791,7 +966,7 @@
end
end
fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table
- ({constrs, ...} : dtype_spec) =
+ ({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
@@ -816,13 +991,13 @@
(kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))
end
fun uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table
- ({constrs, ...} : dtype_spec) =
+ ({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, ...} : dtype_spec) =
+ ({card, constrs, ...} : datatype_spec) =
if forall #exclusive constrs then
[Integer.sum (map effective_constr_max constrs) = card |> formula_for_bool]
else
@@ -840,11 +1015,20 @@
partition_axioms_for_datatype j0 kk rel_table dtype
end
-fun declarative_axioms_for_datatypes hol_ctxt binarize bits ofs kk rel_table
- dtypes =
- acyclicity_axioms_for_datatypes hol_ctxt binarize kk rel_table dtypes @
- maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table)
- dtypes
+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,
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Sun Aug 01 10:26:55 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Sun Aug 01 17:43:51 2010 +0200
@@ -902,8 +902,8 @@
val all_values =
all_values_of_type pool wacky_names scope atomss sel_names rel_table
bounds
- fun is_codatatype_wellformed (cos : dtype_spec list)
- ({typ, card, ...} : dtype_spec) =
+ fun is_codatatype_wellformed (cos : datatype_spec list)
+ ({typ, card, ...} : datatype_spec) =
let
val ts = all_values card typ
val max_depth = Integer.sum (map #card cos)
@@ -935,7 +935,7 @@
[setmp_show_all_types (Syntax.pretty_term ctxt) t1,
Pretty.str oper, Syntax.pretty_term ctxt t2])
end
- fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) =
+ fun pretty_for_datatype ({typ, card, complete, ...} : datatype_spec) =
Pretty.block (Pretty.breaks
(Syntax.pretty_typ ctxt (uniterize_unarize_unbox_etc_type typ) ::
(case typ of
@@ -950,8 +950,8 @@
else [Pretty.str (unrep ())]))]))
fun integer_datatype T =
[{typ = T, card = card_of_type card_assigns T, co = false,
- standard = true, complete = (false, false), concrete = (true, true),
- deep = true, constrs = []}]
+ standard = true, self_rec = true, complete = (false, false),
+ concrete = (true, true), deep = true, constrs = []}]
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
val (codatatypes, datatypes) =
datatypes |> filter #deep |> List.partition #co
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Sun Aug 01 10:26:55 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Sun Aug 01 17:43:51 2010 +0200
@@ -721,7 +721,7 @@
fun choose_rep_for_sels_for_constr scope (x as (_, T)) =
fold_rev (choose_rep_for_nth_sel_for_constr scope x)
(~1 upto num_sels_for_constr_type T - 1)
-fun choose_rep_for_sels_of_datatype _ ({deep = false, ...} : dtype_spec) = I
+fun choose_rep_for_sels_of_datatype _ ({deep = false, ...} : datatype_spec) = I
| choose_rep_for_sels_of_datatype scope {constrs, ...} =
fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs
fun choose_reps_for_all_sels (scope as {datatypes, ...}) =
--- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML Sun Aug 01 10:26:55 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML Sun Aug 01 17:43:51 2010 +0200
@@ -23,6 +23,7 @@
val initial_pool : name_pool
val not3_rel : n_ary_index
val suc_rel : n_ary_index
+ val suc_rels_base : int
val unsigned_bit_word_sel_rel : n_ary_index
val signed_bit_word_sel_rel : n_ary_index
val nat_add_rel : n_ary_index
@@ -46,6 +47,8 @@
val int_for_atom : int * int -> int -> int
val atom_for_int : int * int -> int -> int
val is_twos_complement_representable : int -> int -> bool
+ val suc_rel_for_atom_seq : (int * int) * bool -> n_ary_index
+ val atom_seq_for_suc_rel : n_ary_index -> (int * int) * bool
val inline_rel_expr : rel_expr -> bool
val empty_n_ary_rel : int -> rel_expr
val num_seq : int -> int -> int_expr list
@@ -99,30 +102,27 @@
formula_reg: int,
rel_reg: int}
-(* If you add new built-in relations, make sure to increment the counters here
- as well to avoid name clashes (which fortunately would be detected by
- Kodkodi). *)
-val initial_pool =
- {rels = [(2, 10), (3, 20), (4, 10)], vars = [], formula_reg = 10,
- rel_reg = 10}
+(* FIXME: needed? *)
+val initial_pool = {rels = [], vars = [], formula_reg = 10, rel_reg = 10}
-val not3_rel = (2, 0)
-val suc_rel = (2, 1)
-val unsigned_bit_word_sel_rel = (2, 2)
-val signed_bit_word_sel_rel = (2, 3)
-val nat_add_rel = (3, 0)
-val int_add_rel = (3, 1)
-val nat_subtract_rel = (3, 2)
-val int_subtract_rel = (3, 3)
-val nat_multiply_rel = (3, 4)
-val int_multiply_rel = (3, 5)
-val nat_divide_rel = (3, 6)
-val int_divide_rel = (3, 7)
-val nat_less_rel = (3, 8)
-val int_less_rel = (3, 9)
-val gcd_rel = (3, 10)
-val lcm_rel = (3, 11)
-val norm_frac_rel = (4, 0)
+val not3_rel = (2, ~1)
+val unsigned_bit_word_sel_rel = (2, ~2)
+val signed_bit_word_sel_rel = (2, ~3)
+val suc_rel = (2, ~4)
+val suc_rels_base = ~5 (* must be the last of the binary series *)
+val nat_add_rel = (3, ~1)
+val int_add_rel = (3, ~2)
+val nat_subtract_rel = (3, ~3)
+val int_subtract_rel = (3, ~4)
+val nat_multiply_rel = (3, ~5)
+val int_multiply_rel = (3, ~6)
+val nat_divide_rel = (3, ~7)
+val int_divide_rel = (3, ~8)
+val nat_less_rel = (3, ~9)
+val int_less_rel = (3, ~10)
+val gcd_rel = (3, ~11)
+val lcm_rel = (3, ~12)
+val norm_frac_rel = (4, ~1)
fun atom_for_bool j0 = Atom o Integer.add j0 o int_from_bool
fun formula_for_bool b = if b then True else False
@@ -139,6 +139,23 @@
fun is_twos_complement_representable bits n =
let val max = reasonable_power 2 bits in n >= ~ max andalso n < max end
+val max_squeeze_card = 49
+
+fun squeeze (m, n) =
+ if n > max_squeeze_card then
+ raise TOO_LARGE ("Nitpick_Peephole.squeeze",
+ "too large cardinality (" ^ string_of_int n ^ ")")
+ else
+ (max_squeeze_card + 1) * m + n
+fun unsqueeze p = (p div (max_squeeze_card + 1), p mod (max_squeeze_card + 1))
+
+fun boolify (j, b) = 2 * j + (if b then 0 else 1)
+fun unboolify j = (j div 2, j mod 2 = 0)
+
+fun suc_rel_for_atom_seq (x, tabulate) =
+ (2, suc_rels_base - boolify (squeeze x, tabulate))
+fun atom_seq_for_suc_rel (_, j) = unboolify (~ j + suc_rels_base) |>> unsqueeze
+
fun is_none_product (Product (r1, r2)) =
is_none_product r1 orelse is_none_product r2
| is_none_product None = true
@@ -245,16 +262,18 @@
fun to_nat j = j - main_j0
val to_int = int_for_atom (int_card, main_j0)
+ val exists_empty_decl = exists (fn DeclOne (_, None) => true | _ => false)
+
fun s_all _ True = True
| s_all _ False = False
| s_all [] f = f
- | s_all ds (All (ds', f)) = All (ds @ ds', f)
- | s_all ds f = All (ds, f)
+ | s_all ds (All (ds', f)) = s_all (ds @ ds') f
+ | s_all ds f = if exists_empty_decl ds then True else All (ds, f)
fun s_exist _ True = True
| s_exist _ False = False
| s_exist [] f = f
- | s_exist ds (Exist (ds', f)) = Exist (ds @ ds', f)
- | s_exist ds f = Exist (ds, f)
+ | s_exist ds (Exist (ds', f)) = s_exist (ds @ ds') f
+ | s_exist ds f = if exists_empty_decl ds then False else Exist (ds, f)
fun s_formula_let _ True = True
| s_formula_let _ False = False
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Sun Aug 01 10:26:55 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Sun Aug 01 17:43:51 2010 +0200
@@ -18,11 +18,12 @@
explicit_max: int,
total: bool}
- type dtype_spec =
+ type datatype_spec =
{typ: typ,
card: int,
co: bool,
standard: bool,
+ self_rec: bool,
complete: bool * bool,
concrete: bool * bool,
deep: bool,
@@ -34,20 +35,22 @@
card_assigns: (typ * int) list,
bits: int,
bisim_depth: int,
- datatypes: dtype_spec list,
+ datatypes: datatype_spec list,
ofs: int Typtab.table}
- val datatype_spec : dtype_spec list -> typ -> dtype_spec option
- val constr_spec : dtype_spec list -> styp -> constr_spec
- val is_complete_type : dtype_spec list -> bool -> typ -> bool
- val is_concrete_type : dtype_spec list -> bool -> typ -> bool
- val is_exact_type : dtype_spec list -> bool -> typ -> bool
+ val is_asymmetric_nondatatype : typ -> bool
+ val datatype_spec : datatype_spec list -> typ -> datatype_spec option
+ val constr_spec : datatype_spec list -> styp -> constr_spec
+ val is_complete_type : datatype_spec list -> bool -> typ -> bool
+ val is_concrete_type : datatype_spec list -> bool -> typ -> bool
+ val is_exact_type : datatype_spec list -> bool -> typ -> bool
val offset_of_type : int Typtab.table -> typ -> int
val spec_of_type : scope -> typ -> int * int
val pretties_for_scope : scope -> bool -> Pretty.T list
val multiline_string_for_scope : scope -> string
val scopes_equivalent : scope * scope -> bool
val scope_less_eq : scope -> scope -> bool
+ val is_self_recursive_constr_type : typ -> bool
val all_scopes :
hol_context -> bool -> (typ option * int list) list
-> (styp option * int list) list -> (styp option * int list) list
@@ -69,11 +72,12 @@
explicit_max: int,
total: bool}
-type dtype_spec =
+type datatype_spec =
{typ: typ,
card: int,
co: bool,
standard: bool,
+ self_rec: bool,
complete: bool * bool,
concrete: bool * bool,
deep: bool,
@@ -85,7 +89,7 @@
card_assigns: (typ * int) list,
bits: int,
bisim_depth: int,
- datatypes: dtype_spec list,
+ datatypes: datatype_spec list,
ofs: int Typtab.table}
datatype row_kind = Card of typ | Max of styp
@@ -93,11 +97,14 @@
type row = row_kind * int list
type block = row list
-fun datatype_spec (dtypes : dtype_spec list) T =
+val is_asymmetric_nondatatype =
+ is_iterator_type orf is_integer_type orf is_bit_type
+
+fun datatype_spec (dtypes : datatype_spec list) T =
List.find (curry (op =) T o #typ) dtypes
fun constr_spec [] x = raise TERM ("Nitpick_Scope.constr_spec", [Const x])
- | constr_spec ({constrs, ...} :: dtypes : dtype_spec list) (x as (s, T)) =
+ | constr_spec ({constrs, ...} :: dtypes : datatype_spec list) (x as (s, T)) =
case List.find (curry (op =) (s, body_type T) o (apsnd body_type o #const))
constrs of
SOME c => c
@@ -361,12 +368,11 @@
end
handle Option.Option => NONE
-fun offset_table_for_card_assigns assigns dtypes =
+fun offset_table_for_card_assigns dtypes assigns =
let
fun aux next _ [] = Typtab.update_new (dummyT, next)
| aux next reusable ((T, k) :: assigns) =
- if k = 1 orelse is_iterator_type T orelse is_integer_type T
- orelse is_bit_type T then
+ if k = 1 orelse is_asymmetric_nondatatype T then
aux next reusable assigns
else if length (these (Option.map #constrs (datatype_spec dtypes T)))
> 1 then
@@ -376,7 +382,7 @@
SOME j0 => Typtab.update_new (T, j0) #> aux next reusable assigns
| NONE => Typtab.update_new (T, next)
#> aux (next + k) ((k, next) :: reusable) assigns
- in aux 0 [] assigns Typtab.empty end
+ in Typtab.empty |> aux 0 [] assigns end
fun domain_card max card_assigns =
Integer.prod o map (bounded_card_of_type max max card_assigns) o binder_types
@@ -438,6 +444,7 @@
val self_recs = map (is_self_recursive_constr_type o snd) xs
val (num_self_recs, num_non_self_recs) =
List.partition I self_recs |> pairself length
+ val self_rec = num_self_recs > 0
fun is_complete facto =
has_exact_card hol_ctxt facto finitizable_dataTs card_assigns T
fun is_concrete facto =
@@ -454,8 +461,8 @@
num_non_self_recs)
(sort (bool_ord o swap o pairself fst) (self_recs ~~ xs)) []
in
- {typ = T, card = card, co = co, standard = standard, complete = complete,
- concrete = concrete, deep = deep, constrs = constrs}
+ {typ = T, card = card, co = co, standard = standard, self_rec = self_rec,
+ complete = complete, concrete = concrete, deep = deep, constrs = constrs}
end
fun scope_from_descriptor (hol_ctxt as {ctxt, stds, ...}) binarize deep_dataTs
@@ -473,7 +480,7 @@
in
{hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
datatypes = datatypes, bits = bits, bisim_depth = bisim_depth,
- ofs = offset_table_for_card_assigns card_assigns datatypes}
+ ofs = offset_table_for_card_assigns datatypes card_assigns}
end
fun repair_cards_assigns_wrt_boxing_etc _ _ [] = []