# HG changeset patch
# User bulwahn
# Date 1320996768 -3600
# Node ID 74515e8e6046bed1fd7abd6adce7714812c7dbb3
# Parent  dc2236b19a3def67a26b312b46425abc986460f3
renaming example invocations: tester predicate_compile is renamed to smart_exhaustive

diff -r dc2236b19a3d -r 74515e8e6046 src/HOL/Predicate_Compile_Examples/IMP_1.thy
--- a/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Fri Nov 11 08:32:45 2011 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Fri Nov 11 08:32:48 2011 +0100
@@ -26,7 +26,7 @@
 
 lemma
   "exec c s s' ==> exec (Seq c c) s s'"
-quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 100, timeout = 600.0, expect = counterexample]
+quickcheck[tester = smart_exhaustive, size = 2, iterations = 100, timeout = 600.0, expect = counterexample]
 oops
 
 
diff -r dc2236b19a3d -r 74515e8e6046 src/HOL/Predicate_Compile_Examples/IMP_2.thy
--- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Fri Nov 11 08:32:45 2011 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Fri Nov 11 08:32:48 2011 +0100
@@ -29,7 +29,7 @@
 
 lemma
   "exec c s s' ==> exec (Seq c c) s s'"
-quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 100, timeout = 600.0, expect = counterexample]
+quickcheck[tester = smart_exhaustive, size = 2, iterations = 100, timeout = 600.0, expect = counterexample]
 oops
 
 
diff -r dc2236b19a3d -r 74515e8e6046 src/HOL/Predicate_Compile_Examples/IMP_3.thy
--- a/src/HOL/Predicate_Compile_Examples/IMP_3.thy	Fri Nov 11 08:32:45 2011 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_3.thy	Fri Nov 11 08:32:48 2011 +0100
@@ -29,7 +29,7 @@
 
 lemma
   "exec c s s' ==> exec (Seq c c) s s'"
-  quickcheck[tester = predicate_compile_ff_nofs, size=2, iterations=100, quiet = false, expect = counterexample]
+  quickcheck[tester = smart_exhaustive, size=2, iterations=100, quiet = false, expect = counterexample]
 oops
 
 
diff -r dc2236b19a3d -r 74515e8e6046 src/HOL/Predicate_Compile_Examples/IMP_4.thy
--- a/src/HOL/Predicate_Compile_Examples/IMP_4.thy	Fri Nov 11 08:32:45 2011 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_4.thy	Fri Nov 11 08:32:48 2011 +0100
@@ -30,7 +30,7 @@
 lemma
   "exec c s s' ==> exec (Seq c c) s s'"
   nitpick (* nitpick fails here! *)
-  quickcheck[tester = predicate_compile_wo_ff, size=2, iterations=100, expect=counterexample]
+  quickcheck[tester = smart_exhaustive, size=2, iterations=100, expect=counterexample]
 oops
 
 end
diff -r dc2236b19a3d -r 74515e8e6046 src/HOL/Predicate_Compile_Examples/List_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Fri Nov 11 08:32:45 2011 +0100
+++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Fri Nov 11 08:32:48 2011 +0100
@@ -20,7 +20,7 @@
 
 lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
 quickcheck[tester = random, iterations = 10000]
-quickcheck[tester = predicate_compile_wo_ff, iterations = 1, expect = counterexample]
+quickcheck[tester = smart_exhaustive, iterations = 1, expect = counterexample]
 quickcheck[tester = prolog, expect = counterexample]
 oops
 
diff -r dc2236b19a3d -r 74515e8e6046 src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Fri Nov 11 08:32:45 2011 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Fri Nov 11 08:32:48 2011 +0100
@@ -93,8 +93,7 @@
 (*nitpick
 quickcheck[tester = random, iterations = 10000]
 quickcheck[tester = predicate_compile_wo_ff]
-quickcheck[tester = predicate_compile_ff_fs]
-oops*)
+quickcheck[tester = predicate_compile_ff_fs]*)
 oops
 
 
@@ -117,7 +116,8 @@
  prolog-style generation. *}
 
 lemma "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
-quickcheck[tester = random, iterations = 100000]
+quickcheck[exhaustive]
+quickcheck[tester = random, iterations = 1000]
 (*quickcheck[tester = predicate_compile_wo_ff]*)
 (*quickcheck[tester = predicate_compile_ff_fs, iterations = 1]*)
 (*quickcheck[tester = prolog, iterations = 1, size = 1]*)
@@ -170,13 +170,13 @@
   assumes "q = Seq (Sym N0) (Sym N0)"
   assumes "s = [N0, N0]"
 shows "prop_regex (n, (k, (p, (q, s))))"
-quickcheck[tester = predicate_compile_wo_ff]
+quickcheck[tester = smart_exhaustive, depth = 30]
 quickcheck[tester = prolog]
 oops
 
 lemma "prop_regex a_sol"
 quickcheck[tester = random]
-quickcheck[tester = predicate_compile_ff_fs]
+quickcheck[tester = smart_exhaustive]
 oops
 
 value [code] "prop_regex a_sol"