# HG changeset patch
# User blanchet
# Date 1303206971 -7200
# Node ID 4a929b0630c3f8ca31a900ffa5dded14a098b024
# Parent  13798dcbdca53f7d967f68d2e7d6159e8af33758
check arity of bound variables to avoid generating too large Kodkod problems -- an issue that arose in the context of TPTP/CASC

diff -r 13798dcbdca5 -r 4a929b0630c3 src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Apr 18 17:07:47 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Apr 19 11:56:11 2011 +0200
@@ -698,9 +698,19 @@
 fun choose_reps_for_all_sels (scope as {datatypes, ...}) =
   fold (choose_rep_for_sels_of_datatype scope) datatypes o pair []
 
-fun choose_rep_for_bound_var scope v table =
-  let val R = best_one_rep_for_type scope (type_of v) in
-    NameTable.update (v, R) table
+val min_univ_card = 2
+
+fun choose_rep_for_bound_var scope v =
+  let
+    val R = best_one_rep_for_type scope (type_of v)
+    val arity = arity_of_rep R
+  in
+    if arity > KK.max_arity min_univ_card then
+      raise TOO_LARGE ("Nitpick_Nut.choose_rep_for_bound_var",
+                       "arity " ^ string_of_int arity ^ " of bound variable \
+                       \too large")
+    else
+      NameTable.update (v, R)
   end
 
 (* A nut is said to be constructive if whenever it evaluates to unknown in our