From 6e4b54da538676e8dbed0bc1042450dfb006fd3e Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Thu, 14 Aug 2014 13:43:38 +0200
Subject: [PATCH] TEGIS or test-only CEGIS, using bonsai for tree generation
---
project/Build.scala | 6 +-
.../scala/leon/codegen/CompilationUnit.scala | 65 ++++--
.../leon/codegen/CompiledExpression.scala | 6 +-
.../codegen/runtime/ChooseEntryPoint.scala | 2 +-
.../leon/evaluators/CodeGenEvaluator.scala | 11 +-
.../leon/evaluators/DefaultEvaluator.scala | 6 +-
.../scala/leon/evaluators/DualEvaluator.scala | 98 +++++++++
.../scala/leon/evaluators/Evaluator.scala | 4 +-
.../leon/evaluators/RecursiveEvaluator.scala | 34 ++-
.../leon/evaluators/TracingEvaluator.scala | 18 +-
.../scala/leon/purescala/ScalaPrinter.scala | 1 -
src/main/scala/leon/purescala/TreeOps.scala | 13 +-
.../scala/leon/purescala/TypeTreeOps.scala | 10 +-
.../scala/leon/synthesis/InOutExample.scala | 8 +-
src/main/scala/leon/synthesis/Problem.scala | 46 ++--
src/main/scala/leon/synthesis/Rules.scala | 1 +
.../scala/leon/synthesis/rules/Tegis.scala | 197 ++++++++++++++++++
src/main/scala/leon/utils/DebugSections.scala | 4 +-
src/main/scala/leon/utils/Timer.scala | 32 +--
.../scala/leon/test/purescala/LikelyEq.scala | 112 +++++-----
.../leon/test/purescala/LikelyEqSuite.scala | 2 +-
.../purescala/TreeNormalizationsTests.scala | 2 +-
.../leon/test/purescala/TreeOpsTests.scala | 2 +-
.../test/synthesis/LinearEquationsSuite.scala | 4 +-
testcases/synthesis/io-examples/List.scala | 19 ++
25 files changed, 540 insertions(+), 163 deletions(-)
create mode 100644 src/main/scala/leon/evaluators/DualEvaluator.scala
create mode 100644 src/main/scala/leon/synthesis/rules/Tegis.scala
create mode 100644 testcases/synthesis/io-examples/List.scala
diff --git a/project/Build.scala b/project/Build.scala
index 5adc5a3b2..497cbb33a 100644
--- a/project/Build.scala
+++ b/project/Build.scala
@@ -74,5 +74,9 @@ object Leon extends Build {
id = "leon",
base = file("."),
settings = Project.defaultSettings ++ LeonProject.settings
- )
+ ).dependsOn(Github.bonsai)
+
+ object Github {
+ lazy val bonsai = RootProject(uri("git://github.com/colder/bonsai.git#f52c898960bbb343b2138b896f9297848dc2bdb0"))
+ }
}
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 3139208d7..3aa980ef8 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -121,7 +121,7 @@ class CompilationUnit(val ctx: LeonContext,
// Currently, this method is only used to prepare arguments to reflective calls.
// This means it is safe to return AnyRef (as opposed to primitive types), because
// reflection needs this anyway.
- private[codegen] def exprToJVM(e: Expr)(implicit monitor : LeonCodeGenRuntimeMonitor): AnyRef = e match {
+ def exprToJVM(e: Expr)(implicit monitor : LeonCodeGenRuntimeMonitor): AnyRef = e match {
case IntLiteral(v) =>
new java.lang.Integer(v)
@@ -148,58 +148,85 @@ class CompilationUnit(val ctx: LeonContext,
case f @ FiniteArray(exprs) if f.getType == ArrayType(BooleanType) =>
exprs.map(e => exprToJVM(e).asInstanceOf[java.lang.Boolean].booleanValue).toArray
+ case s @ FiniteSet(els) =>
+ val s = new leon.codegen.runtime.Set()
+ for (e <- els) {
+ s.add(exprToJVM(e))
+ }
+ s
+
+ case m @ FiniteMap(els) =>
+ val m = new leon.codegen.runtime.Map()
+ for ((k,v) <- els) {
+ m.add(exprToJVM(k), exprToJVM(v))
+ }
+ m
+
// Just slightly overkill...
case _ =>
compileExpression(e, Seq()).evalToJVM(Seq(),monitor)
}
// Note that this may produce untyped expressions! (typically: sets, maps)
- private[codegen] def jvmToExpr(e: AnyRef): Expr = e match {
- case i: Integer =>
+ def jvmToExpr(e: AnyRef, tpe: TypeTree): Expr = (e, tpe) match {
+ case (i: Integer, Int32Type) =>
IntLiteral(i.toInt)
- case b: java.lang.Boolean =>
+ case (b: java.lang.Boolean, BooleanType) =>
BooleanLiteral(b.booleanValue)
- case cc: runtime.CaseClass =>
+ case (cc: runtime.CaseClass, ct: ClassType) =>
val fields = cc.productElements()
- jvmClassToLeonClass(e.getClass.getName) match {
- case Some(cc: CaseClassDef) =>
- CaseClass(CaseClassType(cc, Nil), fields.map(jvmToExpr))
+ // identify case class type of ct
+ val cct = ct match {
+ case cc: CaseClassType =>
+ cc
+
case _ =>
- throw CompilationException("Unsupported return value : " + e)
+ jvmClassToLeonClass(cc.getClass.getName) match {
+ case Some(cc: CaseClassDef) =>
+ CaseClassType(cc, ct.tps)
+ case _ =>
+ throw CompilationException("Unable to identify class "+cc.getClass.getName+" to descendent of "+ct)
+ }
}
- case tpl: runtime.Tuple =>
- val elems = for (i <- 0 until tpl.getArity) yield {
- jvmToExpr(tpl.get(i))
+ CaseClass(cct, (fields zip cct.fieldsTypes).map { case (e, tpe) => jvmToExpr(e, tpe) })
+
+ case (tpl: runtime.Tuple, TupleType(stpe)) =>
+ val elems = stpe.zipWithIndex.map { case (tpe, i) =>
+ jvmToExpr(tpl.get(i), tpe)
}
Tuple(elems)
- case gv : GenericValue =>
+ case (gv : GenericValue, _: TypeParameter) =>
gv
- case set : runtime.Set =>
- FiniteSet(set.getElements().asScala.map(jvmToExpr).toSeq)
+ case (set : runtime.Set, SetType(b)) =>
+ FiniteSet(set.getElements().asScala.map(jvmToExpr(_, b)).toSeq).setType(SetType(b))
- case map : runtime.Map =>
+ case (map : runtime.Map, MapType(from, to)) =>
val pairs = map.getElements().asScala.map { entry =>
- val k = jvmToExpr(entry.getKey())
- val v = jvmToExpr(entry.getValue())
+ val k = jvmToExpr(entry.getKey(), from)
+ val v = jvmToExpr(entry.getValue(), to)
(k, v)
}
FiniteMap(pairs.toSeq)
case _ =>
- throw CompilationException("Unsupported return value : " + e.getClass)
+ throw CompilationException("Unsupported return value : " + e.getClass +" while expecting "+tpe)
}
+ var compiledN = 0;
+
def compileExpression(e: Expr, args: Seq[Identifier]): CompiledExpression = {
if(e.getType == Untyped) {
throw new IllegalArgumentException("Cannot compile untyped expression [%s].".format(e))
}
+ compiledN += 1
+
val id = CompilationUnit.nextExprId
val cName = "Leon$CodeGen$Expr$"+id
diff --git a/src/main/scala/leon/codegen/CompiledExpression.scala b/src/main/scala/leon/codegen/CompiledExpression.scala
index 08a8c3b5b..dc2f9767a 100644
--- a/src/main/scala/leon/codegen/CompiledExpression.scala
+++ b/src/main/scala/leon/codegen/CompiledExpression.scala
@@ -51,11 +51,7 @@ class CompiledExpression(unit: CompilationUnit, cf: ClassFile, expression : Expr
// We also need to reattach a type in some cases (sets, maps).
def evalFromJVM(args: Seq[AnyRef], monitor: LM) : Expr = {
try {
- val result = unit.jvmToExpr(evalToJVM(args, monitor))
- if(!result.isTyped) {
- result.setType(exprType)
- }
- result
+ unit.jvmToExpr(evalToJVM(args, monitor), exprType)
} catch {
case ite : InvocationTargetException => throw ite.getCause()
}
diff --git a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
index 2a129e34f..d285aa98a 100644
--- a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
+++ b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
@@ -46,7 +46,7 @@ object ChooseEntryPoint {
val inputsMap = (p.as zip inputs).map {
case (id, v) =>
- Equals(Variable(id), unit.jvmToExpr(v))
+ Equals(Variable(id), unit.jvmToExpr(v, id.getType))
}
solver.assertCnstr(And(Seq(p.pc, p.phi) ++ inputsMap))
diff --git a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
index abdbec318..4805dcfcc 100644
--- a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
+++ b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
@@ -23,13 +23,20 @@ class CodeGenEvaluator(ctx : LeonContext, val unit : CompilationUnit) extends Ev
def eval(expression : Expr, mapping : Map[Identifier,Expr]) : EvaluationResult = {
val toPairs = mapping.toSeq
- compile(expression, toPairs.map(_._1)).map(e => e(toPairs.map(_._2))).getOrElse(EvaluationResults.EvaluatorError("Couldn't compile expression."))
+ compile(expression, toPairs.map(_._1)).map { e =>
+
+ ctx.timers.evaluators.codegen.runtime.start()
+ val res = e(toPairs.map(_._2))
+ ctx.timers.evaluators.codegen.runtime.stop()
+ res
+ }.getOrElse(EvaluationResults.EvaluatorError("Couldn't compile expression."))
}
override def compile(expression : Expr, argorder : Seq[Identifier]) : Option[Seq[Expr]=>EvaluationResult] = {
import leon.codegen.runtime.LeonCodeGenRuntimeException
import leon.codegen.runtime.LeonCodeGenEvaluationException
+ ctx.timers.evaluators.codegen.compilation.start()
try {
val ce = unit.compileExpression(expression, argorder)
@@ -54,6 +61,8 @@ class CodeGenEvaluator(ctx : LeonContext, val unit : CompilationUnit) extends Ev
case t: Throwable =>
ctx.reporter.warning(expression.getPos, "Error while compiling expression: "+t.getMessage)
None
+ } finally {
+ ctx.timers.evaluators.codegen.compilation.stop()
}
}
}
diff --git a/src/main/scala/leon/evaluators/DefaultEvaluator.scala b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
index fcc4f96a0..d92c65399 100644
--- a/src/main/scala/leon/evaluators/DefaultEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
@@ -7,16 +7,14 @@ import purescala.Common._
import purescala.Trees._
import purescala.Definitions._
-class DefaultEvaluator(ctx: LeonContext, prog: Program) extends RecursiveEvaluator(ctx, prog) {
+class DefaultEvaluator(ctx: LeonContext, prog: Program) extends RecursiveEvaluator(ctx, prog, 50000) {
type RC = DefaultRecContext
type GC = GlobalContext
def initRC(mappings: Map[Identifier, Expr]) = DefaultRecContext(mappings)
- def initGC = new GlobalContext(stepsLeft = 50000)
+ def initGC = new GlobalContext()
case class DefaultRecContext(mappings: Map[Identifier, Expr]) extends RecContext {
- def withNewVar(id: Identifier, v: Expr) = copy(mappings + (id -> v))
-
def withVars(news: Map[Identifier, Expr]) = copy(news)
}
}
diff --git a/src/main/scala/leon/evaluators/DualEvaluator.scala b/src/main/scala/leon/evaluators/DualEvaluator.scala
new file mode 100644
index 000000000..67515e4c0
--- /dev/null
+++ b/src/main/scala/leon/evaluators/DualEvaluator.scala
@@ -0,0 +1,98 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon
+package evaluators
+
+import purescala.Common._
+import purescala.Trees._
+import purescala.Definitions._
+
+import codegen._
+
+class DualEvaluator(ctx: LeonContext, prog: Program, params: CodeGenParams) extends RecursiveEvaluator(ctx, prog, params.maxFunctionInvocations) {
+ type RC = DefaultRecContext
+ type GC = GlobalContext
+
+ implicit val debugSection = utils.DebugSectionEvaluation
+
+ def initRC(mappings: Map[Identifier, Expr]) = DefaultRecContext(mappings)
+ def initGC = new GlobalContext()
+
+ var monitor = new runtime.LeonCodeGenRuntimeMonitor(params.maxFunctionInvocations)
+
+ val unit = new CompilationUnit(ctx, prog, params)
+ val isCompiled = prog.definedFunctions.toSet
+
+ case class DefaultRecContext(mappings: Map[Identifier, Expr], needJVMRef: Boolean = false) extends RecContext {
+ def withVars(news: Map[Identifier, Expr]) = copy(news)
+ }
+
+ case class RawObject(o: AnyRef) extends Expr
+
+ def call(tfd: TypedFunDef, args: Seq[AnyRef]): Expr = {
+
+ val (className, methodName, _) = unit.leonFunDefToJVMInfo(tfd.fd).get
+
+ val allArgs = if (params.requireMonitor) monitor +: args else args
+
+ ctx.reporter.debug(s"Calling ${className}.${methodName}(${args.mkString(",")})")
+
+ try {
+ val cl = unit.loader.loadClass(className)
+
+ val meth = cl.getMethods().find(_.getName() == methodName).get
+
+ val res = if (allArgs.isEmpty) {
+ meth.invoke(null)
+ } else {
+ meth.invoke(null, allArgs : _*)
+ }
+
+ RawObject(res).setType(tfd.returnType)
+ } catch {
+ case e: java.lang.reflect.InvocationTargetException =>
+ throw new RuntimeError(e.getCause.getMessage)
+
+ case t: Throwable =>
+ throw new EvalError(t.getMessage)
+ }
+ }
+
+ override def e(expr: Expr)(implicit rctx: RC, gctx: GC): Expr = expr match {
+ case FunctionInvocation(tfd, args) =>
+ if (isCompiled(tfd.fd)) {
+ val rargs = args.map(
+ e(_)(rctx.copy(needJVMRef = true), gctx) match {
+ case RawObject(obj) => obj
+ case _ => throw new EvalError("Failed to get JVM ref when requested")
+ }
+ )
+
+ jvmBarrier(call(tfd, rargs), rctx.needJVMRef)
+ } else {
+ jvmBarrier(super.e(expr)(rctx.copy(needJVMRef = false), gctx), rctx.needJVMRef)
+ }
+ case _ =>
+ jvmBarrier(super.e(expr)(rctx.copy(needJVMRef = false), gctx), rctx.needJVMRef)
+ }
+
+ def jvmBarrier(e: Expr, returnJVMRef: Boolean): Expr = {
+ e match {
+ case RawObject(obj) if returnJVMRef =>
+ e
+ case RawObject(obj) if !returnJVMRef =>
+ unit.jvmToExpr(obj, e.getType)
+ case e if returnJVMRef =>
+ RawObject(unit.exprToJVM(e)(monitor)).setType(e.getType)
+ case e if !returnJVMRef =>
+ e
+ }
+ }
+
+
+ override def eval(ex: Expr, mappings: Map[Identifier, Expr]) = {
+ monitor = new runtime.LeonCodeGenRuntimeMonitor(params.maxFunctionInvocations)
+ super.eval(ex, mappings)
+ }
+
+}
diff --git a/src/main/scala/leon/evaluators/Evaluator.scala b/src/main/scala/leon/evaluators/Evaluator.scala
index 689299d72..93c7129c4 100644
--- a/src/main/scala/leon/evaluators/Evaluator.scala
+++ b/src/main/scala/leon/evaluators/Evaluator.scala
@@ -12,10 +12,10 @@ abstract class Evaluator(val context : LeonContext, val program : Program) exten
type EvaluationResult = EvaluationResults.Result
/** Evaluates an expression, using `mapping` as a valuation function for the free variables. */
- def eval(expr : Expr, mapping : Map[Identifier,Expr]) : EvaluationResult
+ def eval(expr: Expr, mapping: Map[Identifier,Expr]) : EvaluationResult
/** Evaluates a ground expression. */
- final def eval(expr : Expr) : EvaluationResult = eval(expr, Map.empty)
+ final def eval(expr: Expr) : EvaluationResult = eval(expr, Map.empty)
/** Compiles an expression into a function, where the arguments are the free variables in the expression.
* `argorder` specifies in which order the arguments should be passed.
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 425cdc19d..0a825de5f 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -13,26 +13,36 @@ import solvers.TimeoutSolver
import xlang.Trees._
-abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program) extends Evaluator(ctx, prog) {
+abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int) extends Evaluator(ctx, prog) {
val name = "evaluator"
val description = "Recursive interpreter for PureScala expressions"
type RC <: RecContext
type GC <: GlobalContext
+ var lastGC: Option[GC] = None
+
case class EvalError(msg : String) extends Exception
case class RuntimeError(msg : String) extends Exception
- abstract class RecContext {
- val mappings: Map[Identifier, Expr]
-
- def withNewVar(id: Identifier, v: Expr): RC;
+ trait RecContext {
+ def mappings: Map[Identifier, Expr]
def withVars(news: Map[Identifier, Expr]): RC;
+
+ def withNewVar(id: Identifier, v: Expr): RC = {
+ withVars(mappings + (id -> v))
+ }
+
+ def withNewVars(news: Map[Identifier, Expr]): RC = {
+ withVars(mappings ++ news)
+ }
}
- class GlobalContext(var stepsLeft: Int) {
- val maxSteps = stepsLeft
+ class GlobalContext {
+ def maxSteps = RecursiveEvaluator.this.maxSteps
+
+ var stepsLeft = maxSteps
}
def initRC(mappings: Map[Identifier, Expr]): RC
@@ -40,14 +50,20 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program) extends Evalu
def eval(ex: Expr, mappings: Map[Identifier, Expr]) = {
try {
- EvaluationResults.Successful(e(ex)(initRC(mappings), initGC))
+ lastGC = Some(initGC)
+ ctx.timers.evaluators.recursive.runtime.start()
+ EvaluationResults.Successful(e(ex)(initRC(mappings), lastGC.get))
} catch {
case so: StackOverflowError =>
EvaluationResults.EvaluatorError("Stack overflow")
case EvalError(msg) =>
EvaluationResults.EvaluatorError(msg)
- case RuntimeError(msg) =>
+ case e @ RuntimeError(msg) =>
EvaluationResults.RuntimeError(msg)
+ case jre: java.lang.RuntimeException =>
+ EvaluationResults.RuntimeError(jre.getMessage)
+ } finally {
+ ctx.timers.evaluators.recursive.runtime.stop()
}
}
diff --git a/src/main/scala/leon/evaluators/TracingEvaluator.scala b/src/main/scala/leon/evaluators/TracingEvaluator.scala
index b4f8b488e..945a3a121 100644
--- a/src/main/scala/leon/evaluators/TracingEvaluator.scala
+++ b/src/main/scala/leon/evaluators/TracingEvaluator.scala
@@ -9,27 +9,17 @@ import purescala.Definitions._
import purescala.TreeOps._
import purescala.TypeTrees._
-class TracingEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int = 1000) extends RecursiveEvaluator(ctx, prog) {
+class TracingEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int = 1000) extends RecursiveEvaluator(ctx, prog, maxSteps) {
type RC = TracingRecContext
type GC = TracingGlobalContext
- var lastGlobalContext: Option[GC] = None
+ def initRC(mappings: Map[Identifier, Expr]) = TracingRecContext(mappings, 2)
- def initRC(mappings: Map[Identifier, Expr]) = {
- TracingRecContext(mappings, 2)
- }
-
- def initGC = {
- val gc = new TracingGlobalContext(stepsLeft = maxSteps, Nil)
- lastGlobalContext = Some(gc)
- gc
- }
+ def initGC = new TracingGlobalContext(Nil)
- class TracingGlobalContext(stepsLeft: Int, var values: List[(Expr, Expr)]) extends GlobalContext(stepsLeft)
+ class TracingGlobalContext(var values: List[(Expr, Expr)]) extends GlobalContext
case class TracingRecContext(mappings: Map[Identifier, Expr], tracingFrames: Int) extends RecContext {
- def withNewVar(id: Identifier, v: Expr) = copy(mappings = mappings + (id -> v))
-
def withVars(news: Map[Identifier, Expr]) = copy(mappings = news)
}
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 74ff651d1..8305781b9 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -51,7 +51,6 @@ class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) ex
case FiniteArray(exprs) => p"Array($exprs)"
case Distinct(exprs) => p"distinct($exprs)"
case Not(expr) => p"!$expr"
-
case _ =>
super.pp(tree)
}
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 0fa481c68..0f629386c 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -363,15 +363,12 @@ object TreeOps {
* Returns all Function calls found in an expression
*/
def functionCallsOf(expr: Expr): Set[FunctionInvocation] = {
- foldRight[Set[FunctionInvocation]]({
- case (e, subs) =>
- val c: Set[FunctionInvocation] = e match {
- case f: FunctionInvocation => Set(f)
- case _ => Set()
- }
- subs.foldLeft(c)(_ ++ _)
- })(expr)
+ collect[FunctionInvocation] {
+ case f: FunctionInvocation => Set(f)
+ case _ => Set()
+ }(expr)
}
+
def negate(expr: Expr) : Expr = (expr match {
case Let(i,b,e) => Let(i,b,negate(e))
case Not(e) => e
diff --git a/src/main/scala/leon/purescala/TypeTreeOps.scala b/src/main/scala/leon/purescala/TypeTreeOps.scala
index 41c4041cf..0cb7e3c6e 100644
--- a/src/main/scala/leon/purescala/TypeTreeOps.scala
+++ b/src/main/scala/leon/purescala/TypeTreeOps.scala
@@ -65,9 +65,13 @@ object TypeTreeOps {
val NAryType(ts1, _) = tpe
val NAryType(ts2, _) = stpe
- unify((ts1 zip ts2).map { case (tp1, tp2) =>
- canBeSubtypeOf(tp1, freeParams, tp2)
- })
+ if (ts1.size == ts2.size) {
+ unify((ts1 zip ts2).map { case (tp1, tp2) =>
+ canBeSubtypeOf(tp1, freeParams, tp2)
+ })
+ } else {
+ None
+ }
case (t1, t2) =>
if (t1 == t2) {
diff --git a/src/main/scala/leon/synthesis/InOutExample.scala b/src/main/scala/leon/synthesis/InOutExample.scala
index 6c64f3977..8978e38ae 100644
--- a/src/main/scala/leon/synthesis/InOutExample.scala
+++ b/src/main/scala/leon/synthesis/InOutExample.scala
@@ -5,9 +5,5 @@ package synthesis
import purescala.Trees.Expr
-case class InOutExample(ins: Seq[Expr], outs: Seq[Expr]) {
- def inExample = InExample(ins)
-}
-
-
-case class InExample(ins: Seq[Expr])
+class InExample(val ins: Seq[Expr])
+class InOutExample(is: Seq[Expr], val outs: Seq[Expr]) extends InExample(is)
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index 2ed3e5d17..b56974ffc 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -12,18 +12,23 @@ import leon.purescala.Common._
case class Problem(as: List[Identifier], pc: Expr, phi: Expr, xs: List[Identifier]) {
override def toString = "⟦ "+as.mkString(";")+", "+(if (pc != BooleanLiteral(true)) pc+" ≺ " else "")+" ⟨ "+phi+" ⟩ "+xs.mkString(";")+" ⟧ "
- def getTests(sctx: SynthesisContext): Seq[InOutExample] = {
+ def getTests(sctx: SynthesisContext): Seq[InExample] = {
import purescala.Extractors._
import evaluators._
- val TopLevelAnds(predicates) = And(pc, phi)
+ val predicates = And(pc, phi)
val ev = new DefaultEvaluator(sctx.context, sctx.program)
- def isValidExample(ex: InOutExample): Boolean = {
- val mapping = Map((as zip ex.ins) ++ (xs zip ex.outs): _*)
+ def isValidExample(ex: InExample): Boolean = {
+ val (mapping, cond) = ex match {
+ case io: InOutExample =>
+ (Map((as zip io.ins) ++ (xs zip io.outs): _*), And(pc, phi))
+ case i =>
+ ((as zip i.ins).toMap, pc)
+ }
- ev.eval(And(pc, phi), mapping) match {
+ ev.eval(cond, mapping) match {
case EvaluationResults.Successful(BooleanLiteral(true)) => true
case _ => false
}
@@ -74,7 +79,7 @@ case class Problem(as: List[Identifier], pc: Expr, phi: Expr, xs: List[Identifie
case _ => Nil
}
- val testClusters = predicates.collect {
+ val testClusters = collect[Map[Identifier, Expr]] {
case FunctionInvocation(tfd, List(in, out, FiniteMap(inouts))) if tfd.id.name == "passes" =>
val infos = extractIds(Tuple(Seq(in, out)))
val exs = inouts.map{ case (i, o) => Tuple(Seq(i, o)) }
@@ -84,8 +89,11 @@ case class Problem(as: List[Identifier], pc: Expr, phi: Expr, xs: List[Identifie
infos.map{ case (id, f) => id -> f(e) }.toMap
}
- results
- }
+ results.toSet
+
+ case _ =>
+ Set()
+ }(predicates)
/**
* we now need to consolidate different clusters of compatible tests together
@@ -108,7 +116,7 @@ case class Problem(as: List[Identifier], pc: Expr, phi: Expr, xs: List[Identifie
}
var consolidated = Set[Map[Identifier, Expr]]()
- for (ts <- testClusters; t <- ts) {
+ for (t <- testClusters) {
consolidated += t
consolidated = consolidated.map { c =>
@@ -117,12 +125,22 @@ case class Problem(as: List[Identifier], pc: Expr, phi: Expr, xs: List[Identifie
}
// Finally, we keep complete tests covering all as++xs
- val requiredIds = (as ++ xs).toSet
- val complete = consolidated.filter{ t => (t.keySet & requiredIds) == requiredIds }
+ val allIds = (as ++ xs).toSet
+ val insIds = as.toSet
+ val outsIds = xs.toSet
+
+ val examples = consolidated.toSeq.flatMap { t =>
+ val ids = t.keySet
+ if ((ids & allIds) == allIds) {
+ Some(new InOutExample(as.map(t), xs.map(t)))
+ } else if ((ids & insIds) == insIds) {
+ Some(new InExample(as.map(t)))
+ } else {
+ None
+ }
+ }
- complete.toSeq.map { m =>
- InOutExample(as.map(m), xs.map(m))
- }.filter(isValidExample)
+ examples.filter(isValidExample)
}
}
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 2a1b90973..b1b5cd756 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -25,6 +25,7 @@ object Rules {
EqualitySplit,
InequalitySplit,
CEGIS,
+ TEGIS,
rules.Assert,
DetupleOutput,
DetupleInput,
diff --git a/src/main/scala/leon/synthesis/rules/Tegis.scala b/src/main/scala/leon/synthesis/rules/Tegis.scala
new file mode 100644
index 000000000..74052f92b
--- /dev/null
+++ b/src/main/scala/leon/synthesis/rules/Tegis.scala
@@ -0,0 +1,197 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon
+package synthesis
+package rules
+
+import solvers._
+import solvers.z3._
+
+import purescala.Trees._
+import purescala.Common._
+import purescala.Definitions._
+import purescala.TypeTrees._
+import purescala.TreeOps._
+import purescala.TypeTreeOps._
+import purescala.Extractors._
+import purescala.ScalaPrinter
+import purescala.Constructors._
+
+import scala.collection.mutable.{Map=>MutableMap, ArrayBuffer}
+
+import evaluators._
+import datagen._
+import codegen.CodeGenParams
+
+import bonsai._
+import bonsai.enumerators._
+
+case object TEGIS extends Rule("TEGIS") {
+
+ def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
+
+ List(new RuleInstantiation(p, this, SolutionBuilder.none, this.name, this.priority) {
+ def apply(sctx: SynthesisContext): RuleApplicationResult = {
+
+ val evalParams = CodeGenParams(maxFunctionInvocations = 2000, checkContracts = true)
+ //val evaluator = new CodeGenEvaluator(sctx.context, sctx.program, evalParams)
+ //val evaluator = new DefaultEvaluator(sctx.context, sctx.program)
+ val evaluator = new DualEvaluator(sctx.context, sctx.program, evalParams)
+
+ val interruptManager = sctx.context.interruptManager
+
+ def getBaseGenerators(t: TypeTree): Seq[Generator[TypeTree, Expr]] = t match {
+ case BooleanType =>
+ List(
+ Generator(Nil, { _ => BooleanLiteral(true) }),
+ Generator(Nil, { _ => BooleanLiteral(false) })
+ )
+ case Int32Type =>
+ List(
+ Generator(Nil, { _ => IntLiteral(0) }),
+ Generator(Nil, { _ => IntLiteral(1) }),
+ Generator(List(Int32Type, Int32Type), { case Seq(a,b) => Plus(a, b) }),
+ Generator(List(Int32Type, Int32Type), { case Seq(a,b) => Minus(a, b) }),
+ Generator(List(Int32Type, Int32Type), { case Seq(a,b) => Times(a, b) })
+ )
+ case TupleType(stps) =>
+ List(Generator(stps, { sub => Tuple(sub) }))
+
+ case cct: CaseClassType =>
+ List(
+ Generator(cct.fields.map(_.getType), { case rs => CaseClass(cct, rs)} )
+ )
+
+ case act: AbstractClassType =>
+ act.knownCCDescendents.map { cct =>
+ Generator[TypeTree, Expr](cct.fields.map(_.getType), { case rs => CaseClass(cct, rs)} )
+ }
+
+ case _ =>
+ Nil
+ }
+
+ def getInputGenerators(t: TypeTree): Seq[Generator[TypeTree, Expr]] = {
+ p.as.filter(id => isSubtypeOf(id.getType, t)).map {
+ a => Generator[TypeTree, Expr](Nil, { _ => Variable(a) })
+ }
+ }
+
+ def getFcallGenerators(t: TypeTree): Seq[Generator[TypeTree, Expr]] = {
+ def isCandidate(fd: FunDef): Option[TypedFunDef] = {
+ // Prevents recursive calls
+ val isRecursiveCall = sctx.functionContext match {
+ case Some(cfd) =>
+ (sctx.program.callGraph.transitiveCallers(cfd) + cfd) contains fd
+
+ case None =>
+ false
+ }
+
+ val isNotSynthesizable = fd.body match {
+ case Some(b) =>
+ !containsChoose(b)
+
+ case None =>
+ false
+ }
+
+
+ if (!isRecursiveCall && isNotSynthesizable) {
+ val free = fd.tparams.map(_.tp)
+ canBeSubtypeOf(fd.returnType, free, t) match {
+ case Some(tpsMap) =>
+ Some(fd.typed(free.map(tp => tpsMap.getOrElse(tp, tp))))
+ case None =>
+ None
+ }
+ } else {
+ None
+ }
+ }
+
+ val funcs = sctx.program.definedFunctions.flatMap(isCandidate)
+
+ funcs.map{ tfd =>
+ Generator[TypeTree, Expr](tfd.params.map(_.tpe), { sub => FunctionInvocation(tfd, sub) })
+ }
+ }
+
+ def getGenerators(t: TypeTree): Seq[Generator[TypeTree, Expr]] = {
+ getBaseGenerators(t) ++ getInputGenerators(t) ++ getFcallGenerators(t)
+ }
+
+ val enum = new MemoizedEnumerator[TypeTree, Expr](getGenerators)
+
+ val (targetType, isWrapped) = if (p.xs.size == 1) {
+ (p.xs.head.getType, false)
+ } else {
+ (TupleType(p.xs.map(_.getType)), true)
+ }
+
+ val timers = sctx.context.timers.synthesis.rules.tegis;
+
+ val allExprs = enum.iterator(targetType)
+
+ var failStat = Map[Seq[Expr], Int]().withDefaultValue(0)
+ var tests = p.getTests(sctx).map(_.ins).distinct
+
+ if (tests.isEmpty) {
+ return RuleApplicationImpossible;
+ }
+
+ var candidate: Option[Expr] = None
+ var enumLimit = 10000;
+
+
+ var n = 1;
+ timers.generating.start()
+ allExprs.take(enumLimit).takeWhile(e => candidate.isEmpty).foreach { e =>
+ val exprToTest = if (!isWrapped) {
+ Let(p.xs.head, e, p.phi)
+ } else {
+ letTuple(p.xs, e, p.phi)
+ }
+
+ sctx.reporter.debug("Got expression "+e)
+ timers.testing.start()
+ if (tests.forall{ case t =>
+ val ts = System.currentTimeMillis
+ val res = evaluator.eval(exprToTest, p.as.zip(t).toMap) match {
+ case EvaluationResults.Successful(BooleanLiteral(true)) =>
+ sctx.reporter.debug("Test "+t+" passed!")
+ true
+ case _ =>
+ sctx.reporter.debug("Test "+t+" failed on "+e)
+ failStat += t -> (failStat(t) + 1)
+ false
+ }
+ res
+ }) {
+ if (isWrapped) {
+ candidate = Some(e)
+ } else {
+ candidate = Some(Tuple(Seq(e)))
+ }
+ }
+ timers.testing.stop()
+
+ if (n % 50 == 0) {
+ tests = tests.sortBy(t => -failStat(t))
+ }
+ n += 1
+ }
+ timers.generating.stop()
+
+ println("Found candidate "+n)
+ println("Compiled: "+evaluator.unit.compiledN)
+
+ if (candidate.isDefined) {
+ RuleSuccess(Solution(BooleanLiteral(true), Set(), candidate.get), isTrusted = false)
+ } else {
+ RuleApplicationImpossible
+ }
+ }
+ })
+ }
+}
diff --git a/src/main/scala/leon/utils/DebugSections.scala b/src/main/scala/leon/utils/DebugSections.scala
index 902d3b4f6..adcfecf25 100644
--- a/src/main/scala/leon/utils/DebugSections.scala
+++ b/src/main/scala/leon/utils/DebugSections.scala
@@ -17,6 +17,7 @@ case object DebugSectionTermination extends DebugSection("termination", 1 << 5
case object DebugSectionTrees extends DebugSection("trees", 1 << 6)
case object DebugSectionPositions extends DebugSection("positions", 1 << 7)
case object DebugSectionDataGen extends DebugSection("datagen", 1 << 8)
+case object DebugSectionEvaluation extends DebugSection("eval", 1 << 9)
object DebugSections {
val all = Set[DebugSection](
@@ -28,6 +29,7 @@ object DebugSections {
DebugSectionTermination,
DebugSectionTrees,
DebugSectionPositions,
- DebugSectionDataGen
+ DebugSectionDataGen,
+ DebugSectionEvaluation
)
}
diff --git a/src/main/scala/leon/utils/Timer.scala b/src/main/scala/leon/utils/Timer.scala
index 842a508b1..0bc4eae91 100644
--- a/src/main/scala/leon/utils/Timer.scala
+++ b/src/main/scala/leon/utils/Timer.scala
@@ -96,11 +96,11 @@ class TimerStorage extends Dynamic {
table += Row(Seq(
Cell("name"),
- Cell("min"),
- Cell("avg"),
- Cell("max"),
- Cell("n"),
- Cell("total")
+ Cell("min", align = Right),
+ Cell("avg", align = Right),
+ Cell("max", align = Right),
+ Cell("n", align = Right),
+ Cell("total", align = Right)
))
table += Separator
@@ -113,8 +113,10 @@ class TimerStorage extends Dynamic {
} else if (from.isLastKeys(name)) {
closed += from
"â”” "
- } else {
+ } else if((from, name) == path.head) {
"├ "
+ } else {
+ "│ "
}
}.reverse.mkString
@@ -123,24 +125,24 @@ class TimerStorage extends Dynamic {
val n = t.runs.size
val tot = t.runs.sum
- val (min: String, avg: String, max: String, total: String) = if (n == 0) {
- ("", "", "", "N/A")
+ val (min: String, avg: String, max: String, n2: String, total: String) = if (n == 0) {
+ ("", "", "", "", "N/A")
} else if (n > 1) {
val min = t.runs.min
val max = t.runs.max
val avg = tot/n
- (f"$min%d", f"$avg%d", f"$max%d", f"$tot%d")
+ (f"$min%d ms", f"$avg%d ms", f"$max%d ms", f"$n%d", f"$tot%d ms")
} else {
- ("", "", "", f"$tot%d")
+ ("", "", "", "", f"$tot%d ms")
}
table += Row(Seq(
Cell(indent+name),
- Cell(min),
- Cell(avg),
- Cell(max),
- Cell(n),
- Cell(tot)
+ Cell(min, align = Right),
+ Cell(avg, align = Right),
+ Cell(max, align = Right),
+ Cell(n2, align = Right),
+ Cell(total, align = Right)
))
case ((_, name) :: _, None) =>
table += Row(Seq(
diff --git a/src/test/scala/leon/test/purescala/LikelyEq.scala b/src/test/scala/leon/test/purescala/LikelyEq.scala
index 7c45186ec..3dd28dfc7 100644
--- a/src/test/scala/leon/test/purescala/LikelyEq.scala
+++ b/src/test/scala/leon/test/purescala/LikelyEq.scala
@@ -16,70 +16,74 @@ import leon.purescala.Trees._
* This is a probabilistic based approach, it does not rely on any external solver and can
* only prove the non equality of two expressions.
*/
-object LikelyEq extends LeonTestSuite {
- private lazy val evaluator : Evaluator = new DefaultEvaluator(testContext, Program.empty)
+trait WithLikelyEq {
+ this: LeonTestSuite =>
- private val min = -5
- private val max = 5
+ object LikelyEq {
+ private val min = -5
+ private val max = 5
- /*
- * compare e1 and e2, using a list of assignment of integer to the variables in vs.
- * Pre is a boolean expression precondition over the same variables that must be evaluated to true
- * before testing equality.
- * Add a default mapping for some set parameters
- * Note that the default map could contain a mapping for variables to other parameters
- * It is thus necessary to first select values for those parameters and then substitute
- * into the default map !
- */
- def apply(e1: Expr, e2: Expr, vs: Set[Identifier], pre: Expr = BooleanLiteral(true),
- compare: (Expr, Expr) => Boolean = (e1, e2) => e1 == e2,
- defaultMap: Map[Identifier, Expr] = Map()): Boolean = {
- if(vs.isEmpty) {
- val ndm = defaultMap.map { case (id, expr) => (id, evaluator.eval(expr).asInstanceOf[EvaluationResults.Successful].value) } //TODO: not quite sure why I need to do this...
- (evaluator.eval(e1, ndm), evaluator.eval(e2, defaultMap)) match {
- case (EvaluationResults.Successful(v1), EvaluationResults.Successful(v2)) => compare(v1, v2)
- case (err1, err2) => sys.error("evaluation could not complete, got: (" + err1 + ", " + err2 + ")")
- }
- } else {
- var isEq = true
- val vsOrder = vs.toArray
- val counters: Array[Int] = vsOrder.map(_ => min)
- var i = 0
-
- var cont = true
- while(i < counters.size && isEq) {
- val m: Map[Expr, Expr] = vsOrder.zip(counters).map{case (v, c) => (Variable(v), IntLiteral(c))}.toMap
- val ne1 = replace(m, e1)
- val ne2 = replace(m, e2)
- val npre = replace(m, pre)
- val ndm = defaultMap.map{ case (id, expr) => (id, evaluator.eval(expr, m.map{case (Variable(id), t) => (id, t)}).asInstanceOf[EvaluationResults.Successful].value) }
- evaluator.eval(npre, ndm) match {
- case EvaluationResults.Successful(BooleanLiteral(false)) =>
- case EvaluationResults.Successful(BooleanLiteral(true)) =>
- val ev1 = evaluator.eval(ne1, ndm)
- val ev2 = evaluator.eval(ne2, ndm)
- (ev1, ev2) match {
- case (EvaluationResults.Successful(v1), EvaluationResults.Successful(v2)) => if(!compare(v1, v2)) isEq = false
- case (err1, err2) => sys.error("evaluation could not complete, got: (" + err1 + ", " + err2 + ")")
- }
- case err => sys.error("evaluation of precondition could not complete, got: " + err)
+ /*
+ * compare e1 and e2, using a list of assignment of integer to the variables in vs.
+ * Pre is a boolean expression precondition over the same variables that must be evaluated to true
+ * before testing equality.
+ * Add a default mapping for some set parameters
+ * Note that the default map could contain a mapping for variables to other parameters
+ * It is thus necessary to first select values for those parameters and then substitute
+ * into the default map !
+ */
+ def apply(e1: Expr, e2: Expr, vs: Set[Identifier], pre: Expr = BooleanLiteral(true),
+ compare: (Expr, Expr) => Boolean = (e1, e2) => e1 == e2,
+ defaultMap: Map[Identifier, Expr] = Map()): Boolean = {
+ val evaluator = new DefaultEvaluator(testContext, Program.empty)
+ if(vs.isEmpty) {
+ val ndm = defaultMap.map { case (id, expr) => (id, evaluator.eval(expr).asInstanceOf[EvaluationResults.Successful].value) } //TODO: not quite sure why I need to do this...
+ (evaluator.eval(e1, ndm), evaluator.eval(e2, defaultMap)) match {
+ case (EvaluationResults.Successful(v1), EvaluationResults.Successful(v2)) => compare(v1, v2)
+ case (err1, err2) => sys.error("evaluation could not complete, got: (" + err1 + ", " + err2 + ")")
}
+ } else {
+ var isEq = true
+ val vsOrder = vs.toArray
+ val counters: Array[Int] = vsOrder.map(_ => min)
+ var i = 0
- if(counters(i) < max)
- counters(i) += 1
- else {
- while(i < counters.size && counters(i) >= max) {
- counters(i) = min
- i += 1
+ var cont = true
+ while(i < counters.size && isEq) {
+ val m: Map[Expr, Expr] = vsOrder.zip(counters).map{case (v, c) => (Variable(v), IntLiteral(c))}.toMap
+ val ne1 = replace(m, e1)
+ val ne2 = replace(m, e2)
+ val npre = replace(m, pre)
+ val ndm = defaultMap.map{ case (id, expr) => (id, evaluator.eval(expr, m.map{case (Variable(id), t) => (id, t)}).asInstanceOf[EvaluationResults.Successful].value) }
+ evaluator.eval(npre, ndm) match {
+ case EvaluationResults.Successful(BooleanLiteral(false)) =>
+ case EvaluationResults.Successful(BooleanLiteral(true)) =>
+ val ev1 = evaluator.eval(ne1, ndm)
+ val ev2 = evaluator.eval(ne2, ndm)
+ (ev1, ev2) match {
+ case (EvaluationResults.Successful(v1), EvaluationResults.Successful(v2)) => if(!compare(v1, v2)) isEq = false
+ case (err1, err2) => sys.error("evaluation could not complete, got: (" + err1 + ", " + err2 + ")")
+ }
+ case err => sys.error("evaluation of precondition could not complete, got: " + err)
}
- if(i < counters.size) {
+
+ if(counters(i) < max)
counters(i) += 1
- i = 0
+ else {
+ while(i < counters.size && counters(i) >= max) {
+ counters(i) = min
+ i += 1
+ }
+ if(i < counters.size) {
+ counters(i) += 1
+ i = 0
+ }
}
}
+ isEq
}
- isEq
}
+
}
}
diff --git a/src/test/scala/leon/test/purescala/LikelyEqSuite.scala b/src/test/scala/leon/test/purescala/LikelyEqSuite.scala
index 0901ecd2d..8c367a0ce 100644
--- a/src/test/scala/leon/test/purescala/LikelyEqSuite.scala
+++ b/src/test/scala/leon/test/purescala/LikelyEqSuite.scala
@@ -8,7 +8,7 @@ import leon.purescala.Common._
import leon.purescala.Trees._
-class LikelyEqSuite extends LeonTestSuite {
+class LikelyEqSuite extends LeonTestSuite with WithLikelyEq {
def i(x: Int) = IntLiteral(x)
val xId = FreshIdentifier("x")
diff --git a/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala b/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
index d655761f2..f05a5ddef 100644
--- a/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
@@ -12,7 +12,7 @@ import leon.purescala.Trees._
import leon.purescala.TreeOps._
import leon.purescala.TreeNormalizations._
-class TreeNormalizationsTests extends LeonTestSuite {
+class TreeNormalizationsTests extends LeonTestSuite with WithLikelyEq {
def i(x: Int) = IntLiteral(x)
val xId = FreshIdentifier("x").setType(Int32Type)
diff --git a/src/test/scala/leon/test/purescala/TreeOpsTests.scala b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
index d58b17a7c..4bcce108d 100644
--- a/src/test/scala/leon/test/purescala/TreeOpsTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
@@ -15,7 +15,7 @@ import leon.purescala.TreeOps._
import leon.solvers.z3._
-class TreeOpsTests extends LeonTestSuite {
+class TreeOpsTests extends LeonTestSuite with WithLikelyEq {
test("Path-aware simplifications") {
// TODO actually testing something here would be better, sorry
diff --git a/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala b/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
index 2906f7b2c..fe89ed2ab 100644
--- a/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
+++ b/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
@@ -8,13 +8,13 @@ import leon.purescala.TypeTrees._
import leon.purescala.TreeOps._
import leon.purescala.Common._
import leon.purescala.Definitions._
-import leon.test.purescala.LikelyEq
+import leon.test.purescala.WithLikelyEq
import leon.evaluators._
import leon.LeonContext
import leon.synthesis.LinearEquations._
-class LinearEquationsSuite extends LeonTestSuite {
+class LinearEquationsSuite extends LeonTestSuite with WithLikelyEq {
def i(x: Int) = IntLiteral(x)
diff --git a/testcases/synthesis/io-examples/List.scala b/testcases/synthesis/io-examples/List.scala
new file mode 100644
index 000000000..01214c727
--- /dev/null
+++ b/testcases/synthesis/io-examples/List.scala
@@ -0,0 +1,19 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.collection._
+
+object Foo {
+
+ def listOp1(l: List[Int], i: Int) = {
+ //Cons(i, (l-i))
+ //Cons[Int](i, l).slice(0, i)
+ ???[List[Int]]
+ } ensuring { (res: List[Int]) =>
+ passes((l, i), res)(Map[(List[Int], Int), List[Int]](
+ (Nil[Int](), 2) -> Cons(2, Nil[Int]()),
+ (Cons(1, Nil()), 2) -> Cons(2, Cons(1, Nil())),
+ (Cons(1, Cons(2, Cons(3, Nil()))), 3) -> Cons(3, Cons(1, Cons(2, Nil())))
+ ))
+ }
+
+}
--
GitLab