diff --git a/runTests.sh b/runTests.sh
index edf8d289c5e6bea10b5eb206c541d6d6592e8e11..938f44ba34fc9c5fd93edcc1d4c2ebcb603d9537 100755
--- a/runTests.sh
+++ b/runTests.sh
@@ -15,10 +15,12 @@ echo "################################" >> $summaryLog
echo "# Category, File, function, p.S, fuS, foS, Tms, Fms, Rms, verif?" >> $summaryLog
#All benchmarks:
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar1.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar2.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar3.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar4.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar testcases/repair/Compiler/Compiler1.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar testcases/repair/Compiler/Compiler2.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar testcases/repair/Compiler/Compiler3.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar testcases/repair/Compiler/Compiler4.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=simplify testcases/repair/Compiler/Compiler5.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=simplify testcases/repair/Compiler/Compiler6.scala | tee -a $fullLog
./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort3.scala | tee -a $fullLog
./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort4.scala | tee -a $fullLog
diff --git a/src/main/scala/leon/repair/RepairResult.scala b/src/main/scala/leon/repair/RepairResult.scala
index 85dc7a5d5d4fbe3bd87e64fa2044d2fc62e13e3f..697434d6fbb78db68e534169bdff0b3f143bfb1d 100644
--- a/src/main/scala/leon/repair/RepairResult.scala
+++ b/src/main/scala/leon/repair/RepairResult.scala
@@ -23,7 +23,7 @@ case class RepairResult(f: File,
}
def toTableLine = {
- val benchCat = f.getParentFile().getName()
+ val benchCat = f.getAbsoluteFile().getParentFile().getName()
val benchName = f.getName()
val benchFun = name
diff --git a/testcases/repair/Compiler/Compiler.scala b/testcases/repair/Compiler/Compiler.scala
new file mode 100644
index 0000000000000000000000000000000000000000..697f333e0c5c8adcbd555734f939c3e501a85bff
--- /dev/null
+++ b/testcases/repair/Compiler/Compiler.scala
@@ -0,0 +1,212 @@
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon._
+
+object Trees {
+ abstract class Expr
+ case class Plus(lhs: Expr, rhs: Expr) extends Expr
+ case class Minus(lhs: Expr, rhs: Expr) extends Expr
+ case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+ case class And(lhs: Expr, rhs: Expr) extends Expr
+ case class Or(lhs: Expr, rhs: Expr) extends Expr
+ case class Not(e : Expr) extends Expr
+ case class Eq(lhs: Expr, rhs: Expr) extends Expr
+ case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+ case class IntLiteral(v: Int) extends Expr
+ case class BoolLiteral(b : Boolean) extends Expr
+}
+
+object Types {
+ abstract class Type
+ case object IntType extends Type
+ case object BoolType extends Type
+}
+
+
+object TypeChecker {
+ import Trees._
+ import Types._
+
+ def typeOf(e :Expr) : Option[Type] = e match {
+ case Plus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case Minus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case LessThan(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(BoolType)
+ case _ => None()
+ }
+ case And(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Or(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Not(e) => typeOf(e) match {
+ case Some(BoolType) => Some(BoolType)
+ case _ => None()
+ }
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case (Some(t1), Some(t2)) if t1 == t2 => Some(BoolType)
+ case _ => None()
+ }
+ case Ite(c, th, el) => (typeOf(c), typeOf(th), typeOf(el)) match {
+ case (Some(BoolType), Some(t1), Some(t2)) if t1 == t2 => Some(t1)
+ case _ => None()
+ }
+ case IntLiteral(_) => Some(IntType)
+ case BoolLiteral(_) => Some(BoolType)
+ }
+
+ def typeChecks(e : Expr) = typeOf(e).isDefined
+}
+
+
+object Semantics {
+ import Trees._
+ import Types._
+ import TypeChecker._
+
+ def semI(t : Expr) : Int = {
+ require( typeOf(t) == ( Some(IntType) : Option[Type] ))
+ t match {
+ case Plus(lhs , rhs) => semI(lhs) + semI(rhs)
+ case Minus(lhs , rhs) => semI(lhs) - semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semI(thn) else semI(els)
+ case IntLiteral(v) => v
+ }
+ }
+
+ def semB(t : Expr) : Boolean = {
+ require( (Some(BoolType): Option[Type]) == typeOf(t))
+ t match {
+ case And(lhs, rhs ) => semB(lhs) && semB(rhs)
+ case Or(lhs , rhs ) => semB(lhs) || semB(rhs)
+ case Not(e) => !semB(e)
+ case LessThan(lhs, rhs) => semI(lhs) < semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semB(thn) else semB(els)
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case ( Some(IntType), Some(IntType) ) => semI(lhs) == semI(rhs)
+ case ( Some(BoolType), Some(BoolType) ) => semB(lhs) == semB(rhs)
+ }
+ case BoolLiteral(b) => b
+ }
+ }
+
+ def b2i(b : Boolean) = if (b) 1 else 0
+
+ @induct
+ def semUntyped( t : Expr) : Int = { t match {
+ case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
+ case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case Or(lhs, rhs ) =>
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ case Not(e) =>
+ b2i(semUntyped(e) == 0)
+ case LessThan(lhs, rhs) =>
+ b2i(semUntyped(lhs) < semUntyped(rhs))
+ case Eq(lhs, rhs) =>
+ b2i(semUntyped(lhs) == semUntyped(rhs))
+ case Ite(cond, thn, els) =>
+ if (semUntyped(cond) == 0) semUntyped(els) else semUntyped(thn)
+ case IntLiteral(v) => v
+ case BoolLiteral(b) => b2i(b)
+ }} ensuring { res => typeOf(t) match {
+ case Some(IntType) => res == semI(t)
+ case Some(BoolType) => res == b2i(semB(t))
+ case None() => true
+ }}
+
+}
+
+
+object Desugar {
+ import Types._
+ import TypeChecker._
+ import Semantics.b2i
+
+ abstract class SimpleE
+ case class Plus(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Neg(arg : SimpleE) extends SimpleE
+ case class Ite(cond : SimpleE, thn : SimpleE, els : SimpleE) extends SimpleE
+ case class Eq(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class LessThan(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Literal(i : Int) extends SimpleE
+
+ @induct
+ def desugar(e : Trees.Expr) : SimpleE = { e match {
+ case Trees.Plus (lhs, rhs) => Plus(desugar(lhs), desugar(rhs))
+ case Trees.Minus(lhs, rhs) => Plus(desugar(lhs), Neg(desugar(rhs)))
+ case Trees.LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
+ case Trees.And (lhs, rhs) => Ite(desugar(lhs), desugar(rhs), Literal(0))
+ case Trees.Or (lhs, rhs) => Ite(desugar(lhs), Literal(1), desugar(rhs))
+ case Trees.Not(e) => Ite(desugar(e), Literal(0), Literal(1))
+ case Trees.Eq(lhs, rhs) =>
+ Eq(desugar(lhs), desugar(rhs))
+ case Trees.Ite(cond, thn, els) => Ite(desugar(cond), desugar(thn), desugar(els))
+ case Trees.IntLiteral(v) => Literal(v)
+ case Trees.BoolLiteral(b) => Literal(b2i(b))
+ }} ensuring { res =>
+ sem(res) == Semantics.semUntyped(e)
+ }
+
+ def sem(e : SimpleE) : Int = e match {
+ case Plus (lhs, rhs) => sem(lhs) + sem(rhs)
+ case Ite(cond, thn, els) => if (sem(cond) != 0) sem(thn) else sem(els)
+ case Neg(arg) => -sem(arg)
+ case Eq(lhs,rhs) => b2i(sem(lhs) == sem(rhs))
+ case LessThan(lhs, rhs) => b2i(sem(lhs) < sem(rhs))
+ case Literal(i) => i
+ }
+
+}
+
+object Evaluator {
+ import Trees._
+
+ def bToi(b: Boolean) = if (b) 1 else 0
+ def iTob(i: Int) = i == 1
+
+ def eval(e: Expr): Int = {
+ e match {
+ case Plus(lhs, rhs) => eval(lhs) + eval(rhs)
+ case Minus(lhs, rhs) => eval(lhs) + eval(rhs)
+ case LessThan(lhs, rhs) => bToi(eval(lhs) < eval(rhs))
+ case And(lhs, rhs) => bToi(iTob(eval(lhs)) && iTob(eval(rhs)))
+ case Or(lhs, rhs) => bToi(iTob(eval(lhs)) || iTob(eval(rhs)))
+ case Not(e) => bToi(!iTob(eval(e)))
+ case Eq(lhs, rhs) => bToi(eval(lhs) == eval(rhs))
+ case Ite(cond, thn, els) => if (iTob(eval(cond))) eval(thn) else eval(els)
+ case IntLiteral(v) => v
+ case BoolLiteral(b) => bToi(b)
+ }
+ }
+}
+
+object Simplifier {
+ import Trees._
+ import Evaluator._
+
+ @induct
+ def simplify(e: Expr): Expr = {
+ e match {
+ case And(BoolLiteral(false), _) => BoolLiteral(false)
+ case Or(BoolLiteral(true), _) => BoolLiteral(true)
+ case Plus(IntLiteral(a), IntLiteral(b)) => IntLiteral(a+b)
+ case Not(Not(Not(a))) => Not(a)
+ case e => e
+ }
+ } ensuring {
+ res => eval(res) == eval(e)
+ }
+}
diff --git a/testcases/repair/Compiler/Compiler1.scala b/testcases/repair/Compiler/Compiler1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2971855c71b9b765f457886ade24c313595a60f3
--- /dev/null
+++ b/testcases/repair/Compiler/Compiler1.scala
@@ -0,0 +1,176 @@
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon._
+
+object Trees {
+ abstract class Expr
+ case class Plus(lhs: Expr, rhs: Expr) extends Expr
+ case class Minus(lhs: Expr, rhs: Expr) extends Expr
+ case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+ case class And(lhs: Expr, rhs: Expr) extends Expr
+ case class Or(lhs: Expr, rhs: Expr) extends Expr
+ case class Not(e : Expr) extends Expr
+ case class Eq(lhs: Expr, rhs: Expr) extends Expr
+ case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+ case class IntLiteral(v: Int) extends Expr
+ case class BoolLiteral(b : Boolean) extends Expr
+}
+
+object Types {
+ abstract class Type
+ case object IntType extends Type
+ case object BoolType extends Type
+}
+
+
+object TypeChecker {
+ import Trees._
+ import Types._
+
+ def typeOf(e :Expr) : Option[Type] = e match {
+ case Plus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case Minus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case LessThan(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(BoolType)
+ case _ => None()
+ }
+ case And(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Or(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Not(e) => typeOf(e) match {
+ case Some(BoolType) => Some(BoolType)
+ case _ => None()
+ }
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case (Some(t1), Some(t2)) if t1 == t2 => Some(BoolType)
+ case _ => None()
+ }
+ case Ite(c, th, el) => (typeOf(c), typeOf(th), typeOf(el)) match {
+ case (Some(BoolType), Some(t1), Some(t2)) if t1 == t2 => Some(t1)
+ case _ => None()
+ }
+ case IntLiteral(_) => Some(IntType)
+ case BoolLiteral(_) => Some(BoolType)
+ }
+
+ def typeChecks(e : Expr) = typeOf(e).isDefined
+}
+
+
+object Semantics {
+ import Trees._
+ import Types._
+ import TypeChecker._
+
+ def semI(t : Expr) : Int = {
+ require( typeOf(t) == ( Some(IntType) : Option[Type] ))
+ t match {
+ case Plus(lhs , rhs) => semI(lhs) + semI(rhs)
+ case Minus(lhs , rhs) => semI(lhs) - semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semI(thn) else semI(els)
+ case IntLiteral(v) => v
+ }
+ }
+
+ def semB(t : Expr) : Boolean = {
+ require( (Some(BoolType): Option[Type]) == typeOf(t))
+ t match {
+ case And(lhs, rhs ) => semB(lhs) && semB(rhs)
+ case Or(lhs , rhs ) => semB(lhs) || semB(rhs)
+ case Not(e) => !semB(e)
+ case LessThan(lhs, rhs) => semI(lhs) < semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semB(thn) else semB(els)
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case ( Some(IntType), Some(IntType) ) => semI(lhs) == semI(rhs)
+ case ( Some(BoolType), Some(BoolType) ) => semB(lhs) == semB(rhs)
+ }
+ case BoolLiteral(b) => b
+ }
+ }
+
+ def b2i(b : Boolean) = if (b) 1 else 0
+
+ @induct
+ def semUntyped( t : Expr) : Int = { t match {
+ case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
+ case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case Or(lhs, rhs ) =>
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ case Not(e) =>
+ b2i(semUntyped(e) == 0)
+ case LessThan(lhs, rhs) =>
+ b2i(semUntyped(lhs) < semUntyped(rhs))
+ case Eq(lhs, rhs) =>
+ b2i(semUntyped(lhs) == semUntyped(rhs))
+ case Ite(cond, thn, els) =>
+ if (semUntyped(cond) == 0) semUntyped(els) else semUntyped(thn)
+ case IntLiteral(v) => v
+ case BoolLiteral(b) => b2i(b)
+ }} ensuring { res => typeOf(t) match {
+ case Some(IntType) => res == semI(t)
+ case Some(BoolType) => res == b2i(semB(t))
+ case None() => true
+ }}
+
+}
+
+
+object Desugar {
+ import Types._
+ import TypeChecker._
+ import Semantics.b2i
+
+ abstract class SimpleE
+ case class Plus(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Neg(arg : SimpleE) extends SimpleE
+ case class Ite(cond : SimpleE, thn : SimpleE, els : SimpleE) extends SimpleE
+ case class Eq(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class LessThan(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Literal(i : Int) extends SimpleE
+
+ @induct
+ def desugar(e : Trees.Expr) : SimpleE = { e match {
+ case Trees.Plus (lhs, rhs) => Neg(desugar(lhs)) // FIXME: Complete nonsense. Leon can't disprove it, uses example...
+ case Trees.Minus(lhs, rhs) => Plus(desugar(lhs), Neg(desugar(rhs)))
+ case Trees.LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
+ case Trees.And (lhs, rhs) => Ite(desugar(lhs), desugar(rhs), Literal(0))
+ case Trees.Or (lhs, rhs) => Ite(desugar(lhs), Literal(1), desugar(rhs))
+ case Trees.Not(e) => Ite(desugar(e), Literal(0), Literal(1))
+ case Trees.Eq(lhs, rhs) =>
+ Eq(desugar(lhs), desugar(rhs))
+ case Trees.Ite(cond, thn, els) => Ite(desugar(cond), desugar(thn), desugar(els))
+ case Trees.IntLiteral(v) => Literal(v)
+ case Trees.BoolLiteral(b) => Literal(b2i(b))
+ }} ensuring { res =>
+ ((e, res) passes {
+ case Trees.Plus(Trees.IntLiteral(i), Trees.Minus(Trees.IntLiteral(j), Trees.IntLiteral(42))) =>
+ Plus(Literal(i), Plus(Literal(j), Neg(Literal(42))))
+ }) &&
+ sem(res) == Semantics.semUntyped(e)
+ }
+
+ def sem(e : SimpleE) : Int = e match {
+ case Plus (lhs, rhs) => sem(lhs) + sem(rhs)
+ case Ite(cond, thn, els) => if (sem(cond) != 0) sem(thn) else sem(els)
+ case Neg(arg) => -sem(arg)
+ case Eq(lhs,rhs) => b2i(sem(lhs) == sem(rhs))
+ case LessThan(lhs, rhs) => b2i(sem(lhs) < sem(rhs))
+ case Literal(i) => i
+ }
+
+}
diff --git a/testcases/repair/Compiler/Compiler2.scala b/testcases/repair/Compiler/Compiler2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a068dadcba0e35683147b8141bb53e38eb01f7a4
--- /dev/null
+++ b/testcases/repair/Compiler/Compiler2.scala
@@ -0,0 +1,175 @@
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon._
+
+object Trees {
+ abstract class Expr
+ case class Plus(lhs: Expr, rhs: Expr) extends Expr
+ case class Minus(lhs: Expr, rhs: Expr) extends Expr
+ case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+ case class And(lhs: Expr, rhs: Expr) extends Expr
+ case class Or(lhs: Expr, rhs: Expr) extends Expr
+ case class Not(e : Expr) extends Expr
+ case class Eq(lhs: Expr, rhs: Expr) extends Expr
+ case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+ case class IntLiteral(v: Int) extends Expr
+ case class BoolLiteral(b : Boolean) extends Expr
+}
+
+object Types {
+ abstract class Type
+ case object IntType extends Type
+ case object BoolType extends Type
+}
+
+
+object TypeChecker {
+ import Trees._
+ import Types._
+
+ def typeOf(e :Expr) : Option[Type] = e match {
+ case Plus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case Minus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case LessThan(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(BoolType)
+ case _ => None()
+ }
+ case And(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Or(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Not(e) => typeOf(e) match {
+ case Some(BoolType) => Some(BoolType)
+ case _ => None()
+ }
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case (Some(t1), Some(t2)) if t1 == t2 => Some(BoolType)
+ case _ => None()
+ }
+ case Ite(c, th, el) => (typeOf(c), typeOf(th), typeOf(el)) match {
+ case (Some(BoolType), Some(t1), Some(t2)) if t1 == t2 => Some(t1)
+ case _ => None()
+ }
+ case IntLiteral(_) => Some(IntType)
+ case BoolLiteral(_) => Some(BoolType)
+ }
+
+ def typeChecks(e : Expr) = typeOf(e).isDefined
+}
+
+
+object Semantics {
+ import Trees._
+ import Types._
+ import TypeChecker._
+
+ def semI(t : Expr) : Int = {
+ require( typeOf(t) == ( Some(IntType) : Option[Type] ))
+ t match {
+ case Plus(lhs , rhs) => semI(lhs) + semI(rhs)
+ case Minus(lhs , rhs) => semI(lhs) - semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semI(thn) else semI(els)
+ case IntLiteral(v) => v
+ }
+ }
+
+ def semB(t : Expr) : Boolean = {
+ require( (Some(BoolType): Option[Type]) == typeOf(t))
+ t match {
+ case And(lhs, rhs ) => semB(lhs) && semB(rhs)
+ case Or(lhs , rhs ) => semB(lhs) || semB(rhs)
+ case Not(e) => !semB(e)
+ case LessThan(lhs, rhs) => semI(lhs) < semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semB(thn) else semB(els)
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case ( Some(IntType), Some(IntType) ) => semI(lhs) == semI(rhs)
+ case ( Some(BoolType), Some(BoolType) ) => semB(lhs) == semB(rhs)
+ }
+ case BoolLiteral(b) => b
+ }
+ }
+
+ def b2i(b : Boolean) = if (b) 1 else 0
+
+ @induct
+ def semUntyped( t : Expr) : Int = { t match {
+ case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
+ case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case Or(lhs, rhs ) =>
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ case Not(e) =>
+ b2i(semUntyped(e) == 0)
+ case LessThan(lhs, rhs) =>
+ b2i(semUntyped(lhs) < semUntyped(rhs))
+ case Eq(lhs, rhs) =>
+ b2i(semUntyped(lhs) == semUntyped(rhs))
+ case Ite(cond, thn, els) =>
+ if (semUntyped(cond) == 0) semUntyped(els) else semUntyped(thn)
+ case IntLiteral(v) => v
+ case BoolLiteral(b) => b2i(b)
+ }} ensuring { res => typeOf(t) match {
+ case Some(IntType) => res == semI(t)
+ case Some(BoolType) => res == b2i(semB(t))
+ case None() => true
+ }}
+
+}
+
+
+object Desugar {
+ import Types._
+ import TypeChecker._
+ import Semantics.b2i
+
+ abstract class SimpleE
+ case class Plus(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Neg(arg : SimpleE) extends SimpleE
+ case class Ite(cond : SimpleE, thn : SimpleE, els : SimpleE) extends SimpleE
+ case class Eq(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class LessThan(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Literal(i : Int) extends SimpleE
+
+ @induct
+ def desugar(e : Trees.Expr) : SimpleE = { e match {
+ case Trees.Plus (lhs, rhs) => Plus(desugar(lhs), desugar(rhs))
+ case Trees.Minus(lhs, rhs) => Literal(0)//Plus(desugar(lhs), desugar(rhs)) // FIXME forgot Neg
+ case Trees.LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
+ case Trees.And (lhs, rhs) => Ite(desugar(lhs), desugar(rhs), Literal(0))
+ case Trees.Or (lhs, rhs) => Ite(desugar(lhs), Literal(1), desugar(rhs))
+ case Trees.Not(e) => Ite(desugar(e), Literal(0), Literal(1))
+ case Trees.Eq(lhs, rhs) =>
+ Eq(desugar(lhs), desugar(rhs))
+ case Trees.Ite(cond, thn, els) => Ite(desugar(cond), desugar(thn), desugar(els))
+ case Trees.IntLiteral(v) => Literal(v)
+ case Trees.BoolLiteral(b) => Literal(b2i(b))
+ }} ensuring { res =>
+ sem(res) == Semantics.semUntyped(e) && ((e,res) passes {
+ case Trees.Minus(Trees.IntLiteral(42), Trees.IntLiteral(i)) =>
+ Plus(Literal(42), Neg(Literal(i)))
+ })
+ }
+
+ def sem(e : SimpleE) : Int = e match {
+ case Plus (lhs, rhs) => sem(lhs) + sem(rhs)
+ case Ite(cond, thn, els) => if (sem(cond) != 0) sem(thn) else sem(els)
+ case Neg(arg) => -sem(arg)
+ case Eq(lhs,rhs) => b2i(sem(lhs) == sem(rhs))
+ case LessThan(lhs, rhs) => b2i(sem(lhs) < sem(rhs))
+ case Literal(i) => i
+ }
+
+}
diff --git a/testcases/repair/Compiler/Compiler3.scala b/testcases/repair/Compiler/Compiler3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ec61a78a5fb3e5a16a344daf979079f3df78b205
--- /dev/null
+++ b/testcases/repair/Compiler/Compiler3.scala
@@ -0,0 +1,173 @@
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon._
+
+object Trees {
+ abstract class Expr
+ case class Plus(lhs: Expr, rhs: Expr) extends Expr
+ case class Minus(lhs: Expr, rhs: Expr) extends Expr
+ case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+ case class And(lhs: Expr, rhs: Expr) extends Expr
+ case class Or(lhs: Expr, rhs: Expr) extends Expr
+ case class Not(e : Expr) extends Expr
+ case class Eq(lhs: Expr, rhs: Expr) extends Expr
+ case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+ case class IntLiteral(v: Int) extends Expr
+ case class BoolLiteral(b : Boolean) extends Expr
+}
+
+object Types {
+ abstract class Type
+ case object IntType extends Type
+ case object BoolType extends Type
+}
+
+
+object TypeChecker {
+ import Trees._
+ import Types._
+
+ def typeOf(e :Expr) : Option[Type] = e match {
+ case Plus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case Minus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case LessThan(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(BoolType)
+ case _ => None()
+ }
+ case And(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Or(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Not(e) => typeOf(e) match {
+ case Some(BoolType) => Some(BoolType)
+ case _ => None()
+ }
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case (Some(t1), Some(t2)) if t1 == t2 => Some(BoolType)
+ case _ => None()
+ }
+ case Ite(c, th, el) => (typeOf(c), typeOf(th), typeOf(el)) match {
+ case (Some(BoolType), Some(t1), Some(t2)) if t1 == t2 => Some(t1)
+ case _ => None()
+ }
+ case IntLiteral(_) => Some(IntType)
+ case BoolLiteral(_) => Some(BoolType)
+ }
+
+ def typeChecks(e : Expr) = typeOf(e).isDefined
+}
+
+
+object Semantics {
+ import Trees._
+ import Types._
+ import TypeChecker._
+
+ def semI(t : Expr) : Int = {
+ require( typeOf(t) == ( Some(IntType) : Option[Type] ))
+ t match {
+ case Plus(lhs , rhs) => semI(lhs) + semI(rhs)
+ case Minus(lhs , rhs) => semI(lhs) - semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semI(thn) else semI(els)
+ case IntLiteral(v) => v
+ }
+ }
+
+ def semB(t : Expr) : Boolean = {
+ require( (Some(BoolType): Option[Type]) == typeOf(t))
+ t match {
+ case And(lhs, rhs ) => semB(lhs) && semB(rhs)
+ case Or(lhs , rhs ) => semB(lhs) || semB(rhs)
+ case Not(e) => !semB(e)
+ case LessThan(lhs, rhs) => semI(lhs) < semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semB(thn) else semB(els)
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case ( Some(IntType), Some(IntType) ) => semI(lhs) == semI(rhs)
+ case ( Some(BoolType), Some(BoolType) ) => semB(lhs) == semB(rhs)
+ }
+ case BoolLiteral(b) => b
+ }
+ }
+
+ def b2i(b : Boolean) = if (b) 1 else 0
+
+ @induct
+ def semUntyped( t : Expr) : Int = { t match {
+ case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
+ case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case Or(lhs, rhs ) =>
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ case Not(e) =>
+ b2i(semUntyped(e) == 0)
+ case LessThan(lhs, rhs) =>
+ b2i(semUntyped(lhs) < semUntyped(rhs))
+ case Eq(lhs, rhs) =>
+ b2i(semUntyped(lhs) == semUntyped(rhs))
+ case Ite(cond, thn, els) =>
+ if (semUntyped(cond) == 0) semUntyped(els) else semUntyped(thn)
+ case IntLiteral(v) => v
+ case BoolLiteral(b) => b2i(b)
+ }} ensuring { res => typeOf(t) match {
+ case Some(IntType) => res == semI(t)
+ case Some(BoolType) => res == b2i(semB(t))
+ case None() => true
+ }}
+
+}
+
+
+object Desugar {
+ import Types._
+ import TypeChecker._
+ import Semantics.b2i
+
+ abstract class SimpleE
+ case class Plus(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Neg(arg : SimpleE) extends SimpleE
+ case class Ite(cond : SimpleE, thn : SimpleE, els : SimpleE) extends SimpleE
+ case class Eq(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class LessThan(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Literal(i : Int) extends SimpleE
+
+ @induct
+ def desugar(e : Trees.Expr) : SimpleE = { e match {
+ case Trees.Plus (lhs, rhs) => Plus(desugar(lhs), desugar(rhs))
+ case Trees.Minus(lhs, rhs) => Plus(desugar(lhs), Neg(desugar(rhs)))
+ case Trees.LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
+ case Trees.And (lhs, rhs) => Ite(desugar(lhs), desugar(rhs), Literal(0))
+ case Trees.Or (lhs, rhs) => Ite(desugar(lhs), Literal(1), desugar(rhs))
+ case Trees.Not(e) => Ite(desugar(e), Literal(0), Literal(1))
+ case Trees.Eq(lhs, rhs) =>
+ Eq(desugar(lhs), desugar(rhs))
+ // FIXME switched the branches
+ case Trees.Ite(cond, thn, els) => Ite(desugar(cond), desugar(els), desugar(thn))
+ case Trees.IntLiteral(v) => Literal(v)
+ case Trees.BoolLiteral(b) => Literal(b2i(b))
+ }} ensuring { res =>
+ sem(res) == Semantics.semUntyped(e)
+ }
+
+ def sem(e : SimpleE) : Int = e match {
+ case Plus (lhs, rhs) => sem(lhs) + sem(rhs)
+ case Ite(cond, thn, els) => if (sem(cond) != 0) sem(thn) else sem(els)
+ case Neg(arg) => -sem(arg)
+ case Eq(lhs,rhs) => b2i(sem(lhs) == sem(rhs))
+ case LessThan(lhs, rhs) => b2i(sem(lhs) < sem(rhs))
+ case Literal(i) => i
+ }
+
+}
diff --git a/testcases/repair/Compiler/Compiler4.scala b/testcases/repair/Compiler/Compiler4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9f6ac963a2d04e47b66e4eadb172dc19abb4094a
--- /dev/null
+++ b/testcases/repair/Compiler/Compiler4.scala
@@ -0,0 +1,172 @@
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon._
+
+object Trees {
+ abstract class Expr
+ case class Plus(lhs: Expr, rhs: Expr) extends Expr
+ case class Minus(lhs: Expr, rhs: Expr) extends Expr
+ case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+ case class And(lhs: Expr, rhs: Expr) extends Expr
+ case class Or(lhs: Expr, rhs: Expr) extends Expr
+ case class Not(e : Expr) extends Expr
+ case class Eq(lhs: Expr, rhs: Expr) extends Expr
+ case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+ case class IntLiteral(v: Int) extends Expr
+ case class BoolLiteral(b : Boolean) extends Expr
+}
+
+object Types {
+ abstract class Type
+ case object IntType extends Type
+ case object BoolType extends Type
+}
+
+
+object TypeChecker {
+ import Trees._
+ import Types._
+
+ def typeOf(e :Expr) : Option[Type] = e match {
+ case Plus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case Minus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case LessThan(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(BoolType)
+ case _ => None()
+ }
+ case And(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Or(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Not(e) => typeOf(e) match {
+ case Some(BoolType) => Some(BoolType)
+ case _ => None()
+ }
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case (Some(t1), Some(t2)) if t1 == t2 => Some(BoolType)
+ case _ => None()
+ }
+ case Ite(c, th, el) => (typeOf(c), typeOf(th), typeOf(el)) match {
+ case (Some(BoolType), Some(t1), Some(t2)) if t1 == t2 => Some(t1)
+ case _ => None()
+ }
+ case IntLiteral(_) => Some(IntType)
+ case BoolLiteral(_) => Some(BoolType)
+ }
+
+ def typeChecks(e : Expr) = typeOf(e).isDefined
+}
+
+
+object Semantics {
+ import Trees._
+ import Types._
+ import TypeChecker._
+
+ def semI(t : Expr) : Int = {
+ require( typeOf(t) == ( Some(IntType) : Option[Type] ))
+ t match {
+ case Plus(lhs , rhs) => semI(lhs) + semI(rhs)
+ case Minus(lhs , rhs) => semI(lhs) - semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semI(thn) else semI(els)
+ case IntLiteral(v) => v
+ }
+ }
+
+ def semB(t : Expr) : Boolean = {
+ require( (Some(BoolType): Option[Type]) == typeOf(t))
+ t match {
+ case And(lhs, rhs ) => semB(lhs) && semB(rhs)
+ case Or(lhs , rhs ) => semB(lhs) || semB(rhs)
+ case Not(e) => !semB(e)
+ case LessThan(lhs, rhs) => semI(lhs) < semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semB(thn) else semB(els)
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case ( Some(IntType), Some(IntType) ) => semI(lhs) == semI(rhs)
+ case ( Some(BoolType), Some(BoolType) ) => semB(lhs) == semB(rhs)
+ }
+ case BoolLiteral(b) => b
+ }
+ }
+
+ def b2i(b : Boolean) = if (b) 1 else 0
+
+ @induct
+ def semUntyped( t : Expr) : Int = { t match {
+ case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
+ case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case Or(lhs, rhs ) =>
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ case Not(e) =>
+ b2i(semUntyped(e) == 0)
+ case LessThan(lhs, rhs) =>
+ b2i(semUntyped(lhs) < semUntyped(rhs))
+ case Eq(lhs, rhs) =>
+ b2i(semUntyped(lhs) == semUntyped(rhs))
+ case Ite(cond, thn, els) =>
+ if (semUntyped(cond) == 0) semUntyped(els) else semUntyped(thn)
+ case IntLiteral(v) => v
+ case BoolLiteral(b) => b2i(b)
+ }} ensuring { res => typeOf(t) match {
+ case Some(IntType) => res == semI(t)
+ case Some(BoolType) => res == b2i(semB(t))
+ case None() => true
+ }}
+
+}
+
+
+object Desugar {
+ import Types._
+ import TypeChecker._
+ import Semantics.b2i
+
+ abstract class SimpleE
+ case class Plus(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Neg(arg : SimpleE) extends SimpleE
+ case class Ite(cond : SimpleE, thn : SimpleE, els : SimpleE) extends SimpleE
+ case class Eq(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class LessThan(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Literal(i : Int) extends SimpleE
+
+ @induct
+ def desugar(e : Trees.Expr) : SimpleE = { e match {
+ case Trees.Plus (lhs, rhs) => Plus(desugar(lhs), desugar(rhs))
+ case Trees.Minus(lhs, rhs) => Plus(desugar(lhs), Neg(desugar(rhs)))
+ case Trees.LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
+ case Trees.And (lhs, rhs) => Ite(desugar(lhs), desugar(rhs), Literal(0))
+ case Trees.Or (lhs, rhs) => Ite(desugar(lhs), Literal(1), desugar(rhs))
+ case Trees.Not(e) => Ite(desugar(e), Literal(1), Literal(1)) // FIXME else should be 0
+ case Trees.Eq(lhs, rhs) =>
+ Eq(desugar(lhs), desugar(rhs))
+ case Trees.Ite(cond, thn, els) => Ite(desugar(cond), desugar(thn), desugar(els))
+ case Trees.IntLiteral(v) => Literal(v)
+ case Trees.BoolLiteral(b) => Literal(b2i(b))
+ }} ensuring { res =>
+ sem(res) == Semantics.semUntyped(e)
+ }
+
+ def sem(e : SimpleE) : Int = e match {
+ case Plus (lhs, rhs) => sem(lhs) + sem(rhs)
+ case Ite(cond, thn, els) => if (sem(cond) != 0) sem(thn) else sem(els)
+ case Neg(arg) => -sem(arg)
+ case Eq(lhs,rhs) => b2i(sem(lhs) == sem(rhs))
+ case LessThan(lhs, rhs) => b2i(sem(lhs) < sem(rhs))
+ case Literal(i) => i
+ }
+
+}
diff --git a/testcases/repair/Compiler/Compiler5.scala b/testcases/repair/Compiler/Compiler5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..95003d1afe6e56bdf4ab42dbff6c24227f41abc2
--- /dev/null
+++ b/testcases/repair/Compiler/Compiler5.scala
@@ -0,0 +1,212 @@
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon._
+
+object Trees {
+ abstract class Expr
+ case class Plus(lhs: Expr, rhs: Expr) extends Expr
+ case class Minus(lhs: Expr, rhs: Expr) extends Expr
+ case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+ case class And(lhs: Expr, rhs: Expr) extends Expr
+ case class Or(lhs: Expr, rhs: Expr) extends Expr
+ case class Not(e : Expr) extends Expr
+ case class Eq(lhs: Expr, rhs: Expr) extends Expr
+ case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+ case class IntLiteral(v: Int) extends Expr
+ case class BoolLiteral(b : Boolean) extends Expr
+}
+
+object Types {
+ abstract class Type
+ case object IntType extends Type
+ case object BoolType extends Type
+}
+
+
+object TypeChecker {
+ import Trees._
+ import Types._
+
+ def typeOf(e :Expr) : Option[Type] = e match {
+ case Plus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case Minus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case LessThan(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(BoolType)
+ case _ => None()
+ }
+ case And(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Or(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Not(e) => typeOf(e) match {
+ case Some(BoolType) => Some(BoolType)
+ case _ => None()
+ }
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case (Some(t1), Some(t2)) if t1 == t2 => Some(BoolType)
+ case _ => None()
+ }
+ case Ite(c, th, el) => (typeOf(c), typeOf(th), typeOf(el)) match {
+ case (Some(BoolType), Some(t1), Some(t2)) if t1 == t2 => Some(t1)
+ case _ => None()
+ }
+ case IntLiteral(_) => Some(IntType)
+ case BoolLiteral(_) => Some(BoolType)
+ }
+
+ def typeChecks(e : Expr) = typeOf(e).isDefined
+}
+
+
+object Semantics {
+ import Trees._
+ import Types._
+ import TypeChecker._
+
+ def semI(t : Expr) : Int = {
+ require( typeOf(t) == ( Some(IntType) : Option[Type] ))
+ t match {
+ case Plus(lhs , rhs) => semI(lhs) + semI(rhs)
+ case Minus(lhs , rhs) => semI(lhs) - semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semI(thn) else semI(els)
+ case IntLiteral(v) => v
+ }
+ }
+
+ def semB(t : Expr) : Boolean = {
+ require( (Some(BoolType): Option[Type]) == typeOf(t))
+ t match {
+ case And(lhs, rhs ) => semB(lhs) && semB(rhs)
+ case Or(lhs , rhs ) => semB(lhs) || semB(rhs)
+ case Not(e) => !semB(e)
+ case LessThan(lhs, rhs) => semI(lhs) < semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semB(thn) else semB(els)
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case ( Some(IntType), Some(IntType) ) => semI(lhs) == semI(rhs)
+ case ( Some(BoolType), Some(BoolType) ) => semB(lhs) == semB(rhs)
+ }
+ case BoolLiteral(b) => b
+ }
+ }
+
+ def b2i(b : Boolean) = if (b) 1 else 0
+
+ @induct
+ def semUntyped( t : Expr) : Int = { t match {
+ case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
+ case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case Or(lhs, rhs ) =>
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ case Not(e) =>
+ b2i(semUntyped(e) == 0)
+ case LessThan(lhs, rhs) =>
+ b2i(semUntyped(lhs) < semUntyped(rhs))
+ case Eq(lhs, rhs) =>
+ b2i(semUntyped(lhs) == semUntyped(rhs))
+ case Ite(cond, thn, els) =>
+ if (semUntyped(cond) == 0) semUntyped(els) else semUntyped(thn)
+ case IntLiteral(v) => v
+ case BoolLiteral(b) => b2i(b)
+ }} ensuring { res => typeOf(t) match {
+ case Some(IntType) => res == semI(t)
+ case Some(BoolType) => res == b2i(semB(t))
+ case None() => true
+ }}
+
+}
+
+
+object Desugar {
+ import Types._
+ import TypeChecker._
+ import Semantics.b2i
+
+ abstract class SimpleE
+ case class Plus(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Neg(arg : SimpleE) extends SimpleE
+ case class Ite(cond : SimpleE, thn : SimpleE, els : SimpleE) extends SimpleE
+ case class Eq(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class LessThan(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Literal(i : Int) extends SimpleE
+
+ @induct
+ def desugar(e : Trees.Expr) : SimpleE = { e match {
+ case Trees.Plus (lhs, rhs) => Plus(desugar(lhs), desugar(rhs))
+ case Trees.Minus(lhs, rhs) => Plus(desugar(lhs), Neg(desugar(rhs)))
+ case Trees.LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
+ case Trees.And (lhs, rhs) => Ite(desugar(lhs), desugar(rhs), Literal(0))
+ case Trees.Or (lhs, rhs) => Ite(desugar(lhs), Literal(1), desugar(rhs))
+ case Trees.Not(e) => Ite(desugar(e), Literal(0), Literal(1))
+ case Trees.Eq(lhs, rhs) =>
+ Eq(desugar(lhs), desugar(rhs))
+ case Trees.Ite(cond, thn, els) => Ite(desugar(cond), desugar(thn), desugar(els))
+ case Trees.IntLiteral(v) => Literal(v)
+ case Trees.BoolLiteral(b) => Literal(b2i(b))
+ }} ensuring { res =>
+ sem(res) == Semantics.semUntyped(e)
+ }
+
+ def sem(e : SimpleE) : Int = e match {
+ case Plus (lhs, rhs) => sem(lhs) + sem(rhs)
+ case Ite(cond, thn, els) => if (sem(cond) != 0) sem(thn) else sem(els)
+ case Neg(arg) => -sem(arg)
+ case Eq(lhs,rhs) => b2i(sem(lhs) == sem(rhs))
+ case LessThan(lhs, rhs) => b2i(sem(lhs) < sem(rhs))
+ case Literal(i) => i
+ }
+
+}
+
+object Evaluator {
+ import Trees._
+
+ def bToi(b: Boolean) = if (b) 1 else 0
+ def iTob(i: Int) = i == 1
+
+ def eval(e: Expr): Int = {
+ e match {
+ case Plus(lhs, rhs) => eval(lhs) + eval(rhs)
+ case Minus(lhs, rhs) => eval(lhs) + eval(rhs)
+ case LessThan(lhs, rhs) => bToi(eval(lhs) < eval(rhs))
+ case And(lhs, rhs) => bToi(iTob(eval(lhs)) && iTob(eval(rhs)))
+ case Or(lhs, rhs) => bToi(iTob(eval(lhs)) || iTob(eval(rhs)))
+ case Not(e) => bToi(!iTob(eval(e)))
+ case Eq(lhs, rhs) => bToi(eval(lhs) == eval(rhs))
+ case Ite(cond, thn, els) => if (iTob(eval(cond))) eval(thn) else eval(els)
+ case IntLiteral(v) => v
+ case BoolLiteral(b) => bToi(b)
+ }
+ }
+}
+
+object Simplifier {
+ import Trees._
+ import Evaluator._
+
+ @induct
+ def simplify(e: Expr): Expr = {
+ e match {
+ case And(BoolLiteral(false), _) => BoolLiteral(false)
+ case Or(BoolLiteral(true), _) => BoolLiteral(true)
+ case Plus(IntLiteral(a), IntLiteral(b)) => IntLiteral(a-b)
+ case Not(Not(Not(a))) => Not(a)
+ case e => e
+ }
+ } ensuring {
+ res => eval(res) == eval(e)
+ }
+}
diff --git a/testcases/repair/Compiler/Compiler6.scala b/testcases/repair/Compiler/Compiler6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0e6364fc53ec7fd0e7f65c803980689ef310b600
--- /dev/null
+++ b/testcases/repair/Compiler/Compiler6.scala
@@ -0,0 +1,214 @@
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon._
+
+object Trees {
+ abstract class Expr
+ case class Plus(lhs: Expr, rhs: Expr) extends Expr
+ case class Minus(lhs: Expr, rhs: Expr) extends Expr
+ case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+ case class And(lhs: Expr, rhs: Expr) extends Expr
+ case class Or(lhs: Expr, rhs: Expr) extends Expr
+ case class Not(e : Expr) extends Expr
+ case class Eq(lhs: Expr, rhs: Expr) extends Expr
+ case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+ case class IntLiteral(v: Int) extends Expr
+ case class BoolLiteral(b : Boolean) extends Expr
+}
+
+object Types {
+ abstract class Type
+ case object IntType extends Type
+ case object BoolType extends Type
+}
+
+
+object TypeChecker {
+ import Trees._
+ import Types._
+
+ def typeOf(e :Expr) : Option[Type] = e match {
+ case Plus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case Minus(l,r) => (typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(IntType)
+ case _ => None()
+ }
+ case LessThan(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(IntType), Some(IntType)) => Some(BoolType)
+ case _ => None()
+ }
+ case And(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Or(l,r) => ( typeOf(l), typeOf(r)) match {
+ case (Some(BoolType), Some(BoolType)) => Some(BoolType)
+ case _ => None()
+ }
+ case Not(e) => typeOf(e) match {
+ case Some(BoolType) => Some(BoolType)
+ case _ => None()
+ }
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case (Some(t1), Some(t2)) if t1 == t2 => Some(BoolType)
+ case _ => None()
+ }
+ case Ite(c, th, el) => (typeOf(c), typeOf(th), typeOf(el)) match {
+ case (Some(BoolType), Some(t1), Some(t2)) if t1 == t2 => Some(t1)
+ case _ => None()
+ }
+ case IntLiteral(_) => Some(IntType)
+ case BoolLiteral(_) => Some(BoolType)
+ }
+
+ def typeChecks(e : Expr) = typeOf(e).isDefined
+}
+
+
+object Semantics {
+ import Trees._
+ import Types._
+ import TypeChecker._
+
+ def semI(t : Expr) : Int = {
+ require( typeOf(t) == ( Some(IntType) : Option[Type] ))
+ t match {
+ case Plus(lhs , rhs) => semI(lhs) + semI(rhs)
+ case Minus(lhs , rhs) => semI(lhs) - semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semI(thn) else semI(els)
+ case IntLiteral(v) => v
+ }
+ }
+
+ def semB(t : Expr) : Boolean = {
+ require( (Some(BoolType): Option[Type]) == typeOf(t))
+ t match {
+ case And(lhs, rhs ) => semB(lhs) && semB(rhs)
+ case Or(lhs , rhs ) => semB(lhs) || semB(rhs)
+ case Not(e) => !semB(e)
+ case LessThan(lhs, rhs) => semI(lhs) < semI(rhs)
+ case Ite(cond, thn, els) =>
+ if (semB(cond)) semB(thn) else semB(els)
+ case Eq(lhs, rhs) => (typeOf(lhs), typeOf(rhs)) match {
+ case ( Some(IntType), Some(IntType) ) => semI(lhs) == semI(rhs)
+ case ( Some(BoolType), Some(BoolType) ) => semB(lhs) == semB(rhs)
+ }
+ case BoolLiteral(b) => b
+ }
+ }
+
+ def b2i(b : Boolean) = if (b) 1 else 0
+
+ @induct
+ def semUntyped( t : Expr) : Int = { t match {
+ case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
+ case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case Or(lhs, rhs ) =>
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ case Not(e) =>
+ b2i(semUntyped(e) == 0)
+ case LessThan(lhs, rhs) =>
+ b2i(semUntyped(lhs) < semUntyped(rhs))
+ case Eq(lhs, rhs) =>
+ b2i(semUntyped(lhs) == semUntyped(rhs))
+ case Ite(cond, thn, els) =>
+ if (semUntyped(cond) == 0) semUntyped(els) else semUntyped(thn)
+ case IntLiteral(v) => v
+ case BoolLiteral(b) => b2i(b)
+ }} ensuring { res => typeOf(t) match {
+ case Some(IntType) => res == semI(t)
+ case Some(BoolType) => res == b2i(semB(t))
+ case None() => true
+ }}
+
+}
+
+
+object Desugar {
+ import Types._
+ import TypeChecker._
+ import Semantics.b2i
+
+ abstract class SimpleE
+ case class Plus(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Neg(arg : SimpleE) extends SimpleE
+ case class Ite(cond : SimpleE, thn : SimpleE, els : SimpleE) extends SimpleE
+ case class Eq(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class LessThan(lhs : SimpleE, rhs : SimpleE) extends SimpleE
+ case class Literal(i : Int) extends SimpleE
+
+ @induct
+ def desugar(e : Trees.Expr) : SimpleE = { e match {
+ case Trees.Plus (lhs, rhs) => Plus(desugar(lhs), desugar(rhs))
+ case Trees.Minus(lhs, rhs) => Plus(desugar(lhs), Neg(desugar(rhs)))
+ case Trees.LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
+ case Trees.And (lhs, rhs) => Ite(desugar(lhs), desugar(rhs), Literal(0))
+ case Trees.Or (lhs, rhs) => Ite(desugar(lhs), Literal(1), desugar(rhs))
+ case Trees.Not(e) => Ite(desugar(e), Literal(0), Literal(1))
+ case Trees.Eq(lhs, rhs) =>
+ Eq(desugar(lhs), desugar(rhs))
+ case Trees.Ite(cond, thn, els) => Ite(desugar(cond), desugar(thn), desugar(els))
+ case Trees.IntLiteral(v) => Literal(v)
+ case Trees.BoolLiteral(b) => Literal(b2i(b))
+ }} ensuring { res =>
+ sem(res) == Semantics.semUntyped(e)
+ }
+
+ def sem(e : SimpleE) : Int = e match {
+ case Plus (lhs, rhs) => sem(lhs) + sem(rhs)
+ case Ite(cond, thn, els) => if (sem(cond) != 0) sem(thn) else sem(els)
+ case Neg(arg) => -sem(arg)
+ case Eq(lhs,rhs) => b2i(sem(lhs) == sem(rhs))
+ case LessThan(lhs, rhs) => b2i(sem(lhs) < sem(rhs))
+ case Literal(i) => i
+ }
+
+}
+
+object Evaluator {
+ import Trees._
+
+ def bToi(b: Boolean) = if (b) 1 else 0
+ def iTob(i: Int) = i == 1
+
+ def eval(e: Expr): Int = {
+ e match {
+ case Plus(lhs, rhs) => eval(lhs) + eval(rhs)
+ case Minus(lhs, rhs) => eval(lhs) + eval(rhs)
+ case LessThan(lhs, rhs) => bToi(eval(lhs) < eval(rhs))
+ case And(lhs, rhs) => bToi(iTob(eval(lhs)) && iTob(eval(rhs)))
+ case Or(lhs, rhs) => bToi(iTob(eval(lhs)) || iTob(eval(rhs)))
+ case Not(e) => bToi(!iTob(eval(e)))
+ case Eq(lhs, rhs) => bToi(eval(lhs) == eval(rhs))
+ case Ite(cond, thn, els) => if (iTob(eval(cond))) eval(thn) else eval(els)
+ case IntLiteral(v) => v
+ case BoolLiteral(b) => bToi(b)
+ }
+ }
+}
+
+object Simplifier {
+ import Trees._
+ import Evaluator._
+
+ @induct
+ def simplify(e: Expr): Expr = {
+ e match {
+ case And(BoolLiteral(false), _) => BoolLiteral(false)
+ case Or(BoolLiteral(true), _) => BoolLiteral(false)
+ case Plus(IntLiteral(a), IntLiteral(b)) => IntLiteral(a+b)
+ case Not(Not(Not(a))) => Not(a)
+ case e => e
+ }
+ } ensuring {
+ res => eval(res) == eval(e) && ((e, res) passes {
+ case Or(BoolLiteral(true), e) => BoolLiteral(true)
+ })
+ }
+}
diff --git a/testcases/repair/evaluation/Desugar/Desugar1.scala b/testcases/repair/evaluation/Desugar/Desugar1.scala
deleted file mode 120000
index c97e24b0f586788e296e175ffd44db8dbc83423d..0000000000000000000000000000000000000000
--- a/testcases/repair/evaluation/Desugar/Desugar1.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../Desugar/Desugar1.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/Desugar/Desugar2.scala b/testcases/repair/evaluation/Desugar/Desugar2.scala
deleted file mode 120000
index 17e99298c3f2d855be8906b865b421f82229a105..0000000000000000000000000000000000000000
--- a/testcases/repair/evaluation/Desugar/Desugar2.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../Desugar/Desugar2.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/Desugar/Desugar3.scala b/testcases/repair/evaluation/Desugar/Desugar3.scala
deleted file mode 120000
index 4ad63dd72c4e188041b476f7a7e093250860445b..0000000000000000000000000000000000000000
--- a/testcases/repair/evaluation/Desugar/Desugar3.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../Desugar/Desugar3.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/Desugar/Desugar4.scala b/testcases/repair/evaluation/Desugar/Desugar4.scala
deleted file mode 120000
index 2a5a9746e247d3a7aaa0d4a88f395ea78d7117a4..0000000000000000000000000000000000000000
--- a/testcases/repair/evaluation/Desugar/Desugar4.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../Desugar/Desugar4.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/HeapSort/HeapSort3.scala b/testcases/repair/evaluation/HeapSort/HeapSort3.scala
deleted file mode 120000
index efbc7141eea32cc37008296b11d0fb93d6a8b5da..0000000000000000000000000000000000000000
--- a/testcases/repair/evaluation/HeapSort/HeapSort3.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../HeapSort/HeapSort3.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/HeapSort/HeapSort4.scala b/testcases/repair/evaluation/HeapSort/HeapSort4.scala
deleted file mode 120000
index 86163bbc1b6a8920d8477d1222133c5dcea32b18..0000000000000000000000000000000000000000
--- a/testcases/repair/evaluation/HeapSort/HeapSort4.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../HeapSort/HeapSort4.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/HeapSort/HeapSort5.scala b/testcases/repair/evaluation/HeapSort/HeapSort5.scala
deleted file mode 120000
index 3069a2f6a5f3662a205f93e2d5c8b240ddc7d291..0000000000000000000000000000000000000000
--- a/testcases/repair/evaluation/HeapSort/HeapSort5.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../HeapSort/HeapSort5.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/HeapSort/HeapSort6.scala b/testcases/repair/evaluation/HeapSort/HeapSort6.scala
deleted file mode 120000
index 0046983b5e8ab6e4c9582b0d75ef32d7059403aa..0000000000000000000000000000000000000000
--- a/testcases/repair/evaluation/HeapSort/HeapSort6.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../HeapSort/HeapSort6.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/HeapSort/HeapSort7.scala b/testcases/repair/evaluation/HeapSort/HeapSort7.scala
deleted file mode 120000
index 22dfaedb67d5cff119a1fbf9a64172f706d97d89..0000000000000000000000000000000000000000
--- a/testcases/repair/evaluation/HeapSort/HeapSort7.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../HeapSort/HeapSort7.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/HeapSort/HeapSort8.scala b/testcases/repair/evaluation/HeapSort/HeapSort8.scala
deleted file mode 120000
index 2a3343c9abccb2627fcf26222ea81cea6664b5c8..0000000000000000000000000000000000000000
--- a/testcases/repair/evaluation/HeapSort/HeapSort8.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../HeapSort/HeapSort8.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/HeapSort/HeapSort9.scala b/testcases/repair/evaluation/HeapSort/HeapSort9.scala
deleted file mode 120000
index 1bb14b50d495afc1186fddb5ff720793597a320d..0000000000000000000000000000000000000000
--- a/testcases/repair/evaluation/HeapSort/HeapSort9.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../HeapSort/HeapSort9.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/List/List1.scala b/testcases/repair/evaluation/List/List1.scala
deleted file mode 120000
index 88b9348e06c2757b21d83b1ead18c180a98f593c..0000000000000000000000000000000000000000
--- a/testcases/repair/evaluation/List/List1.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../List/List1.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/List/List10.scala b/testcases/repair/evaluation/List/List10.scala
deleted file mode 120000
index 6769b75102904f135289f3ae9bb3722d21d9f155..0000000000000000000000000000000000000000
--- a/testcases/repair/evaluation/List/List10.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../List/List10.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/List/List11.scala b/testcases/repair/evaluation/List/List11.scala
deleted file mode 120000
index 2b1bc3b5112d10b9fab4cd8073600b65dae2d3de..0000000000000000000000000000000000000000
--- a/testcases/repair/evaluation/List/List11.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../List/List11.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/List/List2.scala b/testcases/repair/evaluation/List/List2.scala
deleted file mode 120000
index 5d3bdd5efa69d73578b977ee7c3a25fae5beca1b..0000000000000000000000000000000000000000
--- a/testcases/repair/evaluation/List/List2.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../List/List2.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/List/List3.scala b/testcases/repair/evaluation/List/List3.scala
deleted file mode 120000
index deed1959e1b99707a236e01cc8fa5c2df20bdce9..0000000000000000000000000000000000000000
--- a/testcases/repair/evaluation/List/List3.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../List/List3.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/List/List5.scala b/testcases/repair/evaluation/List/List5.scala
deleted file mode 120000
index a93655c2fd5c436dd566977b14039cacbe063a2c..0000000000000000000000000000000000000000
--- a/testcases/repair/evaluation/List/List5.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../List/List5.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/List/List6.scala b/testcases/repair/evaluation/List/List6.scala
deleted file mode 120000
index bd461d2f68d48b8f5997e8dab84fa7a7e3dd40ce..0000000000000000000000000000000000000000
--- a/testcases/repair/evaluation/List/List6.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../List/List6.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/List/List7.scala b/testcases/repair/evaluation/List/List7.scala
deleted file mode 120000
index e7120d71aaf3a63caad53550b051db152334cee9..0000000000000000000000000000000000000000
--- a/testcases/repair/evaluation/List/List7.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../List/List7.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/List/List8.scala b/testcases/repair/evaluation/List/List8.scala
deleted file mode 120000
index 6b3956d4ea2dd3c4bf9effc60c7f16e71312b1e1..0000000000000000000000000000000000000000
--- a/testcases/repair/evaluation/List/List8.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../List/List8.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/List/List9.scala b/testcases/repair/evaluation/List/List9.scala
deleted file mode 120000
index 37b27167154ad283c9abbd772c5787a2f845b123..0000000000000000000000000000000000000000
--- a/testcases/repair/evaluation/List/List9.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../List/List9.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/PropLogic/PropLogic1.scala b/testcases/repair/evaluation/PropLogic/PropLogic1.scala
deleted file mode 120000
index 2b22c7ffdcc3e9fc91784bee1bba32710d1a5924..0000000000000000000000000000000000000000
--- a/testcases/repair/evaluation/PropLogic/PropLogic1.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../PropLogic/PropLogic1.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/PropLogic/PropLogic2.scala b/testcases/repair/evaluation/PropLogic/PropLogic2.scala
deleted file mode 120000
index b77428fee455d16bb66f7ec26881aeb76c00a127..0000000000000000000000000000000000000000
--- a/testcases/repair/evaluation/PropLogic/PropLogic2.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../PropLogic/PropLogic2.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/PropLogic/PropLogic3.scala b/testcases/repair/evaluation/PropLogic/PropLogic3.scala
deleted file mode 120000
index c7e74b5026a7fdc23e0d9d49647c8469c0df1ebc..0000000000000000000000000000000000000000
--- a/testcases/repair/evaluation/PropLogic/PropLogic3.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../PropLogic/PropLogic3.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/PropLogic/PropLogic4.scala b/testcases/repair/evaluation/PropLogic/PropLogic4.scala
deleted file mode 120000
index fb6548bf10a7879b9f76b6a5c846b587ec4ccde6..0000000000000000000000000000000000000000
--- a/testcases/repair/evaluation/PropLogic/PropLogic4.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../PropLogic/PropLogic4.scala
\ No newline at end of file
diff --git a/testcases/repair/evaluation/PropLogic/PropLogic5.scala b/testcases/repair/evaluation/PropLogic/PropLogic5.scala
deleted file mode 120000
index 2d17e3dc007114d2c7515b52a02f6dbca0ad4af6..0000000000000000000000000000000000000000
--- a/testcases/repair/evaluation/PropLogic/PropLogic5.scala
+++ /dev/null
@@ -1 +0,0 @@
-../../PropLogic/PropLogic5.scala
\ No newline at end of file