From c65833c0cc727e2459f94b2cf7ad1d9ea8abe2c6 Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Tue, 9 Dec 2014 18:01:42 +0100
Subject: [PATCH] Benchmark additions/changes
---
.../repair/DaysToYears/DaysToYears2.scala | 36 ++++
.../repair/DaysToYears/DaysToYears3.scala | 36 ++++
.../synthesis/repair/Desugar/Desugar.scala | 172 +++++++++++++++++
.../synthesis/repair/Desugar/Desugar1.scala | 177 ++++++++++++++++++
.../synthesis/repair/Desugar/Desugar2.scala | 172 +++++++++++++++++
.../synthesis/repair/Desugar/Desugar3.scala | 173 +++++++++++++++++
.../synthesis/repair/Desugar/Desugar4.scala | 172 +++++++++++++++++
.../synthesis/repair/Parser/Parser1.scala | 58 ++++++
.../synthesis/repair/Parser/Parser2.scala | 58 ++++++
.../synthesis/repair/Parser/Parser3.scala | 58 ++++++
.../synthesis/repair/Parser/Parser4.scala | 58 ++++++
.../synthesis/repair/Parser/Parser5.scala | 58 ++++++
.../{PropLogic5.scala => PropLogic2.scala} | 11 +-
.../repair/PropLogic/PropLogic3.scala | 33 +---
.../repair/PropLogic/PropLogic4.scala | 30 +--
.../repair/PropLogic/PropLogic6.scala | 73 --------
16 files changed, 1245 insertions(+), 130 deletions(-)
create mode 100644 testcases/synthesis/repair/DaysToYears/DaysToYears2.scala
create mode 100644 testcases/synthesis/repair/DaysToYears/DaysToYears3.scala
create mode 100644 testcases/synthesis/repair/Desugar/Desugar.scala
create mode 100644 testcases/synthesis/repair/Desugar/Desugar1.scala
create mode 100644 testcases/synthesis/repair/Desugar/Desugar2.scala
create mode 100644 testcases/synthesis/repair/Desugar/Desugar3.scala
create mode 100644 testcases/synthesis/repair/Desugar/Desugar4.scala
create mode 100644 testcases/synthesis/repair/Parser/Parser1.scala
create mode 100644 testcases/synthesis/repair/Parser/Parser2.scala
create mode 100644 testcases/synthesis/repair/Parser/Parser3.scala
create mode 100644 testcases/synthesis/repair/Parser/Parser4.scala
create mode 100644 testcases/synthesis/repair/Parser/Parser5.scala
rename testcases/synthesis/repair/PropLogic/{PropLogic5.scala => PropLogic2.scala} (88%)
delete mode 100644 testcases/synthesis/repair/PropLogic/PropLogic6.scala
diff --git a/testcases/synthesis/repair/DaysToYears/DaysToYears2.scala b/testcases/synthesis/repair/DaysToYears/DaysToYears2.scala
new file mode 100644
index 000000000..de0d31a70
--- /dev/null
+++ b/testcases/synthesis/repair/DaysToYears/DaysToYears2.scala
@@ -0,0 +1,36 @@
+import leon.lang._
+
+object DaysToYears {
+ val base : Int = 1980
+
+ def isLeapYear(y : Int): Boolean = y % 4 == 0
+
+ def daysToYears(days : Int): Int = {
+ require(days > 0)
+ daysToYears1(base, days)._1
+ }
+
+ def daysToYears1(year : Int, days : Int): (Int, Int) = {
+ require(year >= base && days > 0)
+ if (days > 366 && isLeapYear(year))
+ daysToYears1(year + 1, days - 366) // TODO this branch cannot be solved although it is correct because it depends on the erroneous branch
+ else if (days > 365 && !isLeapYear(year))
+ daysToYears1(year + 1, days - 365)
+ else (year + 1, days) // FIXME +1
+ } ensuring { res =>
+ res._2 <= 366 &&
+ res._2 > 0 &&
+ res._1 >= base &&
+ (((year,days), res) passes {
+ case (1980, 366 ) => (1980, 366)
+ case (1980, 1000) => (1982, 269)
+ })
+ }
+
+ def main(args : Array[String]) = {
+ println(daysToYears1(base, 10593 ))
+ println(daysToYears1(base, 366 ))
+ println(daysToYears1(base, 1000 ))
+ }
+}
+
diff --git a/testcases/synthesis/repair/DaysToYears/DaysToYears3.scala b/testcases/synthesis/repair/DaysToYears/DaysToYears3.scala
new file mode 100644
index 000000000..bb6c518b3
--- /dev/null
+++ b/testcases/synthesis/repair/DaysToYears/DaysToYears3.scala
@@ -0,0 +1,36 @@
+import leon.lang._
+
+object DaysToYears {
+ val base : Int = 1980
+
+ def isLeapYear(y : Int): Boolean = y % 4 == 0
+
+ def daysToYears(days : Int): Int = {
+ require(days > 0)
+ daysToYears1(base, days)._1
+ }
+
+ def daysToYears1(year : Int, days : Int): (Int, Int) = {
+ require(year >= base && days > 0)
+ if (days > 366 && isLeapYear(year))
+ daysToYears1(year + 1, days - 366)
+ else if (days > 365 && !isLeapYear(year))
+ daysToYears1(year + 1, days - 365)
+ else (year, days)
+ } ensuring { res =>
+ res._2 <= 366 &&
+ res._2 > 0 &&
+ res._1 >= base &&
+ (((year,days), res) passes {
+ case (1980, 366 ) => (1980, 366)
+ case (1980, 1000) => (1982, 269)
+ })
+ }
+
+ def main(args : Array[String]) = {
+ println(daysToYears1(base, 10593 ))
+ println(daysToYears1(base, 366 ))
+ println(daysToYears1(base, 1000 ))
+ }
+}
+
diff --git a/testcases/synthesis/repair/Desugar/Desugar.scala b/testcases/synthesis/repair/Desugar/Desugar.scala
new file mode 100644
index 000000000..19cd3305a
--- /dev/null
+++ b/testcases/synthesis/repair/Desugar/Desugar.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(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
+ }
+
+}
diff --git a/testcases/synthesis/repair/Desugar/Desugar1.scala b/testcases/synthesis/repair/Desugar/Desugar1.scala
new file mode 100644
index 000000000..2995bb576
--- /dev/null
+++ b/testcases/synthesis/repair/Desugar/Desugar1.scala
@@ -0,0 +1,177 @@
+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 so it's happy...
+ 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 =>
+ // TODO: Z3 fails to disprove this!
+ ((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/synthesis/repair/Desugar/Desugar2.scala b/testcases/synthesis/repair/Desugar/Desugar2.scala
new file mode 100644
index 000000000..fc3b81d88
--- /dev/null
+++ b/testcases/synthesis/repair/Desugar/Desugar2.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), 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)
+ }
+
+ 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/synthesis/repair/Desugar/Desugar3.scala b/testcases/synthesis/repair/Desugar/Desugar3.scala
new file mode 100644
index 000000000..ec61a78a5
--- /dev/null
+++ b/testcases/synthesis/repair/Desugar/Desugar3.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/synthesis/repair/Desugar/Desugar4.scala b/testcases/synthesis/repair/Desugar/Desugar4.scala
new file mode 100644
index 000000000..9f6ac963a
--- /dev/null
+++ b/testcases/synthesis/repair/Desugar/Desugar4.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/synthesis/repair/Parser/Parser1.scala b/testcases/synthesis/repair/Parser/Parser1.scala
new file mode 100644
index 000000000..1a12b820c
--- /dev/null
+++ b/testcases/synthesis/repair/Parser/Parser1.scala
@@ -0,0 +1,58 @@
+import leon._
+import leon.collection._
+
+object Parser {
+ abstract class Token
+ case object LParen extends Token
+ case object RParen extends Token
+ case class Id(id : Int) extends Token
+
+ abstract class Tree
+ case class App(args : List[Tree]) extends Tree
+ case class Leaf(id : Int) extends Tree
+
+ def parse(in : List[Token]) : (Option[Tree], List[Token]) = { in match {
+ case Cons(Id(s), tl) =>
+ (Some[Tree](Leaf(s)),tl)
+ case Cons(LParen, tl) => parseMany(tl) match {
+ case (Some(trees:Cons[Tree]), Cons(RParen,rest)) =>
+ (Some[Tree](App(trees)), rest)
+ case (_, rest) => (None[Tree](), rest)
+ }
+ case _ => (None[Tree](), in)
+ }} ensuring { _ match {
+ case ( Some(tree), rest@Cons(h,_)) =>
+ print(tree, rest) == in
+ case ( None(), Cons(h,_) ) =>
+ h == RParen
+ case _ => true
+ }}
+
+ def parseMany(in : List[Token]) : (Option[List[Tree]], List[Token]) = { parse(in) match {
+ case (None(), rest) /*if rest == in*/ => (Some[List[Tree]](Nil()), in) // FIXME: forgot condition
+ //case (None(), rest) => (None[List[Tree]](), rest)
+ case (Some(tree), rest) => parseMany(rest) match {
+ case ( None(), rest2) => (None[List[Tree]](), rest2)
+ case ( Some(trees), rest2) =>
+ ( Some[List[Tree]](tree::trees), rest2 )
+ }
+ }} ensuring { _ match {
+ case ( Some(t), rest@Cons(h, _) ) =>
+ h == RParen && printL(t, rest) == in
+ case ( None(), Cons(h, _)) =>
+ h == RParen
+ case _ => true
+ }}
+
+
+ def printL(args : List[Tree], rest : List[Token]) : List[Token] = args match {
+ case Nil() => rest
+ case Cons(h,t) => print(h, printL(t, rest))
+ }
+
+ def print(t : Tree, rest : List[Token]) : List[Token] = t match {
+ case Leaf(s) => Id(s) :: rest
+ case App(args) => LParen :: printL(args, RParen :: rest)
+ }
+
+}
diff --git a/testcases/synthesis/repair/Parser/Parser2.scala b/testcases/synthesis/repair/Parser/Parser2.scala
new file mode 100644
index 000000000..24fef5686
--- /dev/null
+++ b/testcases/synthesis/repair/Parser/Parser2.scala
@@ -0,0 +1,58 @@
+import leon._
+import leon.collection._
+
+object Parser {
+ abstract class Token
+ case object LParen extends Token
+ case object RParen extends Token
+ case class Id(id : Int) extends Token
+
+ abstract class Tree
+ case class App(args : List[Tree]) extends Tree
+ case class Leaf(id : Int) extends Tree
+
+ def parse(in : List[Token]) : (Option[Tree], List[Token]) = { in match {
+ case Cons(Id(s), tl) =>
+ (Some[Tree](Leaf(s)),tl)
+ case Cons(LParen, tl) => parseMany(tl) match {
+ case (Some(trees:Cons[Tree]), Cons(RParen,rest)) =>
+ (Some[Tree](App(trees)), rest)
+ case (_, rest) => (None[Tree](), rest)
+ }
+ case _ => (None[Tree](), in)
+ }} ensuring { _ match {
+ case ( Some(tree), rest@Cons(h,_)) =>
+ print(tree, rest) == in
+ case ( None(), Cons(h,_) ) =>
+ h == RParen
+ case _ => true
+ }}
+
+ def parseMany(in : List[Token]) : (Option[List[Tree]], List[Token]) = { parse(in) match {
+ case (None(), rest) if rest == in => (Some[List[Tree]](Nil()), in)
+ case (None(), rest) => (None[List[Tree]](), rest)
+ case (Some(tree), rest) => parseMany(rest) match {
+ case ( None(), rest2) => (None[List[Tree]](), rest2)
+ case ( Some(trees), rest2) =>
+ ( Some[List[Tree]](trees), rest2 ) // FIXME: should be tree::trees
+ }
+ }} ensuring { _ match {
+ case ( Some(t), rest@Cons(h, _) ) =>
+ h == RParen && printL(t, rest) == in
+ case ( None(), Cons(h, _)) =>
+ h == RParen
+ case _ => true
+ }}
+
+
+ def printL(args : List[Tree], rest : List[Token]) : List[Token] = args match {
+ case Nil() => rest
+ case Cons(h,t) => print(h, printL(t, rest))
+ }
+
+ def print(t : Tree, rest : List[Token]) : List[Token] = t match {
+ case Leaf(s) => Id(s) :: rest
+ case App(args) => LParen :: printL(args, RParen :: rest)
+ }
+
+}
diff --git a/testcases/synthesis/repair/Parser/Parser3.scala b/testcases/synthesis/repair/Parser/Parser3.scala
new file mode 100644
index 000000000..dcc8107f3
--- /dev/null
+++ b/testcases/synthesis/repair/Parser/Parser3.scala
@@ -0,0 +1,58 @@
+import leon._
+import leon.collection._
+
+object Parser {
+ abstract class Token
+ case object LParen extends Token
+ case object RParen extends Token
+ case class Id(id : Int) extends Token
+
+ abstract class Tree
+ case class App(args : List[Tree]) extends Tree
+ case class Leaf(id : Int) extends Tree
+
+ def parse(in : List[Token]) : (Option[Tree], List[Token]) = { in match {
+ case Cons(Id(s), tl) =>
+ (Some[Tree](Leaf(s)),tl)
+ case Cons(LParen, tl) => parseMany(tl) match {
+ case (Some(trees:Cons[Tree]), Cons(RParen,rest)) =>
+ (Some[Tree](App(trees)), rest)
+ case (_, rest) => (None[Tree](), rest)
+ }
+ case _ => (None[Tree](), in)
+ }} ensuring { _ match {
+ case ( Some(tree), rest@Cons(h,_)) =>
+ print(tree, rest) == in
+ case ( None(), Cons(h,_) ) =>
+ h == RParen
+ case _ => true
+ }}
+
+ def parseMany(in : List[Token]) : (Option[List[Tree]], List[Token]) = { parse(in) match {
+ case (None(), rest) if rest == in => (Some[List[Tree]](Nil()), in)
+ case (None(), rest) => (None[List[Tree]](), rest)
+ case (Some(tree), rest) => parseMany(rest) match {
+ case ( None(), rest2) => (None[List[Tree]](), rest2)
+ case ( Some(trees), rest2) =>
+ ( Some[List[Tree]](tree::trees), rest2 )
+ }
+ }} ensuring { _ match {
+ case ( Some(t), rest@Cons(h, _) ) =>
+ h == RParen && printL(t, rest) == in
+ case ( None(), Cons(h, _)) =>
+ h == RParen
+ case _ => true
+ }}
+
+
+ def printL(args : List[Tree], rest : List[Token]) : List[Token] = args match {
+ case Nil() => rest
+ case Cons(h,t) => print(h, printL(t, rest))
+ }
+
+ def print(t : Tree, rest : List[Token]) : List[Token] = t match {
+ case Leaf(s) => Id(s) :: rest
+ case App(args) => LParen :: printL(args, RParen :: rest)
+ }
+
+}
diff --git a/testcases/synthesis/repair/Parser/Parser4.scala b/testcases/synthesis/repair/Parser/Parser4.scala
new file mode 100644
index 000000000..dcc8107f3
--- /dev/null
+++ b/testcases/synthesis/repair/Parser/Parser4.scala
@@ -0,0 +1,58 @@
+import leon._
+import leon.collection._
+
+object Parser {
+ abstract class Token
+ case object LParen extends Token
+ case object RParen extends Token
+ case class Id(id : Int) extends Token
+
+ abstract class Tree
+ case class App(args : List[Tree]) extends Tree
+ case class Leaf(id : Int) extends Tree
+
+ def parse(in : List[Token]) : (Option[Tree], List[Token]) = { in match {
+ case Cons(Id(s), tl) =>
+ (Some[Tree](Leaf(s)),tl)
+ case Cons(LParen, tl) => parseMany(tl) match {
+ case (Some(trees:Cons[Tree]), Cons(RParen,rest)) =>
+ (Some[Tree](App(trees)), rest)
+ case (_, rest) => (None[Tree](), rest)
+ }
+ case _ => (None[Tree](), in)
+ }} ensuring { _ match {
+ case ( Some(tree), rest@Cons(h,_)) =>
+ print(tree, rest) == in
+ case ( None(), Cons(h,_) ) =>
+ h == RParen
+ case _ => true
+ }}
+
+ def parseMany(in : List[Token]) : (Option[List[Tree]], List[Token]) = { parse(in) match {
+ case (None(), rest) if rest == in => (Some[List[Tree]](Nil()), in)
+ case (None(), rest) => (None[List[Tree]](), rest)
+ case (Some(tree), rest) => parseMany(rest) match {
+ case ( None(), rest2) => (None[List[Tree]](), rest2)
+ case ( Some(trees), rest2) =>
+ ( Some[List[Tree]](tree::trees), rest2 )
+ }
+ }} ensuring { _ match {
+ case ( Some(t), rest@Cons(h, _) ) =>
+ h == RParen && printL(t, rest) == in
+ case ( None(), Cons(h, _)) =>
+ h == RParen
+ case _ => true
+ }}
+
+
+ def printL(args : List[Tree], rest : List[Token]) : List[Token] = args match {
+ case Nil() => rest
+ case Cons(h,t) => print(h, printL(t, rest))
+ }
+
+ def print(t : Tree, rest : List[Token]) : List[Token] = t match {
+ case Leaf(s) => Id(s) :: rest
+ case App(args) => LParen :: printL(args, RParen :: rest)
+ }
+
+}
diff --git a/testcases/synthesis/repair/Parser/Parser5.scala b/testcases/synthesis/repair/Parser/Parser5.scala
new file mode 100644
index 000000000..dcc8107f3
--- /dev/null
+++ b/testcases/synthesis/repair/Parser/Parser5.scala
@@ -0,0 +1,58 @@
+import leon._
+import leon.collection._
+
+object Parser {
+ abstract class Token
+ case object LParen extends Token
+ case object RParen extends Token
+ case class Id(id : Int) extends Token
+
+ abstract class Tree
+ case class App(args : List[Tree]) extends Tree
+ case class Leaf(id : Int) extends Tree
+
+ def parse(in : List[Token]) : (Option[Tree], List[Token]) = { in match {
+ case Cons(Id(s), tl) =>
+ (Some[Tree](Leaf(s)),tl)
+ case Cons(LParen, tl) => parseMany(tl) match {
+ case (Some(trees:Cons[Tree]), Cons(RParen,rest)) =>
+ (Some[Tree](App(trees)), rest)
+ case (_, rest) => (None[Tree](), rest)
+ }
+ case _ => (None[Tree](), in)
+ }} ensuring { _ match {
+ case ( Some(tree), rest@Cons(h,_)) =>
+ print(tree, rest) == in
+ case ( None(), Cons(h,_) ) =>
+ h == RParen
+ case _ => true
+ }}
+
+ def parseMany(in : List[Token]) : (Option[List[Tree]], List[Token]) = { parse(in) match {
+ case (None(), rest) if rest == in => (Some[List[Tree]](Nil()), in)
+ case (None(), rest) => (None[List[Tree]](), rest)
+ case (Some(tree), rest) => parseMany(rest) match {
+ case ( None(), rest2) => (None[List[Tree]](), rest2)
+ case ( Some(trees), rest2) =>
+ ( Some[List[Tree]](tree::trees), rest2 )
+ }
+ }} ensuring { _ match {
+ case ( Some(t), rest@Cons(h, _) ) =>
+ h == RParen && printL(t, rest) == in
+ case ( None(), Cons(h, _)) =>
+ h == RParen
+ case _ => true
+ }}
+
+
+ def printL(args : List[Tree], rest : List[Token]) : List[Token] = args match {
+ case Nil() => rest
+ case Cons(h,t) => print(h, printL(t, rest))
+ }
+
+ def print(t : Tree, rest : List[Token]) : List[Token] = t match {
+ case Leaf(s) => Id(s) :: rest
+ case App(args) => LParen :: printL(args, RParen :: rest)
+ }
+
+}
diff --git a/testcases/synthesis/repair/PropLogic/PropLogic5.scala b/testcases/synthesis/repair/PropLogic/PropLogic2.scala
similarity index 88%
rename from testcases/synthesis/repair/PropLogic/PropLogic5.scala
rename to testcases/synthesis/repair/PropLogic/PropLogic2.scala
index d86d184ed..192f7e3e7 100644
--- a/testcases/synthesis/repair/PropLogic/PropLogic5.scala
+++ b/testcases/synthesis/repair/PropLogic/PropLogic2.scala
@@ -30,15 +30,14 @@ object SemanticsPreservation {
case Not(And(lhs,rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
case Not(Or(lhs,rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs)))
case Not(Const(v)) => Const(!v)
- case Not(Not(e)) => nnf(e)
case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
+ // FIXME: forgot to handle the Not(Not(_)) case
case other => other
}} ensuring { res =>
- isNNF(res) && ((formula, res) passes {
- case Not(And(Const(a), Const(b))) => Or(Const(!a), Const(!b))
- case x@And(Literal(_), Literal(_)) => x
- })
+ isNNF(res) && ((formula, res) passes {
+ case Not(Not(Not(Const(a)))) => Const(!a)
+ })
}
def isNNF(f : Formula) : Boolean = f match {
@@ -58,7 +57,7 @@ object SemanticsPreservation {
case Or(_, Const(true)) => Const(true)
case Or(Const(false), e) => partEval(e)
case Or(e, Const(false)) => partEval(e)
- case Not(Const(c)) => Const(c) // FIXME should be !c
+ case Not(Const(c)) => Const(!c)
case other => other
}} ensuring { size(_) <= size(formula) }
diff --git a/testcases/synthesis/repair/PropLogic/PropLogic3.scala b/testcases/synthesis/repair/PropLogic/PropLogic3.scala
index 600c59ed2..b65f6e2a2 100644
--- a/testcases/synthesis/repair/PropLogic/PropLogic3.scala
+++ b/testcases/synthesis/repair/PropLogic/PropLogic3.scala
@@ -29,16 +29,16 @@ object SemanticsPreservation {
def nnf(formula : Formula) : Formula = { formula match {
case Not(And(lhs,rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
case Not(Or(lhs,rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs)))
- case Not(Const(v)) => Const(!v)
+ case Not(Const(v)) => Const(v) // FIXME should be !v.
+ case Not(Not(e)) => nnf(e)
case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
- // FIXME: forgot to handle the Not(Not(_)) case
case other => other
- }} ensuring { res =>
- isNNF(res) && ((formula, res) passes {
- case Not(And(Const(a), Const(b))) => Or(Const(!a), Const(!b))
- case x@And(Literal(_), Literal(_)) => x
- })
+ }} ensuring { res =>
+ isNNF(res) && ((formula, res) passes {
+ case Not(Const(true)) => Const(false)
+ case Not(Const(false)) => Const(true)
+ })
}
def isNNF(f : Formula) : Boolean = f match {
@@ -49,23 +49,4 @@ object SemanticsPreservation {
case _ => true
}
- def partEval(formula : Formula) : Formula = { formula match {
- case And(Const(false), _ ) => Const(false)
- case And(_, Const(false)) => Const(false)
- case And(Const(true), e) => partEval(e)
- case And(e, Const(true)) => partEval(e)
- case Or(Const(true), _ ) => Const(true)
- case Or(_, Const(true)) => Const(true)
- case Or(Const(false), e) => partEval(e)
- case Or(e, Const(false)) => partEval(e)
- case Not(Const(c)) => Const(!c)
- case other => other
- }} ensuring { size(_) <= size(formula) }
-
-
- @induct
- def partEvalSound (f : Formula, env : Set[Int]) = {
- eval(partEval(f))(env) == eval(f)(env)
- }.holds
-
}
diff --git a/testcases/synthesis/repair/PropLogic/PropLogic4.scala b/testcases/synthesis/repair/PropLogic/PropLogic4.scala
index facbe08aa..20e44fe92 100644
--- a/testcases/synthesis/repair/PropLogic/PropLogic4.scala
+++ b/testcases/synthesis/repair/PropLogic/PropLogic4.scala
@@ -1,3 +1,4 @@
+// Fails
import leon.lang._
import leon.annotation._
import leon.collection._
@@ -32,13 +33,12 @@ object SemanticsPreservation {
case Not(Const(v)) => Const(!v)
case Not(Not(e)) => nnf(e)
case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
- case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
+ case Or(lhs, rhs) => And(nnf(lhs), nnf(rhs)) // FIXME should be Or
case other => other
}} ensuring { res =>
- isNNF(res) && ((formula, res) passes {
- case Not(And(Const(a), Const(b))) => Or(Const(!a), Const(!b))
- case x@And(Literal(_), Literal(_)) => x
- })
+ isNNF(res) && ((formula, res) passes {
+ case Or(Not(Const(c)), Not(Literal(l))) => Or(Const(c), Not(Literal(l)))
+ })
}
def isNNF(f : Formula) : Boolean = f match {
@@ -49,24 +49,4 @@ object SemanticsPreservation {
case _ => true
}
- def partEval(formula : Formula) : Formula = { formula match {
- case And(Const(false), _ ) => Const(false)
- case And(_, Const(false)) => Const(false)
- case And(Const(true), e) => partEval(e)
- case And(e, Const(true)) => partEval(e)
- // FIXME (hard!) : treats Or as And
- case Or(Const(false), _ ) => Const(false)
- case Or(_, Const(false)) => Const(false)
- case Or(Const(true), e) => partEval(e)
- case Or(e, Const(true)) => partEval(e)
- case Not(Const(c)) => Const(!c)
- case other => other
- }} ensuring { size(_) <= size(formula) }
-
-
- @induct
- def partEvalSound (f : Formula, env : Set[Int]) = {
- eval(partEval(f))(env) == eval(f)(env)
- }.holds
-
}
diff --git a/testcases/synthesis/repair/PropLogic/PropLogic6.scala b/testcases/synthesis/repair/PropLogic/PropLogic6.scala
deleted file mode 100644
index 4fee819e2..000000000
--- a/testcases/synthesis/repair/PropLogic/PropLogic6.scala
+++ /dev/null
@@ -1,73 +0,0 @@
-import leon.lang._
-import leon.annotation._
-import leon.collection._
-
-object SemanticsPreservation {
-
- sealed abstract class Formula
- case class And(lhs : Formula, rhs : Formula) extends Formula
- case class Or(lhs : Formula, rhs : Formula) extends Formula
- case class Not(f: Formula) extends Formula
- case class Const(v: Boolean) extends Formula
- case class Literal(id: Int) extends Formula
-
- def size(f : Formula) : Int = { f match {
- case And(l,r) => 1 + size(l) + size(r)
- case Or(l,r) => 1 + size(l) + size(r)
- case Not(e) => 1 + size(e)
- case _ => 1
- }} ensuring { _ >= 0 }
-
- def eval(formula: Formula)(implicit trueVars : Set[Int]): Boolean = formula match {
- case And(lhs, rhs) => eval(lhs) && eval(rhs)
- case Or(lhs, rhs) => eval(lhs) || eval(rhs)
- case Not(f) => !eval(f)
- case Const(v) => v
- case Literal(id) => trueVars contains id
- }
-
- def nnf(formula : Formula) : Formula = { formula match {
- case Not(And(lhs,rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
- case Not(Or(lhs,rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs)))
- case Not(Const(v)) => Const(!v)
- case Not(Not(e)) => nnf(e)
- case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
- case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
- case other => other
- }} ensuring { res =>
- isNNF(res) && ((formula, res) passes {
- case Not(And(Const(a), Const(b))) => Or(Const(!a), Const(!b))
- case x@And(Literal(_), Literal(_)) => x
- })
- }
-
- def isNNF(f : Formula) : Boolean = f match {
- case Not(Literal(_)) => true
- case Not(_) => false
- case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
- case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
- case _ => true
- }
-
- def partEval(formula : Formula) : Formula = { formula match {
- case And(Const(false), _ ) => Const(false)
- case And(_, Const(false)) => Const(false)
- case And(Const(true), e) => partEval(e)
- case And(e, Const(true)) => partEval(e)
- case Or(Const(true), _ ) => Const(true)
- case Or(_, Const(true)) => Const(true)
- case Or(Const(false), e) => partEval(e)
- case Or(e, Const(false)) => partEval(e)
- case Not(Const(c)) => Const(!c)
- case other => other
- }} ensuring { size(_) < size(formula) }
- // FIXME: should be <=
- // Can you realize you cannot fix this without breaking partEvalSound?
-
-
- @induct
- def partEvalSound (f : Formula, env : Set[Int]) = {
- eval(partEval(f))(env) == eval(f)(env)
- }.holds
-
-}
--
GitLab