From 79020284e9d9294f1e56dd8955545df31713eed1 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 17 Dec 2015 16:20:55 +0100
Subject: [PATCH] latest fixes to testcases/instrumentation
---
src/main/scala/leon/repair/Repairman.scala | 5 +--
.../scala/leon/synthesis/Synthesizer.scala | 2 +-
testcases/repair/Compiler/Compiler4.scala | 2 +-
testcases/repair/List/List4.scala | 22 ++++++------
testcases/repair/List/List5.scala | 2 +-
testcases/repair/runTests.sh | 34 ++++++++++---------
6 files changed, 36 insertions(+), 31 deletions(-)
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 72f3b09e8..6523a1104 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -136,7 +136,8 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
val (solSize, proof) = solutions.headOption match {
case Some((sol, trusted)) =>
- val totalSolSize = formulaSize(sol.toSimplifiedExpr(ctx, program))
+ val solExpr = sol.toSimplifiedExpr(ctx, program)
+ val totalSolSize = formulaSize(solExpr)
(locSize+totalSolSize-fSize, if (trusted) "$\\chmark$" else "")
case _ =>
(0, "X")
@@ -147,7 +148,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou
val fw = new java.io.FileWriter("repair-report.txt", true)
try {
- fw.write(f"$date: $benchName%-30s & $pSize%4d & $fSize%4d & $locSize%4d & $solSize%4d & ${timeTests/1000.0}%.2f & & ${timeSynth/1000.0}%.2f & $proof%7s \\\\\n")
+ fw.write(f"$date: $benchName%-30s & $pSize%4d & $fSize%4d & $locSize%4d & $solSize%4d & ${timeTests/1000.0}%2.1f & ${timeSynth/1000.0}%2.1f & $proof%7s \\\\\n")
} finally {
fw.close
}
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 911a06ce5..bafed6ec2 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -99,7 +99,7 @@ class Synthesizer(val context : LeonContext,
val fw = new java.io.FileWriter("synthesis-report.txt", true)
try {
- fw.write(f"$date: $benchName%-50s & $psize%4d & $size%4d & $calls%4d & $proof%7s & $time%.2f \\\\\n")
+ fw.write(f"$date: $benchName%-50s & $psize%4d & $size%4d & $calls%4d & $proof%7s & $time%2.1f \\\\\n")
} finally {
fw.close
}
diff --git a/testcases/repair/Compiler/Compiler4.scala b/testcases/repair/Compiler/Compiler4.scala
index f49670ddc..6323496df 100644
--- a/testcases/repair/Compiler/Compiler4.scala
+++ b/testcases/repair/Compiler/Compiler4.scala
@@ -150,7 +150,7 @@ object Desugar {
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)) // FIMXE should be 0
+ case Trees.Not(e) => Ite(desugar(e), Literal(1), Literal(1)) // FIXME 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))
diff --git a/testcases/repair/List/List4.scala b/testcases/repair/List/List4.scala
index b6cb5e276..1ee180b33 100644
--- a/testcases/repair/List/List4.scala
+++ b/testcases/repair/List/List4.scala
@@ -78,16 +78,18 @@ sealed abstract class List[T] {
}
}
- def drop(i: BigInt): List[T] = { (this, i) match {
- case (Nil(), _) => Nil[T]()
- case (Cons(h, t), i) =>
- // FIXME
- //if (i == 0) {
- // Cons(h, t)
- //} else {
- t.drop(i-1)
- //}
- }} ensuring { ((this, i), _) passes {
+ def drop(i: BigInt): List[T] = {
+ (this, i) match {
+ case (Nil(), _) => Nil[T]()
+ case (Cons(h, t), i) =>
+ // FIXME
+ if (i != 0) {
+ Cons(h, t)
+ } else {
+ t.drop(i-1)
+ }
+ }
+ } ensuring { ((this, i), _) passes {
case (Cons(_, Nil()), BigInt(42)) => Nil()
case (l@Cons(_, _), BigInt(0)) => l
case (Cons(a, Cons(b, Nil())), BigInt(1)) => Cons(b, Nil())
diff --git a/testcases/repair/List/List5.scala b/testcases/repair/List/List5.scala
index 3c109722c..f13f91da3 100644
--- a/testcases/repair/List/List5.scala
+++ b/testcases/repair/List/List5.scala
@@ -97,7 +97,7 @@ sealed abstract class List[T] {
case Nil() => Nil[T]()
case Cons(h, t) =>
val r = t.replace(from, to)
- if (h != from) {
+ if (h != from) { // FIXME
Cons(to, r)
} else {
Cons(h, r)
diff --git a/testcases/repair/runTests.sh b/testcases/repair/runTests.sh
index 5ad1c857c..fb92991cb 100755
--- a/testcases/repair/runTests.sh
+++ b/testcases/repair/runTests.sh
@@ -16,22 +16,24 @@ echo "# Category, File, function, p.S, fuS
#All benchmarks:
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler1.scala | tee -a $fullLog
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler2.scala | tee -a $fullLog
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler3.scala | tee -a $fullLog
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler4.scala | tee -a $fullLog
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler5.scala | tee -a $fullLog
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=simplify testcases/repair/Compiler/Compiler6.scala | tee -a $fullLog
-#
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap3.scala | tee -a $fullLog
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap4.scala | tee -a $fullLog
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap5.scala | tee -a $fullLog
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap6.scala | tee -a $fullLog
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap7.scala | tee -a $fullLog
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=insert testcases/repair/Heap/Heap8.scala | tee -a $fullLog
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=makeN testcases/repair/Heap/Heap9.scala | tee -a $fullLog
-#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap10.scala | tee -a $fullLog
-#
+echo "=====================================================================" >> repair-report.txt
+
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler1.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler2.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler3.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler4.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=desugar testcases/repair/Compiler/Compiler5.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=simplify testcases/repair/Compiler/Compiler6.scala | tee -a $fullLog
+
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap3.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap4.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap5.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap6.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap7.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=merge testcases/repair/Heap/Heap10.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=insert testcases/repair/Heap/Heap8.scala | tee -a $fullLog
+./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=makeN testcases/repair/Heap/Heap9.scala | tee -a $fullLog
+
#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=nnf testcases/repair/PropLogic/PropLogic1.scala | tee -a $fullLog
#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=nnf testcases/repair/PropLogic/PropLogic2.scala | tee -a $fullLog
#./leon --debug=report --repair --timeout=30 --solvers=fairz3,enum --functions=nnf testcases/repair/PropLogic/PropLogic3.scala | tee -a $fullLog
--
GitLab