diff --git a/library/Option.scala b/library/Option.scala
index 8aff85e7caf8f3dd870bc0c14f46b4336124722b..e35fc9a0fb36f3701caf51d9845bad976e97351a 100644
--- a/library/Option.scala
+++ b/library/Option.scala
@@ -4,29 +4,25 @@ package leon
import leon.annotation._
+@library
sealed abstract class Option[T] {
- @verified
def getOrElse(default: T) = this match {
case Some(v) => v
case None() => default
}
- @verified
def orElse(or: Option[T]) = this match {
case Some(v) => this
case None() => or
}
- @verified
def isEmpty = this match {
case Some(v) => false
case None() => true
}
- @verified
def nonEmpty = !isEmpty
- @verified
def isDefined = !isEmpty
}
diff --git a/library/annotation/package.scala b/library/annotation/package.scala
index 68cf4e4c60f942065c7f78a87bf3a3a0893cdf9c..1aa564cbd6b0d5aa13d3ba20e5444d4013480aad 100644
--- a/library/annotation/package.scala
+++ b/library/annotation/package.scala
@@ -4,13 +4,22 @@ package leon
import scala.annotation.StaticAnnotation
-@annotation.ignore
-object annotation {
+package object annotation {
+ @ignore
+ class library extends StaticAnnotation
+ @ignore
+ class verified extends StaticAnnotation
+
+ @ignore
class induct extends StaticAnnotation
+ @ignore
class axiomatize extends StaticAnnotation
+ @ignore
class main extends StaticAnnotation
- class verified extends StaticAnnotation
+ @ignore
class proxy extends StaticAnnotation
+ @ignore
class ignore extends StaticAnnotation
+
}
diff --git a/library/collection/List.scala b/library/collection/List.scala
index 622cdb77b5eaa1fac525ce54bcbf2beb94b11076..f2f62924376d778e22966ba19ce085cf75600524 100644
--- a/library/collection/List.scala
+++ b/library/collection/List.scala
@@ -5,33 +5,29 @@ package leon.collection
import leon.lang._
import leon.annotation._
+@library
sealed abstract class List[T] {
- @verified
def size: Int = (this match {
case Nil() => 0
case Cons(h, t) => 1 + t.size
}) ensuring (_ >= 0)
- @verified
def content: Set[T] = this match {
case Nil() => Set()
case Cons(h, t) => Set(h) ++ t.content
}
- @verified
def contains(v: T): Boolean = (this match {
case Cons(h, t) if h == v => true
case Cons(_, t) => t.contains(v)
case Nil() => false
}) ensuring { res => res == (content contains v) }
- @verified
def ++(that: List[T]): List[T] = (this match {
case Nil() => that
case Cons(x, xs) => Cons(x, xs ++ that)
}) ensuring { res => (res.content == this.content ++ that.content) && (res.size == this.size + that.size)}
- @verified
def head: T = {
require(this != Nil[T]())
this match {
@@ -39,7 +35,6 @@ sealed abstract class List[T] {
}
}
- @verified
def tail: List[T] = {
require(this != Nil[T]())
this match {
@@ -47,7 +42,6 @@ sealed abstract class List[T] {
}
}
- @verified
def apply(index: Int): T = {
require(0 <= index && index < size)
if (index == 0) {
@@ -57,7 +51,6 @@ sealed abstract class List[T] {
}
}
- @verified
def :+(t:T): List[T] = {
this match {
case Nil() => Cons(t, this)
@@ -65,7 +58,6 @@ sealed abstract class List[T] {
}
} ensuring(res => (res.size == size + 1) && (res.content == content ++ Set(t)))
- @verified
def reverse: List[T] = {
this match {
case Nil() => this
@@ -78,8 +70,8 @@ sealed abstract class List[T] {
case class Cons[T](h: T, t: List[T]) extends List[T]
case class Nil[T]() extends List[T]
+@library
object ListSpecs {
- @verified
def snocIndex[T](l : List[T], t : T, i : Int) : Boolean = {
require(0 <= i && i < l.size + 1)
// proof:
@@ -91,7 +83,6 @@ object ListSpecs {
((l :+ t).apply(i) == (if (i < l.size) l(i) else t))
}.holds
- @verified
def reverseIndex[T](l : List[T], i : Int) : Boolean = {
require(0 <= i && i < l.size)
(l match {
@@ -101,7 +92,6 @@ object ListSpecs {
(l.reverse.apply(i) == l.apply(l.size - 1 - i))
}.holds
- @verified
def appendIndex[T](l1 : List[T], l2 : List[T], i : Int) : Boolean = {
require(0 <= i && i < l1.size + l2.size)
(l1 match {
@@ -111,7 +101,6 @@ object ListSpecs {
((l1 ++ l2).apply(i) == (if (i < l1.size) l1(i) else l2(i - l1.size)))
}.holds
- @verified
def appendAssoc[T](l1 : List[T], l2 : List[T], l3 : List[T]) : Boolean = {
(l1 match {
case Nil() => true
@@ -120,7 +109,6 @@ object ListSpecs {
(((l1 ++ l2) ++ l3) == (l1 ++ (l2 ++ l3)))
}.holds
- @verified
def snocIsAppend[T](l : List[T], t : T) : Boolean = {
(l match {
case Nil() => true
@@ -129,7 +117,6 @@ object ListSpecs {
((l :+ t) == l ++ Cons[T](t, Nil()))
}.holds
- @verified
def snocAfterAppend[T](l1 : List[T], l2 : List[T], t : T) : Boolean = {
(l1 match {
case Nil() => true
@@ -138,7 +125,6 @@ object ListSpecs {
((l1 ++ l2) :+ t == (l1 ++ (l2 :+ t)))
}.holds
- @verified
def snocReverse[T](l : List[T], t : T) : Boolean = {
(l match {
case Nil() => true
@@ -147,7 +133,6 @@ object ListSpecs {
((l :+ t).reverse == Cons(t, l.reverse))
}.holds
- @verified
def reverseReverse[T](l : List[T]) : Boolean = {
(l match {
case Nil() => true
diff --git a/library/lang/package.scala b/library/lang/package.scala
index 8cb68e7a183223698cddecfd9e9c862d8e7f1e4b..41cd25b65252531bedfe3104900a1a9beb226311 100644
--- a/library/lang/package.scala
+++ b/library/lang/package.scala
@@ -5,8 +5,8 @@ package leon
import leon.annotation._
import scala.language.implicitConversions
-@ignore
-object lang {
+package object lang {
+ @ignore
sealed class IsValid(val property : Boolean) {
def holds : Boolean = {
assert(property)
@@ -14,27 +14,17 @@ object lang {
}
}
+ @ignore
implicit def any2IsValid(x: Boolean) : IsValid = new IsValid(x)
- def epsilon[A](pred: (A) => Boolean): A = throw new RuntimeException("Implementation not supported")
-
+ @ignore
object InvariantFunction {
def invariant(x: Boolean): Unit = ()
}
+ @ignore
implicit def while2Invariant(u: Unit) = InvariantFunction
- def waypoint[A](i: Int, expr: A): A = expr
-
- private def noChoose = throw new RuntimeException("Implementation not supported")
-
- def choose[A](predicate: A => Boolean): A = noChoose
- def choose[A, B](predicate: (A, B) => Boolean): (A, B) = noChoose
- def choose[A, B, C](predicate: (A, B, C) => Boolean): (A, B, C) = noChoose
- def choose[A, B, C, D](predicate: (A, B, C, D) => Boolean): (A, B, C, D) = noChoose
- def choose[A, B, C, D, E](predicate: (A, B, C, D, E) => Boolean): (A, B, C, D, E) = noChoose
-
- def ???[A]: A = throw new RuntimeException("Implementation not supported")
-
+ @ignore
def error[T](reason: String): T = sys.error(reason)
}
diff --git a/library/lang/xlang/package.scala b/library/lang/xlang/package.scala
new file mode 100644
index 0000000000000000000000000000000000000000..928498a47fde10683059ef3d640a3ef2bc0afb24
--- /dev/null
+++ b/library/lang/xlang/package.scala
@@ -0,0 +1,13 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon.lang
+
+import leon.annotation._
+
+package object xlang {
+ @ignore
+ def waypoint[A](i: Int, expr: A): A = expr
+
+ @ignore
+ def epsilon[A](pred: (A) => Boolean): A = throw new RuntimeException("Implementation not supported")
+}
diff --git a/scripts/applyLicense.sh b/scripts/applyLicense.sh
index 7bf0aa64fb67943b649098401606d72161333e08..cc809905d4bdb3c84e08f18b11703ba0ff2f8290 100755
--- a/scripts/applyLicense.sh
+++ b/scripts/applyLicense.sh
@@ -9,6 +9,9 @@ for f in $(find {src,library} -name "*.java" -o -name "*.scala") ;do
else
cat $f >> /tmp/newfile
fi
- mv /tmp/newfile "$f"
+ if ! cmp --silent /tmp/newfile "$f"; then
+ echo $f
+ mv /tmp/newfile "$f"
+ fi
fi
done
diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index c9c989e237fd6635b6abf7e4c721a9efb08a586d..fa5c0929f0c22d92fa0fc92f4a447c3de1d1c6c4 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -60,3 +60,39 @@ object ListValue {
}
}
}
+
+object OptionsHelpers {
+ // helper for options that include patterns
+
+ def matcher(patterns: Traversable[String]): String => Boolean = {
+ val regexPatterns = patterns map { s =>
+ import java.util.regex.Pattern
+
+ val p = s.replaceAll("\\.", "\\\\.").replaceAll("_", ".+")
+ Pattern.compile(p)
+ }
+
+ { (name: String) => regexPatterns.exists(p => p.matcher(name).matches()) }
+ }
+
+ import purescala.Definitions.FunDef
+
+ def fdMatcher(patterns: Traversable[String]): FunDef => Boolean = {
+ { (fd: FunDef) => fd.id.name } andThen matcher(patterns)
+ }
+
+ def filterInclusive[T](included: Option[T => Boolean], excluded: Option[T => Boolean]): T => Boolean = {
+ included match {
+ case Some(i) =>
+ i
+ case None =>
+ excluded match {
+ case Some(f) =>
+ { (t: T) => !f(t) }
+
+ case None =>
+ { (t: T) => true }
+ }
+ }
+ }
+}
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 7a30d6530498b123d099334e0449b81fd14e4018..f2cba94b7fb5fefa2ea254667a3bbee3aae233e7 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -187,26 +187,29 @@ object Main {
def computePipeline(settings: Settings): Pipeline[List[String], Any] = {
import purescala.Definitions.Program
+ import frontends.scalac.ExtractionPhase
+ import synthesis.SynthesisPhase
+ import termination.TerminationPhase
+ import xlang.XlangAnalysisPhase
+ import verification.AnalysisPhase
val pipeBegin : Pipeline[List[String],Program] =
- frontends.scalac.ExtractionPhase andThen
- purescala.MethodLifting andThen
- utils.TypingPhase andThen
- purescala.CompleteAbstractDefinitions andThen
- synthesis.ConvertHoles
+ ExtractionPhase andThen
+ PreprocessingPhase
- val pipeProcess: Pipeline[Program, Any] =
+ val pipeProcess: Pipeline[Program, Any] = {
if (settings.synthesis) {
- synthesis.SynthesisPhase
+ SynthesisPhase
} else if (settings.termination) {
- termination.TerminationPhase
+ TerminationPhase
} else if (settings.xlang) {
- xlang.XlangAnalysisPhase
+ XlangAnalysisPhase
} else if (settings.verify) {
- verification.AnalysisPhase
+ AnalysisPhase
} else {
NoopPhase()
}
+ }
pipeBegin andThen
pipeProcess
diff --git a/src/main/scala/leon/Pipeline.scala b/src/main/scala/leon/Pipeline.scala
index 82125a9af5c29b9171fe3e2fb12f309a27290208..64a618129f07c0f825be8eeacaf861c62c692f63 100644
--- a/src/main/scala/leon/Pipeline.scala
+++ b/src/main/scala/leon/Pipeline.scala
@@ -6,7 +6,11 @@ abstract class Pipeline[-F, +T] {
self =>
def andThen[G](thenn: Pipeline[T, G]): Pipeline[F, G] = new Pipeline[F,G] {
- def run(ctx : LeonContext)(v : F) : G = thenn.run(ctx)(self.run(ctx)(v))
+ def run(ctx : LeonContext)(v : F) : G = {
+ val s = self.run(ctx)(v)
+ ctx.reporter.terminateIfError()
+ thenn.run(ctx)(s)
+ }
}
def run(ctx: LeonContext)(v: F): T
diff --git a/src/main/scala/leon/Reporter.scala b/src/main/scala/leon/Reporter.scala
index 4e4963bdbc22c6a72bd6953c6761fa6af0ddcec3..18e93f87055099365044ab2a74c9d470b780a7c6 100644
--- a/src/main/scala/leon/Reporter.scala
+++ b/src/main/scala/leon/Reporter.scala
@@ -147,7 +147,7 @@ class DefaultReporter(settings: Settings) extends Reporter(settings) {
val width = Math.max(ep.col - bp.col, 1)
("^" * width)
} else {
- val width = Math.max(line.length-bp.col, 1)
+ val width = Math.max(line.length+1-bp.col, 1)
("^" * width)+"..."
}
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index bd4910f4c65d3c1c3f5490a8dd604291d15faa65..66034599f2524a3a4d3005d7849641fb21b17a6b 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -22,7 +22,9 @@ object Settings {
private def defaultClassPath() = {
val scalaHome = System.getenv("SCALA_HOME")
- val scalaCPs = if (scalaHome != "") {
+ assert(scalaHome ne null, "SCALA_HOME was not found in the environment, did you run `source setupenv.sh` ?")
+
+ if (scalaHome != "") {
val f = new java.io.File(scalaHome+"/lib")
f.listFiles().collect {
@@ -32,8 +34,6 @@ object Settings {
} else {
Nil
}
-
- scalaCPs
}
private[leon] def defaultLibFiles() = {
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index f1ff028aa6d35cfb7d959cfa59644049de94a337..9a36ab3292caf5c34e3b5dd2b9b86744d3f70628 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -7,6 +7,7 @@ import purescala.Common._
import purescala.Definitions._
import purescala.Trees._
import purescala.TypeTrees._
+import utils._
import cafebabe._
import cafebabe.AbstractByteCodes._
@@ -414,6 +415,9 @@ trait CodeGeneration {
ch << InvokeSpecial(ErrorClass, constructorName, "(Ljava/lang/String;)V")
ch << ATHROW
+ case hole @ Hole(oracle) =>
+ mkExpr(OracleTraverser(oracle, hole.getType, program).value, ch)
+
case choose @ Choose(_, _) =>
val prob = synthesis.Problem.fromChoose(choose)
diff --git a/src/main/scala/leon/datagen/NaiveDataGen.scala b/src/main/scala/leon/datagen/NaiveDataGen.scala
index 6dc3865c95409db168201d00e8076849703b34e5..b1727fb71926e8e067d687a3bb62a42b78f5198f 100644
--- a/src/main/scala/leon/datagen/NaiveDataGen.scala
+++ b/src/main/scala/leon/datagen/NaiveDataGen.scala
@@ -63,11 +63,16 @@ class NaiveDataGen(ctx: LeonContext, p: Program, evaluator: Evaluator, _bounds :
private val streamCache : MutableMap[TypeTree,Stream[Expr]] = MutableMap.empty
def generate(tpe : TypeTree, bounds : Map[TypeTree,Seq[Expr]] = defaultBounds) : Stream[Expr] = {
- streamCache.getOrElse(tpe, {
- val s = generate0(tpe, bounds)
- streamCache(tpe) = s
- s
- })
+ try {
+ streamCache.getOrElse(tpe, {
+ val s = generate0(tpe, bounds)
+ streamCache(tpe) = s
+ s
+ })
+ } catch {
+ case so: StackOverflowError =>
+ Stream.empty
+ }
}
// TODO We should make sure the cache depends on the bounds (i.e. is not reused for different bounds.)
diff --git a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
index 158547f1331668113f761daa40a9c59cf47a853d..abdbec318699bf03e9c912aef7d755c6d0587b3b 100644
--- a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
+++ b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
@@ -52,7 +52,7 @@ class CodeGenEvaluator(ctx : LeonContext, val unit : CompilationUnit) extends Ev
})
} catch {
case t: Throwable =>
- ctx.reporter.warning("Error while compiling expression: "+t.getMessage)
+ ctx.reporter.warning(expression.getPos, "Error while compiling expression: "+t.getMessage)
None
}
}
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index ecad714521bde7a8853f143265854933f642dcc7..92f2b579f509faceb099c0eb6417ac1db526fa73 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -409,7 +409,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program) extends Evalu
}
case other =>
- context.reporter.error("Error: don't know how to handle " + other + " in Evaluator.")
+ context.reporter.error(other.getPos, "Error: don't know how to handle " + other + " in Evaluator.")
throw EvalError("Unhandled case in Evaluator : " + other)
}
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index d5aec11a0703e034931cfc1542d6ee64573ab2a7..97fbbc2ac69919c452256b57bb2152fea490a720 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -15,6 +15,7 @@ trait ASTExtractors {
def classFromName(str: String) = {
rootMirror.getClassByName(newTypeName(str))
}
+
def objectFromName(str: String) = {
rootMirror.getClassByName(newTermName(str))
}
@@ -30,12 +31,14 @@ trait ASTExtractors {
protected lazy val arraySym = classFromName("scala.Array")
protected lazy val someClassSym = classFromName("scala.Some")
protected lazy val function1TraitSym = classFromName("scala.Function1")
+ protected lazy val byNameSym = classFromName("scala.<byname>")
def isTuple2(sym : Symbol) : Boolean = sym == tuple2Sym
def isTuple3(sym : Symbol) : Boolean = sym == tuple3Sym
def isTuple4(sym : Symbol) : Boolean = sym == tuple4Sym
def isTuple5(sym : Symbol) : Boolean = sym == tuple5Sym
+ def isByNameSym(sym : Symbol) : Boolean = getResolvedTypeSym(sym) == byNameSym
// Resolve type aliases
def getResolvedTypeSym(sym: Symbol): Symbol = {
@@ -89,6 +92,12 @@ trait ASTExtractors {
def unapply(name: Name): Option[String] = Some(name.toString)
}
+ object ExSymbol {
+ def unapplySeq(t: Tree): Option[Seq[String]] = {
+ Some(t.symbol.fullName.toString.split('.').toSeq)
+ }
+ }
+
object ExSelected {
def unapplySeq(select: Select): Option[Seq[String]] = select match {
case Select(This(scalaName), name) =>
@@ -122,7 +131,7 @@ trait ASTExtractors {
object ExHoldsExpression {
def unapply(tree: Select) : Option[Tree] = tree match {
- case Select(Apply(ExSelected("leon", "lang", "any2IsValid"), realExpr :: Nil), ExNamed("holds")) =>
+ case Select(Apply(ExSymbol("leon", "lang", "any2IsValid"), realExpr :: Nil), ExNamed("holds")) =>
Some(realExpr)
case _ => None
}
@@ -147,7 +156,7 @@ trait ASTExtractors {
* visibility. Does not match on the automatically generated companion
* objects of case classes (or any synthetic class). */
def unapply(cd: ClassDef): Option[(String,Template)] = cd match {
- case ClassDef(_, name, tparams, impl) if (cd.symbol.isModuleClass && tparams.isEmpty && !cd.symbol.isSynthetic) => {
+ case ClassDef(_, name, tparams, impl) if ((cd.symbol.isModuleClass || cd.symbol.isPackage) && tparams.isEmpty && !cd.symbol.isSynthetic) => {
Some((name.toString, impl))
}
case _ => None
@@ -174,7 +183,7 @@ trait ASTExtractors {
case _ => false
}).get.asInstanceOf[DefDef]
- val args = constructor.vparamss(0).map(vd => (vd.name.toString, vd.tpt))
+ val args = constructor.vparamss.flatten.map(vd => (vd.name.toString, vd.tpt))
Some((name.toString, cd.symbol, args, impl))
}
@@ -201,7 +210,7 @@ trait ASTExtractors {
object ExConstructorDef {
def unapply(dd: DefDef): Boolean = dd match {
- case DefDef(_, name, tparams, vparamss, tpt, rhs) if(name == nme.CONSTRUCTOR && tparams.isEmpty && vparamss.size == 1) => true
+ case DefDef(_, name, tparams, vparamss, tpt, rhs) if(name == nme.CONSTRUCTOR && tparams.isEmpty) => true
case _ => false
}
}
@@ -219,8 +228,8 @@ trait ASTExtractors {
/** Matches a function with a single list of arguments, no type
* parameters and regardless of its visibility. */
def unapply(dd: DefDef): Option[(Symbol, Seq[Symbol], Seq[ValDef], Type, Tree)] = dd match {
- case DefDef(_, name, tparams, vparamss, tpt, rhs) if(vparamss.size <= 1 && name != nme.CONSTRUCTOR) =>
- Some((dd.symbol, tparams.map(_.symbol), vparamss.headOption.getOrElse(Nil), tpt.tpe, rhs))
+ case DefDef(_, name, tparams, vparamss, tpt, rhs) if(name != nme.CONSTRUCTOR) =>
+ Some((dd.symbol, tparams.map(_.symbol), vparamss.flatten, tpt.tpe, rhs))
case _ => None
}
}
@@ -231,48 +240,50 @@ trait ASTExtractors {
import ExtractorHelpers._
object ExEpsilonExpression {
- def unapply(tree: Apply) : Option[(Type, Symbol, Tree)] = tree match {
+ def unapply(tree: Apply) : Option[(Tree, Symbol, Tree)] = tree match {
case Apply(
- TypeApply(ExSelected("leon", "lang", "epsilon"), typeTree :: Nil),
+ TypeApply(ExSymbol("leon", "lang", "xlang", "epsilon"), typeTree :: Nil),
Function((vd @ ValDef(_, _, _, EmptyTree)) :: Nil, predicateBody) :: Nil) =>
- Some((typeTree.tpe, vd.symbol, predicateBody))
+ Some((typeTree, vd.symbol, predicateBody))
+ case _ => None
+ }
+ }
+
+ object ExWaypointExpression {
+ def unapply(tree: Apply) : Option[(Tree, Tree, Tree)] = tree match {
+ case Apply(
+ TypeApply(ExSymbol("leon", "lang", "xlang", "waypoint"), typeTree :: Nil),
+ List(i, expr)) =>
+ Some((typeTree, i, expr))
case _ => None
}
}
object ExErrorExpression {
- def unapply(tree: Apply) : Option[(String, Type)] = tree match {
- case a @ Apply(TypeApply(ExSelected("leon", "lang", "error"), List(tpe)), List(lit : Literal)) =>
- Some((lit.value.stringValue, tpe.tpe))
+ def unapply(tree: Apply) : Option[(String, Tree)] = tree match {
+ case a @ Apply(TypeApply(ExSymbol("leon", "lang", "error"), List(tpe)), List(lit : Literal)) =>
+ Some((lit.value.stringValue, tpe))
case _ =>
None
}
}
- object ExHole {
- def unapply(tree: TypeApply) : Option[Type] = tree match {
- case a @ TypeApply(s @ ExSelected("leon", "lang", _), List(tpe)) if s.symbol.name.decoded == "???" =>
- Some(a.tpe)
+ object ExHoleExpression {
+ def unapply(tree: Tree) : Option[(Tree, List[Tree], List[Tree])] = tree match {
+ case a @ Apply(Apply(TypeApply(s @ ExSymbol("leon", "lang", "synthesis", "$qmark"), List(tpt)), args1), args2) =>
+ Some((tpt, args1, args2))
+ case a @ Apply(TypeApply(s @ ExSymbol("leon", "lang", "synthesis", "$qmark$qmark$qmark"), List(tpt)), List(o)) =>
+ Some((tpt, Nil, List(o)))
case _ => None
}
}
object ExChooseExpression {
- def unapply(tree: Apply) : Option[(List[(Type, Symbol)], Type, Tree, Tree)] = tree match {
+ def unapply(tree: Apply) : Option[(List[(Tree, Symbol)], Tree, Tree, Tree)] = tree match {
case a @ Apply(
- TypeApply(s @ ExSelected("leon", "lang", "choose"), types),
+ TypeApply(s @ ExSymbol("leon", "lang", "synthesis", "choose"), types),
Function(vds, predicateBody) :: Nil) =>
- Some(((types.map(_.tpe) zip vds.map(_.symbol)).toList, a.tpe, predicateBody, s))
- case _ => None
- }
- }
-
- object ExWaypointExpression {
- def unapply(tree: Apply) : Option[(Type, Tree, Tree)] = tree match {
- case Apply(
- TypeApply(ExSelected("leon", "lang", "waypoint"), typeTree :: Nil),
- List(i, expr)) =>
- Some((typeTree.tpe, i, expr))
+ Some(((types zip vds.map(_.symbol)).toList, a, predicateBody, s))
case _ => None
}
}
@@ -681,29 +692,44 @@ trait ASTExtractors {
}
}
- object ExCall {
- def unapply(tree: Tree): Option[(Tree, Symbol, Seq[Tree], Seq[Tree])] = tree match {
+ object ExParameterLessCall {
+ def unapply(tree: Tree): Option[(Tree, Symbol, Seq[Tree])] = tree match {
case s @ Select(t, _) =>
- Some((t, s.symbol, Nil, Nil))
-
- case TypeApply(s @ Select(t, _), tps) =>
- Some((t, s.symbol, tps, Nil))
+ Some((t, s.symbol, Nil))
- case TypeApply(i: Ident, tps) =>
- Some((i, i.symbol, tps, Nil))
+ case TypeApply(s @ Select(t, _), tps) =>
+ Some((t, s.symbol, tps))
- case Apply(TypeApply(s @ Select(t, _), tps), args) =>
- Some((t, s.symbol, tps, args))
+ case TypeApply(i: Ident, tps) =>
+ Some((i, i.symbol, tps))
- case Apply(TypeApply(i: Ident, tps), args) =>
- Some((i, i.symbol, tps, args))
+ case _ =>
+ None
+ }
+ }
- case Apply(s @ Select(t, _), args) =>
- Some((t, s.symbol, Nil, args))
+ object ExCall {
+ def unapply(tree: Tree): Option[(Tree, Symbol, Seq[Tree], Seq[Tree])] = tree match {
+ // foo / foo[T]
+ case ExParameterLessCall(t, s, tps) =>
+ Some((t, s, tps, Nil))
- case Apply(i: Ident, args) =>
+ // foo(args)
+ case Apply(i: Ident, args) =>
Some((i, i.symbol, Nil, args))
+ // foo(args1)(args2)
+ case Apply(Apply(i: Ident, args1), args2) =>
+ Some((i, i.symbol, Nil, args1 ++ args2))
+
+ // foo[T](args)
+ case Apply(ExParameterLessCall(t, s, tps), args) =>
+ Some((t, s, tps, args))
+
+ // foo[T](args1)(args2)
+ case Apply(Apply(ExParameterLessCall(t, s, tps), args1), args2) =>
+ Some((t, s, tps, args1 ++ args2))
+
case _ => None
}
}
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 720aef3199ca51f6f2e5e59868a19d0fd000a90d..95912df292aad6fdf4efdbd9194e4ddb6f9dcd3d 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -32,9 +32,11 @@ trait CodeExtraction extends ASTExtractors {
import ExtractorHelpers._
import scala.collection.immutable.Set
+ val reporter = self.ctx.reporter
+
def annotationsOf(s: Symbol): Set[String] = {
- (for(a <- s.annotations) yield {
- val name = a.atp.safeToString
+ (for(a <- s.annotations ++ s.owner.annotations) yield {
+ val name = a.atp.safeToString.replaceAll("\\.package\\.", ".")
if (name startsWith "leon.annotation.") {
Some(name.split("\\.", 3)(2))
} else {
@@ -58,10 +60,13 @@ trait CodeExtraction extends ASTExtractors {
}
}
- def leonPosToScalaPos(sf: SourceFile, p: LeonPosition): global.Position = {
- p match {
- case dp: DefinedPosition =>
- new OffsetPosition(sf, dp.focusBegin.point)
+ def leonPosToScalaPos(spos: global.Position, p: LeonPosition): global.Position = {
+ (spos, p) match {
+ case (NoPosition, _) =>
+ NoPosition
+
+ case (p, dp: DefinedPosition) =>
+ new OffsetPosition(p.source, dp.focusBegin.point)
case _ =>
NoPosition
@@ -117,7 +122,7 @@ trait CodeExtraction extends ASTExtractors {
}
// This one never fails, on error, it returns Untyped
- def toPureScalaType(tpt: Type)(implicit dctx: DefContext): LeonType = {
+ def toPureScalaType(tpt: Type)(implicit dctx: DefContext, pos: Position): LeonType = {
try {
extractType(tpt)
} catch {
@@ -156,6 +161,14 @@ trait CodeExtraction extends ASTExtractors {
}
}
+ def isIgnored(s: Symbol) = {
+ (annotationsOf(s) contains "ignore") || (s.fullName.toString.endsWith(".main"))
+ }
+
+ def isProxy(s: Symbol) = {
+ annotationsOf(s) contains "proxy"
+ }
+
def extractModules: List[LeonModuleDef] = {
try {
val templates: List[(String, List[Tree])] = units.reverse.flatMap { u => u.body match {
@@ -163,9 +176,12 @@ trait CodeExtraction extends ASTExtractors {
var standaloneDefs = List[Tree]()
val modules: List[(String, List[Tree])] = lst.flatMap { _ match {
- case od @ ExObjectDef(_, _) if annotationsOf(od.symbol) contains "ignore" =>
+ case t if isIgnored(t.symbol) =>
None
+ case PackageDef(_, List(ExObjectDef(n, templ))) =>
+ Some((n.toString, templ.body))
+
case ExObjectDef(n, templ) =>
Some((n.toString, templ.body))
@@ -222,9 +238,19 @@ trait CodeExtraction extends ASTExtractors {
private var seenClasses = Map[Symbol, (Seq[(String, Tree)], Template)]()
private var classesToClasses = Map[Symbol, LeonClassDef]()
+
+ def libraryMethod(classname: String, methodName: String): Option[(LeonClassDef, FunDef)] = {
+ classesToClasses.values.find(_.id.name == classname).flatMap { cl =>
+ cl.methods.find(_.id.name == methodName).map { fd => (cl, fd) }
+ }
+ }
+
private def collectClassSymbols(defs: List[Tree]) {
// We collect all defined classes
for (t <- defs) t match {
+ case t if isIgnored(t.symbol) =>
+ // ignore
+
case ExAbstractClass(o2, sym, tmpl) =>
seenClasses += sym -> ((Nil, tmpl))
@@ -238,11 +264,14 @@ trait CodeExtraction extends ASTExtractors {
private def extractClassDefs(defs: List[Tree]) {
// We collect all defined classes
for (t <- defs) t match {
+ case t if isIgnored(t.symbol) =>
+ // ignore
+
case ExAbstractClass(o2, sym, _) =>
- getClassDef(sym, NoPosition)
+ getClassDef(sym, t.pos)
case ExCaseClass(o2, sym, args, _) =>
- getClassDef(sym, NoPosition)
+ getClassDef(sym, t.pos)
case _ =>
}
@@ -257,6 +286,9 @@ trait CodeExtraction extends ASTExtractors {
extractClassDef(sym, args, tmpl)
} else {
+ if (sym.name.toString == "synthesis") {
+ new Exception().printStackTrace()
+ }
outOfSubsetError(pos, "Class "+sym.name+" not defined?")
}
}
@@ -292,7 +324,7 @@ trait CodeExtraction extends ASTExtractors {
case Some(TypeRef(_, parentSym, tps)) if seenClasses contains parentSym =>
getClassDef(parentSym, sym.pos) match {
case acd: AbstractClassDef =>
- val newTps = tps.map(extractType(_)(defCtx))
+ val newTps = tps.map(extractType(_)(defCtx, sym.pos))
Some(AbstractClassType(acd, newTps))
case cd =>
@@ -318,7 +350,7 @@ trait CodeExtraction extends ASTExtractors {
classesToClasses += sym -> ccd
val fields = args.map { case (name, t) =>
- val tpe = toPureScalaType(t.tpe)(defCtx)
+ val tpe = toPureScalaType(t.tpe)(defCtx, sym.pos)
LeonValDef(FreshIdentifier(name).setType(tpe).setPos(t.pos), tpe).setPos(t.pos)
}
@@ -349,6 +381,9 @@ trait CodeExtraction extends ASTExtractors {
// We collect the methods
for (d <- tmpl.body) d match {
+ case t if isIgnored(t.symbol) =>
+ //ignore
+
case t @ ExFunctionDef(fsym, _, _, _, _) if !fsym.isSynthetic && !fsym.isAccessor =>
if (parent.isDefined) {
outOfSubsetError(t, "Only hierarchy roots can define methods")
@@ -372,12 +407,10 @@ trait CodeExtraction extends ASTExtractors {
// Type params of the function itself
val tparams = extractTypeParams(sym.typeParams.map(_.tpe))
- val isProxy = annotationsOf(sym) contains "proxy"
-
- val nctx = dctx.copy(tparams = dctx.tparams ++ tparams.toMap, isProxy = isProxy)
+ val nctx = dctx.copy(tparams = dctx.tparams ++ tparams.toMap, isProxy = isProxy(sym))
val newParams = sym.info.paramss.flatten.map{ sym =>
- val ptpe = toPureScalaType(sym.tpe)(nctx)
+ val ptpe = toPureScalaType(sym.tpe)(nctx, sym.pos)
val newID = FreshIdentifier(sym.name.toString).setType(ptpe).setPos(sym.pos)
owners += (newID -> None)
LeonValDef(newID, ptpe).setPos(sym.pos)
@@ -385,7 +418,7 @@ trait CodeExtraction extends ASTExtractors {
val tparamsDef = tparams.map(t => TypeParameterDef(t._2))
- val returnType = toPureScalaType(sym.info.finalResultType)(nctx)
+ val returnType = toPureScalaType(sym.info.finalResultType)(nctx, sym.pos)
val name = sym.name.toString
@@ -403,8 +436,8 @@ trait CodeExtraction extends ASTExtractors {
private def collectFunSigs(defs: List[Tree]) = {
// We collect defined function bodies
for (d <- defs) d match {
- case ExMainFunctionDef() =>
- // Ignoring...
+ case t if isIgnored(t.symbol) =>
+ //ignore
case ExFunctionDef(sym, _, _, _, _) =>
defineFunDef(sym)(DefContext())
@@ -442,6 +475,9 @@ trait CodeExtraction extends ASTExtractors {
}
}
for (d <- defs) d match {
+ case t if isIgnored(t.symbol) =>
+ // ignore
+
case ExAbstractClass(_, csym, tmpl) =>
extractFromClass(csym, tmpl)
@@ -455,15 +491,15 @@ trait CodeExtraction extends ASTExtractors {
private def extractFunDefs(defs: List[Tree]) = {
// We collect defined function bodies
for (d <- defs) d match {
- case ExMainFunctionDef() =>
- // Ignoring...
+ case t if isIgnored(t.symbol) =>
+ // ignore
case ExFunctionDef(sym, tparams, params, _, body) =>
val fd = defsToDefs(sym)
val tparamsMap = (tparams zip fd.tparams.map(_.tp)).toMap
- extractFunBody(fd, params, body)(DefContext(tparamsMap))
+ extractFunBody(fd, params, body)(DefContext(tparamsMap, isProxy = isProxy(sym)))
case _ =>
}
@@ -482,16 +518,15 @@ trait CodeExtraction extends ASTExtractors {
private def extractObjectDef(nameStr: String, defs: List[Tree]): LeonModuleDef = {
val newDefs = defs.flatMap{ t => t match {
+ case t if isIgnored(t.symbol) =>
+ None
+
case ExAbstractClass(o2, sym, _) =>
Some(classesToClasses(sym))
case ExCaseClass(o2, sym, args, _) =>
Some(classesToClasses(sym))
- case ExMainFunctionDef() =>
- // Ignoring...
- None
-
case ExFunctionDef(sym, tparams, params, _, body) =>
Some(defsToDefs(sym))
@@ -505,9 +540,8 @@ trait CodeExtraction extends ASTExtractors {
case ExAbstractClass(_,_,_) =>
case ExCaseClass(_,_,_,_) =>
case ExConstructorDef() =>
- case ExMainFunctionDef() =>
case ExFunctionDef(_, _, _, _, _) =>
- case defn if annotationsOf(defn.symbol) contains "ignore" =>
+ case d if isIgnored(d.symbol) =>
case tree =>
outOfSubsetError(tree, "Don't know what to do with this. Not purescala?");
}
@@ -568,15 +602,14 @@ trait CodeExtraction extends ASTExtractors {
})
} catch {
case e: ImpureCodeEncounteredException =>
- if (funDef.annotations contains "proxy") {
+ if (dctx.isProxy) {
// We actually expect errors, no point reporting
} else {
e.emit()
- val pos = if (body.pos == NoPosition) NoPosition else leonPosToScalaPos(body.pos.source, funDef.getPos)
if (ctx.settings.strictCompilation) {
- reporter.error(pos, "Function "+funDef.id.name+" could not be extracted. (Forgot @proxy ?)")
+ reporter.error(funDef.getPos, "Function "+funDef.id.name+" could not be extracted. (Forgot @proxy ?)")
} else {
- reporter.warning(pos, "Function "+funDef.id.name+" is not fully unavailable to Leon.")
+ reporter.warning(funDef.getPos, "Function "+funDef.id.name+" is not fully unavailable to Leon.")
}
}
@@ -609,18 +642,18 @@ trait CodeExtraction extends ASTExtractors {
}
private def extractPattern(p: Tree, binder: Option[Identifier] = None)(implicit dctx: DefContext): (Pattern, DefContext) = p match {
- case b @ Bind(name, t @ Typed(pat, tpe)) =>
- val newID = FreshIdentifier(name.toString).setType(extractType(tpe.tpe)).setPos(b.pos)
+ case b @ Bind(name, t @ Typed(pat, tpt)) =>
+ val newID = FreshIdentifier(name.toString).setType(extractType(tpt)).setPos(b.pos)
val pctx = dctx.withNewVar(b.symbol -> (() => Variable(newID)))
extractPattern(t, Some(newID))(pctx)
case b @ Bind(name, pat) =>
- val newID = FreshIdentifier(name.toString).setType(extractType(b.symbol.tpe)).setPos(b.pos)
+ val newID = FreshIdentifier(name.toString).setType(extractType(b)).setPos(b.pos)
val pctx = dctx.withNewVar(b.symbol -> (() => Variable(newID)))
extractPattern(pat, Some(newID))(pctx)
case t @ Typed(Ident(nme.WILDCARD), tpt) =>
- extractType(tpt.tpe) match {
+ extractType(tpt) match {
case ct: ClassType =>
(InstanceOfPattern(binder, ct).setPos(p.pos), dctx)
@@ -633,7 +666,7 @@ trait CodeExtraction extends ASTExtractors {
case s @ Select(_, b) if s.tpe.typeSymbol.isCase =>
// case Obj =>
- extractType(s.tpe) match {
+ extractType(s) match {
case ct: CaseClassType =>
assert(ct.classDef.fields.size == 0)
(CaseClassPattern(binder, ct, Seq()).setPos(p.pos), dctx)
@@ -643,7 +676,7 @@ trait CodeExtraction extends ASTExtractors {
case a @ Apply(fn, args) =>
- extractType(a.tpe) match {
+ extractType(a) match {
case ct: CaseClassType =>
assert(args.size == ct.classDef.fields.size)
val (subPatterns, subDctx) = args.map(extractPattern(_)).unzip
@@ -698,7 +731,7 @@ trait CodeExtraction extends ASTExtractors {
val res = current match {
case ExArrayLiteral(tpe, args) =>
- FiniteArray(args.map(extractTree)).setType(ArrayType(extractType(tpe)))
+ FiniteArray(args.map(extractTree)).setType(ArrayType(extractType(tpe)(dctx, current.pos)))
case ExCaseObject(sym) =>
getClassDef(sym, current.pos) match {
@@ -713,8 +746,8 @@ trait CodeExtraction extends ASTExtractors {
val tupleType = TupleType(tupleExprs.map(expr => expr.getType))
Tuple(tupleExprs)
- case ExErrorExpression(str, tpe) =>
- Error(str).setType(extractType(tpe))
+ case ExErrorExpression(str, tpt) =>
+ Error(str).setType(extractType(tpt))
case ExTupleExtract(tuple, index) =>
val tupleExpr = extractTree(tuple)
@@ -728,7 +761,7 @@ trait CodeExtraction extends ASTExtractors {
}
case ExValDef(vs, tpt, bdy) =>
- val binderTpe = extractType(tpt.tpe)
+ val binderTpe = extractType(tpt)
val newID = FreshIdentifier(vs.name.toString).setType(binderTpe)
val valTree = extractTree(bdy)
@@ -760,7 +793,7 @@ trait CodeExtraction extends ASTExtractors {
fd.addAnnotation(annotationsOf(d.symbol).toSeq : _*)
- val newDctx = dctx.copy(tparams = dctx.tparams ++ tparamsMap)
+ val newDctx = dctx.copy(tparams = dctx.tparams ++ tparamsMap, isProxy = isProxy(sym))
val oldCurrentFunDef = currentFunDef
@@ -780,7 +813,7 @@ trait CodeExtraction extends ASTExtractors {
*/
case ExVarDef(vs, tpt, bdy) => {
- val binderTpe = extractType(tpt.tpe)
+ val binderTpe = extractType(tpt)
val newID = FreshIdentifier(vs.name.toString).setType(binderTpe)
val valTree = extractTree(bdy)
@@ -834,8 +867,8 @@ trait CodeExtraction extends ASTExtractors {
w.invariant = Some(invTree)
w
- case epsi @ ExEpsilonExpression(tpe, varSym, predBody) =>
- val pstpe = extractType(tpe)
+ case epsi @ ExEpsilonExpression(tpt, varSym, predBody) =>
+ val pstpe = extractType(tpt)
val nctx = dctx.withNewVar(varSym -> (() => EpsilonVariable(epsi.pos).setType(pstpe)))
val c1 = extractTree(predBody)(nctx)
if(containsEpsilon(c1)) {
@@ -843,8 +876,8 @@ trait CodeExtraction extends ASTExtractors {
}
Epsilon(c1).setType(pstpe)
- case ExWaypointExpression(tpe, i, tree) =>
- val pstpe = extractType(tpe)
+ case ExWaypointExpression(tpt, i, tree) =>
+ val pstpe = extractType(tpt)
val IntLiteral(ri) = extractTree(i)
Waypoint(ri, extractTree(tree)).setType(pstpe)
@@ -896,15 +929,39 @@ trait CodeExtraction extends ASTExtractors {
outOfSubsetError(tr, "Unidentified variable "+sym+" "+sym.id+".")
}
- case chs @ ExHole(tpe) =>
- val cTpe = extractType(tpe)
- Hole().setType(cTpe).setPos(chs.pos)
+ case hole @ ExHoleExpression(tpt, exprs, os) =>
+ val leonTpe = extractType(tpt)
+ val leonExprs = exprs.map(extractTree)
+ val leonOracles = os.map(extractTree)
+
+ leonExprs match {
+ case Nil =>
+ Hole(leonOracles(0)).setType(leonTpe)
+
+ case List(e) =>
+ IfExpr(Hole(leonOracles(0)).setType(BooleanType), e, Hole(leonOracles(1)).setType(leonTpe))
+
+ case exs =>
+ val l = exs.last
+ var o = leonOracles(0)
+
+ def rightOf(o: LeonExpr): LeonExpr = {
+ val Some((cl, fd)) = libraryMethod("Oracle", "right")
+ MethodInvocation(o, cl, fd.typed(Nil), Nil)
+ }
+
+ exs.init.foldRight(l)({ (e: LeonExpr, r: LeonExpr) =>
+ val res = IfExpr(Hole(o).setType(BooleanType), e, r)
+ o = rightOf(o)
+ res
+ })
+ }
- case chs @ ExChooseExpression(args, tpe, body, select) =>
- val cTpe = extractType(tpe)
+ case chs @ ExChooseExpression(args, tpt, body, select) =>
+ val cTpe = extractType(tpt)
- val vars = args map { case (tpe, sym) =>
- val aTpe = extractType(tpe)
+ val vars = args map { case (tpt, sym) =>
+ val aTpe = extractType(tpt)
val newID = FreshIdentifier(sym.name.toString).setType(aTpe)
owners += (newID -> None)
newID
@@ -920,7 +977,7 @@ trait CodeExtraction extends ASTExtractors {
Choose(vars, cBody)
case ExCaseClassConstruction(tpt, args) =>
- extractType(tpt.tpe) match {
+ extractType(tpt) match {
case cct: CaseClassType =>
val nargs = args.map(extractTree(_))
CaseClass(cct, nargs)
@@ -963,31 +1020,31 @@ trait CodeExtraction extends ASTExtractors {
}
case ExFiniteSet(tt, args) =>
- val underlying = extractType(tt.tpe)
+ val underlying = extractType(tt)
FiniteSet(args.map(extractTree(_))).setType(SetType(underlying))
case ExFiniteMultiset(tt, args) =>
- val underlying = extractType(tt.tpe)
+ val underlying = extractType(tt)
FiniteMultiset(args.map(extractTree(_))).setType(MultisetType(underlying))
case ExEmptySet(tt) =>
- val underlying = extractType(tt.tpe)
+ val underlying = extractType(tt)
FiniteSet(Seq()).setType(SetType(underlying))
case ExEmptyMultiset(tt) =>
- val underlying = extractType(tt.tpe)
+ val underlying = extractType(tt)
EmptyMultiset(underlying).setType(MultisetType(underlying))
case ExEmptyMap(ft, tt) =>
- val fromUnderlying = extractType(ft.tpe)
- val toUnderlying = extractType(tt.tpe)
+ val fromUnderlying = extractType(ft)
+ val toUnderlying = extractType(tt)
val tpe = MapType(fromUnderlying, toUnderlying)
FiniteMap(Seq()).setType(tpe)
case ExLiteralMap(ft, tt, elems) =>
- val fromUnderlying = extractType(ft.tpe)
- val toUnderlying = extractType(tt.tpe)
+ val fromUnderlying = extractType(ft)
+ val toUnderlying = extractType(tt)
val tpe = MapType(fromUnderlying, toUnderlying)
val singletons: Seq[(LeonExpr, LeonExpr)] = elems.collect {
@@ -1002,7 +1059,7 @@ trait CodeExtraction extends ASTExtractors {
FiniteMap(singletons).setType(tpe)
case ExArrayFill(baseType, length, defaultValue) =>
- val underlying = extractType(baseType.tpe)
+ val underlying = extractType(baseType)
val lengthRec = extractTree(length)
val defaultValueRec = extractTree(defaultValue)
ArrayFill(lengthRec, defaultValueRec).setType(ArrayType(underlying))
@@ -1025,7 +1082,7 @@ trait CodeExtraction extends ASTExtractors {
case ExIsInstanceOf(tt, cc) => {
val ccRec = extractTree(cc)
- val checkType = extractType(tt.tpe)
+ val checkType = extractType(tt)
checkType match {
case cct @ CaseClassType(ccd, tps) => {
val rootType: LeonClassDef = if(ccd.parent != None) ccd.parent.get.classDef else ccd
@@ -1057,7 +1114,7 @@ trait CodeExtraction extends ASTExtractors {
MatchExpr(rs, rc).setType(rt)
case t: This =>
- extractType(t.tpe) match {
+ extractType(t) match {
case ct: ClassType =>
LeonThis(ct)
case _ =>
@@ -1085,7 +1142,7 @@ trait CodeExtraction extends ASTExtractors {
case (null, _, args) =>
val fd = getFunDef(sym, c.pos)
- val newTps = tps.map(t => extractType(t.tpe))
+ val newTps = tps.map(t => extractType(t))
FunctionInvocation(fd.typed(newTps), args).setType(fd.returnType)
@@ -1093,7 +1150,7 @@ trait CodeExtraction extends ASTExtractors {
val fd = getFunDef(sym, c.pos)
val cd = methodToClass(fd)
- val newTps = tps.map(t => extractType(t.tpe))
+ val newTps = tps.map(t => extractType(t))
MethodInvocation(rec, cd, fd.typed(newTps), args)
@@ -1188,7 +1245,11 @@ trait CodeExtraction extends ASTExtractors {
}
}
- private def extractType(tpt: Type)(implicit dctx: DefContext): LeonType = tpt match {
+ private def extractType(t: Tree)(implicit dctx: DefContext): LeonType = {
+ extractType(t.tpe)(dctx, t.pos)
+ }
+
+ private def extractType(tpt: Type)(implicit dctx: DefContext, pos: Position): LeonType = tpt match {
case tpe if tpe == IntClass.tpe =>
Int32Type
@@ -1225,6 +1286,9 @@ trait CodeExtraction extends ASTExtractors {
case TypeRef(_, sym, btt :: Nil) if isArrayClassSym(sym) =>
ArrayType(extractType(btt))
+ case TypeRef(_, sym, tps) if isByNameSym(sym) =>
+ extractType(tps.head)
+
case TypeRef(_, sym, tps) =>
val leontps = tps.map(extractType)
@@ -1232,19 +1296,43 @@ trait CodeExtraction extends ASTExtractors {
if(dctx.tparams contains sym) {
dctx.tparams(sym)
} else {
- outOfSubsetError(NoPosition, "Unknown type parameter "+sym)
+ outOfSubsetError(pos, "Unknown type parameter "+sym)
}
} else {
getClassType(sym, leontps)
}
case tt: ThisType =>
- val cd = getClassDef(tt.sym, NoPosition)
+ val cd = getClassDef(tt.sym, pos)
classDefToClassType(cd, cd.tparams.map(_.tp)) // Typed using own's type parameters
case SingleType(_, sym) =>
getClassType(sym.moduleClass, Nil)
+ case RefinedType(parents, defs) if defs.isEmpty =>
+ /**
+ * For cases like if(a) e1 else e2 where
+ * e1 <: C1,
+ * e2 <: C2,
+ * with C1,C2 <: C
+ *
+ * Scala might infer a type for C such as: Product with Serializable with C
+ * we generalize to the first known type, e.g. C.
+ */
+ parents.flatMap { ptpe =>
+ try {
+ Some(extractType(ptpe))
+ } catch {
+ case e: ImpureCodeEncounteredException =>
+ None
+ }}.headOption match {
+ case Some(tpe) =>
+ tpe
+
+ case None =>
+ outOfSubsetError(tpt.typeSymbol.pos, "Could not extract refined type as PureScala: "+tpt+" ("+tpt.getClass+")")
+ }
+
case _ =>
outOfSubsetError(tpt.typeSymbol.pos, "Could not extract type as PureScala: "+tpt+" ("+tpt.getClass+")")
}
diff --git a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
index cb771c9d2801ce88b3a6f74a3ab52cbbf0d4d471..f538a0d92df9272f925448e0687d115734a1f787 100644
--- a/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
+++ b/src/main/scala/leon/frontends/scalac/ExtractionPhase.scala
@@ -22,6 +22,7 @@ object ExtractionPhase extends LeonPhase[List[String], Program] {
val settings = new NSCSettings
settings.classpath.value = ctx.settings.classPath.mkString(":")
+ settings.usejavacp.value = false
settings.skip.value = List("patmat")
val libFiles = Settings.defaultLibFiles()
@@ -50,22 +51,10 @@ object ExtractionPhase extends LeonPhase[List[String], Program] {
val run = new compiler.Run
run.compile(command.files)
- (compiler.leonExtraction.units, compiler.leonExtraction.modules) match {
- case (Nil, Nil) =>
- ctx.reporter.fatalError("Error while compiling. Empty input?")
-
- case (_, Nil) =>
- ctx.reporter.fatalError("Error while compiling.")
-
- case (_, modules) =>
- if (ctx.reporter.errorCount > 0 && ctx.settings.strictCompilation) {
- ctx.reporter.fatalError("Error while compiling.")
- } else {
- val pgm = Program(FreshIdentifier("<program>"), modules)
- ctx.reporter.debug(pgm.asString(ctx))
- pgm
- }
- }
+
+ val pgm = Program(FreshIdentifier("<program>"), compiler.leonExtraction.modules)
+ ctx.reporter.debug(pgm.asString(ctx))
+ pgm
} else {
ctx.reporter.fatalError("No input program.")
}
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index a82ff2446f9976eec01a806f79f6f023f801c39c..ac99c1146633be43e695bd66e727a608588ed3eb 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -130,7 +130,7 @@ object Definitions {
knownChildren ++ (knownChildren.map(c => c match {
case acd: AbstractClassDef => acd.knownDescendents
case _ => Nil
- }).reduceLeft(_ ++ _))
+ }).foldLeft(List[ClassDef]())(_ ++ _))
}
def knownCCDescendents: Seq[CaseClassDef] = knownDescendents.collect {
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index b04aa62fc43b970a1b00e91042c476aae7045b2e..c8a1f666b4f462a05a61498d29151b9cf5038a78 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -126,10 +126,12 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
pp(t, p)
sb.append("._" + i)
- case h @ Hole() =>
+ case h @ Hole(o) =>
sb.append("???[")
pp(h.getType, p)
- sb.append("]")
+ sb.append("](")
+ pp(o, p)
+ sb.append(")")
case c@Choose(vars, pred) =>
sb.append("choose(")
@@ -329,7 +331,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
sb.append(")")
case WildcardPattern(None) => sb.append("_")
- case WildcardPattern(Some(id)) => pp(id, p)
+ case WildcardPattern(Some(id)) => pp(id.toVariable, p)
case InstanceOfPattern(bndr, cct) =>
bndr.foreach(b => sb.append(b + " : "))
pp(cct, p)
diff --git a/src/main/scala/leon/purescala/SimplifierWithPaths.scala b/src/main/scala/leon/purescala/SimplifierWithPaths.scala
index 70cc667a4e110841e04493bd2f66ba90f5471da3..406e4c46b546c7406c7a09531e65928297cdab63 100644
--- a/src/main/scala/leon/purescala/SimplifierWithPaths.scala
+++ b/src/main/scala/leon/purescala/SimplifierWithPaths.scala
@@ -69,7 +69,7 @@ class SimplifierWithPaths(sf: SolverFactory[Solver]) extends TransformerWithPC {
// unsupported for now
e
} else {
- MatchExpr(rs, cases.flatMap { c =>
+ val newCases = cases.flatMap { c =>
val patternExpr = conditionForPattern(rs, c.pattern, includeBinders = true)
if (stillPossible && !contradictedBy(patternExpr, path)) {
@@ -87,7 +87,12 @@ class SimplifierWithPaths(sf: SolverFactory[Solver]) extends TransformerWithPC {
} else {
None
}
- }).copiedFrom(e)
+ }
+ if (newCases.nonEmpty) {
+ MatchExpr(rs, newCases).copiedFrom(e)
+ } else {
+ Error("Unreachable code").copiedFrom(e)
+ }
}
case Or(es) =>
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 5a8eb39130e7af52913da44eb87d43865555a118..e68f47a488caaccf517876b76a01f28713b5d5cd 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -371,6 +371,58 @@ object TreeOps {
})(expr)
}
+ def normalizeExpression(expr: Expr) : Expr = {
+ def rec(e: Expr): Option[Expr] = e match {
+ case TupleSelect(Let(id, v, b), ts) =>
+ Some(Let(id, v, TupleSelect(b, ts)))
+
+ case TupleSelect(LetTuple(ids, v, b), ts) =>
+ Some(LetTuple(ids, v, TupleSelect(b, ts)))
+
+ case IfExpr(c, thenn, elze) if (thenn == elze) =>
+ Some(thenn)
+
+ case IfExpr(c, BooleanLiteral(true), BooleanLiteral(false)) =>
+ Some(c)
+
+ case IfExpr(Not(c), thenn, elze) =>
+ Some(IfExpr(c, elze, thenn).copiedFrom(e))
+
+ case IfExpr(c, BooleanLiteral(false), BooleanLiteral(true)) =>
+ Some(Not(c))
+
+ case FunctionInvocation(tfd, List(IfExpr(c, thenn, elze))) =>
+ Some(IfExpr(c, FunctionInvocation(tfd, List(thenn)), FunctionInvocation(tfd, List(elze))))
+
+ case _ =>
+ None
+ }
+
+ fixpoint(postMap(rec))(expr)
+ }
+
+
+ def evalGround(ctx: LeonContext, program: Program): Expr => Expr = {
+ import evaluators._
+
+ val eval = new DefaultEvaluator(ctx, program)
+
+ def isGround(e: Expr): Boolean = {
+ variablesOf(e).isEmpty && !usesHoles(e) && !containsChoose(e)
+ }
+
+ def rec(e: Expr): Option[Expr] = e match {
+ case l: Terminal => None
+ case e if isGround(e) => eval.eval(e) match {
+ case EvaluationResults.Successful(v) => Some(v)
+ case _ => None
+ }
+ case _ => None
+ }
+
+ preMap(rec)
+ }
+
/**
* Simplifies let expressions:
* - removes lets when expression never occurs
@@ -922,12 +974,12 @@ object TreeOps {
substMap += prefix -> Variable(binder)
substMap += CaseClassInstanceOf(ct, prefix) -> BooleanLiteral(true)
- val subconds = for (id <- ct.classDef.fieldsIds) yield {
- val fieldSel = CaseClassSelector(ct, prefix, id)
+ val subconds = for (f <- ct.fields) yield {
+ val fieldSel = CaseClassSelector(ct, prefix, f.id)
if (conditions contains fieldSel) {
computePatternFor(conditions(fieldSel), fieldSel)
} else {
- val b = FreshIdentifier(id.name, true).setType(id.getType)
+ val b = FreshIdentifier(f.id.name, true).setType(f.tpe)
substMap += fieldSel -> Variable(b)
WildcardPattern(Some(b))
}
@@ -1156,10 +1208,9 @@ object TreeOps {
case ft : FunctionType => None // FIXME
case a : AbstractClassType => None
- case c : CaseClassType =>
+ case cct : CaseClassType =>
// This is really just one big assertion. We don't rewrite class defs.
- val ccd = c.classDef
- val fieldTypes = ccd.fields.map(_.tpe)
+ val fieldTypes = cct.fields.map(_.tpe)
if(fieldTypes.exists(t => t match {
case TupleType(ts) if ts.size <= 1 => true
case _ => false
@@ -1246,13 +1297,45 @@ object TreeOps {
}
def containsChoose(e: Expr): Boolean = {
- simplePreTransform{
+ preTraversal{
case Choose(_, _) => return true
- case e => e
+ case _ =>
}(e)
false
}
+ def containsHoles(e: Expr): Boolean = {
+ preTraversal{
+ case Hole(_) => return true
+ case _ =>
+ }(e)
+ false
+ }
+
+ /**
+ * Returns true if the expression directly or indirectly relies on a Hole
+ */
+ def usesHoles(e: Expr): Boolean = {
+ var cache = Map[FunDef, Boolean]()
+
+ def callsHolesExpr(e: Expr): Boolean = {
+ containsHoles(e) || functionCallsOf(e).exists(fi => callsHoles(fi.tfd.fd))
+ }
+
+ def callsHoles(fd: FunDef): Boolean = cache.get(fd) match {
+ case Some(r) => r
+ case None =>
+ cache += fd -> false
+
+ val res = fd.body.map(callsHolesExpr _).getOrElse(false)
+
+ cache += fd -> res
+ res
+ }
+
+ callsHolesExpr(e)
+ }
+
/**
* Returns the value for an identifier given a model.
*/
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index a7a46e3c6e78dd647c33acdf815aa2e253abbbfd..b7624a842c5322fb1e482b0d0c5b849d94973d44 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -26,8 +26,6 @@ object Trees {
* the expected type. */
case class Error(description: String) extends Expr with Terminal
- case class Hole() extends Expr with Terminal
-
case class Choose(vars: List[Identifier], pred: Expr) extends Expr with FixedType with UnaryExtractable {
assert(!vars.isEmpty)
@@ -39,6 +37,13 @@ object Trees {
}
}
+ // A hole is like a all-seeing choose
+ case class Hole(oracle: Expr) extends Expr with UnaryExtractable {
+ def extract = {
+ Some((oracle, (o: Expr) => Hole(o).copiedFrom(this)))
+ }
+ }
+
/* Like vals */
case class Let(binder: Identifier, value: Expr, body: Expr) extends Expr with FixedType {
val fixedType = body.getType
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 35b50b8ee0d9e07925533f721fdf6d71de1e9f09..168b8e1936bd073f11ffc4506e919658963bc1b5 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -451,7 +451,7 @@ trait AbstractZ3Solver
case other =>
sorts.toZ3OrCompute(other) {
- reporter.warning("Resorting to uninterpreted type for : " + other)
+ reporter.warning(other.getPos, "Resorting to uninterpreted type for : " + other)
val symbol = z3.mkIntSymbol(nextIntForSymbol())
z3.mkUninterpretedSort(symbol)
}
@@ -638,8 +638,11 @@ trait AbstractZ3Solver
case gv @ GenericValue(tp, id) =>
z3.mkApp(genericValueToDecl(gv))
+ case h @ Hole(o) =>
+ rec(OracleTraverser(o, h.getType, program).value)
+
case _ => {
- reporter.warning("Can't handle this in translation to Z3: " + ex)
+ reporter.warning(ex.getPos, "Can't handle this in translation to Z3: " + ex)
throw new CantTranslateException
}
}
diff --git a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
index ad173d712c8ae9e711450a84c8ba01b5b0e90729..9fe4be2cc7b46e971b439766bf639f3c285afd4a 100644
--- a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
+++ b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
@@ -59,7 +59,7 @@ class FunctionTemplate private(
}
val asZ3Clauses: Seq[Z3AST] = asClauses.map {
- solver.toZ3Formula(_, idToZ3Ids).getOrElse(sys.error("Could not translate to z3. Did you forget --xlang?"))
+ cl => solver.toZ3Formula(cl, idToZ3Ids).getOrElse(sys.error("Could not translate to z3. Did you forget --xlang? @"+cl.getPos))
}
private val blockers : Map[Identifier,Set[FunctionInvocation]] = {
@@ -252,7 +252,6 @@ object FunctionTemplate {
val partitions = groupWhile((e: Expr) => !containsFunctionCalls(e), parts)
val ifExpr = partitions.map(Or(_)).reduceRight{ (a: Expr, b: Expr) => IfExpr(a, BooleanLiteral(true), b) }
-
rec(pathVar, ifExpr)
} else {
o
@@ -262,7 +261,7 @@ object FunctionTemplate {
}
case i @ IfExpr(cond, thenn, elze) => {
- if(!containsFunctionCalls(cond) && !containsFunctionCalls(thenn) && !containsFunctionCalls(elze)) {
+ if(!containsFunctionCalls(i)) {
i
} else {
val newBool1 : Identifier = FreshIdentifier("b", true).setType(BooleanType)
diff --git a/src/main/scala/leon/synthesis/BoundedSearch.scala b/src/main/scala/leon/synthesis/BoundedSearch.scala
index 41bc868940f69648a4153c1bc20beae16d6d91f9..5430d05d267f05dc0b7a0d2a02abeaa39432a893 100644
--- a/src/main/scala/leon/synthesis/BoundedSearch.scala
+++ b/src/main/scala/leon/synthesis/BoundedSearch.scala
@@ -5,12 +5,11 @@ package synthesis
class BoundedSearch(synth: Synthesizer,
problem: Problem,
- rules: Seq[Rule],
costModel: CostModel,
- searchBound: Int) extends SimpleSearch(synth, problem, rules, costModel) {
+ searchBound: Int) extends SimpleSearch(synth, problem, costModel) {
def this(synth: Synthesizer, problem: Problem, searchBound: Int) = {
- this(synth, problem, synth.rules, synth.options.costModel, searchBound)
+ this(synth, problem, synth.options.costModel, searchBound)
}
override def searchStep() {
diff --git a/src/main/scala/leon/synthesis/ChooseInfo.scala b/src/main/scala/leon/synthesis/ChooseInfo.scala
index 2295ff3dcb2330feee96a3da04a064821dcdc05b..85f51ee663fb940d036594eb80f040c483b721fc 100644
--- a/src/main/scala/leon/synthesis/ChooseInfo.scala
+++ b/src/main/scala/leon/synthesis/ChooseInfo.scala
@@ -3,14 +3,16 @@
package leon
package synthesis
+import purescala.Common._
import purescala.Definitions._
import purescala.Trees._
-import purescala.TreeOps.ChooseCollectorWithPaths
+import purescala.TreeOps._
case class ChooseInfo(ctx: LeonContext,
prog: Program,
fd: FunDef,
pc: Expr,
+ source: Expr,
ch: Choose,
options: SynthesisOptions) {
@@ -25,14 +27,34 @@ object ChooseInfo {
var results = List[ChooseInfo]()
// Look for choose()
- for (f <- prog.definedFunctions.sortBy(_.id.toString) if f.body.isDefined) {
+ for (f <- prog.definedFunctions if f.body.isDefined) {
val actualBody = And(f.precondition.getOrElse(BooleanLiteral(true)), f.body.get)
for ((ch, path) <- new ChooseCollectorWithPaths().traverse(actualBody)) {
- results = ChooseInfo(ctx, prog, f, path, ch, options) :: results
+ results = ChooseInfo(ctx, prog, f, path, ch, ch, options) :: results
}
}
- results.reverse
+
+ if (options.allSeeing) {
+ // Functions that call holes are also considered for (all-seeing) synthesis
+
+ val holesFd = prog.definedFunctions.filter(fd => fd.hasBody && containsHoles(fd.body.get)).toSet
+
+ val callers = prog.callGraph.transitiveCallers(holesFd) ++ holesFd
+
+ for (f <- callers if f.hasPostcondition && f.hasBody) {
+ val path = f.precondition.getOrElse(BooleanLiteral(true))
+
+ val x = FreshIdentifier("x", true).setType(f.returnType)
+ val (pid, pex) = f.postcondition.get
+
+ val ch = Choose(List(x), And(Equals(x.toVariable, f.body.get), replaceFromIDs(Map(pid -> x.toVariable), pex)))
+
+ results = ChooseInfo(ctx, prog, f, path, f.body.get, ch, options) :: results
+ }
+ }
+
+ results.sortBy(_.fd.id.toString)
}
}
diff --git a/src/main/scala/leon/synthesis/ConvertHoles.scala b/src/main/scala/leon/synthesis/ConvertHoles.scala
deleted file mode 100644
index 57cc7bf5993b6ec23fdbfe5439cf06d1083e9133..0000000000000000000000000000000000000000
--- a/src/main/scala/leon/synthesis/ConvertHoles.scala
+++ /dev/null
@@ -1,101 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-package leon
-package synthesis
-
-import purescala.Common._
-import purescala.Trees._
-import purescala.TreeOps._
-import purescala.Definitions._
-
-object ConvertHoles extends LeonPhase[Program, Program] {
- val name = "Convert Holes to Choose"
- val description = "Convert holes found in bodies to equivalent Choose"
-
- /**
- * This phase converts a body with "holes" into a choose construct:
- *
- * def foo(a: T) {
- * require(..a..)
- * expr(???, ???)
- * } ensuring { res =>
- * pred(res)
- * }
- *
- * gets converted into:
- *
- * def foo(a: T) {
- * require(..a..)
- * choose { (c1, c2) => {
- * val res = expr(c1, c2)
- * pred(res)
- * }
- * } ensuring { res =>
- * pred(res)
- * }
- *
- */
- def run(ctx: LeonContext)(pgm: Program): Program = {
- pgm.definedFunctions.foreach(fd => {
- if (fd.hasPostcondition && fd.hasBody) {
- var holes = List[Identifier]()
- val body = preMap {
- case h @ Hole() =>
- val id = FreshIdentifier("c", true).copiedFrom(h)
- holes ::= id
-
- Some(id.toVariable)
- case _ => None
- }(fd.body.get)
-
- holes = holes.reverse
-
- if (holes.nonEmpty) {
- val res = FreshIdentifier("b", true).copiedFrom(body)
- val (pid, pbody) = fd.postcondition.get
-
- val c = Choose(holes, Let(res, body, replaceFromIDs(Map(pid -> res.toVariable), pbody)))
-
- if (holes.size > 1) {
- val newHoles = holes.map(_.freshen)
- fd.body = Some(LetTuple(newHoles, c.setPos(body), replaceFromIDs((holes zip newHoles.map(_.toVariable)).toMap, body)).setPos(body))
- } else {
- fd.body = Some(preMap {
- case h @ Hole() => Some(c.setPos(h))
- case _ => None
- }(fd.body.get))
- }
- }
- } else {
- // No post-condition: we replace holes with local-chooses without
- // predicates
- fd.body = fd.body.map { preMap {
- case h @ Hole() =>
- val id = FreshIdentifier("c", true).copiedFrom(h)
- Some(Choose(List(id), BooleanLiteral(true)).copiedFrom(h))
- case _ => None
- } }
- }
-
- // Ensure that holes are not found in pre and/or post conditions
- fd.precondition.foreach {
- preTraversal{
- case Hole() =>
- ctx.reporter.error("Hole expressions are not supported in preconditions. (function "+fd.id.asString(ctx)+")")
- case _ =>
- }
- }
-
- fd.postcondition.foreach { case (id, post) =>
- preTraversal{
- case Hole() =>
- ctx.reporter.error("Hole expressions are not supported in postconditions. (function "+fd.id.asString(ctx)+")")
- case _ =>
- }(post)
- }
-
- })
-
- pgm
- }
-}
diff --git a/src/main/scala/leon/synthesis/CostModel.scala b/src/main/scala/leon/synthesis/CostModel.scala
index 75bdb7f4a5eb9711fc97082c12c93a64debfd784..85e5285eedd9e14f5d28042949df8db62fb40b8d 100644
--- a/src/main/scala/leon/synthesis/CostModel.scala
+++ b/src/main/scala/leon/synthesis/CostModel.scala
@@ -97,7 +97,13 @@ case object WeightedBranchesCostModel extends CostModel("WeightedBranches") {
}
def problemCost(p: Problem): Cost = new Cost {
- val value = p.xs.size
+ val value = {
+ if (usesHoles(p.phi)) {
+ p.xs.size + 50
+ } else {
+ p.xs.size
+ }
+ }
}
}
diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index d48e943858b05dee13c1571a0adb48da99cd1a4b..5c3fe9a07879bb8aff23688af298cda1ad0373e8 100644
--- a/src/main/scala/leon/synthesis/Heuristics.scala
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -25,34 +25,3 @@ trait Heuristic {
override def toString = "H: "+name
}
-
-object HeuristicInstantiation {
- def verifyPre(sctx: SynthesisContext, problem: Problem)(s: Solution): Option[Solution] = {
- //sctx.solver.solveSAT(And(Not(s.pre), problem.phi)) match {
- // case (Some(true), model) =>
- // sctx.reporter.warning("Heuristic failed to produce weakest precondition:")
- // sctx.reporter.warning(" - problem: "+problem)
- // sctx.reporter.warning(" - precondition: "+s.pre)
- // None
- // case _ =>
- // Some(s)
- //}
-
- Some(s)
- }
-
- def apply(problem: Problem, rule: Rule, subProblems: List[Problem], onSuccess: List[Solution] => Option[Solution], description: String): RuleInstantiation = {
- val subTypes = subProblems.map(p => TupleType(p.xs.map(_.getType)))
-
- val builder = new SolutionBuilder(subProblems.size, subTypes) {
- def apply(sols: List[Solution]) = {
- onSuccess(sols)
- }
- }
-
- new RuleInstantiation(problem, rule, builder, description) {
- def apply(sctx: SynthesisContext) = RuleDecomposed(subProblems)
-
- }
- }
-}
diff --git a/src/main/scala/leon/synthesis/ManualSearch.scala b/src/main/scala/leon/synthesis/ManualSearch.scala
index 5964eadc435c709453f22e236256aa2cd6d82d92..137d79c6828e0599cdc71ec830d72c764e2bb555 100644
--- a/src/main/scala/leon/synthesis/ManualSearch.scala
+++ b/src/main/scala/leon/synthesis/ManualSearch.scala
@@ -7,11 +7,10 @@ import leon.purescala.ScalaPrinter
class ManualSearch(synth: Synthesizer,
problem: Problem,
- rules: Seq[Rule],
- costModel: CostModel) extends SimpleSearch(synth, problem, rules, costModel) {
+ costModel: CostModel) extends SimpleSearch(synth, problem, costModel) {
def this(synth: Synthesizer, problem: Problem) = {
- this(synth, problem, synth.rules, synth.options.costModel)
+ this(synth, problem, synth.options.costModel)
}
import synth.reporter._
@@ -33,24 +32,32 @@ class ManualSearch(synth: Synthesizer,
def failed(str: String) = "\033[31m"+str+"\033[0m"
def solved(str: String) = "\033[32m"+str+"\033[0m"
+ def displayApp(app: RuleInstantiation): String = {
+ f"(${costModel.ruleAppCost(app).value}%3d) $app"
+ }
+
+ def displayProb(p: Problem): String = {
+ f"(${costModel.problemCost(p).value}%3d) $p"
+ }
+
def traversePathFrom(n: g.Tree, prefix: List[Int]) {
n match {
case l: g.AndLeaf =>
if (prefix.endsWith(cd.reverse)) {
- println(pathToString(prefix)+" \u2508 "+l.task.app)
+ println(pathToString(prefix)+" \u2508 "+displayApp(l.task.app))
}
case l: g.OrLeaf =>
if (prefix.endsWith(cd.reverse)) {
- println(pathToString(prefix)+" \u2508 "+l.task.p)
+ println(pathToString(prefix)+" \u2508 "+displayProb(l.task.p))
}
case an: g.AndNode =>
if (an.isSolved) {
if (prefix.endsWith(cd.reverse)) {
- println(solved(pathToString(prefix)+" \u2508 "+an.task.app))
+ println(solved(pathToString(prefix)+" \u2508 "+displayApp(an.task.app)))
}
} else {
if (prefix.endsWith(cd.reverse)) {
- println(title(pathToString(prefix)+" \u2510 "+an.task.app))
+ println(title(pathToString(prefix)+" \u2510 "+displayApp(an.task.app)))
}
for ((st, i) <- an.subTasks.zipWithIndex) {
traversePathFrom(an.subProblems(st), i :: prefix)
@@ -64,12 +71,12 @@ class ManualSearch(synth: Synthesizer,
}
} else {
if (prefix.endsWith(cd.reverse)) {
- println(title(pathToString(prefix)+" \u2510 "+on.task.p))
+ println(title(pathToString(prefix)+" \u2510 "+displayProb(on.task.p)))
}
for ((at, i) <- on.altTasks.zipWithIndex) {
if (on.triedAlternatives contains at) {
if (prefix.endsWith(cd.reverse)) {
- println(failed(pathToString(i :: prefix)+" \u2508 "+at.app))
+ println(failed(pathToString(i :: prefix)+" \u2508 "+displayApp(at.app)))
}
} else {
traversePathFrom(on.alternatives(at), i :: prefix)
diff --git a/src/main/scala/leon/synthesis/ParallelSearch.scala b/src/main/scala/leon/synthesis/ParallelSearch.scala
index e8eb0fbceba24f02e6afa15c15b5ec8bc394598b..b0af9cab8dbefab2ca3563ce9bd29b4de16f5525 100644
--- a/src/main/scala/leon/synthesis/ParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/ParallelSearch.scala
@@ -9,12 +9,11 @@ import solvers.z3._
class ParallelSearch(synth: Synthesizer,
problem: Problem,
- rules: Seq[Rule],
costModel: CostModel,
nWorkers: Int) extends AndOrGraphParallelSearch[SynthesisContext, TaskRunRule, TaskTryRules, Solution](new AndOrGraph(TaskTryRules(problem), SearchCostModel(costModel)), nWorkers) {
def this(synth: Synthesizer, problem: Problem, nWorkers: Int) = {
- this(synth, problem, synth.rules, synth.options.costModel, nWorkers)
+ this(synth, problem, synth.options.costModel, nWorkers)
}
import synth.reporter._
@@ -60,22 +59,12 @@ class ParallelSearch(synth: Synthesizer,
}
def expandOrTask(ref: ActorRef, sctx: SynthesisContext)(t: TaskTryRules) = {
- val (normRules, otherRules) = rules.partition(_.isInstanceOf[NormalizingRule])
+ val apps = Rules.getInstantiations(sctx, t.p)
- val normApplications = normRules.flatMap(_.instantiateOn(sctx, t.p))
-
- if (!normApplications.isEmpty) {
- Expanded(List(TaskRunRule(normApplications.head)))
+ if (apps.nonEmpty) {
+ Expanded(apps.map(TaskRunRule(_)))
} else {
- val sub = otherRules.flatMap { r =>
- r.instantiateOn(sctx, t.p).map(TaskRunRule(_))
- }
-
- if (!sub.isEmpty) {
- Expanded(sub.toList)
- } else {
- ExpandFailure()
- }
+ ExpandFailure()
}
}
}
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 9fd44cb0f1993ce8576c147c85b890f3767fab4a..aa79a14703d0da8a278dca069b1aeed835cb79d4 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -29,9 +29,25 @@ object Rules {
DetupleOutput,
DetupleInput,
ADTSplit,
+ InlineHoles,
IntegerEquation,
- IntegerInequalities
+ IntegerInequalities,
+ AngelicHoles
)
+
+ def getInstantiations(sctx: SynthesisContext, problem: Problem) = {
+ val sub = sctx.rules.flatMap { r =>
+ r.instantiateOn(sctx, problem)
+ }
+
+ val res = sub.groupBy(_.priority).toSeq.sortBy(_._1)
+
+ if (res.nonEmpty) {
+ res.head._2.toList
+ } else {
+ Nil
+ }
+ }
}
abstract class SolutionBuilder(val arity: Int, val types: Seq[TypeTree]) {
@@ -53,7 +69,13 @@ object SolutionBuilder {
}
}
-abstract class RuleInstantiation(val problem: Problem, val rule: Rule, val onSuccess: SolutionBuilder, val description: String) {
+abstract class RuleInstantiation(
+ val problem: Problem,
+ val rule: Rule,
+ val onSuccess: SolutionBuilder,
+ val description: String,
+ val priority: RulePriority) {
+
def apply(sctx: SynthesisContext): RuleApplicationResult
override def toString = description
@@ -64,17 +86,56 @@ case class RuleSuccess(solution: Solution, isTrusted: Boolean = true) extends R
case class RuleDecomposed(sub: List[Problem]) extends RuleApplicationResult
case object RuleApplicationImpossible extends RuleApplicationResult
+sealed abstract class RulePriority(val v: Int) extends Ordered[RulePriority] {
+ def compare(that: RulePriority) = this.v - that.v
+}
+
+case object RulePriorityDefault extends RulePriority(2)
+case object RulePriorityNormalizing extends RulePriority(0)
+case object RulePriorityHoles extends RulePriority(1)
+
object RuleInstantiation {
- def immediateDecomp(problem: Problem, rule: Rule, sub: List[Problem], onSuccess: List[Solution] => Option[Solution], description: String) = {
+ def immediateDecomp(problem: Problem,
+ rule: Rule,
+ sub: List[Problem],
+ onSuccess: List[Solution] => Option[Solution]): RuleInstantiation = {
+
+ immediateDecomp(problem, rule, sub, onSuccess, rule.name, rule.priority)
+ }
+
+ def immediateDecomp(problem: Problem,
+ rule: Rule,
+ sub: List[Problem],
+ onSuccess: List[Solution] => Option[Solution],
+ description: String): RuleInstantiation = {
+ immediateDecomp(problem, rule, sub, onSuccess, description, rule.priority)
+ }
+
+ def immediateDecomp(problem: Problem,
+ rule: Rule,
+ sub: List[Problem],
+ onSuccess: List[Solution] => Option[Solution],
+ description: String,
+ priority: RulePriority): RuleInstantiation = {
val subTypes = sub.map(p => TupleType(p.xs.map(_.getType)))
- new RuleInstantiation(problem, rule, new SolutionCombiner(sub.size, subTypes, onSuccess), description) {
+ new RuleInstantiation(problem, rule, new SolutionCombiner(sub.size, subTypes, onSuccess), description, priority) {
def apply(sctx: SynthesisContext) = RuleDecomposed(sub)
}
}
- def immediateSuccess(problem: Problem, rule: Rule, solution: Solution) = {
- new RuleInstantiation(problem, rule, new SolutionCombiner(0, Seq(), ls => Some(solution)), "Solve with "+solution) {
+ def immediateSuccess(problem: Problem,
+ rule: Rule,
+ solution: Solution): RuleInstantiation = {
+ immediateSuccess(problem, rule, solution, rule.priority)
+
+ }
+
+ def immediateSuccess(problem: Problem,
+ rule: Rule,
+ solution: Solution,
+ priority: RulePriority): RuleInstantiation = {
+ new RuleInstantiation(problem, rule, new SolutionCombiner(0, Seq(), ls => Some(solution)), "Solve with "+solution, priority) {
def apply(sctx: SynthesisContext) = RuleSuccess(solution)
}
}
@@ -83,6 +144,8 @@ object RuleInstantiation {
abstract class Rule(val name: String) {
def instantiateOn(sctx: SynthesisContext, problem: Problem): Traversable[RuleInstantiation]
+ val priority: RulePriority = RulePriorityDefault
+
def subst(what: Tuple2[Identifier, Expr], in: Expr): Expr = replace(Map(Variable(what._1) -> what._2), in)
def substAll(what: Map[Identifier, Expr], in: Expr): Expr = replace(what.map(w => Variable(w._1) -> w._2), in)
@@ -95,12 +158,21 @@ abstract class Rule(val name: String) {
None
}
+ def project(firstN: Int): List[Solution] => Option[Solution] = {
+ project(0 until firstN)
+ }
+
+
+ def project(ids: Seq[Int]): List[Solution] => Option[Solution] = {
+ case List(s) =>
+ Some(s.project(ids))
+ case _ =>
+ None
+ }
+
override def toString = "R: "+name
}
-// Note: Rules that extend NormalizingRule should all be commutative, The will
-// be applied before others in a deterministic order and their application
-// should never fail!
abstract class NormalizingRule(name: String) extends Rule(name) {
- override def toString = "N: "+name
+ override val priority = RulePriorityNormalizing
}
diff --git a/src/main/scala/leon/synthesis/SimpleSearch.scala b/src/main/scala/leon/synthesis/SimpleSearch.scala
index 491188cef28637f240250195fd4d23e4793c3ec3..b069a1c738c1f6ae6deb331e4aed36b51f9e41ae 100644
--- a/src/main/scala/leon/synthesis/SimpleSearch.scala
+++ b/src/main/scala/leon/synthesis/SimpleSearch.scala
@@ -9,11 +9,10 @@ import synthesis.search._
class SimpleSearch(synth: Synthesizer,
problem: Problem,
- rules: Seq[Rule],
costModel: CostModel) extends AndOrGraphSearch[TaskRunRule, TaskTryRules, Solution](new AndOrGraph(TaskTryRules(problem), SearchCostModel(costModel))) with Interruptible {
def this(synth: Synthesizer, problem: Problem) = {
- this(synth, problem, synth.rules, synth.options.costModel)
+ this(synth, problem, synth.options.costModel)
}
import synth.reporter._
@@ -45,22 +44,12 @@ class SimpleSearch(synth: Synthesizer,
}
def expandOrTask(t: TaskTryRules): ExpandResult[TaskRunRule] = {
- val (normRules, otherRules) = rules.partition(_.isInstanceOf[NormalizingRule])
+ val apps = Rules.getInstantiations(sctx, t.p)
- val normApplications = normRules.flatMap(_.instantiateOn(sctx, t.p))
-
- if (!normApplications.isEmpty) {
- Expanded(List(TaskRunRule(normApplications.head)))
+ if (apps.nonEmpty) {
+ Expanded(apps.map(TaskRunRule(_)))
} else {
- val sub = otherRules.flatMap { r =>
- r.instantiateOn(sctx, t.p).map(TaskRunRule(_))
- }
-
- if (!sub.isEmpty) {
- Expanded(sub.toList)
- } else {
- ExpandFailure()
- }
+ ExpandFailure()
}
}
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index ef04d34b88069112b3251cb98b44287836c71fa2..c504eadacb8c59f05153ff587f6dd0300225f99f 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -3,6 +3,7 @@
package leon
package synthesis
+import purescala.Common._
import purescala.Trees._
import purescala.TypeTrees.{TypeTree,TupleType}
import purescala.Definitions._
@@ -28,6 +29,20 @@ class Solution(val pre: Expr, val defs: Set[FunDef], val term: Expr) {
defs.foldLeft(result){ case (t, fd) => LetDef(fd, t) }
}
+ // Projects a solution (ignore several output variables)
+ //
+ // e.g. Given solution for [[ a < .. > x1, x2, x3, x4 ]] and List(0, 1, 3)
+ // It produces a solution for [[ a < .. > x1, x2, x4 ]]
+ //
+ // Indices are 0-indexed
+ def project(indices: Seq[Int]): Solution = {
+ val t = FreshIdentifier("t", true).setType(term.getType)
+ val newTerm = Let(t, term, Tuple(indices.map(i => TupleSelect(t.toVariable, i+1))))
+
+ Solution(pre, defs, newTerm)
+ }
+
+
def fullTerm =
defs.foldLeft(term){ case (t, fd) => LetDef(fd, t) }
@@ -41,13 +56,22 @@ class Solution(val pre: Expr, val defs: Set[FunDef], val term: Expr) {
matchToIfThenElse _,
simplifyPaths(uninterpretedZ3)(_),
patternMatchReconstruction _,
- simplifyTautologies(uninterpretedZ3)(_),
- simplifyLets _,
rewriteTuples _,
- (new ScopeSimplifier).transform _
+ evalGround(ctx, p),
+ normalizeExpression _
)
- simplifiers.foldLeft(toExpr){ (x, sim) => sim(x) }
+ val simple = { expr: Expr =>
+ simplifiers.foldLeft(expr){ case (x, sim) =>
+ sim(x)
+ }
+ }
+
+ // Simplify first using stable simplifiers
+ val s = fixpoint(simple)(toExpr)
+
+ // Clean up ids/names
+ (new ScopeSimplifier).transform(s)
}
}
diff --git a/src/main/scala/leon/synthesis/SynthesisContext.scala b/src/main/scala/leon/synthesis/SynthesisContext.scala
index b699c8bc8a3d7bfe09f5193d28d0c77c8449cc53..47bac75591896c4410edcf5b46f608fa485b4ccb 100644
--- a/src/main/scala/leon/synthesis/SynthesisContext.scala
+++ b/src/main/scala/leon/synthesis/SynthesisContext.scala
@@ -21,6 +21,8 @@ case class SynthesisContext(
reporter: Reporter
) {
+ val rules = options.rules
+
val allSolvers: Map[String, SolverFactory[SynthesisContext.SynthesisSolver]] = Map(
"fairz3" -> SolverFactory(() => new FairZ3Solver(context, program) with TimeoutAssumptionSolver),
"enum" -> SolverFactory(() => new EnumerationSolver(context, program) with TimeoutAssumptionSolver)
diff --git a/src/main/scala/leon/synthesis/SynthesisOptions.scala b/src/main/scala/leon/synthesis/SynthesisOptions.scala
index 90f0e3c84a39604b970f1af8e1dfaceea8dadb8b..706fc69fff03d9cd600ad88c9739029346f70eb5 100644
--- a/src/main/scala/leon/synthesis/SynthesisOptions.scala
+++ b/src/main/scala/leon/synthesis/SynthesisOptions.scala
@@ -5,6 +5,7 @@ package synthesis
case class SynthesisOptions(
inPlace: Boolean = false,
+ allSeeing: Boolean = false,
generateDerivationTrees: Boolean = false,
filterFuns: Option[Set[String]] = None,
searchWorkers: Int = 1,
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 98e8a8d6e358a35dbe8fea3ca4b3e5095ccf6066..e68dbf292e97d34d3f971753d8554ec894e236ca 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -17,6 +17,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
override val definedOptions : Set[LeonOptionDef] = Set(
LeonFlagOptionDef( "inplace", "--inplace", "Debug level"),
+ LeonFlagOptionDef( "allseeing", "--allseeing", "Also synthesize functions using holes"),
LeonValueOptionDef("parallel", "--parallel[=N]", "Parallel synthesis search using N workers", Some("5")),
LeonFlagOptionDef( "manual", "--manual", "Manual search"),
LeonFlagOptionDef( "derivtrees", "--derivtrees", "Generate derivation trees"),
@@ -43,6 +44,9 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
case LeonFlagOption("manual", v) =>
options = options.copy(manualSearch = v)
+ case LeonFlagOption("allseeing", v) =>
+ options = options.copy(allSeeing = v)
+
case LeonFlagOption("inplace", v) =>
options = options.copy(inPlace = v)
@@ -122,11 +126,16 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
def run(ctx: LeonContext)(p: Program): Program = {
val options = processOptions(ctx)
- def toProcess(ci: ChooseInfo) = {
- options.filterFuns.isEmpty || options.filterFuns.get.contains(ci.fd.id.toString)
+ def excludeByDefault(fd: FunDef): Boolean = (fd.annotations contains "library")
+
+ val fdFilter = {
+ import OptionsHelpers._
+ val ciTofd = { (ci: ChooseInfo) => ci.fd }
+
+ filterInclusive(options.filterFuns.map(fdMatcher), Some(excludeByDefault _)) compose ciTofd
}
- var chooses = ChooseInfo.extractFromProgram(ctx, p, options).filter(toProcess)
+ var chooses = ChooseInfo.extractFromProgram(ctx, p, options).filter(fdFilter)
var functions = Set[FunDef]()
@@ -136,7 +145,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
val fd = ci.fd
val expr = sol.toSimplifiedExpr(ctx, p)
- fd.body = fd.body.map(b => replace(Map(ci.ch -> expr), b))
+ fd.body = fd.body.map(b => replace(Map(ci.source -> expr), b))
functions += fd
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 11189cefc3e67c0512aeacbbf3cfde55789be084..483dc9b36556630c3c2111fa1cb95297011c0d38 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -23,8 +23,6 @@ class Synthesizer(val context : LeonContext,
val problem: Problem,
val options: SynthesisOptions) {
- val rules: Seq[Rule] = options.rules
-
val reporter = context.reporter
def synthesize(): (Solution, Boolean) = {
@@ -84,7 +82,7 @@ class Synthesizer(val context : LeonContext,
val solverf = SolverFactory(() => (new FairZ3Solver(context, npr) with TimeoutSolver).setTimeout(timeoutMs))
val vctx = VerificationContext(context, npr, solverf, context.reporter)
- val vcs = generateVerificationConditions(vctx, fds.map(_.id.name))
+ val vcs = generateVerificationConditions(vctx, Some(fds.map(_.id.name).toSeq))
val vcreport = checkVerificationConditions(vctx, vcs)
if (vcreport.totalValid == vcreport.totalConditions) {
diff --git a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
index f3136fbbb17f089e96b37f2d689d1461736772e3..87e4b14c854ce1ed66fe7aeceb5788da89ae24ee 100644
--- a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
@@ -110,7 +110,7 @@ case object ADTInduction extends Rule("ADT Induction") with Heuristic {
}
}
- Some(HeuristicInstantiation(p, this, subProblemsInfo.map(_._1).toList, onSuccess, "ADT Induction on '"+origId+"'"))
+ Some(RuleInstantiation.immediateDecomp(p, this, subProblemsInfo.map(_._1).toList, onSuccess, "ADT Induction on '"+origId+"'"))
} else {
None
}
diff --git a/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala
index 5ab3f672b446c656feadaa10e3a2504bbd1caa11..9c29ec85972fdf2ba7ed6257a1b5c49251b5d19b 100644
--- a/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala
@@ -71,7 +71,7 @@ case object ADTLongInduction extends Rule("ADT Long Induction") with Heuristic {
val newIds = ids.filterNot(_ == id) ++ subIds
val newCalls = if (!subIds.isEmpty) {
- List(subIds.find(isRec).get)
+ List(subIds.find(isRec)).flatten
} else {
List()
}
@@ -159,7 +159,7 @@ case object ADTLongInduction extends Rule("ADT Long Induction") with Heuristic {
}
}
- Some(HeuristicInstantiation(p, this, subProblemsInfo.map(_._1).toList, onSuccess, "ADT Long Induction on '"+origId+"'"))
+ Some(RuleInstantiation.immediateDecomp(p, this, subProblemsInfo.map(_._1).toList, onSuccess, "ADT Long Induction on '"+origId+"'"))
} else {
None
}
diff --git a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
index ac01105b49d103fd2c36b6a6435eb2dcb945fb88..37cf77a0ba97c679144b62a74482d4dbb1d0c759 100644
--- a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
@@ -65,7 +65,7 @@ case object IntInduction extends Rule("Int Induction") with Heuristic {
None
}
- Some(HeuristicInstantiation(p, this, List(subBase, subGT, subLT), onSuccess, "Int Induction on '"+origId+"'"))
+ Some(RuleInstantiation.immediateDecomp(p, this, List(subBase, subGT, subLT), onSuccess, "Int Induction on '"+origId+"'"))
case _ =>
None
}
diff --git a/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala b/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
index e33c3eee397b4a28f5a5a833bf1fca79ee6ae67b..7cd1e2342ad8d3c71271961aa9676ef4cd548f16 100644
--- a/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
+++ b/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
@@ -38,7 +38,7 @@ case object OptimisticInjection extends Rule("Opt. Injection") with Heuristic {
val sub = p.copy(phi = And(newExprs))
- Some(HeuristicInstantiation(p, this, List(sub), forward, this.name))
+ Some(RuleInstantiation.immediateDecomp(p, this, List(sub), forward))
} else {
None
}
diff --git a/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala b/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
index 3de094c8c11a589e4e0fae9c90ffcb8cdc1882e8..dc7bf0526ddcfc5e4409edf81e241aea6548c141 100644
--- a/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
+++ b/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
@@ -38,7 +38,7 @@ case object SelectiveInlining extends Rule("Sel. Inlining") with Heuristic {
val sub = p.copy(phi = And(newExprs))
- Some(HeuristicInstantiation(p, this, List(sub), forward, this.name))
+ Some(RuleInstantiation.immediateDecomp(p, this, List(sub), forward))
} else {
None
}
diff --git a/src/main/scala/leon/synthesis/rules/AngelicHoles.scala b/src/main/scala/leon/synthesis/rules/AngelicHoles.scala
new file mode 100644
index 0000000000000000000000000000000000000000..07c5f687fb9a16a9c825995d07c84cc7a93aa7c8
--- /dev/null
+++ b/src/main/scala/leon/synthesis/rules/AngelicHoles.scala
@@ -0,0 +1,50 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon
+package synthesis
+package rules
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.TreeOps._
+import purescala.TypeTrees._
+import purescala.Extractors._
+
+// Synthesizing a function with Hole is actually synthesizing an Oracle, so Oracle becomes output:
+// [[ a,o < Phi(a,o,x) > x ]] ---> [[ a < Phi(a,o,x) > x, o ]]
+case object AngelicHoles extends NormalizingRule("Angelic Holes") {
+ def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
+ val oracleClass = sctx.program.definedClasses.find(_.id.name == "Oracle").getOrElse {
+ sctx.reporter.fatalError("Can't find Oracle class")
+ }
+
+ def isOracle(i: Identifier) = {
+ i.getType match {
+ case AbstractClassType(acd, _) if acd == oracleClass => true
+ case _ => false
+ }
+ }
+
+ if (usesHoles(p.phi)) {
+ val (oracles, as) = p.as.partition(isOracle)
+
+ if (oracles.nonEmpty) {
+ val sub = p.copy(as = as, xs = p.xs ++ oracles)
+ List(RuleInstantiation.immediateDecomp(p, this, List(sub), {
+ case List(s) =>
+ // We ignore the last output params that are oracles
+ Some(s.project(0 until p.xs.size))
+
+ case _ =>
+ None
+ }, "Hole Semantics"))
+ } else {
+ Nil
+ }
+ } else {
+ Nil
+ }
+ }
+}
+
diff --git a/src/main/scala/leon/synthesis/rules/AsChoose.scala b/src/main/scala/leon/synthesis/rules/AsChoose.scala
index 5aefa03dcb8ea9083bc7c5f647ad2198ade18b65..fc43972f0ac5eefb48d858b877b8a17924c14d1a 100644
--- a/src/main/scala/leon/synthesis/rules/AsChoose.scala
+++ b/src/main/scala/leon/synthesis/rules/AsChoose.scala
@@ -6,7 +6,7 @@ package rules
case object AsChoose extends Rule("As Choose") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
- Some(new RuleInstantiation(p, this, SolutionBuilder.none, this.name) {
+ Some(new RuleInstantiation(p, this, SolutionBuilder.none, this.name, this.priority) {
def apply(sctx: SynthesisContext) = {
RuleSuccess(Solution.choose(p))
}
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 4cd54bf9ec38198d9029cba78463e4a4e8c68fd0..83c5a3bf4d223386a5dbe73f18838e02b56e8cda 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -20,6 +20,7 @@ import scala.collection.mutable.{Map=>MutableMap}
import evaluators._
import datagen._
+import codegen.CodeGenParams
case object CEGIS extends Rule("CEGIS") {
@@ -38,7 +39,8 @@ case object CEGIS extends Rule("CEGIS") {
val testUpTo = 5
val useBssFiltering = sctx.options.cegisUseBssFiltering
val filterThreshold = 1.0/2
- val evaluator = new CodeGenEvaluator(sctx.context, sctx.program)
+ val evalParams = CodeGenParams(maxFunctionInvocations = 2000)
+ val evaluator = new CodeGenEvaluator(sctx.context, sctx.program, evalParams)
val interruptManager = sctx.context.interruptManager
@@ -71,7 +73,7 @@ case object CEGIS extends Rule("CEGIS") {
{ () =>
val alts: Seq[(Expr, Set[Identifier])] = cd.knownDescendents.flatMap(i => i match {
case acd: AbstractClassDef =>
- sctx.reporter.error("Unnexpected abstract class in descendants!")
+ sctx.reporter.error(acd.getPos, "Unnexpected abstract class in descendants!")
None
case cd: CaseClassDef =>
val cct = CaseClassType(cd, tpes)
@@ -110,7 +112,7 @@ case object CEGIS extends Rule("CEGIS") {
val isNotSynthesizable = fd.body match {
case Some(b) =>
- !containsChoose(b)
+ !containsChoose(b) && !usesHoles(b)
case None =>
false
@@ -437,7 +439,7 @@ case object CEGIS extends Rule("CEGIS") {
def css : Set[Identifier] = mappings.values.map(_._1).toSet ++ guardedTerms.flatMap(_._2)
}
- List(new RuleInstantiation(p, this, SolutionBuilder.none, "CEGIS") {
+ List(new RuleInstantiation(p, this, SolutionBuilder.none, this.name, this.priority) {
def apply(sctx: SynthesisContext): RuleApplicationResult = {
var result: Option[RuleApplicationResult] = None
diff --git a/src/main/scala/leon/synthesis/rules/Ground.scala b/src/main/scala/leon/synthesis/rules/Ground.scala
index 96a1e125016ae8cc2cca320eb00cbc028bafdbf6..52e5e0c135306518f11fe5cbc2ee82cd6fa097f9 100644
--- a/src/main/scala/leon/synthesis/rules/Ground.scala
+++ b/src/main/scala/leon/synthesis/rules/Ground.scala
@@ -13,7 +13,7 @@ import purescala.Extractors._
case object Ground extends Rule("Ground") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
if (p.as.isEmpty) {
- List(new RuleInstantiation(p, this, SolutionBuilder.none, "Ground") {
+ List(new RuleInstantiation(p, this, SolutionBuilder.none, this.name, this.priority) {
def apply(sctx: SynthesisContext): RuleApplicationResult = {
val solver = SimpleSolverAPI(new TimeoutSolverFactory(sctx.solverFactory, 10000L))
diff --git a/src/main/scala/leon/synthesis/rules/InlineHoles.scala b/src/main/scala/leon/synthesis/rules/InlineHoles.scala
new file mode 100644
index 0000000000000000000000000000000000000000..82fb1d13556cddce9ebeac6aa43fa4202732392f
--- /dev/null
+++ b/src/main/scala/leon/synthesis/rules/InlineHoles.scala
@@ -0,0 +1,103 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon
+package synthesis
+package rules
+
+import scala.annotation.tailrec
+
+import leon.utils._
+
+import solvers._
+
+import purescala.Common._
+import purescala.Trees._
+import purescala.TreeOps._
+import purescala.TypeTrees._
+import purescala.Extractors._
+
+case object InlineHoles extends Rule("Inline-Holes") {
+ override val priority = RulePriorityHoles
+
+ def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
+
+ @tailrec
+ def inlineUntilHoles(e: Expr): Expr = {
+ if (containsHoles(e)) {
+ // Holes are exposed, no need to inline (yet)
+ e
+ } else {
+ // Inline all functions "once" that contain holes
+ val newE = postMap {
+ case fi @ FunctionInvocation(tfd, args) if usesHoles(fi) && tfd.hasBody =>
+ val inlined = replaceFromIDs((tfd.params.map(_.id) zip args).toMap, tfd.body.get)
+ Some(inlined)
+
+ case _ => None
+ }(e)
+
+ inlineUntilHoles(newE)
+ }
+ }
+
+ def inlineHoles(phi: Expr): (List[Identifier], Expr) = {
+ var newXs = List[Identifier]()
+
+ val res = preMap {
+ case h @ Hole(o) =>
+ val tpe = h.getType
+ val x = FreshIdentifier("h", true).setType(tpe)
+ newXs ::= x
+
+ Some(x.toVariable)
+
+ case _ => None
+ }(phi)
+
+ (newXs.reverse, res)
+ }
+
+ if (usesHoles(p.phi)) {
+ val pathsToCalls = new CollectorWithPaths({
+ case fi: FunctionInvocation if usesHoles(fi) => fi
+ }).traverse(p.phi).map(_._2)
+
+ val pc = if (pathsToCalls.nonEmpty) {
+ Not(Or(pathsToCalls))
+ } else {
+ BooleanLiteral(false)
+ }
+
+ // Creates two alternative branches:
+ // 1) a version with holes unreachable, on which this rule won't re-apply
+ val sfact = new TimeoutSolverFactory(sctx.solverFactory, 500L)
+ val solver = SimpleSolverAPI(new TimeoutSolverFactory(sctx.solverFactory, 2000L))
+
+ val(holesAvoidable, _) = solver.solveSAT(And(p.pc, pc))
+
+ val avoid = if (holesAvoidable != Some(false)) {
+ val newPhi = simplifyPaths(sfact)(And(pc, p.phi))
+ val newProblem1 = p.copy(phi = newPhi)
+
+ Some(RuleInstantiation.immediateDecomp(p, this, List(newProblem1), {
+ case List(s) if (s.pre != BooleanLiteral(false)) => Some(s)
+ case _ => None
+ }, "Avoid Holes"))
+ } else {
+ None
+ }
+
+
+ // 2) a version with holes reachable to continue applying itself
+ val newPhi = inlineUntilHoles(p.phi)
+ val (newXs, newPhiInlined) = inlineHoles(newPhi)
+
+ val newProblem2 = p.copy(phi = newPhiInlined, xs = p.xs ::: newXs)
+ val rec = Some(RuleInstantiation.immediateDecomp(p, this, List(newProblem2), project(p.xs.size), "Inline Holes"))
+
+ List(rec, avoid).flatten
+ } else {
+ Nil
+ }
+ }
+}
diff --git a/src/main/scala/leon/synthesis/rules/OnePoint.scala b/src/main/scala/leon/synthesis/rules/OnePoint.scala
index df0e4965f6438f66701859b91a86e9f7ab47fa03..2091e67dc3a98a214620e264a8cd390751e9bfd8 100644
--- a/src/main/scala/leon/synthesis/rules/OnePoint.scala
+++ b/src/main/scala/leon/synthesis/rules/OnePoint.scala
@@ -4,6 +4,7 @@ package leon
package synthesis
package rules
+import purescala.Common._
import purescala.Trees._
import purescala.TreeOps._
import purescala.Extractors._
@@ -12,10 +13,14 @@ case object OnePoint extends NormalizingRule("One-point") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
val TopLevelAnds(exprs) = p.phi
+ def validOnePoint(x: Identifier, e: Expr) = {
+ !(variablesOf(e) contains x) && !usesHoles(e)
+ }
+
val candidates = exprs.collect {
- case eq @ Equals(Variable(x), e) if (p.xs contains x) && !(variablesOf(e) contains x) =>
+ case eq @ Equals(Variable(x), e) if (p.xs contains x) && validOnePoint(x, e) =>
(x, e, eq)
- case eq @ Equals(e, Variable(x)) if (p.xs contains x) && !(variablesOf(e) contains x) =>
+ case eq @ Equals(e, Variable(x)) if (p.xs contains x) && validOnePoint(x, e) =>
(x, e, eq)
}
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index f5cdb08ac1908d6c6c1db020119e354846297a29..148085a5a9d87a69ef2ec7b5a941ac77392b66b8 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -14,7 +14,7 @@ import solvers._
case object OptimisticGround extends Rule("Optimistic Ground") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
if (!p.as.isEmpty && !p.xs.isEmpty) {
- val res = new RuleInstantiation(p, this, SolutionBuilder.none, this.name) {
+ val res = new RuleInstantiation(p, this, SolutionBuilder.none, this.name, this.priority) {
def apply(sctx: SynthesisContext) = {
val solver = SimpleSolverAPI(sctx.fastSolverFactory) // Optimistic ground is given a simple solver (uninterpreted)
diff --git a/src/main/scala/leon/utils/OracleTraverser.scala b/src/main/scala/leon/utils/OracleTraverser.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d70d1fb5d0a9f024227924636f8748f2c4b84982
--- /dev/null
+++ b/src/main/scala/leon/utils/OracleTraverser.scala
@@ -0,0 +1,32 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon
+package utils
+
+import purescala.Trees._
+import purescala.TypeTrees._
+import purescala.Definitions._
+import utils._
+
+case class OracleTraverser(oracle: Expr, tpe: TypeTree, program: Program) {
+ private def call(name: String) = {
+ program.definedFunctions.find(_.id.name == "Oracle."+name) match {
+ case Some(fd) =>
+ FunctionInvocation(fd.typed(List(tpe)), List(oracle))
+ case None =>
+ sys.error("Unable to find Oracle."+name)
+ }
+ }
+
+ def value: Expr = {
+ call("head")
+ }
+
+ def left: OracleTraverser = {
+ OracleTraverser(call("left"), tpe, program)
+ }
+
+ def right: OracleTraverser = {
+ OracleTraverser(call("right"), tpe, program)
+ }
+}
diff --git a/src/main/scala/leon/utils/PreprocessingPhase.scala b/src/main/scala/leon/utils/PreprocessingPhase.scala
new file mode 100644
index 0000000000000000000000000000000000000000..896e16c786d5af7daf83a39febd7a8c217728041
--- /dev/null
+++ b/src/main/scala/leon/utils/PreprocessingPhase.scala
@@ -0,0 +1,24 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon
+package utils
+
+import purescala.Definitions.Program
+
+import purescala.{MethodLifting, CompleteAbstractDefinitions}
+
+object PreprocessingPhase extends TransformationPhase {
+
+ val name = "preprocessing"
+ val description = "Various preprocessings on Leon programs"
+
+ def apply(ctx: LeonContext, p: Program): Program = {
+
+ val phases =
+ MethodLifting andThen
+ TypingPhase andThen
+ CompleteAbstractDefinitions
+
+ phases.run(ctx)(p)
+ }
+}
diff --git a/src/main/scala/leon/utils/TypingPhase.scala b/src/main/scala/leon/utils/TypingPhase.scala
index 1dc7b561609f87aa3ff6c173b02a1d813f492803..a3e1f3e61961fc5472ea66e18799f15caaa457d5 100644
--- a/src/main/scala/leon/utils/TypingPhase.scala
+++ b/src/main/scala/leon/utils/TypingPhase.scala
@@ -24,6 +24,8 @@ object TypingPhase extends LeonPhase[Program, Program] {
*
* 2) Report warnings in case parts of the tree are not correctly typed
* (Untyped).
+ *
+ * 3) Make sure that abstract classes have at least one descendent
*/
def run(ctx: LeonContext)(pgm: Program): Program = {
pgm.definedFunctions.foreach(fd => {
@@ -63,12 +65,24 @@ object TypingPhase extends LeonPhase[Program, Program] {
fd.body.foreach {
preTraversal{
case t if !t.isTyped =>
- ctx.reporter.warning("Tree "+t.asString(ctx)+" is not properly typed ("+t.getPos.fullString+")")
+ ctx.reporter.warning(t.getPos, "Tree "+t.asString(ctx)+" is not properly typed ("+t.getPos.fullString+")")
case _ =>
}
}
+
})
+
+ // Part (3)
+ pgm.definedClasses.foreach {
+ case acd: AbstractClassDef =>
+ if (acd.knownCCDescendents.isEmpty) {
+ ctx.reporter.error(acd.getPos, "Class "+acd.id.asString(ctx)+" has no concrete descendent!")
+ }
+ case _ =>
+ }
+
+
pgm
}
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 7b1a1bea3aaf42de09faf75ab9e29b47ebcb0fc3..17d0222b3c3625d41636b50654f441bb427d690b 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -27,7 +27,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
LeonValueOptionDef("timeout", "--timeout=T", "Timeout after T seconds when trying to prove a verification condition.")
)
- def generateVerificationConditions(vctx: VerificationContext, functionsToAnalyse: Set[String]): Map[FunDef, List[VerificationCondition]] = {
+ def generateVerificationConditions(vctx: VerificationContext, filterFuns: Option[Seq[String]]): Map[FunDef, List[VerificationCondition]] = {
import vctx.reporter
import vctx.program
@@ -39,25 +39,20 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
var allVCs = Map[FunDef, List[VerificationCondition]]()
- val patterns = functionsToAnalyse.map{ s =>
- import java.util.regex.Pattern
-
- val p = s.replaceAll("\\.", "\\\\.").replaceAll("_", ".+")
- Pattern.compile(p)
+ def excludeByDefault(fd: FunDef): Boolean = {
+ (fd.annotations contains "verified") || (fd.annotations contains "library")
}
- def markedForVerification(name: String): Boolean = {
- patterns.exists(p => p.matcher(name).matches())
- }
+ val fdFilter = {
+ import OptionsHelpers._
- val toVerify = program.definedFunctions.toList.sortWith((fd1, fd2) => fd1.getPos < fd2.getPos).filter {
- fd =>
- (functionsToAnalyse.isEmpty && !(fd.annotations contains "verified")) ||
- (markedForVerification(fd.id.name))
+ filterInclusive(filterFuns.map(fdMatcher), Some(excludeByDefault _))
}
+ val toVerify = program.definedFunctions.toList.sortWith((fd1, fd2) => fd1.getPos < fd2.getPos).filter(fdFilter)
+
for(funDef <- toVerify) {
- if (funDef.annotations contains "verified") {
+ if (excludeByDefault(funDef)) {
reporter.warning("Forcing verification of "+funDef.id.name+" which was assumed verified")
}
@@ -156,9 +151,9 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
}
def run(ctx: LeonContext)(program: Program) : VerificationReport = {
- var functionsToAnalyse = Set[String]()
- var timeout: Option[Int] = None
- var selectedSolvers = Set[String]("fairz3")
+ var filterFuns: Option[Seq[String]] = None
+ var timeout: Option[Int] = None
+ var selectedSolvers = Set[String]("fairz3")
val allSolvers = Map(
"fairz3" -> SolverFactory(() => new FairZ3Solver(ctx, program) with TimeoutSolver),
@@ -169,7 +164,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
for(opt <- ctx.options) opt match {
case LeonValueOption("functions", ListValue(fs)) =>
- functionsToAnalyse = Set() ++ fs
+ filterFuns = Some(fs)
case LeonValueOption("solvers", ListValue(ss)) =>
val unknownSolvers = ss.toSet -- allSolvers.keySet
@@ -206,7 +201,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val vctx = VerificationContext(ctx, program, mainSolver, reporter)
reporter.debug("Running verification condition generation...")
- val vcs = generateVerificationConditions(vctx, functionsToAnalyse)
+ val vcs = generateVerificationConditions(vctx, filterFuns)
checkVerificationConditions(vctx, vcs)
}
}
diff --git a/src/main/scala/leon/verification/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
index df08846ca39ff124340afc55886ecb127dc574b1..70824c7edaa57011a80b52d39691e10d668ed527 100644
--- a/src/main/scala/leon/verification/InductionTactic.scala
+++ b/src/main/scala/leon/verification/InductionTactic.scala
@@ -64,7 +64,7 @@ class InductionTactic(reporter: Reporter) extends DefaultTactic(reporter) {
}
case None =>
- reporter.warning("Could not find abstract class type argument to induct on")
+ reporter.warning(funDef.getPos, "Could not find abstract class type argument to induct on")
super.generatePostconditions(funDef)
}
}
@@ -132,7 +132,7 @@ class InductionTactic(reporter: Reporter) extends DefaultTactic(reporter) {
toRet
}
case None => {
- reporter.warning("Induction tactic currently supports exactly one argument of abstract class type")
+ reporter.warning(function.getPos, "Induction tactic currently supports exactly one argument of abstract class type")
defaultPrec
}
}
diff --git a/src/test/resources/regression/synthesis/Church/Add.scala b/src/test/resources/regression/synthesis/Church/Add.scala
index 542550eb180c1d96dc82682547d9edc21ce5da0d..d060360c201b590095b5bac16a6a2e8218a4352f 100644
--- a/src/test/resources/regression/synthesis/Church/Add.scala
+++ b/src/test/resources/regression/synthesis/Church/Add.scala
@@ -1,6 +1,8 @@
/* Copyright 2009-2014 EPFL, Lausanne */
import leon.lang._
+import leon.lang.synthesis._
+
object ChurchNumerals {
sealed abstract class Num
case object Z extends Num
diff --git a/src/test/resources/regression/synthesis/Church/Distinct.scala b/src/test/resources/regression/synthesis/Church/Distinct.scala
index c702d3c142bcf76f322e3a0bb7daf9d1f1e7e5e3..3e503f4ab896d5632d8f9ea2e5f1a5a8d1203625 100644
--- a/src/test/resources/regression/synthesis/Church/Distinct.scala
+++ b/src/test/resources/regression/synthesis/Church/Distinct.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2014 EPFL, Lausanne */
import leon.lang._
+import leon.lang.synthesis._
object ChurchNumerals {
sealed abstract class Num
case object Z extends Num
diff --git a/src/test/resources/regression/synthesis/Church/Mult.scala b/src/test/resources/regression/synthesis/Church/Mult.scala
index 8251e0a2fd54123b7db933a2041bf612fb237ebc..39c0286d08edb25a8c3e737da5f9175dd5202c1d 100644
--- a/src/test/resources/regression/synthesis/Church/Mult.scala
+++ b/src/test/resources/regression/synthesis/Church/Mult.scala
@@ -1,6 +1,8 @@
/* Copyright 2009-2014 EPFL, Lausanne */
import leon.lang._
+import leon.lang.synthesis._
+
object ChurchNumerals {
sealed abstract class Num
case object Z extends Num
diff --git a/src/test/resources/regression/synthesis/Church/Squared.scala b/src/test/resources/regression/synthesis/Church/Squared.scala
index bf390fea7efb214325674071e7f1319f91da4a2b..9328e70ff65874a445d41f2c01635f3d9ca2311a 100644
--- a/src/test/resources/regression/synthesis/Church/Squared.scala
+++ b/src/test/resources/regression/synthesis/Church/Squared.scala
@@ -1,6 +1,8 @@
/* Copyright 2009-2014 EPFL, Lausanne */
import leon.lang._
+import leon.lang.synthesis._
+
object ChurchNumerals {
sealed abstract class Num
case object Z extends Num
diff --git a/src/test/resources/regression/synthesis/Holes/Hole1.scala b/src/test/resources/regression/synthesis/Holes/Hole1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..084185b0efcb96208163158049ebfac429a6a116
--- /dev/null
+++ b/src/test/resources/regression/synthesis/Holes/Hole1.scala
@@ -0,0 +1,13 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+import leon.lang._
+import leon.annotation._
+import leon.lang.synthesis._
+import leon.collection._
+import leon._
+
+object Hole1 {
+ def largestInt(a: Int, b: Int)(implicit o: Oracle[Boolean]) = {
+ ?(a, b)
+ } ensuring { r => r >= b && r >= a }
+}
diff --git a/src/test/resources/regression/synthesis/Holes/Hole2.scala b/src/test/resources/regression/synthesis/Holes/Hole2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3a10748eb70d48aab7a46cc8379dfb3bbaacbfca
--- /dev/null
+++ b/src/test/resources/regression/synthesis/Holes/Hole2.scala
@@ -0,0 +1,17 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+import leon.lang._
+import leon.annotation._
+import leon.lang.synthesis._
+import leon.collection._
+import leon._
+
+object Hole2 {
+ def genList()(implicit o: Oracle[Boolean]): List[Int] = ?(Nil[Int](), Cons[Int](0, genList()(o.right)))
+
+ def listOfSize2(implicit o: Oracle[Boolean]) = {
+ genList()
+ } ensuring {
+ _.size == 2
+ }
+}
diff --git a/src/test/resources/regression/synthesis/List/Delete.scala b/src/test/resources/regression/synthesis/List/Delete.scala
index 113eedb44dd5724978b62f162125e5ab0f136259..02f13ec3837b5b96b2ace88269ecede8fd7744d2 100644
--- a/src/test/resources/regression/synthesis/List/Delete.scala
+++ b/src/test/resources/regression/synthesis/List/Delete.scala
@@ -2,6 +2,7 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Delete {
sealed abstract class List
diff --git a/src/test/resources/regression/synthesis/List/Diff.scala b/src/test/resources/regression/synthesis/List/Diff.scala
index a6bebd6423d1fbb5bff898f42dd796e951c0a5b5..5ae469ea7c04e6373707ad9d6083798f2d5fe16a 100644
--- a/src/test/resources/regression/synthesis/List/Diff.scala
+++ b/src/test/resources/regression/synthesis/List/Diff.scala
@@ -2,6 +2,7 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Diff {
sealed abstract class List
diff --git a/src/test/resources/regression/synthesis/List/Insert.scala b/src/test/resources/regression/synthesis/List/Insert.scala
index 21a758ecec4b3373b34ef69d16c1f3cc47df4f1d..13c1294d7000c4b8fce4fbe229a3a5b54ea27790 100644
--- a/src/test/resources/regression/synthesis/List/Insert.scala
+++ b/src/test/resources/regression/synthesis/List/Insert.scala
@@ -2,6 +2,7 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Insert {
sealed abstract class List
diff --git a/src/test/resources/regression/synthesis/List/Split.scala b/src/test/resources/regression/synthesis/List/Split.scala
index 944ee9d0b5fffe496365cd6145c634efc4bd71c3..989d509da8018aca3f96be9834275796258887f3 100644
--- a/src/test/resources/regression/synthesis/List/Split.scala
+++ b/src/test/resources/regression/synthesis/List/Split.scala
@@ -2,6 +2,7 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Complete {
sealed abstract class List
diff --git a/src/test/resources/regression/synthesis/List/Union.scala b/src/test/resources/regression/synthesis/List/Union.scala
index 3b3130d7f86179db9b1397a3b55bfa39c9cd8169..a4acf629b8a4ec2bbb22e7f95a46af965b18fd63 100644
--- a/src/test/resources/regression/synthesis/List/Union.scala
+++ b/src/test/resources/regression/synthesis/List/Union.scala
@@ -2,6 +2,7 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Union {
sealed abstract class List
diff --git a/src/test/resources/regression/verification/purescala/invalid/Choose1.scala b/src/test/resources/regression/verification/purescala/invalid/Choose1.scala
index 74e7f0db5680d3f4c978f0790a7b088fbdb7cf72..20d5885231c38d0ea858152d112fe43e5e546f23 100644
--- a/src/test/resources/regression/verification/purescala/invalid/Choose1.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Choose1.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2014 EPFL, Lausanne */
import leon.annotation._
+import leon.lang.synthesis._
import leon.lang._
object Choose1 {
diff --git a/src/test/resources/regression/verification/purescala/valid/Choose1.scala b/src/test/resources/regression/verification/purescala/valid/Choose1.scala
index 408dafa8717435d20ff5519b09e660653d29deeb..2b033c809ca1e5c71ad9c7592aa4482ab13ef083 100644
--- a/src/test/resources/regression/verification/purescala/valid/Choose1.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Choose1.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2014 EPFL, Lausanne */
import leon.annotation._
+import leon.lang.synthesis._
import leon.lang._
object Choose1 {
diff --git a/src/test/resources/regression/verification/purescala/valid/IsolatedAbstract.scala b/src/test/resources/regression/verification/purescala/valid/IsolatedAbstract.scala
deleted file mode 100644
index 52077b3545d2967d89979b09238449c8686ecaaa..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/verification/purescala/valid/IsolatedAbstract.scala
+++ /dev/null
@@ -1,23 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-import leon.lang._
-import leon.annotation._
-
-object LoneAbstract {
-
- /*
- * create a structure with all these fields
- */
- sealed abstract class TrackedFields
- case class TreeFields(isBST: Boolean)
-
- /* add this structure to Tree class */
- sealed abstract class Tree
- case class Leaf(fields:TreeFields) extends Tree
- case class Node(left : Tree, value : Int, right: Tree, fields:TreeFields) extends Tree
-
-
- def foo(): Int = {
- 42
- } ensuring ( _ > 0 )
-}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon1.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon1.scala
index b6eb6a05d392fa3eea5a14d7c4239ab2569929aa..f1878f35d3086fb626aebe9a24f83b1e39746178 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Epsilon1.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon1.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2014 EPFL, Lausanne */
import leon.lang._
+import leon.lang.xlang._
object Epsilon1 {
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon2.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon2.scala
index ee620237f367b85595bc6ee9ac07e2055058b7a0..45c4adf7939124d36c083fce717c97ab172c6d1d 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Epsilon2.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon2.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2014 EPFL, Lausanne */
import leon.lang._
+import leon.lang.xlang._
object Epsilon1 {
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon3.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon3.scala
index b12fcbbe0a488d9853c7d6f39a2bf9d76a87fca0..ec44138ca7388305c9e902eceb9b843edf4a9a3b 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Epsilon3.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon3.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2014 EPFL, Lausanne */
import leon.lang._
+import leon.lang.xlang._
object Epsilon3 {
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon4.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon4.scala
index 22beb0849732a5225bb052cd4b9005bb6eef7a1c..5437d93b3f71d942616ca23237d5064b29652795 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Epsilon4.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon4.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2014 EPFL, Lausanne */
import leon.lang._
+import leon.lang.xlang._
object Epsilon4 {
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon5.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon5.scala
index 75f9dd813f3aec574dcd4111b1b7b6d6bb15bc4c..18eb98709a22956e54904d9195e8bfc302a1162c 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Epsilon5.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon5.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2014 EPFL, Lausanne */
import leon.lang._
+import leon.lang.xlang._
object Epsilon5 {
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon6.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon6.scala
index 0fadb741422a50e242378df8f1e426d5bfa87ae8..7cdf4fc288775a354c772f7b4082130974593290 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Epsilon6.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon6.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2014 EPFL, Lausanne */
import leon.lang._
+import leon.lang.xlang._
object Epsilon6 {
diff --git a/src/test/resources/regression/verification/xlang/valid/Choose1.scala b/src/test/resources/regression/verification/xlang/valid/Choose1.scala
index 0ea5e51224ebcb0295ec3e7a08f52a6c7bc397a2..893db3e784b2abc9e607fef274f41ed426a33c48 100644
--- a/src/test/resources/regression/verification/xlang/valid/Choose1.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Choose1.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2014 EPFL, Lausanne */
import leon.lang._
+import leon.lang.synthesis._
object Test {
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon1.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon1.scala
index 108ea647733422f724e573040ec5bbce0447bef2..b9af3dc12c7bd32eac2411982451b33586ca95a2 100644
--- a/src/test/resources/regression/verification/xlang/valid/Epsilon1.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Epsilon1.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2014 EPFL, Lausanne */
import leon.lang._
+import leon.lang.xlang._
object Epsilon1 {
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala
index dbdb96c9a7f06b606fb069d2cc13e9860dbb31b2..289bdd4d114f43defcb6134340eae9be42595784 100644
--- a/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2014 EPFL, Lausanne */
import leon.lang._
+import leon.lang.xlang._
object Epsilon1 {
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon3.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon3.scala
index 541933cd8545edf8e8d65135a13cfe6d3b076794..ece6f7bf08b18de3fcae027538324fa324d19c2f 100644
--- a/src/test/resources/regression/verification/xlang/valid/Epsilon3.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Epsilon3.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2014 EPFL, Lausanne */
import leon.lang._
+import leon.lang.xlang._
object Epsilon3 {
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon4.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon4.scala
index 8b7f7af3b9935f48fff0cc6f85ad24e4f9db5612..49cd971fad06ddd765241200bbd847793a0fedc3 100644
--- a/src/test/resources/regression/verification/xlang/valid/Epsilon4.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Epsilon4.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2014 EPFL, Lausanne */
import leon.lang._
+import leon.lang.xlang._
object Epsilon4 {
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon5.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon5.scala
index 565e99ec22d7c2602bad534a9aa9e01dff4b9772..008cef8368c84a582ee61f38dc32416f492c2e35 100644
--- a/src/test/resources/regression/verification/xlang/valid/Epsilon5.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Epsilon5.scala
@@ -1,6 +1,7 @@
/* Copyright 2009-2014 EPFL, Lausanne */
import leon.lang._
+import leon.lang.xlang._
object Epsilon5 {
diff --git a/src/test/scala/leon/test/LeonTestSuite.scala b/src/test/scala/leon/test/LeonTestSuite.scala
index be5f00802515d25925cde9b07896dc64c23c930d..9b460d5841958c34fec28da8e6dbc9e9fc2eb678 100644
--- a/src/test/scala/leon/test/LeonTestSuite.scala
+++ b/src/test/scala/leon/test/LeonTestSuite.scala
@@ -35,17 +35,16 @@ trait LeonTestSuite extends FunSuite with Timeouts {
}
+ def createLeonContext(opts: String*): LeonContext = {
+ val reporter = new TestSilentReporter
+
+ Main.processOptions(opts.toList).copy(reporter = reporter, interruptManager = new InterruptManager(reporter))
+ }
+
var testContext = generateContext
def generateContext = {
- val reporter = new TestSilentReporter
-
- LeonContext(
- settings = Settings(),
- files = List(),
- reporter = reporter,
- interruptManager = new InterruptManager(reporter)
- )
+ createLeonContext()
}
def testIdentifier(name: String): String = {
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index 77237afc0ec55aebb22c11882474e6dfdc8db9b9..055eb3ed62107fdf20b51140139a9fccdfa9f0bd 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -7,7 +7,7 @@ import leon._
import leon.evaluators._
-import leon.utils.TemporaryInputPhase
+import leon.utils.{TemporaryInputPhase, PreprocessingPhase}
import leon.frontends.scalac.ExtractionPhase
import leon.purescala.Common._
@@ -26,7 +26,7 @@ class EvaluatorsTests extends LeonTestSuite {
private def prepareEvaluators(implicit ctx : LeonContext, prog : Program) : List[Evaluator] = evaluatorConstructors.map(c => c(leonContext, prog))
private def parseString(str : String) : Program = {
- val pipeline = TemporaryInputPhase andThen ExtractionPhase
+ val pipeline = TemporaryInputPhase andThen ExtractionPhase andThen PreprocessingPhase
val errorsBefore = leonContext.reporter.errorCount
val warningsBefore = leonContext.reporter.warningCount
@@ -431,6 +431,7 @@ class EvaluatorsTests extends LeonTestSuite {
test("Executing Chooses") {
val p = """|object Program {
| import leon.lang._
+ | import leon.lang.synthesis._
|
| def c(i : Int) : Int = choose { (j : Int) => j > i && j < i + 2 }
|}
diff --git a/src/test/scala/leon/test/purescala/DataGen.scala b/src/test/scala/leon/test/purescala/DataGen.scala
index c9b19e5e456f9a179ee80c1cf61edfc885e25f84..9259e483a9af05a2516a78b366276c2f5120a2f1 100644
--- a/src/test/scala/leon/test/purescala/DataGen.scala
+++ b/src/test/scala/leon/test/purescala/DataGen.scala
@@ -4,7 +4,7 @@ package leon.test
package purescala
import leon._
-import leon.utils.TemporaryInputPhase
+import leon.utils.{TemporaryInputPhase, PreprocessingPhase}
import leon.frontends.scalac.ExtractionPhase
import leon.purescala.Common._
@@ -19,7 +19,7 @@ import org.scalatest.FunSuite
class DataGen extends LeonTestSuite {
private def parseString(str : String) : Program = {
- val pipeline = TemporaryInputPhase andThen ExtractionPhase
+ val pipeline = TemporaryInputPhase andThen ExtractionPhase andThen PreprocessingPhase
val errorsBefore = testContext.reporter.errorCount
val warningsBefore = testContext.reporter.warningCount
@@ -67,15 +67,19 @@ class DataGen extends LeonTestSuite {
generator.generate(BooleanType).toSet.size === 2
generator.generate(TupleType(Seq(BooleanType,BooleanType))).toSet.size === 4
- val listType : TypeTree = classDefToClassType(prog.classHierarchyRoots.head)
- val sizeDef : FunDef = prog.definedFunctions.find(_.id.name == "size").get
- val sortedDef : FunDef = prog.definedFunctions.find(_.id.name == "isSorted").get
- val contentDef : FunDef = prog.definedFunctions.find(_.id.name == "content").get
- val insSpecDef : FunDef = prog.definedFunctions.find(_.id.name == "insertSpec").get
+ // Make sure we target our own lists
+ val module = prog.modules.find(_.id.name == "Program").get
+ val listType : TypeTree = classDefToClassType(module.classHierarchyRoots.head)
+ val sizeDef : FunDef = module.definedFunctions.find(_.id.name == "size").get
+ val sortedDef : FunDef = module.definedFunctions.find(_.id.name == "isSorted").get
+ val contentDef : FunDef = module.definedFunctions.find(_.id.name == "content").get
+ val insSpecDef : FunDef = module.definedFunctions.find(_.id.name == "insertSpec").get
- val consDef : CaseClassDef = prog.caseClassDef("Cons")
+ val consDef : CaseClassDef = module.definedClasses.collect {
+ case ccd: CaseClassDef if ccd.id.name == "Cons" => ccd
+ }.head
- generator.generate(listType).take(100).toSet.size === 100
+ assert(generator.generate(listType).take(100).toSet.size === 100, "Should be able to generate 100 different lists")
val evaluator = new CodeGenEvaluator(testContext, prog)
@@ -95,14 +99,14 @@ class DataGen extends LeonTestSuite {
GreaterThan(sizeX, IntLiteral(0)),
10,
500
- ).size === 10)
+ ).size === 10, "Should find 10 non-empty lists in the first 500 enumerated")
assert(generator.generateFor(
Seq(x.id, y.id),
And(Equals(contentX, contentY), sortedY),
10,
500
- ).size === 10)
+ ).size === 10, "Should find 2x 10 lists with same content in the first 500 enumerated")
assert(generator.generateFor(
Seq(x.id, y.id),
diff --git a/src/test/scala/leon/test/purescala/TransformationTests.scala b/src/test/scala/leon/test/purescala/TransformationTests.scala
index e358e14369d58ee192bf7df68fbbc530dc4a45f1..d3123f4d209086b20a04b33594d5c1c4070a9ef0 100644
--- a/src/test/scala/leon/test/purescala/TransformationTests.scala
+++ b/src/test/scala/leon/test/purescala/TransformationTests.scala
@@ -4,7 +4,7 @@ package leon.test
package purescala
import leon._
-import leon.utils.TemporaryInputPhase
+import leon.utils.{TemporaryInputPhase, PreprocessingPhase}
import leon.frontends.scalac.ExtractionPhase
import leon.purescala.ScalaPrinter
@@ -16,7 +16,7 @@ import leon.purescala.TypeTrees._
class TransformationTests extends LeonTestSuite {
- val pipeline = ExtractionPhase andThen leon.utils.TypingPhase
+ val pipeline = ExtractionPhase andThen PreprocessingPhase
filesInResourceDir("regression/transformations").foreach { file =>
val ctx = testContext.copy(
diff --git a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
index 38971a80b7369efcc483198c8918f24243e6a91e..32eee19c2443aebd041e7db450a6e849e9c67f51 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisRegressionSuite.scala
@@ -25,15 +25,12 @@ class SynthesisRegressionSuite extends LeonTestSuite {
}
private def testSynthesis(cat: String, f: File, bound: Int) {
- val ctx = testContext.copy(settings = Settings(
- synthesis = true,
- xlang = false,
- verify = false
- ))
- val opts = SynthesisOptions(searchBound = Some(bound))
+ val ctx = createLeonContext("--synthesis", "--library")
- val pipeline = frontends.scalac.ExtractionPhase andThen leon.utils.TypingPhase
+ val opts = SynthesisOptions(searchBound = Some(bound), allSeeing = true)
+
+ val pipeline = frontends.scalac.ExtractionPhase andThen leon.utils.PreprocessingPhase
val program = pipeline.run(ctx)(f.getAbsolutePath :: Nil)
@@ -57,11 +54,7 @@ class SynthesisRegressionSuite extends LeonTestSuite {
testSynthesis("List", f, 200)
}
- //forEachFileIn("regression/synthesis/SortedList/") { f =>
- // testSynthesis("SortedList", f, 400)
- //}
-
- //forEachFileIn("regression/synthesis/StrictSortedList/") { f =>
- // testSynthesis("StrictSortedList", f, 400)
- //}
+ forEachFileIn("regression/synthesis/Holes/") { f =>
+ testSynthesis("Holes", f, 1000)
+ }
}
diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index b7cefba50d26eca526a4933f8674796c901be850..ab07f81169b75c96cfbe836f5d2aee282539e7bb 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -11,6 +11,7 @@ import leon.solvers.z3._
import leon.solvers.Solver
import leon.synthesis._
import leon.synthesis.utils._
+import leon.utils.PreprocessingPhase
import org.scalatest.matchers.ShouldMatchers._
@@ -31,34 +32,34 @@ class SynthesisSuite extends LeonTestSuite {
verify = false
))
- val pipeline = leon.utils.TemporaryInputPhase andThen leon.frontends.scalac.ExtractionPhase andThen SynthesisProblemExtractionPhase
+ try {
+ val pipeline = leon.utils.TemporaryInputPhase andThen leon.frontends.scalac.ExtractionPhase andThen PreprocessingPhase andThen SynthesisProblemExtractionPhase
- val (program, results) = pipeline.run(ctx)((content, Nil))
+ val (program, results) = pipeline.run(ctx)((content, Nil))
- for ((f, ps) <- results; p <- ps) {
- test("Synthesizing %3d: %-20s [%s]".format(nextInt(), f.id.toString, title)) {
- val sctx = SynthesisContext(ctx,
- opts,
- Some(f),
- program,
- ctx.reporter)
+ for ((f, ps) <- results; p <- ps) {
+ test("Synthesizing %3d: %-20s [%s]".format(nextInt(), f.id.toString, title)) {
+ val sctx = SynthesisContext(ctx,
+ opts,
+ Some(f),
+ program,
+ ctx.reporter)
- block(sctx, f, p)
+ block(sctx, f, p)
+ }
}
+ } catch {
+ case lfe: LeonFatalError =>
+ test("Synthesizing %3d: %-20s [%s]".format(nextInt(), "", title)) {
+ assert(false, "Failed to compile "+title)
+ }
}
}
case class Apply(desc: String, andThen: List[Apply] = Nil)
def synthesizeWith(sctx: SynthesisContext, p: Problem, ss: Apply): Solution = {
- val (normRules, otherRules) = sctx.options.rules.partition(_.isInstanceOf[NormalizingRule])
- val normApplications = normRules.flatMap(_.instantiateOn(sctx, p))
-
- val apps = if (!normApplications.isEmpty) {
- normApplications
- } else {
- otherRules.flatMap { r => r.instantiateOn(sctx, p) }
- }
+ val apps = Rules.getInstantiations(sctx, p)
def matchingDesc(app: RuleInstantiation, ss: Apply): Boolean = {
import java.util.regex.Pattern;
@@ -123,9 +124,9 @@ class SynthesisSuite extends LeonTestSuite {
forProgram("Ground Enum", SynthesisOptions(selectedSolvers = Set("enum")))(
"""
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Injection {
sealed abstract class List
@@ -148,9 +149,9 @@ object Injection {
forProgram("Cegis 1")(
"""
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Injection {
sealed abstract class List
@@ -173,9 +174,9 @@ object Injection {
forProgram("Cegis 2")(
"""
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Injection {
sealed abstract class List
@@ -212,6 +213,7 @@ object Injection {
synthesize("Lists")("""
import leon.lang._
+import leon.lang.synthesis._
object SortedList {
sealed abstract class List
@@ -277,6 +279,8 @@ object SortedList {
synthesize("Church")("""
import leon.lang._
+import leon.lang.synthesis._
+
object ChurchNumerals {
sealed abstract class Num
case object Z extends Num
@@ -310,6 +314,8 @@ object ChurchNumerals {
synthesize("Church")("""
import leon.lang._
+import leon.lang.synthesis._
+
object ChurchNumerals {
sealed abstract class Num
case object Z extends Num
diff --git a/src/test/scala/leon/test/termination/TerminationRegression.scala b/src/test/scala/leon/test/termination/TerminationRegression.scala
index 6fa5909049ebcaba9934ceb8fcbd3a0f823c45e0..65f20d0362f94bace3160979b37a1403b0f5414a 100644
--- a/src/test/scala/leon/test/termination/TerminationRegression.scala
+++ b/src/test/scala/leon/test/termination/TerminationRegression.scala
@@ -17,7 +17,7 @@ class TerminationRegression extends LeonTestSuite {
private case class Output(report : TerminationReport, reporter : Reporter)
private def mkPipeline : Pipeline[List[String],TerminationReport] =
- leon.frontends.scalac.ExtractionPhase andThen leon.utils.TypingPhase andThen leon.termination.TerminationPhase
+ leon.frontends.scalac.ExtractionPhase andThen leon.utils.PreprocessingPhase andThen leon.termination.TerminationPhase
private def mkTest(file : File, leonOptions: Seq[LeonOption], forError: Boolean)(block: Output=>Unit) = {
val fullName = file.getPath()
diff --git a/src/test/scala/leon/test/verification/LibraryVerificationRegression.scala b/src/test/scala/leon/test/verification/LibraryVerificationRegression.scala
index bf54de0070f697e845087fa3bdb8de16fc901c2a..a1d7c26906d0429fc28c9dba8d4d23f431889a55 100644
--- a/src/test/scala/leon/test/verification/LibraryVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/LibraryVerificationRegression.scala
@@ -6,13 +6,15 @@ package verification
import java.io.File
+import leon.frontends.scalac.ExtractionPhase
+import leon.utils.PreprocessingPhase
+import leon.verification.AnalysisPhase
+
class LibraryVerificationRegression extends LeonTestSuite {
test("Verify the library") {
- val pipeline = leon.frontends.scalac.ExtractionPhase andThen
- leon.purescala.MethodLifting andThen
- leon.utils.TypingPhase andThen
- leon.purescala.CompleteAbstractDefinitions andThen
- leon.verification.AnalysisPhase
+ val pipeline = ExtractionPhase andThen
+ PreprocessingPhase andThen
+ AnalysisPhase
val ctx = Main.processOptions(Seq("--library", "--functions=_")).copy(reporter = new TestSilentReporter())
diff --git a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
index 18d39fa7679e3448e1f62287c1245b59de25764f..4bfd35e92d8337b210d5dd8d1ee204a5303f6dad 100644
--- a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -6,6 +6,9 @@ package verification
import leon.verification.{AnalysisPhase,VerificationReport}
+import leon.frontends.scalac.ExtractionPhase
+import leon.utils.PreprocessingPhase
+
import java.io.File
class PureScalaVerificationRegression extends LeonTestSuite {
@@ -16,8 +19,10 @@ class PureScalaVerificationRegression extends LeonTestSuite {
}
private case class Output(report : VerificationReport, reporter : Reporter)
- private def mkPipeline : Pipeline[List[String],VerificationReport] =
- leon.frontends.scalac.ExtractionPhase andThen leon.utils.TypingPhase andThen leon.verification.AnalysisPhase
+ private def mkPipeline : Pipeline[List[String], VerificationReport] =
+ ExtractionPhase andThen
+ PreprocessingPhase andThen
+ AnalysisPhase
private def mkTest(file : File, leonOptions : Seq[LeonOption], forError: Boolean)(block: Output=>Unit) = {
val fullName = file.getPath()
diff --git a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
index 89eaaca6427f1a8a23386fa328cd696989f4184d..726b039e0c977b8e31a82d69f5b9b0912eedadc6 100644
--- a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
@@ -4,7 +4,10 @@ package leon
package test
package verification
-import leon.verification.{AnalysisPhase,VerificationReport}
+import leon.verification.VerificationReport
+import leon.xlang.XlangAnalysisPhase
+import leon.frontends.scalac.ExtractionPhase
+import leon.utils.PreprocessingPhase
import java.io.File
@@ -17,7 +20,9 @@ class XLangVerificationRegression extends LeonTestSuite {
private case class Output(report : VerificationReport, reporter : Reporter)
private def mkPipeline : Pipeline[List[String],VerificationReport] =
- leon.frontends.scalac.ExtractionPhase andThen leon.utils.TypingPhase andThen xlang.XlangAnalysisPhase
+ ExtractionPhase andThen
+ PreprocessingPhase andThen
+ XlangAnalysisPhase
private def mkTest(file : File, forError: Boolean = false)(block: Output=>Unit) = {
val fullName = file.getPath()
diff --git a/testcases/case-studies/Lambda.scala b/testcases/case-studies/Lambda.scala
index ecc82053da783a500ab88f6233e3068c98bae1d5..05df4cf57332fced12b3dd1eda809816d71c6490 100644
--- a/testcases/case-studies/Lambda.scala
+++ b/testcases/case-studies/Lambda.scala
@@ -1,6 +1,7 @@
import leon.lang._
import leon.annotation._
import leon.collection._
+import leon.lang.synthesis._
import leon._
object Lang {
diff --git a/testcases/condabd/benchmarks/AddressBook/AddressesMakeAddressBook.scala b/testcases/condabd/benchmarks/AddressBook/AddressesMakeAddressBook.scala
index ccd1d6ad3db6fc7c3dd6e682a32ab97939d39fa9..e7067c756d047cb101b25dde6a3ae51313ffb8cf 100644
--- a/testcases/condabd/benchmarks/AddressBook/AddressesMakeAddressBook.scala
+++ b/testcases/condabd/benchmarks/AddressBook/AddressesMakeAddressBook.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Addresses {
case class Info(
diff --git a/testcases/condabd/benchmarks/AddressBook/AddressesMakeAddressBookWithHelpers.scala b/testcases/condabd/benchmarks/AddressBook/AddressesMakeAddressBookWithHelpers.scala
index f04399105adbdd36e994ccfdabadeb24ffdf3da6..3dfd21465f2743d99a0c2365b49c43ad5827aa32 100644
--- a/testcases/condabd/benchmarks/AddressBook/AddressesMakeAddressBookWithHelpers.scala
+++ b/testcases/condabd/benchmarks/AddressBook/AddressesMakeAddressBookWithHelpers.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Addresses {
diff --git a/testcases/condabd/benchmarks/AddressBook/AddressesMergeAddressBooks.scala b/testcases/condabd/benchmarks/AddressBook/AddressesMergeAddressBooks.scala
index a9154bc7694564291a819dfec6bc0bc641bbffdf..8436ef25f5ba3569b6b181847ed142f818dd63c8 100644
--- a/testcases/condabd/benchmarks/AddressBook/AddressesMergeAddressBooks.scala
+++ b/testcases/condabd/benchmarks/AddressBook/AddressesMergeAddressBooks.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Addresses {
case class Info(
diff --git a/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueCheckf.scala b/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueCheckf.scala
index 52e582ffb2c850f60dac404f375da2aa486f637f..7d85a2c9bb96d5eae615f33b3557ecbb4a709e8e 100644
--- a/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueCheckf.scala
+++ b/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueCheckf.scala
@@ -1,6 +1,5 @@
-import scala.collection.immutable.Set
-
import leon.lang._
+import leon.lang.synthesis._
object BatchedQueue {
sealed abstract class List
diff --git a/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueSnoc.scala b/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueSnoc.scala
index 26e70e64995bdf559add3538f4cd23355d1303f6..c595f8253a4501bd56d7ada06a96091587003595 100644
--- a/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueSnoc.scala
+++ b/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueSnoc.scala
@@ -1,6 +1,5 @@
-import scala.collection.immutable.Set
-
import leon.lang._
+import leon.lang.synthesis._
object BatchedQueue {
sealed abstract class List
diff --git a/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueSnocWeird.scala b/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueSnocWeird.scala
index f74b8d8eaffa429632f19f5e66ab01f22092dd4e..2a82511d59eec356413da146f144d8cdf8935eb2 100644
--- a/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueSnocWeird.scala
+++ b/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueSnocWeird.scala
@@ -1,6 +1,5 @@
-import scala.collection.immutable.Set
-
import leon.lang._
+import leon.lang.synthesis._
object BatchedQueue {
sealed abstract class List
diff --git a/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueTail.scala b/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueTail.scala
index 31b67f6a850f0f75e2a79af82ec855605d416337..4c7d22df90293201fde63efe09b693314805ba8c 100644
--- a/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueTail.scala
+++ b/testcases/condabd/benchmarks/BatchedQueue/BatchedQueueTail.scala
@@ -1,6 +1,5 @@
-import scala.collection.immutable.Set
-
import leon.lang._
+import leon.lang.synthesis._
object BatchedQueue {
sealed abstract class List
diff --git a/testcases/condabd/benchmarks/BinarySearch.scala b/testcases/condabd/benchmarks/BinarySearch.scala
index b8883a3bbebb6283136dcd777d3c333678c8131c..40f91c988fb2771364b98ae93b795f9386d9c9b4 100644
--- a/testcases/condabd/benchmarks/BinarySearch.scala
+++ b/testcases/condabd/benchmarks/BinarySearch.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.lang.synthesis._
object BinarySearch {
diff --git a/testcases/condabd/benchmarks/BinarySearchTree/BinarySearchTreeMember.scala b/testcases/condabd/benchmarks/BinarySearchTree/BinarySearchTreeMember.scala
index 5ca4fb8c3abe56168ec3dd8ff7fa1da57c90af89..661e02e5c37823039bbdccc59a0379b8f477a3c1 100644
--- a/testcases/condabd/benchmarks/BinarySearchTree/BinarySearchTreeMember.scala
+++ b/testcases/condabd/benchmarks/BinarySearchTree/BinarySearchTreeMember.scala
@@ -1,7 +1,6 @@
-import scala.collection.immutable.Set
-
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object BinarySearchTree {
sealed abstract class Tree
diff --git a/testcases/condabd/benchmarks/InsertionSort/InsertionSortInsert.scala b/testcases/condabd/benchmarks/InsertionSort/InsertionSortInsert.scala
index 7afa8f2b8ba2b90d6fc6e3da518f621e145a4425..7aa7fdd52f9869b9e387b9623c7bb68ba93d14c5 100644
--- a/testcases/condabd/benchmarks/InsertionSort/InsertionSortInsert.scala
+++ b/testcases/condabd/benchmarks/InsertionSort/InsertionSortInsert.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object InsertionSort {
sealed abstract class List
diff --git a/testcases/condabd/benchmarks/InsertionSort/InsertionSortSort.scala b/testcases/condabd/benchmarks/InsertionSort/InsertionSortSort.scala
index 823011be40fa82df76f9da08580aa46455948c25..21fc426cab62022b5bdc457f8765ec853d1fa5e8 100644
--- a/testcases/condabd/benchmarks/InsertionSort/InsertionSortSort.scala
+++ b/testcases/condabd/benchmarks/InsertionSort/InsertionSortSort.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object InsertionSort {
sealed abstract class List
diff --git a/testcases/condabd/benchmarks/List/ListConcat.scala b/testcases/condabd/benchmarks/List/ListConcat.scala
index 271082886e28c46bb98d6aa1d7e77e4036a9f39c..a4c4523454ad7e7d8df85cd165de2b1b8241fc0a 100644
--- a/testcases/condabd/benchmarks/List/ListConcat.scala
+++ b/testcases/condabd/benchmarks/List/ListConcat.scala
@@ -1,6 +1,5 @@
-import scala.collection.immutable.Set
-
import leon.lang._
+import leon.lang.synthesis._
object ListOperations {
sealed abstract class List
diff --git a/testcases/condabd/benchmarks/MergeSort/MergeSortMerge.scala b/testcases/condabd/benchmarks/MergeSort/MergeSortMerge.scala
index c43a3c598f6ab5b44898acd0bdff8cf1d34fdf24..1fadb1d803d96cd78377f2dbb52f355b3fcd2365 100644
--- a/testcases/condabd/benchmarks/MergeSort/MergeSortMerge.scala
+++ b/testcases/condabd/benchmarks/MergeSort/MergeSortMerge.scala
@@ -1,6 +1,5 @@
-import scala.collection.immutable.Set
-
import leon.lang._
+import leon.lang.synthesis._
object MergeSort {
sealed abstract class List
diff --git a/testcases/condabd/benchmarks/MergeSort/MergeSortSort.scala b/testcases/condabd/benchmarks/MergeSort/MergeSortSort.scala
index e96b37543e7636a2870d25cbf967e312e41f5cd5..feff019ed6b44024e001f7624a9c3c8db9791aad 100644
--- a/testcases/condabd/benchmarks/MergeSort/MergeSortSort.scala
+++ b/testcases/condabd/benchmarks/MergeSort/MergeSortSort.scala
@@ -1,6 +1,5 @@
-import scala.collection.immutable.Set
-
import leon.lang._
+import leon.lang.synthesis._
object MergeSort {
sealed abstract class List
diff --git a/testcases/condabd/benchmarks/MergeSort/MergeSortSortWithVal.scala b/testcases/condabd/benchmarks/MergeSort/MergeSortSortWithVal.scala
index 8df35ea8f7c2377cb1d883416bbfcc79627c7409..2f59d1ca59aad23cafd1f94437dc4e18188f3597 100644
--- a/testcases/condabd/benchmarks/MergeSort/MergeSortSortWithVal.scala
+++ b/testcases/condabd/benchmarks/MergeSort/MergeSortSortWithVal.scala
@@ -1,6 +1,5 @@
-import scala.collection.immutable.Set
-
import leon.lang._
+import leon.lang.synthesis._
object MergeSort {
sealed abstract class List
diff --git a/testcases/condabd/benchmarks/RedBlackTree/RedBlackTreeInsert.scala b/testcases/condabd/benchmarks/RedBlackTree/RedBlackTreeInsert.scala
index b32b6165ac0d8e7debdf74848b4c2c01f3b67ae5..b6336fab5794ca295c6ec4a72f4d1d0eabd3c11b 100644
--- a/testcases/condabd/benchmarks/RedBlackTree/RedBlackTreeInsert.scala
+++ b/testcases/condabd/benchmarks/RedBlackTree/RedBlackTreeInsert.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object RedBlackTree {
sealed abstract class Color
diff --git a/testcases/condabd/test/insynth/Addresses.scala b/testcases/condabd/test/insynth/Addresses.scala
index 8a958cca412c0ea1792187624936e7630e3fc1b3..48fa32d739b7eef780ac970068f7214c4084f425 100644
--- a/testcases/condabd/test/insynth/Addresses.scala
+++ b/testcases/condabd/test/insynth/Addresses.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Addresses {
diff --git a/testcases/condabd/test/insynth/AddressesWithAddition.scala b/testcases/condabd/test/insynth/AddressesWithAddition.scala
index c5df950772581d4d7f45007d45490fc398daf0f6..b9371603ad362f681bd3c14f37c51d009cbe9b35 100644
--- a/testcases/condabd/test/insynth/AddressesWithAddition.scala
+++ b/testcases/condabd/test/insynth/AddressesWithAddition.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object AddressesWithAddition {
diff --git a/testcases/condabd/test/insynth/ListConcat.scala b/testcases/condabd/test/insynth/ListConcat.scala
index 3091e9e472d094dcab1a5482ef14d4bba11144fb..bce1c20ea7bee5ed87fec0056e86fe99c1b0acd8 100644
--- a/testcases/condabd/test/insynth/ListConcat.scala
+++ b/testcases/condabd/test/insynth/ListConcat.scala
@@ -1,6 +1,5 @@
-import scala.collection.immutable.Set
-
import leon.lang._
+import leon.lang.synthesis._
object ListOperations {
diff --git a/testcases/condabd/test/lesynth/Addresses.scala b/testcases/condabd/test/lesynth/Addresses.scala
index 8a958cca412c0ea1792187624936e7630e3fc1b3..84870731196e01c342a6a0e4e3c189d19ac1e788 100644
--- a/testcases/condabd/test/lesynth/Addresses.scala
+++ b/testcases/condabd/test/lesynth/Addresses.scala
@@ -1,5 +1,5 @@
-import scala.collection.immutable.Set
import leon.annotation._
+import leon.lang.synthesis._
import leon.lang._
object Addresses {
diff --git a/testcases/condabd/test/lesynth/AddressesMergeAddressBooks.scala b/testcases/condabd/test/lesynth/AddressesMergeAddressBooks.scala
index a9154bc7694564291a819dfec6bc0bc641bbffdf..8436ef25f5ba3569b6b181847ed142f818dd63c8 100644
--- a/testcases/condabd/test/lesynth/AddressesMergeAddressBooks.scala
+++ b/testcases/condabd/test/lesynth/AddressesMergeAddressBooks.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Addresses {
case class Info(
diff --git a/testcases/condabd/test/lesynth/BinarySearchTree.scala b/testcases/condabd/test/lesynth/BinarySearchTree.scala
index fc49d721c04271af119eae1886282248a78c63ff..aee07c36702ae3122cd917812bdbd1359b3ea5a8 100644
--- a/testcases/condabd/test/lesynth/BinarySearchTree.scala
+++ b/testcases/condabd/test/lesynth/BinarySearchTree.scala
@@ -1,7 +1,6 @@
-import scala.collection.immutable.Set
-
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object BinarySearchTree {
sealed abstract class Tree
diff --git a/testcases/condabd/test/lesynth/InsertionSortInsert.scala b/testcases/condabd/test/lesynth/InsertionSortInsert.scala
index 7afa8f2b8ba2b90d6fc6e3da518f621e145a4425..7aa7fdd52f9869b9e387b9623c7bb68ba93d14c5 100644
--- a/testcases/condabd/test/lesynth/InsertionSortInsert.scala
+++ b/testcases/condabd/test/lesynth/InsertionSortInsert.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object InsertionSort {
sealed abstract class List
diff --git a/testcases/condabd/test/lesynth/ListConcat.scala b/testcases/condabd/test/lesynth/ListConcat.scala
index 3091e9e472d094dcab1a5482ef14d4bba11144fb..bce1c20ea7bee5ed87fec0056e86fe99c1b0acd8 100644
--- a/testcases/condabd/test/lesynth/ListConcat.scala
+++ b/testcases/condabd/test/lesynth/ListConcat.scala
@@ -1,6 +1,5 @@
-import scala.collection.immutable.Set
-
import leon.lang._
+import leon.lang.synthesis._
object ListOperations {
diff --git a/testcases/condabd/test/lesynth/ListConcatVerifierTest.scala b/testcases/condabd/test/lesynth/ListConcatVerifierTest.scala
index d3e1446ff2640b435998aae6060f82a1cf2c7389..51876f0d998fec48a7c1e1dca38c2a4e71c3b178 100644
--- a/testcases/condabd/test/lesynth/ListConcatVerifierTest.scala
+++ b/testcases/condabd/test/lesynth/ListConcatVerifierTest.scala
@@ -1,6 +1,5 @@
-import scala.collection.immutable.Set
-
import leon.lang._
+import leon.lang.synthesis._
object ListOperations {
sealed abstract class List
diff --git a/testcases/condabd/test/lesynth/ListConcatWithEmpty.scala b/testcases/condabd/test/lesynth/ListConcatWithEmpty.scala
index 5b6ae3e46024224597dc4a4af1150c88e7ad3385..8c6f1662f51a0631da127cc9a546b49e9b601432 100644
--- a/testcases/condabd/test/lesynth/ListConcatWithEmpty.scala
+++ b/testcases/condabd/test/lesynth/ListConcatWithEmpty.scala
@@ -1,6 +1,5 @@
-import scala.collection.immutable.Set
-
import leon.lang._
+import leon.lang.synthesis._
object ListOperations {
sealed abstract class List
diff --git a/testcases/condabd/test/lesynth/MergeSortSort.scala b/testcases/condabd/test/lesynth/MergeSortSort.scala
index e96b37543e7636a2870d25cbf967e312e41f5cd5..feff019ed6b44024e001f7624a9c3c8db9791aad 100644
--- a/testcases/condabd/test/lesynth/MergeSortSort.scala
+++ b/testcases/condabd/test/lesynth/MergeSortSort.scala
@@ -1,6 +1,5 @@
-import scala.collection.immutable.Set
-
import leon.lang._
+import leon.lang.synthesis._
object MergeSort {
sealed abstract class List
diff --git a/testcases/condabd/test/lesynth/RedBlackTreeInsert.scala b/testcases/condabd/test/lesynth/RedBlackTreeInsert.scala
index b32b6165ac0d8e7debdf74848b4c2c01f3b67ae5..b6336fab5794ca295c6ec4a72f4d1d0eabd3c11b 100644
--- a/testcases/condabd/test/lesynth/RedBlackTreeInsert.scala
+++ b/testcases/condabd/test/lesynth/RedBlackTreeInsert.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object RedBlackTree {
sealed abstract class Color
diff --git a/testcases/graveyard/Choose.scala b/testcases/graveyard/Choose.scala
index 0584edd430169825d3e1d6e5b2acc20e8d0f4b8b..7e69f6d92c7008ad29d76fae9dbf9cc4e489e4e2 100644
--- a/testcases/graveyard/Choose.scala
+++ b/testcases/graveyard/Choose.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.lang.synthesis._
object ChooseTest {
diff --git a/testcases/graveyard/Sat.scala b/testcases/graveyard/Sat.scala
index 28dd0057efbf97b5211111f6441e18761bd0847e..9e19d46667ad7dce612407248ce5a8f7bd182377 100644
--- a/testcases/graveyard/Sat.scala
+++ b/testcases/graveyard/Sat.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.lang.synthesis._
object Sat {
diff --git a/testcases/runtime/CachedList.scala b/testcases/runtime/CachedList.scala
index bf56ed8d1f991613c3068dd4f46c60abf8c84b6f..031503a9d8eb411d1c441caba98a8f0afbf441f3 100644
--- a/testcases/runtime/CachedList.scala
+++ b/testcases/runtime/CachedList.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.lang.synthesis._
object SortedList {
abstract class List
diff --git a/testcases/runtime/SquareRoot.scala b/testcases/runtime/SquareRoot.scala
index 9b0ea5c49440f9628a2326ad96a81ff60e2ccd31..87b3e985a6209da18606c28ca189440043b6e25d 100644
--- a/testcases/runtime/SquareRoot.scala
+++ b/testcases/runtime/SquareRoot.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.lang.synthesis._
object SquareRoot {
diff --git a/testcases/synthesis/ADTInduction.scala b/testcases/synthesis/ADTInduction.scala
index edd5ab10147b9c0b7d0b915a78f2c0edb1c810c7..0824a9928d71a5fc7d03be9aff39ce723b01193e 100644
--- a/testcases/synthesis/ADTInduction.scala
+++ b/testcases/synthesis/ADTInduction.scala
@@ -1,5 +1,5 @@
-import scala.collection.immutable.Set
import leon.annotation._
+import leon.lang.synthesis._
import leon.lang._
object SortedList {
diff --git a/testcases/synthesis/BinaryTree.scala b/testcases/synthesis/BinaryTree.scala
index a298ca980ff5108c7e118a6b3fd47d8c1dbfed88..b24a6ddbc07623dd877f3113e1965594cc867fab 100644
--- a/testcases/synthesis/BinaryTree.scala
+++ b/testcases/synthesis/BinaryTree.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object BinaryTree {
sealed abstract class Tree
diff --git a/testcases/synthesis/CegisExamples.scala b/testcases/synthesis/CegisExamples.scala
index 1c077055cdc7e545fc563890853ee769113a3da0..a43a3e948cb8dd4b775094fb349fa69c6968270c 100644
--- a/testcases/synthesis/CegisExamples.scala
+++ b/testcases/synthesis/CegisExamples.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.lang.synthesis._
object CegisTests {
sealed abstract class List
diff --git a/testcases/synthesis/CegisFunctions.scala b/testcases/synthesis/CegisFunctions.scala
index 3139d130e92ad9649e652e518c74a1a01759b4c1..92d79426ef3d3a5c47ce92c18e4295a3ea6ae060 100644
--- a/testcases/synthesis/CegisFunctions.scala
+++ b/testcases/synthesis/CegisFunctions.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.lang.synthesis._
object CegisTests {
sealed abstract class List
diff --git a/testcases/synthesis/ChooseArith.scala b/testcases/synthesis/ChooseArith.scala
index bee28c19dbbb327f5a9ae87e0f65be87d8ce111b..572cf790d0f5a55d2dd5b8a18ed1f33f6f8448ef 100644
--- a/testcases/synthesis/ChooseArith.scala
+++ b/testcases/synthesis/ChooseArith.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.lang.synthesis._
object ChooseArith {
def c1(a : Int) : (Int, Int) =
diff --git a/testcases/synthesis/ChooseIneq.scala b/testcases/synthesis/ChooseIneq.scala
index bb5921bea1ab83521ceff5976036eaf8b9f7efa7..127b047d35d221daecd1346c14e08854641d3428 100644
--- a/testcases/synthesis/ChooseIneq.scala
+++ b/testcases/synthesis/ChooseIneq.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.lang.synthesis._
object ChooseIneq {
def c1(a: Int, b: Int): (Int, Int) = {
diff --git a/testcases/synthesis/ChoosePos.scala b/testcases/synthesis/ChoosePos.scala
index decf2875d424d520267fa90673311d207a01fa89..cdacbd72bcabade3420e1ba9d9cfcd3b80956c14 100644
--- a/testcases/synthesis/ChoosePos.scala
+++ b/testcases/synthesis/ChoosePos.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.lang.synthesis._
object ChoosePos {
diff --git a/testcases/synthesis/ChurchNumerals.scala b/testcases/synthesis/ChurchNumerals.scala
index ba858741091239e6f5b9a65e6d9eed31edafe856..5f6f6c1cdc3b9a5e4adf2af4ec9c1e0fbff2ec95 100644
--- a/testcases/synthesis/ChurchNumerals.scala
+++ b/testcases/synthesis/ChurchNumerals.scala
@@ -1,4 +1,6 @@
import leon.lang._
+import leon.lang.synthesis._
+
object ChurchNumerals {
sealed abstract class Num
case class Zero() extends Num
diff --git a/testcases/synthesis/DrSuter.scala b/testcases/synthesis/DrSuter.scala
index 39b5d7edce186427c5b52a608250eea4001a9580..42adaa55be57e2c70751a556ac730239d419e5ee 100644
--- a/testcases/synthesis/DrSuter.scala
+++ b/testcases/synthesis/DrSuter.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.lang.synthesis._
object DrSuter {
diff --git a/testcases/synthesis/FastExp.scala b/testcases/synthesis/FastExp.scala
index c230771289952998e15d489aa80949beeb842e65..ef288f3bb960b0c0a6b656550d67405ecaa6f9f6 100644
--- a/testcases/synthesis/FastExp.scala
+++ b/testcases/synthesis/FastExp.scala
@@ -1,4 +1,5 @@
import leon.annotation._
+import leon.lang.synthesis._
import leon.lang._
object FastExp {
diff --git a/testcases/synthesis/FiniteSort.scala b/testcases/synthesis/FiniteSort.scala
index e4660ebb47107a7fce36335b97085e077e48994c..afe827bb76a857aea1e500aec7427585e11016d9 100644
--- a/testcases/synthesis/FiniteSort.scala
+++ b/testcases/synthesis/FiniteSort.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.lang.synthesis._
object FiniteSort {
diff --git a/testcases/synthesis/Injection.scala b/testcases/synthesis/Injection.scala
index 43a4be6768df1056387ef2eb9fc8466020c6cd08..5bc7a41b51624e2596e4fac22d1fac1f07f16f97 100644
--- a/testcases/synthesis/Injection.scala
+++ b/testcases/synthesis/Injection.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Injection {
sealed abstract class List
diff --git a/testcases/synthesis/InnerSplit.scala b/testcases/synthesis/InnerSplit.scala
index 7b2be7741dd6b703703b1c07391073a321a8870b..1db595ba9954f21f9aba9e14c77bc3e513d86fc7 100644
--- a/testcases/synthesis/InnerSplit.scala
+++ b/testcases/synthesis/InnerSplit.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.lang.synthesis._
object Test {
def test(x: Int, y: Int) = choose((z: Int) => z >= x && z >= y && (z == x || z == y))
diff --git a/testcases/synthesis/Justify.scala b/testcases/synthesis/Justify.scala
index 53a362f8a07c2d5a0259fc8c63a3df802f170105..c396d6a01ebbdb34ba398163bbf88a282712405f 100644
--- a/testcases/synthesis/Justify.scala
+++ b/testcases/synthesis/Justify.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.lang.synthesis._
object Justify {
diff --git a/testcases/synthesis/Matching.scala b/testcases/synthesis/Matching.scala
index 393d64c53a49908eb3a21adafab7b15b9744c208..861798cf7465e2622f69fcc70d8c48a32d6f4cb8 100644
--- a/testcases/synthesis/Matching.scala
+++ b/testcases/synthesis/Matching.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.lang.synthesis._
object Matching {
def t1(a: NatList) = choose( (x: Nat) => Cons(x, Nil()) == a)
diff --git a/testcases/synthesis/NewYearsSong.scala b/testcases/synthesis/NewYearsSong.scala
index 9a25333f51161e9fd5da91c5fbc000565256a450..0bcdf0130dd4dfc76b664a28e2bd19cadac75f0a 100644
--- a/testcases/synthesis/NewYearsSong.scala
+++ b/testcases/synthesis/NewYearsSong.scala
@@ -1,4 +1,4 @@
-import scala.collection.immutable.Set
+import leon.lang.synthesis._
import leon.annotation._
import leon.lang._
diff --git a/testcases/synthesis/ScaleWeight.scala b/testcases/synthesis/ScaleWeight.scala
index 6a47e288616fb51bfdbbcd8e4f1c4c434973ef38..52081df23c5dfc8d674548367ee9513077a11646 100644
--- a/testcases/synthesis/ScaleWeight.scala
+++ b/testcases/synthesis/ScaleWeight.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.lang.synthesis._
object ScaleWeight {
diff --git a/testcases/synthesis/Sec2Time.scala b/testcases/synthesis/Sec2Time.scala
index 68e5963c540e8f20a45a824e0c3110c48a8907c6..02ab40320580899844504233ffb8bfde2b35b6f9 100644
--- a/testcases/synthesis/Sec2Time.scala
+++ b/testcases/synthesis/Sec2Time.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.lang.synthesis._
object Sec2Time {
diff --git a/testcases/synthesis/Simple.scala b/testcases/synthesis/Simple.scala
index c8a7e24f8561fdb894ce357657b5a3d4f0b69797..0f1d8b76bfc0726d7d37086cd05c9587aacf3233 100644
--- a/testcases/synthesis/Simple.scala
+++ b/testcases/synthesis/Simple.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.lang.synthesis._
object SimpleSynthesis {
diff --git a/testcases/synthesis/SimplestCegis.scala b/testcases/synthesis/SimplestCegis.scala
index b4b574d64a6eb344f5005b8577515b16eb6f2134..804279046f0063cf8c2e0327799f23a3397f041a 100644
--- a/testcases/synthesis/SimplestCegis.scala
+++ b/testcases/synthesis/SimplestCegis.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Injection {
sealed abstract class List
diff --git a/testcases/synthesis/SortedList.scala b/testcases/synthesis/SortedList.scala
index 378b182ec0c63e95a754ded0abd30c51bc7315f6..b97642ef36176fbb0a25ca1698b9d96bc05d329a 100644
--- a/testcases/synthesis/SortedList.scala
+++ b/testcases/synthesis/SortedList.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object SortedList {
sealed abstract class List
diff --git a/testcases/synthesis/Spt.scala b/testcases/synthesis/Spt.scala
index 22d2457c826e60a0ba0940d21d61265b8a2bd20c..98cb72e9eefe77316844ca067beead97d9979465 100644
--- a/testcases/synthesis/Spt.scala
+++ b/testcases/synthesis/Spt.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.lang.synthesis._
// Examples taken from http://lara.epfl.ch/~psuter/spt/
object SynthesisProceduresToolkit {
diff --git a/testcases/synthesis/Unification.scala b/testcases/synthesis/Unification.scala
index a73a470c3dd24db5d9f050a6a5a307da75bc5227..121644deca6a35343c835e6aadc0f44457d284cc 100644
--- a/testcases/synthesis/Unification.scala
+++ b/testcases/synthesis/Unification.scala
@@ -1,4 +1,5 @@
import leon.lang._
+import leon.lang.synthesis._
object UnificationSynthesis {
diff --git a/testcases/synthesis/cav2013/AVLTree.scala b/testcases/synthesis/cav2013/AVLTree.scala
index b5e7c1dd864a8df099cf0f8058e0c3cde01c3836..c9b4b116e3a08b78e631e9d86cefc6e1ce229688 100644
--- a/testcases/synthesis/cav2013/AVLTree.scala
+++ b/testcases/synthesis/cav2013/AVLTree.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object AVLTree {
sealed abstract class Tree
diff --git a/testcases/synthesis/cav2013/BinaryTree.scala b/testcases/synthesis/cav2013/BinaryTree.scala
index e8c1bc742f6f6ff9b3609ebb822b23a7f8e325ef..84894af10cf0f7f1653798d6ef0f22091616f707 100644
--- a/testcases/synthesis/cav2013/BinaryTree.scala
+++ b/testcases/synthesis/cav2013/BinaryTree.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object BinaryTree {
sealed abstract class Tree
diff --git a/testcases/synthesis/cav2013/List.scala b/testcases/synthesis/cav2013/List.scala
index 37129a90dd95f37cb1295d31d6cf639d0b9a7f6a..08fcfc4c175dcbaad1985e8e0562a968fba4dc55 100644
--- a/testcases/synthesis/cav2013/List.scala
+++ b/testcases/synthesis/cav2013/List.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object List {
sealed abstract class List
diff --git a/testcases/synthesis/cav2013/ListByExample.scala b/testcases/synthesis/cav2013/ListByExample.scala
index 87737d02c7e6c7662f432c9154bdcf850d78317b..9b450f4ab7e570ab6cb256438983773ea330b03b 100644
--- a/testcases/synthesis/cav2013/ListByExample.scala
+++ b/testcases/synthesis/cav2013/ListByExample.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Lists {
sealed abstract class List
diff --git a/testcases/synthesis/cav2013/ManyTimeSec.scala b/testcases/synthesis/cav2013/ManyTimeSec.scala
index 2589c99ea4507c691431d2d89ba341e269a99910..3aba9ecac24ba6ae6c63e537bf47e18f1fed7e35 100644
--- a/testcases/synthesis/cav2013/ManyTimeSec.scala
+++ b/testcases/synthesis/cav2013/ManyTimeSec.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object ManyTimeSec {
case class Time(h:Int,m:Int,s:Int)
diff --git a/testcases/synthesis/cav2013/SortedList.scala b/testcases/synthesis/cav2013/SortedList.scala
index ba9bb3802e5380e9013014c00a15fc287e10d1d7..32b59d6011e3ca29ac0d3bff96c735ee29e56669 100644
--- a/testcases/synthesis/cav2013/SortedList.scala
+++ b/testcases/synthesis/cav2013/SortedList.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object SortedList {
sealed abstract class List
diff --git a/testcases/synthesis/cav2013/Sorting.scala b/testcases/synthesis/cav2013/Sorting.scala
index e031995d5d9421161e867f42d9bbdb161d4af1af..bdbd870c92cac14fb743251624f44536a39eab59 100644
--- a/testcases/synthesis/cav2013/Sorting.scala
+++ b/testcases/synthesis/cav2013/Sorting.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
// Sorting lists is a fundamental problem in CS.
object Sorting {
diff --git a/testcases/synthesis/cav2013/StrictlySortedList.scala b/testcases/synthesis/cav2013/StrictlySortedList.scala
index efd57e78f172d629462b91ee499616f28767e80d..dd6beeb36909d323d3625b9ff5867c182f735296 100644
--- a/testcases/synthesis/cav2013/StrictlySortedList.scala
+++ b/testcases/synthesis/cav2013/StrictlySortedList.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object SortedList {
sealed abstract class List
diff --git a/testcases/synthesis/cav2013/SynAddresses.scala b/testcases/synthesis/cav2013/SynAddresses.scala
index cf33e9a7358de0a464ed6d162234326d3f9e78ab..efb9a76a1d8ad49b11825666269b34fdf09dc7b2 100644
--- a/testcases/synthesis/cav2013/SynAddresses.scala
+++ b/testcases/synthesis/cav2013/SynAddresses.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Addresses {
// list of integers
diff --git a/testcases/synthesis/cav2013/SynTreeListSet.scala b/testcases/synthesis/cav2013/SynTreeListSet.scala
index d5b4d972a2740490df16a7039d5fa64060656607..23be38f875c4047aba8c2e4d3301706ef1c65f6d 100644
--- a/testcases/synthesis/cav2013/SynTreeListSet.scala
+++ b/testcases/synthesis/cav2013/SynTreeListSet.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object BinaryTree {
// list of integers
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBook.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBook.scala
index 02348024d1f2de125af654d20c34ed0ef3c38b12..cdcb8b1c962e078922e9797999ecd5b7c39fb17c 100644
--- a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBook.scala
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBook.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Addresses {
case class Info(
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookStrong.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookStrong.scala
index 9d3087669423ac567f1188ee96cb50b2c34182bf..5d4a788b8fd65aac5faee31e85cc10b4f53d07da 100644
--- a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookStrong.scala
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookStrong.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Addresses {
case class Info(
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookSynthWrong.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookSynthWrong.scala
index 76537952f27b729cc8bec21fe1768268167fbaf6..548bb98494293574668b940362492d4813e901fc 100644
--- a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookSynthWrong.scala
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookSynthWrong.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Addresses {
case class Info(
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookWithHelpers.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookWithHelpers.scala
index 96b1e6fd88ea937ff7d112238673956e11f8965f..194d194c35276356d2122770cbc1889c9647b9b2 100644
--- a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookWithHelpers.scala
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookWithHelpers.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Addresses {
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooks.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooks.scala
index 21fde00c582edeb128335679209c2b9db36e2ff2..a281e7423cef6266b00e8a0126b2ea66767dc46e 100644
--- a/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooks.scala
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooks.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Addresses {
case class Info(
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep1.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep1.scala
index 5235d651d517cd4ef0cecf1a2fb9ccfca89ce186..e3b6c8c7ef8130f37ba74800007e1c9a8f2bc857 100644
--- a/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep1.scala
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep1.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Addresses {
case class Info(
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep2.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep2.scala
index de45e44e8befe0f3605ff910822483f751eedcda..6729bbb2da63e3233118a9c49f089a0ad45e95ce 100644
--- a/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep2.scala
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep2.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Addresses {
case class Info(
diff --git a/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueCheckf.scala b/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueCheckf.scala
index 52e582ffb2c850f60dac404f375da2aa486f637f..7d85a2c9bb96d5eae615f33b3557ecbb4a709e8e 100644
--- a/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueCheckf.scala
+++ b/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueCheckf.scala
@@ -1,6 +1,5 @@
-import scala.collection.immutable.Set
-
import leon.lang._
+import leon.lang.synthesis._
object BatchedQueue {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueSnoc.scala b/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueSnoc.scala
index 26e70e64995bdf559add3538f4cd23355d1303f6..c595f8253a4501bd56d7ada06a96091587003595 100644
--- a/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueSnoc.scala
+++ b/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueSnoc.scala
@@ -1,6 +1,5 @@
-import scala.collection.immutable.Set
-
import leon.lang._
+import leon.lang.synthesis._
object BatchedQueue {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/BinaryTree/Batch.scala b/testcases/synthesis/oopsla2013/BinaryTree/Batch.scala
index 093c645f28c99276a4d04c26f72509dfe63d5ff9..1329aa1fe0366a0fbb314b51fd34cf6a087d1a33 100644
--- a/testcases/synthesis/oopsla2013/BinaryTree/Batch.scala
+++ b/testcases/synthesis/oopsla2013/BinaryTree/Batch.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object BinaryTree {
sealed abstract class Tree
diff --git a/testcases/synthesis/oopsla2013/BinaryTree/Complete.scala b/testcases/synthesis/oopsla2013/BinaryTree/Complete.scala
index c30bcdf788a76c58fada4053f6b8bfb91807be39..c863167738c5f78808b38bea7013ef10e5ce4bb7 100644
--- a/testcases/synthesis/oopsla2013/BinaryTree/Complete.scala
+++ b/testcases/synthesis/oopsla2013/BinaryTree/Complete.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object BinaryTree {
sealed abstract class Tree
diff --git a/testcases/synthesis/oopsla2013/BinaryTree/Delete.scala b/testcases/synthesis/oopsla2013/BinaryTree/Delete.scala
index 38b85a26371d4701cdb3bddd2f40e6ed0a10acd5..905c1aea49179ff05f64f4c5a20736db76e11ea2 100644
--- a/testcases/synthesis/oopsla2013/BinaryTree/Delete.scala
+++ b/testcases/synthesis/oopsla2013/BinaryTree/Delete.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object BinaryTree {
sealed abstract class Tree
diff --git a/testcases/synthesis/oopsla2013/BinaryTree/Diff.scala b/testcases/synthesis/oopsla2013/BinaryTree/Diff.scala
index 450cecc28cacabac813f8c92c1a7f2385a39c897..1b95fabe552d9f9dc3a80733b81be7c3a10f290d 100644
--- a/testcases/synthesis/oopsla2013/BinaryTree/Diff.scala
+++ b/testcases/synthesis/oopsla2013/BinaryTree/Diff.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object BinaryTree {
sealed abstract class Tree
diff --git a/testcases/synthesis/oopsla2013/BinaryTree/Insert.scala b/testcases/synthesis/oopsla2013/BinaryTree/Insert.scala
index d0a7e50f3c0aa3ab7f3e5e3b96bb400a9f9fa8c1..5a4ce2059868f91e2a0fce542f45530b84262f25 100644
--- a/testcases/synthesis/oopsla2013/BinaryTree/Insert.scala
+++ b/testcases/synthesis/oopsla2013/BinaryTree/Insert.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object BinaryTree {
sealed abstract class Tree
diff --git a/testcases/synthesis/oopsla2013/BinaryTree/Union.scala b/testcases/synthesis/oopsla2013/BinaryTree/Union.scala
index 776c21f0daeab2426c041436ffc772e9311d6421..40d20ec46ceebebea9dc0be97007645b6ecd6c37 100644
--- a/testcases/synthesis/oopsla2013/BinaryTree/Union.scala
+++ b/testcases/synthesis/oopsla2013/BinaryTree/Union.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object BinaryTree {
sealed abstract class Tree
diff --git a/testcases/synthesis/oopsla2013/Church/Add.scala b/testcases/synthesis/oopsla2013/Church/Add.scala
index f9374897c38824193ef6167ebcdda286f35c0690..937a13e38d79484bb1c888f4ebe34f7e473e9eef 100644
--- a/testcases/synthesis/oopsla2013/Church/Add.scala
+++ b/testcases/synthesis/oopsla2013/Church/Add.scala
@@ -1,4 +1,6 @@
import leon.lang._
+import leon.lang.synthesis._
+
object ChurchNumerals {
sealed abstract class Num
case object Z extends Num
diff --git a/testcases/synthesis/oopsla2013/Church/Batch.scala b/testcases/synthesis/oopsla2013/Church/Batch.scala
index 4129382d212fa1d6a0fe5c6f12db12b0fbda64a7..b511b94e6f3bba219529519beef9907978c63f47 100644
--- a/testcases/synthesis/oopsla2013/Church/Batch.scala
+++ b/testcases/synthesis/oopsla2013/Church/Batch.scala
@@ -1,4 +1,6 @@
import leon.lang._
+import leon.lang.synthesis._
+
object ChurchNumerals {
sealed abstract class Num
case object Z extends Num
diff --git a/testcases/synthesis/oopsla2013/Church/Complete.scala b/testcases/synthesis/oopsla2013/Church/Complete.scala
index 049bf442cd6c33eef2ffb30a88e7d4fe6e9d5cb2..94e94cc21ebe0ad49c8ff237954b1d07b708f476 100644
--- a/testcases/synthesis/oopsla2013/Church/Complete.scala
+++ b/testcases/synthesis/oopsla2013/Church/Complete.scala
@@ -1,4 +1,6 @@
import leon.lang._
+import leon.lang.synthesis._
+
object ChurchNumerals {
sealed abstract class Num
case object Z extends Num
diff --git a/testcases/synthesis/oopsla2013/Church/Distinct.scala b/testcases/synthesis/oopsla2013/Church/Distinct.scala
index 9472f04f7922f71d5819bef023b663479b13a5e6..5e718f3a0b1f200998afc9ede1b5a55ad1ac98ff 100644
--- a/testcases/synthesis/oopsla2013/Church/Distinct.scala
+++ b/testcases/synthesis/oopsla2013/Church/Distinct.scala
@@ -1,4 +1,6 @@
import leon.lang._
+import leon.lang.synthesis._
+
object ChurchNumerals {
sealed abstract class Num
case object Z extends Num
diff --git a/testcases/synthesis/oopsla2013/Church/Mult.scala b/testcases/synthesis/oopsla2013/Church/Mult.scala
index bb51979eaafdf4ab9a665666f2e11c6ace81cb98..70a6d68f4c3b30ee51063c16ef66a4a92eef4c97 100644
--- a/testcases/synthesis/oopsla2013/Church/Mult.scala
+++ b/testcases/synthesis/oopsla2013/Church/Mult.scala
@@ -1,4 +1,6 @@
import leon.lang._
+import leon.lang.synthesis._
+
object ChurchNumerals {
sealed abstract class Num
case object Z extends Num
diff --git a/testcases/synthesis/oopsla2013/Church/Squared.scala b/testcases/synthesis/oopsla2013/Church/Squared.scala
index 08a71c46288b4b6b0a9eb2d0763e06bc8387a763..b5b764d06ea5873b4fa8d9dad199ec7ca6e12c8d 100644
--- a/testcases/synthesis/oopsla2013/Church/Squared.scala
+++ b/testcases/synthesis/oopsla2013/Church/Squared.scala
@@ -1,4 +1,6 @@
import leon.lang._
+import leon.lang.synthesis._
+
object ChurchNumerals {
sealed abstract class Num
case object Z extends Num
diff --git a/testcases/synthesis/oopsla2013/InsertionSort/Insert.scala b/testcases/synthesis/oopsla2013/InsertionSort/Insert.scala
index a79a061330257fbaaac214f34e9073f5134329b6..cff8535f32b7f92262cfa7d35dd5409a0f760f51 100644
--- a/testcases/synthesis/oopsla2013/InsertionSort/Insert.scala
+++ b/testcases/synthesis/oopsla2013/InsertionSort/Insert.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object InsertionSort {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/InsertionSort/Sort.scala b/testcases/synthesis/oopsla2013/InsertionSort/Sort.scala
index 081819ec00542ff7d5f47fc6d968d38c7c71a3bf..11f9302794570b210c2f81d5c8d687169fd7ae64 100644
--- a/testcases/synthesis/oopsla2013/InsertionSort/Sort.scala
+++ b/testcases/synthesis/oopsla2013/InsertionSort/Sort.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object InsertionSort {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/List/Batch.scala b/testcases/synthesis/oopsla2013/List/Batch.scala
index c19c5347f8372de5f6d2d08ed4ba0f687d156de0..c7fcf02d0e0cca67121f132f02426b83ea0d5161 100644
--- a/testcases/synthesis/oopsla2013/List/Batch.scala
+++ b/testcases/synthesis/oopsla2013/List/Batch.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object List {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/List/Complete.scala b/testcases/synthesis/oopsla2013/List/Complete.scala
index 9a0a19d8460fb96accd012fd0d89daa7482a7b33..75377777ecd840af67baff0e6adcd0e2efe2d928 100644
--- a/testcases/synthesis/oopsla2013/List/Complete.scala
+++ b/testcases/synthesis/oopsla2013/List/Complete.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Complete {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/List/Delete.scala b/testcases/synthesis/oopsla2013/List/Delete.scala
index 998249371a3ed370b319990662061237e7c9eb9f..a61e312c9d60adc07c99685408c1f10bb8c81d14 100644
--- a/testcases/synthesis/oopsla2013/List/Delete.scala
+++ b/testcases/synthesis/oopsla2013/List/Delete.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Delete {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/List/Diff.scala b/testcases/synthesis/oopsla2013/List/Diff.scala
index a6c2c181db716f9f546c80df3c720987d2e985c4..dcf4f372cd805ed5f7d0f3e83fb9bbc51f77b2dc 100644
--- a/testcases/synthesis/oopsla2013/List/Diff.scala
+++ b/testcases/synthesis/oopsla2013/List/Diff.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Diff {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/List/Insert.scala b/testcases/synthesis/oopsla2013/List/Insert.scala
index 91862f1a6440df3d6dff68ab4e9b5560e922392a..3f6fcd23a5ce47cdc065506c679427b273775337 100644
--- a/testcases/synthesis/oopsla2013/List/Insert.scala
+++ b/testcases/synthesis/oopsla2013/List/Insert.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Insert {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/List/Split.scala b/testcases/synthesis/oopsla2013/List/Split.scala
index 649f0b8b1e50aece88c4095baf9a4e4b215950f9..e02c0a7a09efe73c05aca827eb9010d9b94bbb3a 100644
--- a/testcases/synthesis/oopsla2013/List/Split.scala
+++ b/testcases/synthesis/oopsla2013/List/Split.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Complete {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/List/Union.scala b/testcases/synthesis/oopsla2013/List/Union.scala
index c92d0c6c0bcba2cd53738e39e6943e4d365f45af..17dda5cfd9f016d8cfefcd119223b0d742bc5b6f 100644
--- a/testcases/synthesis/oopsla2013/List/Union.scala
+++ b/testcases/synthesis/oopsla2013/List/Union.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Union {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/MergeSort/MergeSortSort.scala b/testcases/synthesis/oopsla2013/MergeSort/MergeSortSort.scala
index e96b37543e7636a2870d25cbf967e312e41f5cd5..feff019ed6b44024e001f7624a9c3c8db9791aad 100644
--- a/testcases/synthesis/oopsla2013/MergeSort/MergeSortSort.scala
+++ b/testcases/synthesis/oopsla2013/MergeSort/MergeSortSort.scala
@@ -1,6 +1,5 @@
-import scala.collection.immutable.Set
-
import leon.lang._
+import leon.lang.synthesis._
object MergeSort {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/MergeSort/MergeSortSortWithVal.scala b/testcases/synthesis/oopsla2013/MergeSort/MergeSortSortWithVal.scala
index 8df35ea8f7c2377cb1d883416bbfcc79627c7409..2f59d1ca59aad23cafd1f94437dc4e18188f3597 100644
--- a/testcases/synthesis/oopsla2013/MergeSort/MergeSortSortWithVal.scala
+++ b/testcases/synthesis/oopsla2013/MergeSort/MergeSortSortWithVal.scala
@@ -1,6 +1,5 @@
-import scala.collection.immutable.Set
-
import leon.lang._
+import leon.lang.synthesis._
object MergeSort {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedBinaryTree/Batch.scala b/testcases/synthesis/oopsla2013/SortedBinaryTree/Batch.scala
index 643e824211a4e880e2be00641364157443c9d37a..a35eaca9f5a4d7fac794d52a737d7156d3219855 100644
--- a/testcases/synthesis/oopsla2013/SortedBinaryTree/Batch.scala
+++ b/testcases/synthesis/oopsla2013/SortedBinaryTree/Batch.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object BinaryTree {
sealed abstract class Tree
diff --git a/testcases/synthesis/oopsla2013/SortedList/Batch.scala b/testcases/synthesis/oopsla2013/SortedList/Batch.scala
index f96978e6cd5a83b616ca521c6da3f71c4e30324f..35e60c8d887185c4ffd8c896918ad74250670719 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Batch.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Batch.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object SortedList {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/Complete.scala b/testcases/synthesis/oopsla2013/SortedList/Complete.scala
index fecaa26a9d6b436bb2c121137ef64ab28144e704..b2465c9705c9d4299feb83226fb2654ddc724976 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Complete.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Complete.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Complete {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/Delete.scala b/testcases/synthesis/oopsla2013/SortedList/Delete.scala
index e858390aa374c6da50114cb6ef0952868b1540b8..b66aa8b3308a677d28634d18dc328b9fe2fd6e00 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Delete.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Delete.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Complete {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/Diff.scala b/testcases/synthesis/oopsla2013/SortedList/Diff.scala
index df5427f89c4c380ce0bf34f51388f7df5e4eca3f..45ff5133851208a5884408107a0f30885d9bbcff 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Diff.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Diff.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Complete {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/Insert1.scala b/testcases/synthesis/oopsla2013/SortedList/Insert1.scala
index fdd5d1d5f1667bc748ff1307e502c58cff79a4bc..b785401c1d8e3919620b550fe78910f394d23849 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Insert1.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Insert1.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Complete {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/Insert2.scala b/testcases/synthesis/oopsla2013/SortedList/Insert2.scala
index 159ebeaf294aeb98d66cb8f5b489e3e624b9325c..9b86ba2a0c74743a11a2877ee6ea575b49130c2d 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Insert2.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Insert2.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Complete {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/Sort.scala b/testcases/synthesis/oopsla2013/SortedList/Sort.scala
index bd4054c0d4eeceeb7b1487dcafd745693bd5da71..28e6de67b3ba357d13b8c7ad5461bba151848a1e 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Sort.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Sort.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Complete {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/SortInsert.scala b/testcases/synthesis/oopsla2013/SortedList/SortInsert.scala
index 6be3478ef0591d6d82cf8b0b0281def47a036374..b53ca0d05d4c40c7c66c5250a2d5a3e1114177fa 100644
--- a/testcases/synthesis/oopsla2013/SortedList/SortInsert.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/SortInsert.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Complete {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/SortMerge.scala b/testcases/synthesis/oopsla2013/SortedList/SortMerge.scala
index 8fefa5089e7f38b98d3c89689899faa5010ffca0..fb216a4c4d4278bf6499553d8220313f3ee89cd5 100644
--- a/testcases/synthesis/oopsla2013/SortedList/SortMerge.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/SortMerge.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Complete {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/SortMergeWithHint.scala b/testcases/synthesis/oopsla2013/SortedList/SortMergeWithHint.scala
index d9b74a8cdaf11bdcb31d66edc1cd91ce9d5256e7..06ed93ba9e5f715505eb53029bcbbd16fccee778 100644
--- a/testcases/synthesis/oopsla2013/SortedList/SortMergeWithHint.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/SortMergeWithHint.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Complete {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/Split.scala b/testcases/synthesis/oopsla2013/SortedList/Split.scala
index 10118f274f51b3dc64bac70e8c58bbb73bcf601f..77a883c6056befede247b84e6e1fc22860ed7a0f 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Split.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Split.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Complete {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/Split1.scala b/testcases/synthesis/oopsla2013/SortedList/Split1.scala
index 6ddf97b380a0b7b6884a90edcda6fcbbd1e4aebc..69a604755468e0e2d5bc6b38685de5f87769043a 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Split1.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Split1.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Complete {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/Split2.scala b/testcases/synthesis/oopsla2013/SortedList/Split2.scala
index 4317e993275c02f3489595558e4a9b4a43f997c9..c3f30be7f571060414cccc2b454787ce4ed1a001 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Split2.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Split2.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Complete {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/Split3.scala b/testcases/synthesis/oopsla2013/SortedList/Split3.scala
index 02d678eb3240d71fc2887803ac50a00e19f30d3d..eb27d44140f32c3ad3cfa974e36608d9d78d864a 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Split3.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Split3.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Complete {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/Union.scala b/testcases/synthesis/oopsla2013/SortedList/Union.scala
index c5b8ec1387b58c36fbb2f59128717f10fd514214..7681b838fe89811328c0abdcddbc7d46795fdc6c 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Union.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Union.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Complete {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SortedList/UnionIO.scala b/testcases/synthesis/oopsla2013/SortedList/UnionIO.scala
index 6590525f838b81dd379359e104097624e6f62859..8e851fd9ba6d5969cd9ff3b8f92ef9552d309b75 100644
--- a/testcases/synthesis/oopsla2013/SortedList/UnionIO.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/UnionIO.scala
@@ -1,6 +1,6 @@
-import scala.collection.immutable.Set
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Complete {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/SparseVector/Batch.scala b/testcases/synthesis/oopsla2013/SparseVector/Batch.scala
index 5a0582c98a90ded5b1337ac4d8df85cd341738dd..f7b603cd1e271888f22fbc790bed359c114ffd05 100644
--- a/testcases/synthesis/oopsla2013/SparseVector/Batch.scala
+++ b/testcases/synthesis/oopsla2013/SparseVector/Batch.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object SparseVector {
sealed abstract class SparseVector
diff --git a/testcases/synthesis/oopsla2013/SparseVector/Complete.scala b/testcases/synthesis/oopsla2013/SparseVector/Complete.scala
index 66be72a519492e974552fa88f0da53ba04bec9d5..2cf542ae5fc761e088836d37610ffb26b5dba061 100644
--- a/testcases/synthesis/oopsla2013/SparseVector/Complete.scala
+++ b/testcases/synthesis/oopsla2013/SparseVector/Complete.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object SparseVector {
sealed abstract class SparseVector
diff --git a/testcases/synthesis/oopsla2013/SparseVector/Delete.scala b/testcases/synthesis/oopsla2013/SparseVector/Delete.scala
index b821b2c80cfa28982956a29c682885d0d8abc19a..1f94b26352783c27862a8a713a0f2c42111aa98f 100644
--- a/testcases/synthesis/oopsla2013/SparseVector/Delete.scala
+++ b/testcases/synthesis/oopsla2013/SparseVector/Delete.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object SparseVector {
sealed abstract class SparseVector
diff --git a/testcases/synthesis/oopsla2013/SparseVector/Get.scala b/testcases/synthesis/oopsla2013/SparseVector/Get.scala
index 87e133dd6be56f028b3596d2995764351e372849..53e0c57527b63a7f46cd4121cb32a495050369af 100644
--- a/testcases/synthesis/oopsla2013/SparseVector/Get.scala
+++ b/testcases/synthesis/oopsla2013/SparseVector/Get.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object SparseVector {
sealed abstract class SparseVector
diff --git a/testcases/synthesis/oopsla2013/SparseVector/Set.scala b/testcases/synthesis/oopsla2013/SparseVector/Set.scala
index 2699fe291a5c406f478f1997557791a92e670e3a..8a5f379ea7231b2fca2171cdc219f4c5b7c68c72 100644
--- a/testcases/synthesis/oopsla2013/SparseVector/Set.scala
+++ b/testcases/synthesis/oopsla2013/SparseVector/Set.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object SparseVector {
sealed abstract class SparseVector
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Batch.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Batch.scala
index e5f8e453606bcfc316df9ce16719406bee0e2ee1..58d0e8b420e330913701207aa3117ab3b5d754f6 100644
--- a/testcases/synthesis/oopsla2013/StrictSortedList/Batch.scala
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Batch.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object StrictSortedList {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Complete.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Complete.scala
index 07ac7201a25d665121e3cc2c9a8edd002f40e861..fca32e4f17ab84ba708377873129534a00a86805 100644
--- a/testcases/synthesis/oopsla2013/StrictSortedList/Complete.scala
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Complete.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Complete {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Delete.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Delete.scala
index b75f09401699affd9efda788b48bcdda31df60d8..3fa6e78c70cf4bb38463eb5b28ffbafec94c7814 100644
--- a/testcases/synthesis/oopsla2013/StrictSortedList/Delete.scala
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Delete.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Delete {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Diff.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Diff.scala
index cd059f68d14315be454276bcc37dc4113f14ef03..31481b52eed0878f1ef3e212d46410a80a6bae9d 100644
--- a/testcases/synthesis/oopsla2013/StrictSortedList/Diff.scala
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Diff.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Complete {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Insert.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Insert.scala
index e8d7ff7f449881205923c50fe6edacf325a5a01e..d21176df0564636de0c5834e52de19a4ee808e24 100644
--- a/testcases/synthesis/oopsla2013/StrictSortedList/Insert.scala
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Insert.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Complete {
sealed abstract class List
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Union.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Union.scala
index 4d835f51afbfb1fc1fc0f09277736c59fbfd4286..595b11257f1176f30c7a732e12dd059a8ee43adb 100644
--- a/testcases/synthesis/oopsla2013/StrictSortedList/Union.scala
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Union.scala
@@ -1,5 +1,6 @@
import leon.annotation._
import leon.lang._
+import leon.lang.synthesis._
object Complete {
sealed abstract class List