diff --git a/src/main/scala/leon/synthesis/rules/CEGIS.scala b/src/main/scala/leon/synthesis/rules/CEGIS.scala index de9e7bedb8dbffa1f025ec00c589e34b66c558c3..038e9842789c6a0e501451dc5f1bc89ca078db13 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 2eabcfe44a0f7322012869382dd9935bfb61714d..52f104bae48d0870a24541a8266cdec2ea8d1cb5 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] {