From 572d4125135deea75f0cf3683fc40c750dac5162 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 3 Feb 2016 19:15:39 +0100
Subject: [PATCH] Improve value generation with generic types
ValueGrammar only generates one generic value.
GrammarDataGen will expand to all non-redundant value combinations.
Use GrammarDataGen instead of bonsai everywhere in Leon (except TEGISLike)
---
.../scala/leon/datagen/GrammarDataGen.scala | 42 ++++++++++++++++-
.../scala/leon/grammars/EqualityGrammar.scala | 2 -
.../scala/leon/grammars/ValueGrammar.scala | 6 +--
src/main/scala/leon/purescala/DefOps.scala | 7 ---
src/main/scala/leon/purescala/ExprOps.scala | 8 ++--
.../scala/leon/purescala/ScalaPrinter.scala | 4 +-
src/main/scala/leon/repair/Repairman.scala | 28 ++---------
.../scala/leon/synthesis/ExamplesFinder.scala | 39 +++++-----------
.../disambiguation/ExamplesAdder.scala | 5 +-
.../disambiguation/QuestionBuilder.scala | 46 ++++++++-----------
.../leon/synthesis/rules/BottomUpTegis.scala | 1 -
.../leon/synthesis/rules/CEGISLike.scala | 10 +++-
.../leon/synthesis/rules/StringRender.scala | 31 +++++--------
.../scala/leon/synthesis/rules/TEGIS.scala | 1 -
src/main/scala/leon/utils/UniqueCounter.scala | 1 +
.../etienne-thesis/BatchedQueue/Enqueue.scala | 15 ++----
16 files changed, 111 insertions(+), 135 deletions(-)
diff --git a/src/main/scala/leon/datagen/GrammarDataGen.scala b/src/main/scala/leon/datagen/GrammarDataGen.scala
index 23c1ed5b8..04541e78a 100644
--- a/src/main/scala/leon/datagen/GrammarDataGen.scala
+++ b/src/main/scala/leon/datagen/GrammarDataGen.scala
@@ -4,14 +4,17 @@ package leon
package datagen
import purescala.Expressions._
-import purescala.Types.TypeTree
+import purescala.Types._
import purescala.Common._
import purescala.Constructors._
import purescala.Extractors._
+import purescala.ExprOps._
import evaluators._
import bonsai.enumerators._
import grammars._
+import utils.UniqueCounter
+import utils.SeqUtils.cartesianProduct
/** Utility functions to generate values of a given type.
* In fact, it could be used to generate *terms* of a given type,
@@ -19,9 +22,40 @@ import grammars._
class GrammarDataGen(evaluator: Evaluator, grammar: ExpressionGrammar[TypeTree] = ValueGrammar) extends DataGenerator {
implicit val ctx = evaluator.context
+ // Assume e contains generic values with index 0.
+ // Return a series of expressions with all normalized combinations of generic values.
+ private def expandGenerics(e: Expr): Seq[Expr] = {
+ val c = new UniqueCounter[TypeParameter]
+ val withUniqueCounters: Expr = postMap {
+ case GenericValue(t, _) =>
+ Some(GenericValue(t, c.next(t)))
+ case _ => None
+ }(e)
+
+ val indices = c.current
+
+ val (tps, substInt) = (for {
+ tp <- indices.keySet.toSeq
+ } yield tp -> (for {
+ from <- 0 to indices(tp)
+ to <- 0 to from
+ } yield (from, to))).unzip
+
+ val combos = cartesianProduct(substInt)
+
+ val substitutions = combos map { subst =>
+ tps.zip(subst).map { case (tp, (from, to)) =>
+ (GenericValue(tp, from): Expr) -> (GenericValue(tp, to): Expr)
+ }.toMap
+ }
+
+ substitutions map (replace(_, withUniqueCounters))
+
+ }
+
def generate(tpe: TypeTree): Iterator[Expr] = {
val enum = new MemoizedEnumerator[TypeTree, Expr, ProductionRule[TypeTree, Expr]](grammar.getProductions)
- enum.iterator(tpe)
+ enum.iterator(tpe).flatMap(expandGenerics)
}
def generateFor(ins: Seq[Identifier], satisfying: Expr, maxValid: Int, maxEnumerated: Int): Iterator[Seq[Expr]] = {
@@ -51,4 +85,8 @@ class GrammarDataGen(evaluator: Evaluator, grammar: ExpressionGrammar[TypeTree]
}
}
+ def generateMapping(ins: Seq[Identifier], satisfying: Expr, maxValid: Int, maxEnumerated: Int) = {
+ generateFor(ins, satisfying, maxValid, maxEnumerated) map (ins zip _)
+ }
+
}
diff --git a/src/main/scala/leon/grammars/EqualityGrammar.scala b/src/main/scala/leon/grammars/EqualityGrammar.scala
index fdcf079fa..a2f9c4136 100644
--- a/src/main/scala/leon/grammars/EqualityGrammar.scala
+++ b/src/main/scala/leon/grammars/EqualityGrammar.scala
@@ -6,8 +6,6 @@ package grammars
import purescala.Types._
import purescala.Constructors._
-import bonsai._
-
/** A grammar of equalities
*
* @param types The set of types for which equalities will be generated
diff --git a/src/main/scala/leon/grammars/ValueGrammar.scala b/src/main/scala/leon/grammars/ValueGrammar.scala
index 8548c1a95..d3c422017 100644
--- a/src/main/scala/leon/grammars/ValueGrammar.scala
+++ b/src/main/scala/leon/grammars/ValueGrammar.scala
@@ -35,9 +35,9 @@ case object ValueGrammar extends ExpressionGrammar[TypeTree] {
)
case tp: TypeParameter =>
- for (ind <- (1 to 3).toList) yield {
- terminal(GenericValue(tp, ind))
- }
+ List(
+ terminal(GenericValue(tp, 0))
+ )
case TupleType(stps) =>
List(
diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index 4085050d2..578f52bff 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -275,13 +275,6 @@ object DefOps {
None
}
- /**
- *
- * @param p
- * @param fdMapF
- * @param fiMapF
- * @return
- */
def replaceFunDefs(p: Program)(fdMapF: FunDef => Option[FunDef],
fiMapF: (FunctionInvocation, FunDef) => Option[Expr] = defaultFiMap) = {
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index ed86c1806..73fcb4849 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -442,7 +442,7 @@ object ExprOps {
case l @ Let(i,e,b) =>
val newID = FreshIdentifier(i.name, i.getType, alwaysShowUniqueID = true).copiedFrom(i)
- Some(Let(newID, e, replace(Map(Variable(i) -> Variable(newID)), b)))
+ Some(Let(newID, e, replaceFromIDs(Map(i -> Variable(newID)), b)))
case _ => None
}(expr)
@@ -597,7 +597,7 @@ object ExprOps {
def simplerLet(t: Expr) : Option[Expr] = t match {
case letExpr @ Let(i, t: Terminal, b) if isDeterministic(b) =>
- Some(replace(Map(Variable(i) -> t), b))
+ Some(replaceFromIDs(Map(i -> t), b))
case letExpr @ Let(i,e,b) if isDeterministic(b) => {
val occurrences = count {
@@ -608,7 +608,7 @@ object ExprOps {
if(occurrences == 0) {
Some(b)
} else if(occurrences == 1) {
- Some(replace(Map(Variable(i) -> e), b))
+ Some(replaceFromIDs(Map(i -> e), b))
} else {
None
}
@@ -619,7 +619,7 @@ object ExprOps {
val (remIds, remExprs) = (ids zip exprs).filter {
case (id, value: Terminal) =>
- newBody = replace(Map(Variable(id) -> value), newBody)
+ newBody = replaceFromIDs(Map(id -> value), newBody)
//we replace, so we drop old
false
case (id, value) =>
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 67cc99464..11f0c187e 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -9,14 +9,12 @@ import Common._
import Expressions._
import Types._
import Definitions._
-import org.apache.commons.lang3.StringEscapeUtils
-/** This pretty-printer only print valid scala syntax */
+/** This pretty-printer only prints valid scala syntax */
class ScalaPrinter(opts: PrinterOptions,
opgm: Option[Program],
sb: StringBuffer = new StringBuffer) extends PrettyPrinter(opts, opgm, sb) {
- private val dbquote = "\""
override def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = {
tree match {
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 19095f6f4..4f308e279 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -3,6 +3,7 @@
package leon
package repair
+import leon.datagen.GrammarDataGen
import purescala.Common._
import purescala.Definitions._
import purescala.Expressions._
@@ -236,29 +237,10 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
def discoverTests(): ExamplesBank = {
- import bonsai.enumerators._
-
val maxEnumerated = 1000
val maxValid = 400
val evaluator = new CodeGenEvaluator(ctx, program, CodeGenParams.default)
- val enum = new MemoizedEnumerator[TypeTree, Expr, ProductionRule[TypeTree, Expr]](ValueGrammar.getProductions)
-
- val inputs = enum.iterator(tupleTypeWrap(fd.params map { _.getType})).map(unwrapTuple(_, fd.params.size))
-
- val filtering: Seq[Expr] => Boolean = fd.precondition match {
- case None =>
- _ => true
- case Some(pre) =>
- val argIds = fd.paramIds
- evaluator.compile(pre, argIds) match {
- case Some(evalFun) =>
- val sat = EvaluationResults.Successful(BooleanLiteral(true));
- { (es: Seq[Expr]) => evalFun(new solvers.Model((argIds zip es).toMap)) == sat }
- case None =>
- { _ => false }
- }
- }
val inputsToExample: Seq[Expr] => Example = { ins =>
evaluator.eval(functionInvocation(fd, ins)) match {
@@ -269,10 +251,10 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
}
}
- val generatedTests = inputs
- .take(maxEnumerated)
- .filter(filtering)
- .take(maxValid)
+ val dataGen = new GrammarDataGen(evaluator)
+
+ val generatedTests = dataGen
+ .generateFor(fd.paramIds, fd.precOrTrue, maxValid, maxEnumerated)
.map(inputsToExample)
.toList
diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala
index 5728d3b14..1755966e0 100644
--- a/src/main/scala/leon/synthesis/ExamplesFinder.scala
+++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala
@@ -6,13 +6,10 @@ package synthesis
import purescala.Expressions._
import purescala.Definitions._
import purescala.ExprOps._
-import purescala.Types.TypeTree
import purescala.Common._
import purescala.Constructors._
-import purescala.Extractors._
import evaluators._
import grammars._
-import bonsai.enumerators._
import codegen._
import datagen._
import solvers._
@@ -110,9 +107,9 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
val datagen = new GrammarDataGen(evaluator, ValueGrammar)
val solverDataGen = new SolverDataGen(ctx, program, (ctx, pgm) => SolverFactory(() => new FairZ3Solver(ctx, pgm)))
- val generatedExamples = datagen.generateFor(ids, pc, maxValid, maxEnumerated).map(InExample(_))
+ val generatedExamples = datagen.generateFor(ids, pc, maxValid, maxEnumerated).map(InExample)
- val solverExamples = solverDataGen.generateFor(ids, pc, maxValid, maxEnumerated).map(InExample(_))
+ val solverExamples = solverDataGen.generateFor(ids, pc, maxValid, maxEnumerated).map(InExample)
ExamplesBank(generatedExamples.toSeq ++ solverExamples.toList, Nil)
}
@@ -180,34 +177,20 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
case (a, b, c) =>
None
}) getOrElse {
+
// If the input contains free variables, it does not provide concrete examples.
// We will instantiate them according to a simple grammar to get them.
- val enum = new MemoizedEnumerator[TypeTree, Expr, ProductionRule[TypeTree, Expr]](ValueGrammar.getProductions)
- val values = enum.iterator(tupleTypeWrap(freeVars.map { _.getType }))
- val instantiations = values.map {
- v => freeVars.zip(unwrapTuple(v, freeVars.size)).toMap
- }
- def filterGuard(e: Expr, mapping: Map[Identifier, Expr]): Boolean = cs.optGuard match {
- case Some(guard) =>
- // in -> e should be enough. We shouldn't find any subexpressions of in.
- evaluator.eval(replace(Map(in -> e), guard), mapping) match {
- case EvaluationResults.Successful(BooleanLiteral(true)) => true
- case _ => false
- }
+ val dataGen = new GrammarDataGen(evaluator)
+
+ val theGuard = replace(Map(in -> pattExpr), cs.optGuard.getOrElse(BooleanLiteral(true)))
- case None =>
- true
+ dataGen.generateFor(freeVars, theGuard, examplesPerCase, 1000).toSeq map { vals =>
+ val inst = freeVars.zip(vals).toMap
+ val inR = replaceFromIDs(inst, pattExpr)
+ val outR = replaceFromIDs(inst, doSubstitute(ieMap, cs.rhs))
+ (inR, outR)
}
-
- if(cs.optGuard == Some(BooleanLiteral(false))) {
- Nil
- } else (for {
- inst <- instantiations.toSeq
- inR = replaceFromIDs(inst, pattExpr)
- outR = replaceFromIDs(inst, doSubstitute(ieMap, cs.rhs))
- if filterGuard(inR, inst)
- } yield (inR, outR)).take(examplesPerCase)
}
}
}
diff --git a/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala b/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
index 6e9dc2376..6ce5f020a 100644
--- a/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
+++ b/src/main/scala/leon/synthesis/disambiguation/ExamplesAdder.scala
@@ -3,15 +3,12 @@ package leon
package synthesis
package disambiguation
-import leon.LeonContext
-import leon.purescala.Expressions._
import purescala.Common.FreshIdentifier
import purescala.Constructors.{ and, tupleWrap }
import purescala.Definitions.{ FunDef, Program, ValDef }
import purescala.ExprOps.expressionToPattern
-import purescala.Expressions.{ BooleanLiteral, Equals, Expr, Lambda, MatchCase, Passes, Variable, WildcardPattern }
import purescala.Extractors.TopLevelAnds
-import leon.purescala.Expressions._
+import purescala.Expressions._
/**
* @author Mikael
diff --git a/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala b/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala
index 244925b90..d77c06c97 100644
--- a/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala
+++ b/src/main/scala/leon/synthesis/disambiguation/QuestionBuilder.scala
@@ -1,21 +1,18 @@
package leon
package synthesis.disambiguation
+import datagen.GrammarDataGen
import synthesis.Solution
import evaluators.DefaultEvaluator
import purescala.Expressions._
import purescala.ExprOps
-import purescala.Constructors._
-import purescala.Extractors._
import purescala.Types.{StringType, TypeTree}
import purescala.Common.Identifier
import purescala.Definitions.Program
import purescala.DefOps
-import grammars.ValueGrammar
-import bonsai.enumerators.MemoizedEnumerator
+import grammars._
import solvers.ModelBuilder
import scala.collection.mutable.ListBuffer
-import grammars._
object QuestionBuilder {
/** Sort methods for questions. You can build your own */
@@ -92,11 +89,9 @@ object QuestionBuilder {
*
* @tparam T A subtype of Expr that will be the type used in the Question[T] results.
* @param input The identifier of the unique function's input. Must be typed or the type should be defined by setArgumentType
- * @param ruleApplication The set of solutions for the body of f
* @param filter A function filtering which outputs should be considered for comparison.
- * It takes as input the sequence of outputs already considered for comparison, and the new output.
- * It should return Some(result) if the result can be shown, and None else.
- * @return An ordered
+ * It takes as input the sequence of outputs already considered for comparison, and the new output.
+ * It should return Some(result) if the result can be shown, and None else.
*
*/
class QuestionBuilder[T <: Expr](
@@ -139,25 +134,22 @@ class QuestionBuilder[T <: Expr](
/** Returns a list of input/output questions to ask to the user. */
def result(): List[Question[T]] = {
if(solutions.isEmpty) return Nil
-
- val enum = new MemoizedEnumerator[TypeTree, Expr, ProductionRule[TypeTree,Expr]](value_enumerator.getProductions)
- val values = enum.iterator(tupleTypeWrap(_argTypes))
- val instantiations = values.map {
- v => input.zip(unwrapTuple(v, input.size))
- }
-
- val enumerated_inputs = instantiations.take(expressionsToTake).toList
-
+
+ val datagen = new GrammarDataGen(new DefaultEvaluator(c, p), value_enumerator)
+ val enumerated_inputs = datagen.generateMapping(input, BooleanLiteral(true), expressionsToTake, expressionsToTake).toList
+
val solution = solutions.head
val alternatives = solutions.drop(1).take(solutionsToTake).toList
val questions = ListBuffer[Question[T]]()
- for{possible_input <- enumerated_inputs
- current_output_nonfiltered <- run(solution, possible_input)
- current_output <- filter(Seq(), current_output_nonfiltered)} {
+ for {
+ possibleInput <- enumerated_inputs
+ currentOutputNonFiltered <- run(solution, possibleInput)
+ currentOutput <- filter(Seq(), currentOutputNonFiltered)
+ } {
- val alternative_outputs = ((ListBuffer[T](current_output) /: alternatives) { (prev, alternative) =>
- run(alternative, possible_input) match {
- case Some(alternative_output) if alternative_output != current_output =>
+ val alternative_outputs = (ListBuffer[T](currentOutput) /: alternatives) { (prev, alternative) =>
+ run(alternative, possibleInput) match {
+ case Some(alternative_output) if alternative_output != currentOutput =>
filter(prev, alternative_output) match {
case Some(alternative_output_filtered) =>
prev += alternative_output_filtered
@@ -165,9 +157,9 @@ class QuestionBuilder[T <: Expr](
}
case _ => prev
}
- }).drop(1).toList.distinct
- if(alternative_outputs.nonEmpty || keepEmptyAlternativeQuestions(current_output)) {
- questions += Question(possible_input.map(_._2), current_output, alternative_outputs.sortWith((e,f) => _alternativeSortMethod.compare(e, f) <= 0))
+ }.drop(1).toList.distinct
+ if(alternative_outputs.nonEmpty || keepEmptyAlternativeQuestions(currentOutput)) {
+ questions += Question(possibleInput.map(_._2), currentOutput, alternative_outputs.sortWith((e,f) => _alternativeSortMethod.compare(e, f) <= 0))
}
}
questions.toList.sortBy(_questionSorMethod(_))
diff --git a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
index f716997f4..4c12f5822 100644
--- a/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
+++ b/src/main/scala/leon/synthesis/rules/BottomUpTegis.scala
@@ -14,7 +14,6 @@ import codegen.CodeGenParams
import grammars._
import bonsai.enumerators._
-import bonsai.{Generator => Gen}
case object BottomUpTEGIS extends BottomUpTEGISLike[TypeTree]("BU TEGIS") {
def getGrammar(sctx: SynthesisContext, p: Problem) = {
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 368608b90..fba29e2f0 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -765,7 +765,11 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
}
}
-
+ println("BASE EXAMPLES")
+ baseExampleInputs.foreach { in =>
+ println(" - "+in.asString)
+ }
+ println("BASE EXAMPLES END")
/**
* We generate tests for discarding potential programs
*/
@@ -842,6 +846,10 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
}
}
+ allInputExamples().foreach { in =>
+ println(" - "+in.asString)
+ }
+
val nPassing = prunedPrograms.size
val nTotal = ndProgram.allProgramsCount()
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index f03c54b56..7b72da539 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -7,35 +7,28 @@ package rules
import scala.annotation.tailrec
import scala.collection.mutable.ListBuffer
-import bonsai.enumerators.MemoizedEnumerator
-import leon.evaluators.DefaultEvaluator
-import leon.evaluators.StringTracingEvaluator
-import leon.synthesis.programsets.DirectProgramSet
-import leon.synthesis.programsets.JoinProgramSet
-import leon.purescala.Common.FreshIdentifier
-import leon.purescala.Common.Identifier
-import leon.purescala.DefOps
-import leon.purescala.Definitions.FunDef
-import leon.purescala.Definitions.FunDef
-import leon.purescala.Definitions.ValDef
-import leon.purescala.ExprOps
-import leon.solvers.Model
-import leon.solvers.ModelBuilder
-import leon.solvers.string.StringSolver
-import leon.utils.DebugSectionSynthesis
+import purescala.Common._
+import purescala.Types._
import purescala.Constructors._
import purescala.Definitions._
-import purescala.ExprOps._
import purescala.Expressions._
import purescala.Extractors._
import purescala.TypeOps
-import purescala.Types._
+import purescala.DefOps
+import purescala.ExprOps
+
+import evaluators.StringTracingEvaluator
+import synthesis.programsets.DirectProgramSet
+import synthesis.programsets.JoinProgramSet
+
+import solvers.ModelBuilder
+import solvers.string.StringSolver
/** A template generator for a given type tree.
* Extend this class using a concrete type tree,
* Then use the apply method to get a hole which can be a placeholder for holes in the template.
- * Each call to the ``.instantiate` method of the subsequent Template will provide different instances at each position of the hole.
+ * Each call to the `.instantiate` method of the subsequent Template will provide different instances at each position of the hole.
*/
abstract class TypedTemplateGenerator(t: TypeTree) {
import StringRender.WithIds
diff --git a/src/main/scala/leon/synthesis/rules/TEGIS.scala b/src/main/scala/leon/synthesis/rules/TEGIS.scala
index d7ec34617..3d496d059 100644
--- a/src/main/scala/leon/synthesis/rules/TEGIS.scala
+++ b/src/main/scala/leon/synthesis/rules/TEGIS.scala
@@ -6,7 +6,6 @@ package rules
import purescala.Types._
import grammars._
-import utils._
case object TEGIS extends TEGISLike[TypeTree]("TEGIS") {
def getParams(sctx: SynthesisContext, p: Problem) = {
diff --git a/src/main/scala/leon/utils/UniqueCounter.scala b/src/main/scala/leon/utils/UniqueCounter.scala
index 06a6c0bb4..7c7862747 100644
--- a/src/main/scala/leon/utils/UniqueCounter.scala
+++ b/src/main/scala/leon/utils/UniqueCounter.scala
@@ -17,4 +17,5 @@ class UniqueCounter[K] {
globalId
}
+ def current = nameIds
}
diff --git a/testcases/synthesis/etienne-thesis/BatchedQueue/Enqueue.scala b/testcases/synthesis/etienne-thesis/BatchedQueue/Enqueue.scala
index fe01946d1..0f30a5ba1 100644
--- a/testcases/synthesis/etienne-thesis/BatchedQueue/Enqueue.scala
+++ b/testcases/synthesis/etienne-thesis/BatchedQueue/Enqueue.scala
@@ -72,17 +72,12 @@ object BatchedQueue {
def enqueue(v: T): Queue[T] = {
require(invariant)
- f match {
- case Cons(h, t) =>
- Queue(f, Cons(v, r))
- case Nil() =>
- Queue(Cons(v, f), Nil())
- }
-
+ ???[Queue[T]]
} ensuring { (res: Queue[T]) =>
- res.invariant &&
- res.toList.last == v &&
- res.content == this.content ++ Set(v)
+ res.invariant &&
+ res.toList.last == v &&
+ res.size == size + 1 &&
+ res.content == this.content ++ Set(v)
}
}
}
--
GitLab