From f3f28f6e1c1cdee9278a0d97ff94de6d4fed58c4 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 1 Jul 2015 18:38:26 +0200
Subject: [PATCH] Update benchmarks
---
testcases/repair/Compiler/Compiler7.scala | 212 ---------------------
testcases/repair/Heap/Heap.scala | 18 +-
testcases/repair/List/List1.scala | 4 +-
testcases/repair/PropLogic/PropLogic.scala | 6 +-
4 files changed, 13 insertions(+), 227 deletions(-)
delete mode 100644 testcases/repair/Compiler/Compiler7.scala
diff --git a/testcases/repair/Compiler/Compiler7.scala b/testcases/repair/Compiler/Compiler7.scala
deleted file mode 100644
index 890f42f6e..000000000
--- a/testcases/repair/Compiler/Compiler7.scala
+++ /dev/null
@@ -1,212 +0,0 @@
-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: BigInt) 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) : BigInt = {
- 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): BigInt = if (b) 1 else 0
-
- @induct
- def semUntyped( t : Expr) : BigInt = { 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 : BigInt) 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) : BigInt = e match {
- case Plus (lhs, rhs) => sem(lhs) + sem(rhs)
- case Ite(cond, thn, els) => if (sem(cond) != 0) sem(thn) else sem(els)
- case Neg(arg) => -sem(arg)
- case Eq(lhs,rhs) => b2i(sem(lhs) == sem(rhs))
- case LessThan(lhs, rhs) => b2i(sem(lhs) < sem(rhs))
- case Literal(i) => i
- }
-
-}
-
-object Evaluator {
- import Trees._
-
- def bToi(b: Boolean): BigInt = if (b) 1 else 0
- def iTob(i: BigInt) = i == 1
-
- def eval(e: Expr): BigInt = {
- e match {
- case Plus(lhs, rhs) => eval(lhs) + eval(rhs)
- case Minus(lhs, rhs) => eval(lhs) + eval(rhs)
- case LessThan(lhs, rhs) => bToi(eval(lhs) < eval(rhs))
- case And(lhs, rhs) => bToi(iTob(eval(lhs)) && iTob(eval(rhs)))
- case Or(lhs, rhs) => bToi(iTob(eval(lhs)) || iTob(eval(rhs)))
- case Not(e) => bToi(!iTob(eval(e)))
- case Eq(lhs, rhs) => bToi(eval(lhs) == eval(rhs))
- case Ite(cond, thn, els) => if (iTob(eval(cond))) eval(thn) else eval(els)
- case IntLiteral(v) => v
- case BoolLiteral(b) => bToi(b)
- }
- }
-}
-
-object Simplifier {
- import Trees._
- import Evaluator._
-
- @induct
- def simplify(e: Expr): Expr = {
- e match {
- case And(BoolLiteral(false), _) => BoolLiteral(false)
- case Or(BoolLiteral(true), _) => BoolLiteral(false) // FIMXE
- case Plus(IntLiteral(a), IntLiteral(b)) => IntLiteral(a+b)
- case Not(Not(Not(a))) => Not(a)
- case e => e
- }
- } ensuring {
- res => eval(res) == eval(e)
- }
-}
diff --git a/testcases/repair/Heap/Heap.scala b/testcases/repair/Heap/Heap.scala
index c7df65b60..71f18a760 100644
--- a/testcases/repair/Heap/Heap.scala
+++ b/testcases/repair/Heap/Heap.scala
@@ -10,20 +10,20 @@ import leon.collection._
object Heaps {
sealed abstract class Heap {
- val rank : BigBigInt = this match {
+ val rank : BigInt = this match {
case Leaf() => 0
case Node(_, l, r) =>
1 + max(l.rank, r.rank)
}
- def content : Set[BigBigInt] = this match {
- case Leaf() => Set[BigBigInt]()
+ def content : Set[BigInt] = this match {
+ case Leaf() => Set[BigInt]()
case Node(v,l,r) => l.content ++ Set(v) ++ r.content
}
}
case class Leaf() extends Heap
- case class Node(value:BigBigInt, left: Heap, right: Heap) extends Heap
+ case class Node(value: BigInt, left: Heap, right: Heap) extends Heap
- def max(i1 : BigBigInt, i2 : BigBigInt) = if (i1 >= i2) i1 else i2
+ def max(i1: BigInt, i2: BigInt) = if (i1 >= i2) i1 else i2
def hasHeapProperty(h : Heap) : Boolean = h match {
case Leaf() => true
@@ -46,7 +46,7 @@ object Heaps {
l.rank >= r.rank
}
- def heapSize(t: Heap): BigBigInt = { t match {
+ def heapSize(t: Heap): BigInt = { t match {
case Leaf() => 0
case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
}} ensuring(_ >= 0)
@@ -71,7 +71,7 @@ object Heaps {
h1.content ++ h2.content == res.content
}
- private def makeN(value: BigBigInt, left: Heap, right: Heap) : Heap = {
+ private def makeN(value: BigInt, left: Heap, right: Heap) : Heap = {
require(
hasLeftistProperty(left) && hasLeftistProperty(right)
)
@@ -82,7 +82,7 @@ object Heaps {
} ensuring { res =>
hasLeftistProperty(res) }
- def insert(element: BigBigInt, heap: Heap) : Heap = {
+ def insert(element: BigInt, heap: Heap) : Heap = {
require(hasLeftistProperty(heap) && hasHeapProperty(heap))
merge(Node(element, Leaf(), Leaf()), heap)
@@ -93,7 +93,7 @@ object Heaps {
res.content == heap.content ++ Set(element)
}
- def findMax(h: Heap) : Option[BigBigInt] = {
+ def findMax(h: Heap) : Option[BigInt] = {
h match {
case Node(m,_,_) => Some(m)
case Leaf() => None()
diff --git a/testcases/repair/List/List1.scala b/testcases/repair/List/List1.scala
index ffa4f480e..53a496055 100644
--- a/testcases/repair/List/List1.scala
+++ b/testcases/repair/List/List1.scala
@@ -173,9 +173,7 @@ sealed abstract class List[T] {
case (Cons(h, t), s) =>
Cons(h, t.pad(s-1, e)) // FIXME should be s
}} ensuring { res =>
- ((this,s,e), res) passes {
- case (Cons(a,Nil()), BigInt(2), x) => Cons(a, Cons(x, Cons(x, Nil())))
- }
+ (s > 0) ==> (res.size == this.size + s && res.contains(e))
}
def find(e: T): Option[BigInt] = this match {
diff --git a/testcases/repair/PropLogic/PropLogic.scala b/testcases/repair/PropLogic/PropLogic.scala
index b654b8fbc..2819234ff 100644
--- a/testcases/repair/PropLogic/PropLogic.scala
+++ b/testcases/repair/PropLogic/PropLogic.scala
@@ -9,16 +9,16 @@ object SemanticsPreservation {
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: BigBigInt) extends Formula
+ case class Literal(id: BigInt) extends Formula
- def size(f : Formula) : BigBigInt = { f match {
+ def size(f : Formula) : BigInt = { 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[BigBigInt]): Boolean = formula match {
+ def eval(formula: Formula)(implicit trueVars : Set[BigInt]): Boolean = formula match {
case And(lhs, rhs) => eval(lhs) && eval(rhs)
case Or(lhs, rhs) => eval(lhs) || eval(rhs)
case Not(f) => !eval(f)
--
GitLab