Added script to test for string repair

Added repair functions for TupleWrapperRender.scala
Added reference to leon.lang.String

testcases/stringrender/BinaryTreeRender.scala

@@ -6,6 +6,7 @@
   */
 
 import leon.lang._
+import string.String
 import leon.annotation._
 import leon.collection._
 import leon.collection.ListOps._

testcases/stringrender/GrammarRender.scala

 /**
   * Name:     GrammarRender.scala
   * Creation: 15.10.2015
-  * Author:   Mikal Mayer (mikael.mayer@epfl.ch)
+  * Author:   Mika�l Mayer (mikael.mayer@epfl.ch)
   * Comments: Grammar rendering specifications.
   */
 
 import leon.lang._
+import string.String
 import leon.annotation._
 import leon.collection._
 import leon.collection.ListOps._
 import leon.lang.synthesis._
 
-object GraarRender {
+object Gra��arRender {
   abstract class Symbol
   case class Terminal(i: Int) extends Symbol
   case class NonTerminal(i: Int) extends Symbol

testcases/stringrender/IntWrapperRender.scala

@@ -6,6 +6,7 @@
   */
 
 import leon.lang._
+import string.String
 import leon.annotation._
 import leon.collection._
 import leon.collection.ListOps._
@@ -44,6 +45,22 @@ object IntWrapperRender {
     case IntWrapper(12) => "12 12"
   }
   
+  def repairUnWrapped(s: IntWrapper): String = {
+    "IntWrapper(" + s.i + ")""
+  } ensuring psUnWrapped(s)
+  
+  def repairNameChangedPrefix(s: IntWrapper): String = {
+    "IntWrapper(" + s.i + ")""
+  } ensuring psNameChangedPrefix(s)
+  
+  def repairNameChangedSuffix(s: IntWrapper): String = {
+    "IntWrapper(" + s.i + ")""
+  } ensuring psNameChangedSuffix(s)
+  
+  def repairDuplicate(s: IntWrapper): String = {
+    "IntWrapper(" + s.i + ")""
+  } ensuring psDuplicate(s)
+  
   def synthesisStandard(s: IntWrapper): String = {
      ???[String]
   } ensuring psStandard(s)

testcases/stringrender/ListBigIntRender.scala

 /** 
   * Name:     ListBigIntRender.scala
   * Creation: 15.10.2015
-  * Author:   Mikaël Mayer (mikael.mayer@epfl.ch)
+  * Author:   Mika�l Mayer (mikael.mayer@epfl.ch)
   * Comments: List of BigInt specifications.
   */
 
 import leon.lang._
+import string.String
 import leon.annotation._
 import leon.collection._
 import leon.collection.ListOps._

testcases/stringrender/ListRender.scala

 /** 
   * Name:     ListRender.scala
   * Creation: 14.10.2015
-  * Author:   Mikaël Mayer (mikael.mayer@epfl.ch)
+  * Author:   Mika�l Mayer (mikael.mayer@epfl.ch)
   * Comments: First benchmark ever for solving string transformation problems. List specifications.
   */
 
 import leon.lang._
+import string.String
 import leon.annotation._
 import leon.collection._
 import leon.collection.ListOps._

testcases/stringrender/TupleWrapperRender.scala

@@ -6,6 +6,7 @@
   */
 
 import leon.lang._
+import string.String
 import leon.annotation._
 import leon.collection._
 import leon.collection.ListOps._
@@ -44,6 +45,23 @@ object TupleWrapperRender {
     case TupleWrapper(12, 5) => "d 12,5 12,15 15,15 15,5"
   }
   
+  def repairUnWrapped(s: IntWrapper): String = {
+    "TupleWrapper(" + s.i + ", " + s.j + ")""
+  } ensuring psUnWrapped(s)
+  
+  def repairNameChangedPrefix(s: IntWrapper): String = {
+    "TupleWrapper(" + s.i + ", " + s.j + ")""
+  } ensuring psNameChangedPrefix(s)
+  
+  def repairNameChangedSuffix(s: IntWrapper): String = {
+    "TupleWrapper(" + s.i + ", " + s.j + ")""
+  } ensuring psNameChangedSuffix(s)
+  
+  def repairDuplicate(s: IntWrapper): String = {
+    "TupleWrapper(" + s.i + ", " + s.j + ")""
+  } ensuring psDuplicate(s)
+  
+  
   def synthesisStandard(s: TupleWrapper): String = {
      ???[String]
   } ensuring psStandard(s)

testcases/stringrender/runTests.sh

+#!/bin/bash
+log=stringrender.last
+summaryLog=stringrender.log
+fullLog=fullLog.log
+
+echo -n "" > $log;
+echo -n "" > "stringrender.table";
+
+
+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 --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairUnWrapped          testcases/stringrender/IntWrapperRender.scala     | tee -a $fullLog
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairNameChangedPrefix  testcases/stringrender/IntWrapperRender.scala     | tee -a $fullLog
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairNameChangedSuffix  testcases/stringrender/IntWrapperRender.scala     | tee -a $fullLog
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairDuplicate          testcases/stringrender/IntWrapperRender.scala     | tee -a $fullLog
+
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairUnWrapped          testcases/stringrender/TupleWrapperRender.scala   | tee -a $fullLog
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairNameChangedPrefix  testcases/stringrender/TupleWrapperRender.scala   | tee -a $fullLog
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairNameChangedSuffix  testcases/stringrender/TupleWrapperRender.scala   | tee -a $fullLog
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairDuplicate          testcases/stringrender/TupleWrapperRender.scala   | tee -a $fullLog
+
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=render1RemoveCons        testcases/stringrender/ListRender.scala           | tee -a $fullLog
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=render2RemoveNil         testcases/stringrender/ListRender.scala           | tee -a $fullLog
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=render3RemoveLastComma   testcases/stringrender/ListRender.scala           | tee -a $fullLog
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=render4RemoveParentheses testcases/stringrender/ListRender.scala           | tee -a $fullLog
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=render5WrapParentheses   testcases/stringrender/ListRender.scala           | tee -a $fullLog
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=render6List              testcases/stringrender/ListRender.scala           | tee -a $fullLog
+
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=render0RemoveBigInt      testcases/stringrender/ListBigIntRender.scala     | tee -a $fullLog
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=render1RemoveCons        testcases/stringrender/ListBigIntRender.scala     | tee -a $fullLog
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=render2RemoveNil         testcases/stringrender/ListBigIntRender.scala     | tee -a $fullLog
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=render3RemoveLastComma   testcases/stringrender/ListBigIntRender.scala     | tee -a $fullLog
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=render4RemoveParentheses testcases/stringrender/ListBigIntRender.scala     | tee -a $fullLog
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=render5WrapParentheses   testcases/stringrender/ListBigIntRender.scala     | tee -a $fullLog
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=render6List              testcases/stringrender/ListBigIntRender.scala     | tee -a $fullLog
+
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=render0RemoveNames       testcases/stringrender/GrammarRender.scala        | tee -a $fullLog
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=render1ArrowRules        testcases/stringrender/GrammarRender.scala        | tee -a $fullLog
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=render2ListRules         testcases/stringrender/GrammarRender.scala        | tee -a $fullLog
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=render3SpaceRules        testcases/stringrender/GrammarRender.scala        | tee -a $fullLog
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=render4HTMLRules         testcases/stringrender/GrammarRender.scala        | tee -a $fullLog
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=render5PlainTextRules    testcases/stringrender/GrammarRender.scala        | tee -a $fullLog
+
+
+# Average results
+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
+