From 7dabf49077b7e7671ebfae52b43486db98efe0ab Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 10 Jul 2015 15:03:35 +0200
Subject: [PATCH] Get more tests if they are easy to get

---
 src/main/scala/leon/synthesis/rules/CEGIS.scala     | 2 +-
 src/main/scala/leon/synthesis/rules/CEGISLike.scala | 6 ++++--
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/leon/synthesis/rules/CEGIS.scala b/src/main/scala/leon/synthesis/rules/CEGIS.scala
index de9e7bedb..038e98427 100644
--- a/src/main/scala/leon/synthesis/rules/CEGIS.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGIS.scala
@@ -12,7 +12,7 @@ case object CEGIS extends CEGISLike[TypeTree]("CEGIS") {
   def getParams(sctx: SynthesisContext, p: Problem) = {
     import ExpressionGrammars._
     CegisParams(
-      grammar = depthBound(default(sctx, p), 2),
+      grammar = depthBound(default(sctx, p), 2), // This limits type depth
       rootLabel = {(tpe: TypeTree) => tpe }
     )
   }
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 2eabcfe44..52f104bae 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -701,11 +701,13 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
         /**
          * We generate tests for discarding potential programs
          */
+        val nTests = if (p.pc == BooleanLiteral(true)) 50 else 20
+
         val inputIterator: Iterator[Seq[Expr]] = if (useVanuatoo) {
-          new VanuatooDataGen(sctx.context, sctx.program).generateFor(p.as, p.pc, 20, 3000)
+          new VanuatooDataGen(sctx.context, sctx.program).generateFor(p.as, p.pc, nTests, 3000)
         } else {
           val evaluator = new DualEvaluator(sctx.context, sctx.program, CodeGenParams.default)
-          new GrammarDataGen(evaluator, ExpressionGrammars.ValueGrammar).generateFor(p.as, p.pc, 20, 1000)
+          new GrammarDataGen(evaluator, ExpressionGrammars.ValueGrammar).generateFor(p.as, p.pc, nTests, 1000)
         }
 
         val cachedInputIterator = new Iterator[Example] {
-- 
GitLab