diff --git a/src/main/scala/leon/datagen/GrammarDataGen.scala b/src/main/scala/leon/datagen/GrammarDataGen.scala index 29e102281ae6572f86a286404cee9dfb1d670bdd..ffe7b8b4741d7323a99bdfc2741722fb356b5394 100644 --- a/src/main/scala/leon/datagen/GrammarDataGen.scala +++ b/src/main/scala/leon/datagen/GrammarDataGen.scala @@ -59,8 +59,20 @@ class GrammarDataGen(evaluator: Evaluator, grammar: ExpressionGrammar = ValueGra } def generateFor(ins: Seq[Identifier], satisfying: Expr, maxValid: Int, maxEnumerated: Int): Iterator[Seq[Expr]] = { + + 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 + } + } + if (ins.isEmpty) { - Iterator.empty + Iterator(Seq[Expr]()).filter(filterCond) } else { val values = generate(tupleTypeWrap(ins.map{ _.getType })) @@ -68,17 +80,6 @@ class GrammarDataGen(evaluator: Evaluator, grammar: ExpressionGrammar = ValueGra 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)