From 8f2438cc67f4718d80e0f1b6f7e4156b31d812ab Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Wed, 9 Apr 2014 12:51:15 +0200
Subject: [PATCH] All-seeing synthesis with Oracles, library reorganisation
- NormalizationRule becomes priorities, so that we can have multiple
distinct layers
- Use the @library annotation, move synthesis stuff to synthesis,
Oracles.
- Make sure tests use PreprocessingPhase and import synthesis when
adequate
- Extract proper package objects fix patternRecons and simplifiers
- Reorganize library:
- leon.{choose,???} -> leon.lang.synthesis
- leon.{waypoint,epsilon} -> leon.lang.xlang
---
library/Option.scala | 6 +-
library/annotation/package.scala | 15 +-
library/collection/List.scala | 19 +-
library/lang/package.scala | 22 +-
library/lang/xlang/package.scala | 13 +
scripts/applyLicense.sh | 5 +-
src/main/scala/leon/LeonOption.scala | 36 +++
src/main/scala/leon/Main.scala | 23 +-
src/main/scala/leon/Pipeline.scala | 6 +-
src/main/scala/leon/Reporter.scala | 2 +-
src/main/scala/leon/Settings.scala | 6 +-
.../scala/leon/codegen/CodeGeneration.scala | 4 +
.../scala/leon/datagen/NaiveDataGen.scala | 15 +-
.../leon/evaluators/CodeGenEvaluator.scala | 2 +-
.../leon/evaluators/RecursiveEvaluator.scala | 2 +-
.../leon/frontends/scalac/ASTExtractors.scala | 114 +++++----
.../frontends/scalac/CodeExtraction.scala | 232 ++++++++++++------
.../frontends/scalac/ExtractionPhase.scala | 21 +-
.../scala/leon/purescala/Definitions.scala | 2 +-
.../scala/leon/purescala/PrettyPrinter.scala | 8 +-
.../leon/purescala/SimplifierWithPaths.scala | 9 +-
src/main/scala/leon/purescala/TreeOps.scala | 99 +++++++-
src/main/scala/leon/purescala/Trees.scala | 9 +-
.../leon/solvers/z3/AbstractZ3Solver.scala | 7 +-
.../leon/solvers/z3/FunctionTemplate.scala | 5 +-
.../scala/leon/synthesis/BoundedSearch.scala | 5 +-
.../scala/leon/synthesis/ChooseInfo.scala | 30 ++-
.../scala/leon/synthesis/ConvertHoles.scala | 101 --------
src/main/scala/leon/synthesis/CostModel.scala | 8 +-
.../scala/leon/synthesis/Heuristics.scala | 31 ---
.../scala/leon/synthesis/ManualSearch.scala | 25 +-
.../scala/leon/synthesis/ParallelSearch.scala | 21 +-
src/main/scala/leon/synthesis/Rules.scala | 92 ++++++-
.../scala/leon/synthesis/SimpleSearch.scala | 21 +-
src/main/scala/leon/synthesis/Solution.scala | 32 ++-
.../leon/synthesis/SynthesisContext.scala | 2 +
.../leon/synthesis/SynthesisOptions.scala | 1 +
.../scala/leon/synthesis/SynthesisPhase.scala | 17 +-
.../scala/leon/synthesis/Synthesizer.scala | 4 +-
.../synthesis/heuristics/ADTInduction.scala | 2 +-
.../heuristics/ADTLongInduction.scala | 4 +-
.../synthesis/heuristics/IntInduction.scala | 2 +-
.../heuristics/OptimisticInjection.scala | 2 +-
.../heuristics/SelectiveInlining.scala | 2 +-
.../leon/synthesis/rules/AngelicHoles.scala | 50 ++++
.../scala/leon/synthesis/rules/AsChoose.scala | 2 +-
.../scala/leon/synthesis/rules/Cegis.scala | 10 +-
.../scala/leon/synthesis/rules/Ground.scala | 2 +-
.../leon/synthesis/rules/InlineHoles.scala | 103 ++++++++
.../scala/leon/synthesis/rules/OnePoint.scala | 9 +-
.../synthesis/rules/OptimisticGround.scala | 2 +-
.../scala/leon/utils/OracleTraverser.scala | 32 +++
.../scala/leon/utils/PreprocessingPhase.scala | 24 ++
src/main/scala/leon/utils/TypingPhase.scala | 16 +-
.../leon/verification/AnalysisPhase.scala | 33 ++-
.../leon/verification/InductionTactic.scala | 4 +-
.../regression/synthesis/Church/Add.scala | 2 +
.../synthesis/Church/Distinct.scala | 1 +
.../regression/synthesis/Church/Mult.scala | 2 +
.../regression/synthesis/Church/Squared.scala | 2 +
.../regression/synthesis/Holes/Hole1.scala | 13 +
.../regression/synthesis/Holes/Hole2.scala | 17 ++
.../regression/synthesis/List/Delete.scala | 1 +
.../regression/synthesis/List/Diff.scala | 1 +
.../regression/synthesis/List/Insert.scala | 1 +
.../regression/synthesis/List/Split.scala | 1 +
.../regression/synthesis/List/Union.scala | 1 +
.../purescala/invalid/Choose1.scala | 1 +
.../purescala/valid/Choose1.scala | 1 +
.../purescala/valid/IsolatedAbstract.scala | 23 --
.../verification/xlang/invalid/Epsilon1.scala | 1 +
.../verification/xlang/invalid/Epsilon2.scala | 1 +
.../verification/xlang/invalid/Epsilon3.scala | 1 +
.../verification/xlang/invalid/Epsilon4.scala | 1 +
.../verification/xlang/invalid/Epsilon5.scala | 1 +
.../verification/xlang/invalid/Epsilon6.scala | 1 +
.../verification/xlang/valid/Choose1.scala | 1 +
.../verification/xlang/valid/Epsilon1.scala | 1 +
.../verification/xlang/valid/Epsilon2.scala | 1 +
.../verification/xlang/valid/Epsilon3.scala | 1 +
.../verification/xlang/valid/Epsilon4.scala | 1 +
.../verification/xlang/valid/Epsilon5.scala | 1 +
src/test/scala/leon/test/LeonTestSuite.scala | 15 +-
.../test/evaluators/EvaluatorsTests.scala | 5 +-
.../scala/leon/test/purescala/DataGen.scala | 26 +-
.../test/purescala/TransformationTests.scala | 4 +-
.../synthesis/SynthesisRegressionSuite.scala | 21 +-
.../leon/test/synthesis/SynthesisSuite.scala | 48 ++--
.../termination/TerminationRegression.scala | 2 +-
.../LibraryVerificationRegression.scala | 12 +-
.../PureScalaVerificationRegression.scala | 9 +-
.../XLangVerificationRegression.scala | 9 +-
testcases/case-studies/Lambda.scala | 1 +
.../AddressesMakeAddressBook.scala | 2 +-
.../AddressesMakeAddressBookWithHelpers.scala | 2 +-
.../AddressesMergeAddressBooks.scala | 2 +-
.../BatchedQueue/BatchedQueueCheckf.scala | 3 +-
.../BatchedQueue/BatchedQueueSnoc.scala | 3 +-
.../BatchedQueue/BatchedQueueSnocWeird.scala | 3 +-
.../BatchedQueue/BatchedQueueTail.scala | 3 +-
.../condabd/benchmarks/BinarySearch.scala | 1 +
.../BinarySearchTreeMember.scala | 3 +-
.../InsertionSort/InsertionSortInsert.scala | 2 +-
.../InsertionSort/InsertionSortSort.scala | 2 +-
.../condabd/benchmarks/List/ListConcat.scala | 3 +-
.../benchmarks/MergeSort/MergeSortMerge.scala | 3 +-
.../benchmarks/MergeSort/MergeSortSort.scala | 3 +-
.../MergeSort/MergeSortSortWithVal.scala | 3 +-
.../RedBlackTree/RedBlackTreeInsert.scala | 1 +
.../condabd/test/insynth/Addresses.scala | 2 +-
.../test/insynth/AddressesWithAddition.scala | 2 +-
.../condabd/test/insynth/ListConcat.scala | 3 +-
.../condabd/test/lesynth/Addresses.scala | 2 +-
.../lesynth/AddressesMergeAddressBooks.scala | 2 +-
.../test/lesynth/BinarySearchTree.scala | 3 +-
.../test/lesynth/InsertionSortInsert.scala | 2 +-
.../condabd/test/lesynth/ListConcat.scala | 3 +-
.../test/lesynth/ListConcatVerifierTest.scala | 3 +-
.../test/lesynth/ListConcatWithEmpty.scala | 3 +-
.../condabd/test/lesynth/MergeSortSort.scala | 3 +-
.../test/lesynth/RedBlackTreeInsert.scala | 1 +
testcases/graveyard/Choose.scala | 1 +
testcases/graveyard/Sat.scala | 1 +
testcases/runtime/CachedList.scala | 1 +
testcases/runtime/SquareRoot.scala | 1 +
testcases/synthesis/ADTInduction.scala | 2 +-
testcases/synthesis/BinaryTree.scala | 2 +-
testcases/synthesis/CegisExamples.scala | 1 +
testcases/synthesis/CegisFunctions.scala | 1 +
testcases/synthesis/ChooseArith.scala | 1 +
testcases/synthesis/ChooseIneq.scala | 1 +
testcases/synthesis/ChoosePos.scala | 1 +
testcases/synthesis/ChurchNumerals.scala | 2 +
testcases/synthesis/DrSuter.scala | 1 +
testcases/synthesis/FastExp.scala | 1 +
testcases/synthesis/FiniteSort.scala | 1 +
testcases/synthesis/Injection.scala | 2 +-
testcases/synthesis/InnerSplit.scala | 1 +
testcases/synthesis/Justify.scala | 1 +
testcases/synthesis/Matching.scala | 1 +
testcases/synthesis/NewYearsSong.scala | 2 +-
testcases/synthesis/ScaleWeight.scala | 1 +
testcases/synthesis/Sec2Time.scala | 1 +
testcases/synthesis/Simple.scala | 1 +
testcases/synthesis/SimplestCegis.scala | 2 +-
testcases/synthesis/SortedList.scala | 2 +-
testcases/synthesis/Spt.scala | 1 +
testcases/synthesis/Unification.scala | 1 +
testcases/synthesis/cav2013/AVLTree.scala | 2 +-
testcases/synthesis/cav2013/BinaryTree.scala | 2 +-
testcases/synthesis/cav2013/List.scala | 2 +-
.../synthesis/cav2013/ListByExample.scala | 2 +-
testcases/synthesis/cav2013/ManyTimeSec.scala | 2 +-
testcases/synthesis/cav2013/SortedList.scala | 2 +-
testcases/synthesis/cav2013/Sorting.scala | 1 +
.../cav2013/StrictlySortedList.scala | 2 +-
.../synthesis/cav2013/SynAddresses.scala | 2 +-
.../synthesis/cav2013/SynTreeListSet.scala | 2 +-
.../AddressesMakeAddressBook.scala | 2 +-
.../AddressesMakeAddressBookStrong.scala | 2 +-
.../AddressesMakeAddressBookSynthWrong.scala | 2 +-
.../AddressesMakeAddressBookWithHelpers.scala | 2 +-
.../AddressesMergeAddressBooks.scala | 2 +-
.../AddressesMergeAddressBooksStep1.scala | 2 +-
.../AddressesMergeAddressBooksStep2.scala | 2 +-
.../BatchedQueue/BatchedQueueCheckf.scala | 3 +-
.../BatchedQueue/BatchedQueueSnoc.scala | 3 +-
.../oopsla2013/BinaryTree/Batch.scala | 1 +
.../oopsla2013/BinaryTree/Complete.scala | 1 +
.../oopsla2013/BinaryTree/Delete.scala | 1 +
.../oopsla2013/BinaryTree/Diff.scala | 1 +
.../oopsla2013/BinaryTree/Insert.scala | 1 +
.../oopsla2013/BinaryTree/Union.scala | 1 +
.../synthesis/oopsla2013/Church/Add.scala | 2 +
.../synthesis/oopsla2013/Church/Batch.scala | 2 +
.../oopsla2013/Church/Complete.scala | 2 +
.../oopsla2013/Church/Distinct.scala | 2 +
.../synthesis/oopsla2013/Church/Mult.scala | 2 +
.../synthesis/oopsla2013/Church/Squared.scala | 2 +
.../oopsla2013/InsertionSort/Insert.scala | 2 +-
.../oopsla2013/InsertionSort/Sort.scala | 2 +-
.../synthesis/oopsla2013/List/Batch.scala | 1 +
.../synthesis/oopsla2013/List/Complete.scala | 1 +
.../synthesis/oopsla2013/List/Delete.scala | 1 +
.../synthesis/oopsla2013/List/Diff.scala | 1 +
.../synthesis/oopsla2013/List/Insert.scala | 1 +
.../synthesis/oopsla2013/List/Split.scala | 1 +
.../synthesis/oopsla2013/List/Union.scala | 1 +
.../oopsla2013/MergeSort/MergeSortSort.scala | 3 +-
.../MergeSort/MergeSortSortWithVal.scala | 3 +-
.../oopsla2013/SortedBinaryTree/Batch.scala | 2 +-
.../oopsla2013/SortedList/Batch.scala | 1 +
.../oopsla2013/SortedList/Complete.scala | 1 +
.../oopsla2013/SortedList/Delete.scala | 1 +
.../oopsla2013/SortedList/Diff.scala | 1 +
.../oopsla2013/SortedList/Insert1.scala | 1 +
.../oopsla2013/SortedList/Insert2.scala | 1 +
.../oopsla2013/SortedList/Sort.scala | 1 +
.../oopsla2013/SortedList/SortInsert.scala | 1 +
.../oopsla2013/SortedList/SortMerge.scala | 1 +
.../SortedList/SortMergeWithHint.scala | 1 +
.../oopsla2013/SortedList/Split.scala | 1 +
.../oopsla2013/SortedList/Split1.scala | 1 +
.../oopsla2013/SortedList/Split2.scala | 1 +
.../oopsla2013/SortedList/Split3.scala | 1 +
.../oopsla2013/SortedList/Union.scala | 2 +-
.../oopsla2013/SortedList/UnionIO.scala | 2 +-
.../oopsla2013/SparseVector/Batch.scala | 1 +
.../oopsla2013/SparseVector/Complete.scala | 1 +
.../oopsla2013/SparseVector/Delete.scala | 1 +
.../oopsla2013/SparseVector/Get.scala | 1 +
.../oopsla2013/SparseVector/Set.scala | 1 +
.../oopsla2013/StrictSortedList/Batch.scala | 1 +
.../StrictSortedList/Complete.scala | 1 +
.../oopsla2013/StrictSortedList/Delete.scala | 1 +
.../oopsla2013/StrictSortedList/Diff.scala | 1 +
.../oopsla2013/StrictSortedList/Insert.scala | 1 +
.../oopsla2013/StrictSortedList/Union.scala | 1 +
218 files changed, 1187 insertions(+), 622 deletions(-)
create mode 100644 library/lang/xlang/package.scala
delete mode 100644 src/main/scala/leon/synthesis/ConvertHoles.scala
create mode 100644 src/main/scala/leon/synthesis/rules/AngelicHoles.scala
create mode 100644 src/main/scala/leon/synthesis/rules/InlineHoles.scala
create mode 100644 src/main/scala/leon/utils/OracleTraverser.scala
create mode 100644 src/main/scala/leon/utils/PreprocessingPhase.scala
create mode 100644 src/test/resources/regression/synthesis/Holes/Hole1.scala
create mode 100644 src/test/resources/regression/synthesis/Holes/Hole2.scala
delete mode 100644 src/test/resources/regression/verification/purescala/valid/IsolatedAbstract.scala
diff --git a/library/Option.scala b/library/Option.scala
index 8aff85e7c..e35fc9a0f 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 68cf4e4c6..1aa564cbd 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 622cdb77b..f2f629243 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 8cb68e7a1..41cd25b65 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 000000000..928498a47
--- /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 7bf0aa64f..cc809905d 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 c9c989e23..fa5c0929f 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 7a30d6530..f2cba94b7 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 82125a9af..64a618129 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 4e4963bdb..18e93f870 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 bd4910f4c..66034599f 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 f1ff028aa..9a36ab329 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 6dc3865c9..b1727fb71 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 158547f13..abdbec318 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 ecad71452..92f2b579f 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 d5aec11a0..97fbbc2ac 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 720aef319..95912df29 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 cb771c9d2..f538a0d92 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 a82ff2446..ac99c1146 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 b04aa62fc..c8a1f666b 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 70cc667a4..406e4c46b 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 5a8eb3913..e68f47a48 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 a7a46e3c6..b7624a842 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 35b50b8ee..168b8e193 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 ad173d712..9fe4be2cc 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 41bc86894..5430d05d2 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 2295ff3dc..85f51ee66 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 57cc7bf59..000000000
--- 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 75bdb7f4a..85e5285ee 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 d48e94385..5c3fe9a07 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 5964eadc4..137d79c68 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 e8eb0fbce..b0af9cab8 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 9fd44cb0f..aa79a1470 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 491188cef..b069a1c73 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 ef04d34b8..c504eadac 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 b699c8bc8..47bac7559 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 90f0e3c84..706fc69ff 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 98e8a8d6e..e68dbf292 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 11189cefc..483dc9b36 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 f3136fbbb..87e4b14c8 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 5ab3f672b..9c29ec859 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 ac01105b4..37cf77a0b 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 e33c3eee3..7cd1e2342 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 3de094c8c..dc7bf0526 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 000000000..07c5f687f
--- /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 5aefa03dc..fc43972f0 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 4cd54bf9e..83c5a3bf4 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 96a1e1250..52e5e0c13 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 000000000..82fb1d135
--- /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 df0e4965f..2091e67dc 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 f5cdb08ac..148085a5a 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 000000000..d70d1fb5d
--- /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 000000000..896e16c78
--- /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 1dc7b5616..a3e1f3e61 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 7b1a1bea3..17d0222b3 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 df08846ca..70824c7ed 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 542550eb1..d060360c2 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 c702d3c14..3e503f4ab 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 8251e0a2f..39c0286d0 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 bf390fea7..9328e70ff 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 000000000..084185b0e
--- /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 000000000..3a10748eb
--- /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 113eedb44..02f13ec38 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 a6bebd642..5ae469ea7 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 21a758ece..13c1294d7 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 944ee9d0b..989d509da 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 3b3130d7f..a4acf629b 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 74e7f0db5..20d588523 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 408dafa87..2b033c809 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 52077b354..000000000
--- 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 b6eb6a05d..f1878f35d 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 ee620237f..45c4adf79 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 b12fcbbe0..ec44138ca 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 22beb0849..5437d93b3 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 75f9dd813..18eb98709 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 0fadb7414..7cdf4fc28 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 0ea5e5122..893db3e78 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 108ea6477..b9af3dc12 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 dbdb96c9a..289bdd4d1 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 541933cd8..ece6f7bf0 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 8b7f7af3b..49cd971fa 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 565e99ec2..008cef836 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 be5f00802..9b460d584 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 77237afc0..055eb3ed6 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 c9b19e5e4..9259e483a 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 e358e1436..d3123f4d2 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 38971a80b..32eee19c2 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 b7cefba50..ab07f8116 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 6fa590904..65f20d036 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 bf54de007..a1d7c2690 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 18d39fa76..4bfd35e92 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 89eaaca64..726b039e0 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 ecc82053d..05df4cf57 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 ccd1d6ad3..e7067c756 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 f04399105..3dfd21465 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 a9154bc76..8436ef25f 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 52e582ffb..7d85a2c9b 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 26e70e649..c595f8253 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 f74b8d8ea..2a82511d5 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 31b67f6a8..4c7d22df9 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 b8883a3bb..40f91c988 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 5ca4fb8c3..661e02e5c 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 7afa8f2b8..7aa7fdd52 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 823011be4..21fc426ca 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 271082886..a4c452345 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 c43a3c598..1fadb1d80 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 e96b37543..feff019ed 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 8df35ea8f..2f59d1ca5 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 b32b6165a..b6336fab5 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 8a958cca4..48fa32d73 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 c5df95077..b9371603a 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 3091e9e47..bce1c20ea 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 8a958cca4..848707311 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 a9154bc76..8436ef25f 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 fc49d721c..aee07c367 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 7afa8f2b8..7aa7fdd52 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 3091e9e47..bce1c20ea 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 d3e1446ff..51876f0d9 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 5b6ae3e46..8c6f1662f 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 e96b37543..feff019ed 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 b32b6165a..b6336fab5 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 0584edd43..7e69f6d92 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 28dd0057e..9e19d4666 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 bf56ed8d1..031503a9d 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 9b0ea5c49..87b3e985a 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 edd5ab101..0824a9928 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 a298ca980..b24a6ddbc 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 1c077055c..a43a3e948 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 3139d130e..92d79426e 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 bee28c19d..572cf790d 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 bb5921bea..127b047d3 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 decf2875d..cdacbd72b 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 ba8587410..5f6f6c1cd 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 39b5d7edc..42adaa55b 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 c23077128..ef288f3bb 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 e4660ebb4..afe827bb7 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 43a4be676..5bc7a41b5 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 7b2be7741..1db595ba9 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 53a362f8a..c396d6a01 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 393d64c53..861798cf7 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 9a25333f5..0bcdf0130 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 6a47e2886..52081df23 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 68e5963c5..02ab40320 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 c8a7e24f8..0f1d8b76b 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 b4b574d64..804279046 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 378b182ec..b97642ef3 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 22d2457c8..98cb72e9e 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 a73a470c3..121644dec 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 b5e7c1dd8..c9b4b116e 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 e8c1bc742..84894af10 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 37129a90d..08fcfc4c1 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 87737d02c..9b450f4ab 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 2589c99ea..3aba9ecac 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 ba9bb3802..32b59d601 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 e031995d5..bdbd870c9 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 efd57e78f..dd6beeb36 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 cf33e9a73..efb9a76a1 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 d5b4d972a..23be38f87 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 02348024d..cdcb8b1c9 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 9d3087669..5d4a788b8 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 76537952f..548bb9849 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 96b1e6fd8..194d194c3 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 21fde00c5..a281e7423 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 5235d651d..e3b6c8c7e 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 de45e44e8..6729bbb2d 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 52e582ffb..7d85a2c9b 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 26e70e649..c595f8253 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 093c645f2..1329aa1fe 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 c30bcdf78..c86316773 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 38b85a263..905c1aea4 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 450cecc28..1b95fabe5 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 d0a7e50f3..5a4ce2059 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 776c21f0d..40d20ec46 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 f9374897c..937a13e38 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 4129382d2..b511b94e6 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 049bf442c..94e94cc21 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 9472f04f7..5e718f3a0 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 bb51979ea..70a6d68f4 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 08a71c462..b5b764d06 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 a79a06133..cff8535f3 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 081819ec0..11f930279 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 c19c5347f..c7fcf02d0 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 9a0a19d84..75377777e 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 998249371..a61e312c9 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 a6c2c181d..dcf4f372c 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 91862f1a6..3f6fcd23a 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 649f0b8b1..e02c0a7a0 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 c92d0c6c0..17dda5cfd 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 e96b37543..feff019ed 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 8df35ea8f..2f59d1ca5 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 643e82421..a35eaca9f 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 f96978e6c..35e60c8d8 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 fecaa26a9..b2465c970 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 e858390aa..b66aa8b33 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 df5427f89..45ff51338 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 fdd5d1d5f..b785401c1 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 159ebeaf2..9b86ba2a0 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 bd4054c0d..28e6de67b 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 6be3478ef..b53ca0d05 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 8fefa5089..fb216a4c4 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 d9b74a8cd..06ed93ba9 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 10118f274..77a883c60 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 6ddf97b38..69a604755 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 4317e9932..c3f30be7f 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 02d678eb3..eb27d4414 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 c5b8ec138..7681b838f 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 6590525f8..8e851fd9b 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 5a0582c98..f7b603cd1 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 66be72a51..2cf542ae5 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 b821b2c80..1f94b2635 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 87e133dd6..53e0c5752 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 2699fe291..8a5f379ea 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 e5f8e4536..58d0e8b42 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 07ac7201a..fca32e4f1 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 b75f09401..3fa6e78c7 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 cd059f68d..31481b52e 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 e8d7ff7f4..d21176df0 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 4d835f51a..595b11257 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
--
GitLab