From f60acb81f06a7cf74a1f20cd55670c0bc86abd4c Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Wed, 4 Feb 2015 17:33:57 +0100
Subject: [PATCH] Small changes
---
runTests.sh | 78 ++++++++++---------
src/main/scala/leon/repair/Repairman.scala | 7 +-
.../leon/synthesis/rules/CegisLike.scala | 2 +-
testcases/repair/List/List5.scala | 7 +-
4 files changed, 49 insertions(+), 45 deletions(-)
diff --git a/runTests.sh b/runTests.sh
index 8f571b316..d7ca90f21 100755
--- a/runTests.sh
+++ b/runTests.sh
@@ -1,49 +1,51 @@
#!/bin/bash
log=repairs.last
-fullLog=repairs.log
+summaryLog=repairs.log
+fullLog=fullLog.log
echo -n "" > $log;
-echo "################################" >> $fullLog
-echo "#" `hostname` >> $fullLog
-echo "#" `date +"%d.%m.%Y %T"` >> $fullLog
-echo "#" `git log -1 --pretty=format:"%h - %cd"` >> $fullLog
-echo "################################" >> $fullLog
-echo "# Category, File, function, p.S, fuS, foS, Tms, Fms, Rms, verif?" >> $fullLog
+echo "################################" >> $summaryLog
+echo "#" `hostname` >> $summaryLog
+echo "#" `date +"%d.%m.%Y %T"` >> $summaryLog
+echo "#" `git log -1 --pretty=format:"%h - %cd"` >> $summaryLog
+echo "################################" >> $summaryLog
+echo "# Category, File, function, p.S, fuS, foS, Tms, Fms, Rms, verif?" >> $summaryLog
#All benchmarks:
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar1.scala
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar2.scala
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar3.scala
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar4.scala
-
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort3.scala
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort4.scala
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort5.scala
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort6.scala
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort7.scala
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=insert testcases/repair/HeapSort/HeapSort8.scala
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=makeN testcases/repair/HeapSort/HeapSort9.scala
-
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=nnf testcases/repair/PropLogic/PropLogic1.scala
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=nnf testcases/repair/PropLogic/PropLogic2.scala
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=nnf testcases/repair/PropLogic/PropLogic3.scala
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=nnf testcases/repair/PropLogic/PropLogic4.scala
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=nnf testcases/repair/PropLogic/PropLogic5.scala
-
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=_pad testcases/repair/List/List1.scala
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=_ap testcases/repair/List/List3.scala
-./leon --repair --timeout=30 --functions=_drop testcases/repair/List/List4.scala
-./leon --repair --timeout=30 --functions=_replace testcases/repair/List/List5.scala
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=_count testcases/repair/List/List6.scala
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=_find testcases/repair/List/List7.scala
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=_find testcases/repair/List/List8.scala
-./leon --repair --timeout=30 --functions=_find testcases/repair/List/List9.scala
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=_size testcases/repair/List/List10.scala
-./leon --repair --timeout=30 --solvers=fairz3:enum --functions=sum testcases/repair/List/List11.scala
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar1.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar2.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar3.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=desugar testcases/repair/Desugar/Desugar4.scala | tee -a $fullLog
+
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort3.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort4.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort5.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort6.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=merge testcases/repair/HeapSort/HeapSort7.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=insert testcases/repair/HeapSort/HeapSort8.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=makeN testcases/repair/HeapSort/HeapSort9.scala | tee -a $fullLog
+
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=nnf testcases/repair/PropLogic/PropLogic1.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=nnf testcases/repair/PropLogic/PropLogic2.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=nnf testcases/repair/PropLogic/PropLogic3.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=nnf testcases/repair/PropLogic/PropLogic4.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=nnf testcases/repair/PropLogic/PropLogic5.scala | tee -a $fullLog
+
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=_pad testcases/repair/List/List1.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=_++ testcases/repair/List/List2.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=_ap testcases/repair/List/List3.scala | tee -a $fullLog
+./leon --repair --timeout=30 --functions=_drop testcases/repair/List/List4.scala | tee -a $fullLog
+./leon --repair --timeout=30 --functions=_replace testcases/repair/List/List5.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=_count testcases/repair/List/List6.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=_find testcases/repair/List/List7.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=_find testcases/repair/List/List8.scala | tee -a $fullLog
+./leon --repair --timeout=30 --functions=_find testcases/repair/List/List9.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=_size testcases/repair/List/List10.scala | tee -a $fullLog
+./leon --repair --timeout=30 --solvers=fairz3:enum --functions=sum testcases/repair/List/List11.scala | tee -a $fullLog
# Average results
-cat $log >> $fullLog
-awk '{ total1 += $7; total2 += $8; total3 += $9; count++ } END { printf "#%74s Avg: %5d, %5d, %5d\n\n", "", total1/count, total2/count, total3/count }' $log >> $fullLog
+cat $log >> $summaryLog
+awk '{ total1 += $7; total2 += $8; total3 += $9; count++ } END { printf "#%74s Avg: %5d, %5d, %5d\n\n", "", total1/count, total2/count, total3/count }' $log >> $summaryLog
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 1ee872e64..e1bd46593 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -79,6 +79,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
val t3 = new Timer().start
synth.synthesize() match {
case (search, sols) =>
+ result = result.copy(repairTime = Some(t3.stop))
for (sol <- sols) {
// Validate solution if not trusted
@@ -115,7 +116,6 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
if (solutions.isEmpty) {
reporter.error(ASCIIHelpers.title("Failed to repair!"))
} else {
- result = result.copy(repairTime = Some(t3.stop))
reporter.info(ASCIIHelpers.title("Repair successful:"))
for ((sol, i) <- solutions.reverse.zipWithIndex) {
@@ -157,11 +157,12 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
val size = formulaSize(body)
val focusSize = formulaSize(replacedExpr)
+ result = result.copy(name = fd.id.name, fsize = size, focusSize = Some(focusSize))
+
+ reporter.info("Program size : "+result.psize)
reporter.info("Original body size: "+size)
reporter.info("Focused expr size : "+focusSize)
- result = result.copy(name = fd.id.name, fsize = size, focusSize = Some(focusSize))
-
val guide = Guide(replacedExpr)
// Return synthesizer for this choose
diff --git a/src/main/scala/leon/synthesis/rules/CegisLike.scala b/src/main/scala/leon/synthesis/rules/CegisLike.scala
index 98d7b68cd..5cb20981e 100644
--- a/src/main/scala/leon/synthesis/rules/CegisLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CegisLike.scala
@@ -859,7 +859,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
val e = examples.next()
if (!ndProgram.testForProgram(bs)(e)) {
failedTestsStats(e) += 1
- //sctx.reporter.debug(" Program: "+ndProgram.getExpr(bs)+" failed on "+e)
+ sctx.reporter.debug(" Program: "+ndProgram.getExpr(bs)+" failed on "+e.mkString(" ; "))
wrongPrograms += bs
prunedPrograms -= bs
diff --git a/testcases/repair/List/List5.scala b/testcases/repair/List/List5.scala
index 82e604eaf..46e6e4d50 100644
--- a/testcases/repair/List/List5.scala
+++ b/testcases/repair/List/List5.scala
@@ -96,10 +96,11 @@ sealed abstract class List0[T] {
case Nil0() => Nil0()
case Cons0(h, t) =>
val r = t.replace(from, to)
- Cons0(to, r) // FIXME
+ Cons0(h, r) // FIXME
}} ensuring { res =>
- (if(this.contains(from)) res.contains(to) else true) &&
- !res.contains(from) && res.size == this.size
+ (((this.content -- Set(from)) ++
+ (if (this.content contains from) Set(to) else Set[T]())) == res.content) &&
+ res.size == this.size
}
private def chunk0(s: Int, l: List0[T], acc: List0[T], res: List0[List0[T]], s0: Int): List0[List0[T]] = l match {
--
GitLab