From da29c210d734820bd2d591ab094ebbe4447c654a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Mon, 7 Mar 2016 17:23:44 +0100
Subject: [PATCH] Benchmarks are now more readable thanks to "ask"
---
testcases/stringrender/ModularRender.scala | 10 ++-------
.../stringrender/SymbolGrammarRender.scala | 10 ++-------
.../web/synthesis/26_Modular_Render.scala | 21 ++++++-------------
3 files changed, 10 insertions(+), 31 deletions(-)
diff --git a/testcases/stringrender/ModularRender.scala b/testcases/stringrender/ModularRender.scala
index 4757e3cc3..cf46ab0ab 100644
--- a/testcases/stringrender/ModularRender.scala
+++ b/testcases/stringrender/ModularRender.scala
@@ -31,12 +31,6 @@ object ModularRender {
case class Configuration(flags: List[Boolean])
// We want to write Config:[Up,Down,Up....]
- def ConfigToString(config : Configuration): String = {
- ???
- } ensuring {
- (res : String) => (config, res) passes {
- case _ if false =>
- ""
- }
- }
+ def ConfigToString(config : Configuration): String =
+ ???[String] ask config
}
diff --git a/testcases/stringrender/SymbolGrammarRender.scala b/testcases/stringrender/SymbolGrammarRender.scala
index 5998e6b38..af03bdbbf 100644
--- a/testcases/stringrender/SymbolGrammarRender.scala
+++ b/testcases/stringrender/SymbolGrammarRender.scala
@@ -49,12 +49,6 @@ object GrammarRender {
}
}
- def grammarToString(p : Grammar): String = {
- ???[String]
- } ensuring {
- (res : String) => (p, res) passes {
- case _ if false =>
- ""
- }
- }
+ def grammarToString(p : Grammar): String =
+ ???[String] ask p
}
\ No newline at end of file
diff --git a/testcases/web/synthesis/26_Modular_Render.scala b/testcases/web/synthesis/26_Modular_Render.scala
index 54a5cc3fb..d180d7e4c 100644
--- a/testcases/web/synthesis/26_Modular_Render.scala
+++ b/testcases/web/synthesis/26_Modular_Render.scala
@@ -11,31 +11,22 @@ import leon.collection.ListOps._
import leon.lang.synthesis._
object ModularRender {
- def customToString[T](l : List[T], f : (T) => String): String = {
- ???
- } ensuring {
- (res : String) => (l, res) passes {
- case _ if false => ""
- }
- }
def booleanToString(b: Boolean) = if(b) "Up" else "Down"
+
def intToString(b: BigInt) = b.toString
+ def customToString[T](l : List[T], f : (T) => String): String =
+ ???[String] ask l
+
case class Configuration(flags: List[Boolean], strokes: List[BigInt])
// We want to write
// Solution:
// [Up, Down, Up....]
// [1, 2, 5, ...]
- def ConfigToString(config : Configuration): String = {
- ???
- } ensuring {
- (res : String) => (config, res) passes {
- case _ if false =>
- ""
- }
- }
+ def ConfigToString(config : Configuration): String =
+ ???[String] ask config
/** Wrong lemma for demonstration */
def configurationsAreSimple(c: Configuration) =
--
GitLab