optimize generated Kodkod formula
authorblanchet
Mon, 02 Aug 2010 15:52:32 +0200
changeset 38164 346df80a0924
parent 38163 bc546396b818
child 38165 9797be44df23
optimize generated Kodkod formula
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Aug 02 14:27:20 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Aug 02 15:52:32 2010 +0200
@@ -436,13 +436,11 @@
   case arity_of_rep R1 of
     1 => kk_join r1 r2
   | arity1 =>
-    let
-      val unpacked_rs1 =
-        if inline_rel_expr r1 then unpack_vect_in_chunks kk 1 arity1 r1
-        else unpack_products r1
-    in
+    let val unpacked_rs1 = unpack_products r1 in
       if one andalso length unpacked_rs1 = arity1 then
         fold kk_join unpacked_rs1 r2
+      else if one andalso inline_rel_expr r1 then
+        fold kk_join (unpack_vect_in_chunks kk 1 arity1 r1) r2
       else
         kk_project_seq
             (kk_intersect (kk_product r1 (full_rel_for_rep res_R)) r2)