Benchmark additions/changes

testcases/synthesis/repair/DaysToYears/DaysToYears2.scala

+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 ))
+  }
+}
+

testcases/synthesis/repair/DaysToYears/DaysToYears3.scala

+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 ))
+  }
+}
+

testcases/synthesis/repair/Desugar/Desugar.scala

+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
+  }
+
+}

testcases/synthesis/repair/Desugar/Desugar1.scala

+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
+  }
+
+}

testcases/synthesis/repair/Desugar/Desugar2.scala

+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
+  }
+
+}

testcases/synthesis/repair/Desugar/Desugar3.scala

+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
+  }
+
+}

testcases/synthesis/repair/Desugar/Desugar4.scala

+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
+  }
+
+}

testcases/synthesis/repair/Parser/Parser1.scala

+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) 
+  }
+
+}

testcases/synthesis/repair/Parser/Parser2.scala

+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) 
+  }
+
+}

testcases/synthesis/repair/Parser/Parser3.scala

+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) 
+  }
+
+}

testcases/synthesis/repair/Parser/Parser4.scala

+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) 
+  }
+
+}

testcases/synthesis/repair/Parser/Parser5.scala

+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) 
+  }
+
+}

testcases/synthesis/repair/PropLogic/PropLogic5.scala → 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) }
 

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
-  
 }

testcases/synthesis/repair/PropLogic/PropLogic4.scala

+// 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
-  
 }

testcases/synthesis/repair/PropLogic/PropLogic6.scala

-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
-  
-}