diff --git a/testcases/stringrender/IntWrapperRender.scala b/testcases/stringrender/IntWrapperRender.scala
index cdac8112c6ff660e6c8c68f4ffad4796260e8b49..fda0004afa3f52454d62d544e272c5d40be229a6 100644
--- a/testcases/stringrender/IntWrapperRender.scala
+++ b/testcases/stringrender/IntWrapperRender.scala
@@ -38,11 +38,11 @@ object IntWrapperRender {
case IntWrapper(12) => "12.0"
}
- @inline def psDuplicate(s: IntWrapper) = (res: String) => (s, res) passes {
+ /*@inline def psDuplicate(s: IntWrapper) = (res: String) => (s, res) passes {
case IntWrapper(0) => "0 0"
case IntWrapper(-1) => "-1 -1"
case IntWrapper(12) => "12 12"
- }
+ }*/
def repairUnwrapped(s: IntWrapper): String = {
"IntWrapper(" + s.i + ")"
@@ -56,27 +56,27 @@ object IntWrapperRender {
"IntWrapper(" + s.i + ")"
} ensuring psNameChangedSuffix(s)
- def repairDuplicate(s: IntWrapper): String = {
+ /*def repairDuplicate(s: IntWrapper): String = {
"IntWrapper(" + s.i + ")"
- } ensuring psDuplicate(s)
+ } ensuring psDuplicate(s)*/
- def synthesisStandard(s: IntWrapper): String = {
+ def synthesizeStandard(s: IntWrapper): String = {
???[String]
} ensuring psStandard(s)
- def synthesisUnwrapped(s: IntWrapper): String = {
+ def synthesizeUnwrapped(s: IntWrapper): String = {
???[String]
} ensuring psUnwrapped(s)
- def synthesisNameChangedPrefix(s: IntWrapper): String = {
+ def synthesizeNameChangedPrefix(s: IntWrapper): String = {
???[String]
} ensuring psNameChangedPrefix(s)
- def synthesisNameChangedSuffix(s: IntWrapper): String = {
+ def synthesizeNameChangedSuffix(s: IntWrapper): String = {
???[String]
} ensuring psNameChangedSuffix(s)
- def synthesisDuplicate(s: IntWrapper): String = {
+ /*def synthesizeDuplicate(s: IntWrapper): String = {
???[String]
- } ensuring psDuplicate(s)
+ } ensuring psDuplicate(s)*/
}
\ No newline at end of file
diff --git a/testcases/stringrender/ListRender.scala b/testcases/stringrender/ListRender.scala
index dda6c44ef3922e671b8d32edee1773961793d835..b7519eac255947a73f15ba14423f2dd7ca75e900 100644
--- a/testcases/stringrender/ListRender.scala
+++ b/testcases/stringrender/ListRender.scala
@@ -6,7 +6,6 @@
*/
import leon.lang._
-import string.String
import leon.annotation._
import leon.collection._
import leon.collection.ListOps._
@@ -14,76 +13,76 @@ import leon.lang.synthesis._
object ListRender {
/** Synthesis by example specs */
- @inline def psStandard(s: List[Int])(res: String) = (s, res) passes {
- case Cons(12, Cons(-1, Nil)) => "Cons(12, Cons(-1, Nil))"
- case Cons(1, Nil) => "Cons(1, Nil)"
- case Nil => "Nil"
+ @inline def psStandard(s: List[Int]) = (res: String) =>(s, res) passes {
+ case Cons(12, Cons(-1, Nil())) => "Cons(12, Cons(-1, Nil))"
+ case Cons(1, Nil()) => "Cons(1, Nil)"
+ case Nil() => "Nil"
}
- @inline def psRemoveCons(s: List[Int])(res: String) = (s, res) passes {
- case Cons(12, Cons(-1, Nil)) => "(12, (-1, Nil))"
- case Cons(1, Nil) => "(1, Nil)"
- case Nil => "Nil"
+ @inline def psRemoveCons(s: List[Int]) = (res: String) =>(s, res) passes {
+ case Cons(12, Cons(-1, Nil())) => "(12, (-1, Nil))"
+ case Cons(1, Nil()) => "(1, Nil)"
+ case Nil() => "Nil"
}
- @inline def psRemoveNil(s: List[Int])(res: String) = (s, res) passes {
- case Cons(12, Cons(-1, Nil)) => "(12, (-1, ))"
- case Cons(1, Nil) => "(1, )"
- case Nil => ""
+ @inline def psRemoveNil(s: List[Int]) = (res: String) =>(s, res) passes {
+ case Cons(12, Cons(-1, Nil())) => "(12, (-1, ))"
+ case Cons(1, Nil()) => "(1, )"
+ case Nil() => ""
}
- @inline def psRemoveLastComma(s: List[Int])(res: String) = (s, res) passes {
- case Cons(12, Cons(-1, Nil)) => "(12, (-1))"
- case Cons(1, Nil) => "(1)"
- case Nil => "()"
+ @inline def psRemoveLastComma(s: List[Int]) = (res: String) =>(s, res) passes {
+ case Cons(12, Cons(-1, Nil())) => "(12, (-1))"
+ case Cons(1, Nil()) => "(1)"
+ case Nil() => "()"
}
- @inline def psRemoveParentheses(s: List[Int])(res: String) = (s, res) passes {
- case Cons(12, Cons(-1, Nil)) => "12, -1"
- case Cons(1, Nil) => "1"
- case Nil => ""
+ @inline def psRemoveParentheses(s: List[Int]) = (res: String) =>(s, res) passes {
+ case Cons(12, Cons(-1, Nil())) => "12, -1"
+ case Cons(1, Nil()) => "1"
+ case Nil() => ""
}
- @inline def psWrapParentheses(s: List[Int])(res: String) = (s, res) passes {
- case Cons(12, Cons(-1, Nil)) => "(12, -1)"
- case Cons(1, Nil) => "(1)"
- case Nil => "()"
+ @inline def psWrapParentheses(s: List[Int]) = (res: String) =>(s, res) passes {
+ case Cons(12, Cons(-1, Nil())) => "(12, -1)"
+ case Cons(1, Nil()) => "(1)"
+ case Nil() => "()"
}
- @inline def psList(s: List[Int])(res: String) = (s, res) passes {
- case Nil => "List()"
- case Cons(1, Nil) => "List(1)"
- case Cons(12, Cons(-1, Nil)) => "List(12, -1)"
+ @inline def psList(s: List[Int]) = (res: String) =>(s, res) passes {
+ case Nil() => "List()"
+ case Cons(1, Nil()) => "List(1)"
+ case Cons(12, Cons(-1, Nil())) => "List(12, -1)"
}
/** Each function's body is the solution of the previous problem.
* We want to check that the Leon can repair the programs and also find some ambiguities.*/
def render1RemoveCons(s: List[Int]): String = {
s match {
- case Nil => "Nil"
- case Cons(a, b) => "Cons(" + a + ", " + render1RemoveCons(b) + ")"
+ case Nil() => "Nil"
+ case Cons(a, b) => "Cons(" + a.toString + ", " + render1RemoveCons(b) + ")"
}
} ensuring psRemoveCons(s)
def render2RemoveNil(s: List[Int]): String = {
s match {
- case Nil => "Nil"
- case Cons(a, b) => "(" + a + ", " + render2RemoveNil(b) + ")"
+ case Nil() => "Nil"
+ case Cons(a, b) => "(" + a.toString + ", " + render2RemoveNil(b) + ")"
}
} ensuring psRemoveNil(s)
def render3RemoveLastComma(s: List[Int]): String = {
s match {
- case Nil => ""
- case Cons(a, b) => "(" + a + ", " + render3RemoveLastComma(b) + ")"
+ case Nil() => ""
+ case Cons(a, b) => "(" + a.toString + ", " + render3RemoveLastComma(b) + ")"
}
} ensuring psRemoveLastComma(s)
def render4RemoveParentheses(s: List[Int]): String = {
s match {
- case Nil => ""
- case Cons(a, Nil) => "(" + a + ")"
- case Cons(a, b) => "(" + a + ", " + render4RemoveParentheses(b) + ")"
+ case Nil() => ""
+ case Cons(a, Nil()) => "(" + a.toString + ")"
+ case Cons(a, b) => "(" + a.toString + ", " + render4RemoveParentheses(b) + ")"
}
} ensuring psRemoveParentheses(s)
@@ -91,18 +90,18 @@ object ListRender {
* in order to add strings to the left and to the right (see render6List) */
def render5WrapParentheses(s: List[Int]): String = {
s match {
- case Nil => ""
- case Cons(a, Nil) => a.toString
- case Cons(a, b) => a + ", " + render5WrapParentheses(b)
+ case Nil() => ""
+ case Cons(a, Nil()) => a.toString
+ case Cons(a, b) => a.toString + ", " + render5WrapParentheses(b)
}
} ensuring psWrapParentheses(s)
def render6List(s: List[Int]): String = {
def rec(s: List[Int]): String =
s match {
- case Nil => ""
- case Cons(a, Nil) => a
- case Cons(a, b) => a + ", " + render6List(b)
+ case Nil() => ""
+ case Cons(a, Nil()) => a.toString
+ case Cons(a, b) => a.toString + ", " + render6List(b)
}
"(" + rec(s) + ")"
} ensuring psList(s)
diff --git a/testcases/stringrender/TupleWrapperRender.scala b/testcases/stringrender/TupleWrapperRender.scala
index fcfc87991898e3a9270a3e44fe9767828fa49ef4..6df42174bc4f9e4a7cadec3067ce0df8ae028fd1 100644
--- a/testcases/stringrender/TupleWrapperRender.scala
+++ b/testcases/stringrender/TupleWrapperRender.scala
@@ -14,70 +14,70 @@ import leon.lang.synthesis._
object TupleWrapperRender {
case class TupleWrapper(i: Int, j: Int)
- def psStandard(s: TupleWrapper) = (res: String) => (s, res) passes {
+ @inline def psStandard(s: TupleWrapper) = (res: String) => (s, res) passes {
case TupleWrapper(0, 0) => "TupleWrapper(0, 0)"
case TupleWrapper(-1, 2) => "TupleWrapper(-1, 2)"
case TupleWrapper(12, 5) => "TupleWrapper(12, 5)"
}
- def psUnwrapped(s: TupleWrapper) = (res: String) => (s, res) passes {
+ @inline def psUnwrapped(s: TupleWrapper) = (res: String) => (s, res) passes {
case TupleWrapper(0, 0) => "0, 0"
case TupleWrapper(-1, 2) => "-1, 2"
case TupleWrapper(12, 5) => "12, 5"
}
- def psNameChangedPrefix(s: TupleWrapper) = (res: String) => (s, res) passes {
+ @inline def psNameChangedPrefix(s: TupleWrapper) = (res: String) => (s, res) passes {
case TupleWrapper(0, 0) => "x = 0, y = 0"
case TupleWrapper(-1, 2) => "x = -1, y = 2"
case TupleWrapper(12, 5) => "x = 12, y = 5"
}
- def psNameChangedSuffix(s: TupleWrapper) = (res: String) => (s, res) passes {
+ @inline def psNameChangedSuffix(s: TupleWrapper) = (res: String) => (s, res) passes {
case TupleWrapper(0, 0) => "0.0,0.0"
case TupleWrapper(-1, 2) => "-1.0,2.0" // Here there should be an ambiguity before this line.
case TupleWrapper(12, 5) => "12.0,5.0"
}
- def psDuplicate(s: TupleWrapper) = (res: String) => (s, res) passes {
+ /*@inline def psDuplicate(s: TupleWrapper) = (res: String) => (s, res) passes {
case TupleWrapper(0, 0) => "d 0,0 0,15 15,15 15,0"
case TupleWrapper(-1, 2) => "d -1,-2 -1,15 15,15 15,2"
case TupleWrapper(12, 5) => "d 12,5 12,15 15,15 15,5"
- }
+ }*/
def repairUnWrapped(s: TupleWrapper): String = {
- "TupleWrapper(" + s.i + ", " + s.j + ")""
- } ensuring psUnWrapped(s)
+ "TupleWrapper(" + s.i + ", " + s.j + ")"
+ } ensuring psUnwrapped(s)
def repairNameChangedPrefix(s: TupleWrapper): String = {
- "TupleWrapper(" + s.i + ", " + s.j + ")""
+ "TupleWrapper(" + s.i + ", " + s.j + ")"
} ensuring psNameChangedPrefix(s)
def repairNameChangedSuffix(s: TupleWrapper): String = {
- "TupleWrapper(" + s.i + ", " + s.j + ")""
+ "TupleWrapper(" + s.i + ", " + s.j + ")"
} ensuring psNameChangedSuffix(s)
- def repairDuplicate(s: TupleWrapper): String = {
- "TupleWrapper(" + s.i + ", " + s.j + ")""
- } ensuring psDuplicate(s)
+ /*def repairDuplicate(s: TupleWrapper): String = {
+ "TupleWrapper(" + s.i + ", " + s.j + ")"
+ } ensuring psDuplicate(s)*/
- def synthesisStandard(s: TupleWrapper): String = {
+ def synthesizeStandard(s: TupleWrapper): String = {
???[String]
} ensuring psStandard(s)
- def synthesisUnwrapped(s: TupleWrapper): String = {
+ def synthesizeUnwrapped(s: TupleWrapper): String = {
???[String]
} ensuring psUnwrapped(s)
- def synthesisNameChangedPrefix(s: TupleWrapper): String = {
+ def synthesizeNameChangedPrefix(s: TupleWrapper): String = {
???[String]
} ensuring psNameChangedPrefix(s)
- def synthesisNameChangedSuffix(s: TupleWrapper): String = {
+ def synthesizeNameChangedSuffix(s: TupleWrapper): String = {
???[String]
} ensuring psNameChangedSuffix(s)
- def synthesisDuplicate(s: TupleWrapper): String = {
+ /*def synthesizeDuplicate(s: TupleWrapper): String = {
???[String]
- } ensuring psDuplicate(s)
+ } ensuring psDuplicate(s)*/
}
\ No newline at end of file
diff --git a/testcases/stringrender/TwoArgsWrapperRender.scala b/testcases/stringrender/TwoArgsWrapperRender.scala
index 880023ef8f89cb701e1001961c29795a97301f78..e438affa73ea7af0352e7937cc5afb328f25b9cb 100644
--- a/testcases/stringrender/TwoArgsWrapperRender.scala
+++ b/testcases/stringrender/TwoArgsWrapperRender.scala
@@ -9,72 +9,73 @@ import leon.annotation._
import leon.collection._
import leon.collection.ListOps._
import leon.lang.synthesis._
+import leon.lang._
object TwoArgsWrapperRender {
- def psStandard(s: Int, t: Int) = (res: String) => ((s, t), res) passes {
+ @inline def psStandard(s: Int, t: Int) = (res: String) => ((s, t), res) passes {
case (0, 0) => "TupleWrapper(0, 0)"
case (-1, 2) => "TupleWrapper(-1, 2)"
case (12, 5) => "TupleWrapper(12, 5)"
}
- def psUnwrapped(s: Int, t: Int) = (res: String) => ((s, t), res) passes {
+ @inline def psUnwrapped(s: Int, t: Int) = (res: String) => ((s, t), res) passes {
case (0, 0) => "0, 0"
case (-1, 2) => "-1, 2"
case (12, 5) => "12, 5"
}
- def psNameChangedPrefix(s: Int, t: Int) = (res: String) => ((s, t), res) passes {
+ @inline def psNameChangedPrefix(s: Int, t: Int) = (res: String) => ((s, t), res) passes {
case (0, 0) => "x = 0, y = 0"
case (-1, 2) => "x = -1, y = 2"
case (12, 5) => "x = 12, y = 5"
}
- def psNameChangedSuffix(s: Int, t: Int) = (res: String) => ((s, t), res) passes {
+ @inline def psNameChangedSuffix(s: Int, t: Int) = (res: String) => ((s, t), res) passes {
case (0, 0) => "0.0,0.0"
case (-1, 2) => "-1.0,2.0" // Here there should be an ambiguity before this line.
case (12, 5) => "12.0,5.0"
}
- def psDuplicate(s: Int, t: Int) = (res: String) => ((s, t), res) passes {
+ /*def psDuplicate(s: Int, t: Int) = (res: String) => ((s, t), res) passes {
case (0, 0) => "d 0,0 0,15 15,15 15,0"
case (-1, 2) => "d -1,-2 -1,15 15,15 15,2"
case (12, 5) => "d 12,5 12,15 15,15 15,5"
- }
+ }*/
def repairUnWrapped(s: Int, t: Int): String = {
- "(" + s + ", " + t + ")""
- } ensuring psUnWrapped(s)
+ "(" + s + ", " + t + ")"
+ } ensuring psUnwrapped(s, t)
def repairNameChangedPrefix(s: Int, t: Int): String = {
- "(" + s + ", " + t + ")""
- } ensuring psNameChangedPrefix(s)
+ "(" + s + ", " + t + ")"
+ } ensuring psNameChangedPrefix(s, t)
def repairNameChangedSuffix(s: Int, t: Int): String = {
- "(" + s + ", " + t + ")""
- } ensuring psNameChangedSuffix(s)
+ "(" + s + ", " + t + ")"
+ } ensuring psNameChangedSuffix(s, t)
- def repairDuplicate(s: Int, t: Int): String = {
- "(" + s + ", " + t + ")""
- } ensuring psDuplicate(s)
+ /*def repairDuplicate(s: Int, t: Int): String = {
+ "(" + s + ", " + t + ")"
+ } ensuring psDuplicate(s)*/
- def synthesisStandard(s: Int, t: Int): String = {
+ def synthesizeStandard(s: Int, t: Int): String = {
???[String]
- } ensuring psStandard(s)
+ } ensuring psStandard(s, t)
- def synthesisUnwrapped(s: Int, t: Int): String = {
+ def synthesizeUnwrapped(s: Int, t: Int): String = {
???[String]
- } ensuring psUnwrapped(s)
+ } ensuring psUnwrapped(s, t)
- def synthesisNameChangedPrefix(s: Int, t: Int): String = {
+ def synthesizeNameChangedPrefix(s: Int, t: Int): String = {
???[String]
- } ensuring psNameChangedPrefix(s)
+ } ensuring psNameChangedPrefix(s, t)
- def synthesisNameChangedSuffix(s: Int, t: Int): String = {
+ def synthesizeNameChangedSuffix(s: Int, t: Int): String = {
???[String]
- } ensuring psNameChangedSuffix(s)
+ } ensuring psNameChangedSuffix(s, t)
- def synthesisDuplicate(s: Int, t: Int): String = {
+ /*def synthesizeDuplicate(s: Int, t: Int): String = {
???[String]
- } ensuring psDuplicate(s)
+ } ensuring psDuplicate(s)*/
}
\ No newline at end of file
diff --git a/testcases/stringrender/runRepair.sh b/testcases/stringrender/runRepair.sh
index af25c35da8c46582f8bb27e6680cc5e182f01aba..c1b616351dc8cfd326b38358e80e722f3a31f4cf 100644
--- a/testcases/stringrender/runRepair.sh
+++ b/testcases/stringrender/runRepair.sh
@@ -23,17 +23,17 @@ echo "# Category, File, function, p.S, fuS
./leon --repair --timeout=30 --solvers=smt-cvc4 --functions=repairUnwrapped testcases/stringrender/IntWrapperRender.scala | tee -a $fullLog
./leon --repair --timeout=30 --solvers=smt-cvc4 --functions=repairNameChangedPrefix testcases/stringrender/IntWrapperRender.scala | tee -a $fullLog
./leon --repair --timeout=30 --solvers=smt-cvc4 --functions=repairNameChangedSuffix testcases/stringrender/IntWrapperRender.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=smt-cvc4 --functions=repairDuplicate testcases/stringrender/IntWrapperRender.scala | tee -a $fullLog
+# ./leon --repair --timeout=30 --solvers=smt-cvc4 --functions=repairDuplicate testcases/stringrender/IntWrapperRender.scala | tee -a $fullLog
./leon --repair --timeout=30 --solvers=smt-cvc4 --functions=repairUnwrapped testcases/stringrender/TwoArgsWrapperRender.scala | tee -a $fullLog
./leon --repair --timeout=30 --solvers=smt-cvc4 --functions=repairNameChangedPrefix testcases/stringrender/TwoArgsWrapperRender.scala | tee -a $fullLog
./leon --repair --timeout=30 --solvers=smt-cvc4 --functions=repairNameChangedSuffix testcases/stringrender/TwoArgsWrapperRender.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=smt-cvc4 --functions=repairDuplicate testcases/stringrender/TwoArgsWrapperRender.scala | tee -a $fullLog
+# ./leon --repair --timeout=30 --solvers=smt-cvc4 --functions=repairDuplicate testcases/stringrender/TwoArgsWrapperRender.scala | tee -a $fullLog
./leon --repair --timeout=30 --solvers=smt-cvc4 --functions=repairUnwrapped testcases/stringrender/TupleWrapperRender.scala | tee -a $fullLog
./leon --repair --timeout=30 --solvers=smt-cvc4 --functions=repairNameChangedPrefix testcases/stringrender/TupleWrapperRender.scala | tee -a $fullLog
./leon --repair --timeout=30 --solvers=smt-cvc4 --functions=repairNameChangedSuffix testcases/stringrender/TupleWrapperRender.scala | tee -a $fullLog
-./leon --repair --timeout=30 --solvers=smt-cvc4 --functions=repairDuplicate testcases/stringrender/TupleWrapperRender.scala | tee -a $fullLog
+# ./leon --repair --timeout=30 --solvers=smt-cvc4 --functions=repairDuplicate testcases/stringrender/TupleWrapperRender.scala | tee -a $fullLog
./leon --repair --timeout=30 --solvers=smt-cvc4 --functions=render1RemoveCons testcases/stringrender/ListRender.scala | tee -a $fullLog
./leon --repair --timeout=30 --solvers=smt-cvc4 --functions=render2RemoveNil testcases/stringrender/ListRender.scala | tee -a $fullLog