Skip to content
Snippets Groups Projects
Commit da29c210 authored by Mikaël Mayer's avatar Mikaël Mayer
Browse files

Benchmarks are now more readable thanks to "ask"

parent 94cda5d8
Branches
Tags
No related merge requests found
......@@ -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
}
......@@ -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
......@@ -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) =
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment