diff --git a/src/main/scala/leon/datagen/GrammarDataGen.scala b/src/main/scala/leon/datagen/GrammarDataGen.scala index da2e54a48929006ccc2a8c23fc65c9a28f71bd83..c483233e6324752575dfaab275c3313ece077db0 100644 --- a/src/main/scala/leon/datagen/GrammarDataGen.scala +++ b/src/main/scala/leon/datagen/GrammarDataGen.scala @@ -28,28 +28,36 @@ import synthesis.utils._ * e.g. by passing trees representing variables for the "bounds". */ class GrammarDataGen(evaluator: Evaluator, grammar: ExpressionGrammar[TypeTree] = ExpressionGrammars.ValueGrammar) extends DataGenerator { - def generateFor(ins: Seq[Identifier], satisfying: Expr, maxValid: Int, maxEnumerated: Int): Iterator[Seq[Expr]] = { + def generate(tpe: TypeTree): Iterator[Expr] = { val enum = new MemoizedEnumerator[TypeTree, Expr](grammar.getProductions) - val values = enum.iterator(tupleTypeWrap(ins.map{ _.getType })) + enum.iterator(tpe) + } - val detupled = values.map { - v => unwrapTuple(v, ins.size) - } - - def filterCond(vs: Seq[Expr]): Boolean = satisfying match { - case BooleanLiteral(true) => - true - case e => - // in -> e should be enough. We shouldn't find any subexpressions of in. - evaluator.eval(e, (ins zip vs).toMap) match { - case EvaluationResults.Successful(BooleanLiteral(true)) => true - case _ => false - } + def generateFor(ins: Seq[Identifier], satisfying: Expr, maxValid: Int, maxEnumerated: Int): Iterator[Seq[Expr]] = { + if (ins.isEmpty) { + Iterator.empty + } else { + val values = generate(tupleTypeWrap(ins.map{ _.getType })) + + val detupled = values.map { + v => unwrapTuple(v, ins.size) + } + + def filterCond(vs: Seq[Expr]): Boolean = satisfying match { + case BooleanLiteral(true) => + true + case e => + // in -> e should be enough. We shouldn't find any subexpressions of in. + evaluator.eval(e, (ins zip vs).toMap) match { + case EvaluationResults.Successful(BooleanLiteral(true)) => true + case _ => false + } + } + + detupled.take(maxEnumerated) + .filter(filterCond) + .take(maxValid) } - - detupled.take(maxEnumerated) - .filter(filterCond) - .take(maxValid) } } diff --git a/src/main/scala/leon/datagen/NaiveDataGen.scala b/src/main/scala/leon/datagen/NaiveDataGen.scala index e7034d75256dd967bde5698a9fec2e7dc734736b..81f50f65b20cb58fa2f0675c5861055a6769b6f0 100644 --- a/src/main/scala/leon/datagen/NaiveDataGen.scala +++ b/src/main/scala/leon/datagen/NaiveDataGen.scala @@ -16,6 +16,7 @@ import scala.collection.mutable.{Map=>MutableMap} /** Utility functions to generate values of a given type. * In fact, it could be used to generate *terms* of a given type, * e.g. by passing trees representing variables for the "bounds". */ +@deprecated("3.4", "NaiveDataGen is deprecated, use GrammarDataGen with ValueGrammar") class NaiveDataGen(ctx: LeonContext, p: Program, evaluator: Evaluator, _bounds : Option[Map[TypeTree,Seq[Expr]]] = None) extends DataGenerator { val bounds = _bounds.getOrElse(Map()) diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala index c9fbbff703e82b993c2fe3dd0506512d260069d9..ecb764eb48b0976841d3c0cd91939f72b3ae2309 100644 --- a/src/main/scala/leon/datagen/VanuatooDataGen.scala +++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala @@ -12,13 +12,14 @@ import purescala.Extractors._ import purescala.Constructors._ import codegen.CompilationUnit +import codegen.CodeGenParams import codegen.runtime.LeonCodeGenRuntimeMonitor import vanuatoo.{Pattern => VPattern, _} import evaluators._ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator { - val unit = new CompilationUnit(ctx, p) + val unit = new CompilationUnit(ctx, p, CodeGenParams.default.copy(doInstrument = true)) val ints = (for (i <- Set(0, 1, 2, 3)) yield { i -> Constructor[Expr, TypeTree](List(), Int32Type, s => IntLiteral(i), ""+i) diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala index dbb7f361bdbd8a968ae201175e28ad2731393038..3c4af36ed6cf7a30b07839e33b3ecd1e8b60cb39 100644 --- a/src/main/scala/leon/purescala/Constructors.scala +++ b/src/main/scala/leon/purescala/Constructors.scala @@ -278,21 +278,17 @@ object Constructors { case (IsTyped(_, Int32Type), IsTyped(_, Int32Type)) => BVMinus(lhs, rhs) } - def times(lhs: Expr, rhs: Expr): Expr = { - val r = (lhs, rhs) match { - case (InfiniteIntegerLiteral(bi), _) if bi == 1 => rhs - case (_, InfiniteIntegerLiteral(bi)) if bi == 1 => lhs - case (InfiniteIntegerLiteral(bi), _) if bi == 0 => InfiniteIntegerLiteral(0) - case (_, InfiniteIntegerLiteral(bi)) if bi == 0 => InfiniteIntegerLiteral(0) - case (IntLiteral(1), _) => rhs - case (_, IntLiteral(1)) => lhs - case (IntLiteral(0), _) => IntLiteral(0) - case (_, IntLiteral(0)) => IntLiteral(0) - case (IsTyped(_, IntegerType), IsTyped(_, IntegerType)) => Times(lhs, rhs) - case (IsTyped(_, Int32Type), IsTyped(_, Int32Type)) => BVTimes(lhs, rhs) - } - println("!@#!@# "+lhs+" * "+rhs+" == "+r) - r + def times(lhs: Expr, rhs: Expr): Expr = (lhs, rhs) match { + case (InfiniteIntegerLiteral(bi), _) if bi == 1 => rhs + case (_, InfiniteIntegerLiteral(bi)) if bi == 1 => lhs + case (InfiniteIntegerLiteral(bi), _) if bi == 0 => InfiniteIntegerLiteral(0) + case (_, InfiniteIntegerLiteral(bi)) if bi == 0 => InfiniteIntegerLiteral(0) + case (IntLiteral(1), _) => rhs + case (_, IntLiteral(1)) => lhs + case (IntLiteral(0), _) => IntLiteral(0) + case (_, IntLiteral(0)) => IntLiteral(0) + case (IsTyped(_, IntegerType), IsTyped(_, IntegerType)) => Times(lhs, rhs) + case (IsTyped(_, Int32Type), IsTyped(_, Int32Type)) => BVTimes(lhs, rhs) } } diff --git a/src/test/scala/leon/test/purescala/DataGen.scala b/src/test/scala/leon/test/purescala/DataGen.scala index e2b89ad050a14ab7cae64b456f0be14f0d01e963..2e1420b256005ac2710187da1af22e7e828940e7 100644 --- a/src/test/scala/leon/test/purescala/DataGen.scala +++ b/src/test/scala/leon/test/purescala/DataGen.scala @@ -59,7 +59,7 @@ class DataGen extends LeonTestSuite { val prog = parseString(p) val eval = new DefaultEvaluator(testContext, prog) - val generator = new NaiveDataGen(testContext, prog, eval) + val generator = new GrammarDataGen(eval) generator.generate(BooleanType).toSet.size === 2 generator.generate(TupleType(Seq(BooleanType,BooleanType))).toSet.size === 4