From 4277183321ea00962acdc7c055e6daa4e5bc68bb Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 15 Apr 2015 02:17:56 +0200
Subject: [PATCH] Remove dependencies on NaiveDataGen, fix testgen when no
input
---
.../scala/leon/datagen/GrammarDataGen.scala | 46 +++++++++++--------
.../scala/leon/datagen/NaiveDataGen.scala | 1 +
.../scala/leon/datagen/VanuatooDataGen.scala | 3 +-
.../scala/leon/purescala/Constructors.scala | 26 +++++------
.../scala/leon/test/purescala/DataGen.scala | 2 +-
5 files changed, 42 insertions(+), 36 deletions(-)
diff --git a/src/main/scala/leon/datagen/GrammarDataGen.scala b/src/main/scala/leon/datagen/GrammarDataGen.scala
index da2e54a48..c483233e6 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 e7034d752..81f50f65b 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 c9fbbff70..ecb764eb4 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 dbb7f361b..3c4af36ed 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 e2b89ad05..2e1420b25 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
--
GitLab