From 0e5c4297434c8da7181fff948b246b7b35183f08 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <a-mikmay@microsoft.com>
Date: Wed, 2 Dec 2015 17:55:12 +0100
Subject: [PATCH] Consistent rendering of IDs Better evaluator.
---
src/main/scala/leon/purescala/DefOps.scala | 2 +-
.../leon/synthesis/rules/StringRender.scala | 4 ++--
.../verification/VerificationCondition.scala | 1 +
.../verification/VerificationReport.scala | 20 ++++++++++++++++++-
testcases/web/synthesis/22_String_List.scala | 19 ++++++++++++++++++
5 files changed, 42 insertions(+), 4 deletions(-)
create mode 100644 testcases/web/synthesis/22_String_List.scala
diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index 1e5e12011..81ebbdbec 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -151,7 +151,7 @@ object DefOps {
if (useUniqueIds) {
List(d.id.uniqueName)
} else {
- List(d.id.name)
+ List(d.id.toString)
}
}
}
diff --git a/src/main/scala/leon/synthesis/rules/StringRender.scala b/src/main/scala/leon/synthesis/rules/StringRender.scala
index 04cf074d3..3416a9851 100644
--- a/src/main/scala/leon/synthesis/rules/StringRender.scala
+++ b/src/main/scala/leon/synthesis/rules/StringRender.scala
@@ -211,7 +211,7 @@ case object StringRender extends Rule("StringRender") {
def getMapping(fd: FunDef): FunDef = {
transformMap.getOrElse(fd, {
- val newfunDef = new FunDef(FreshIdentifier(fd.id.name), fd.tparams, fd.params, fd.returnType) // With empty body
+ val newfunDef = new FunDef(fd.id.freshen, fd.tparams, fd.params, fd.returnType) // With empty body
transformMap += fd -> newfunDef
newfunDef.body = fd.body.map(mapExpr _)
newfunDef
@@ -241,7 +241,7 @@ case object StringRender extends Rule("StringRender") {
}
val funName3 = funName2.replaceAll("[^a-zA-Z0-9_]","")
val funName = funName3(0).toLower + funName3.substring(1)
- val funId = FreshIdentifier(funName, alwaysShowUniqueID = true)
+ val funId = FreshIdentifier(funName, alwaysShowUniqueID = false)
val argId= FreshIdentifier(tpe.typeToConvert.asString(hctx.context).toLowerCase()(0).toString, tpe.typeToConvert)
val fd = new FunDef(funId, Nil, ValDef(argId) :: Nil, StringType) // Empty function.
fd
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index de3e41985..79fc62b45 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -95,4 +95,5 @@ object VCStatus {
case object Unknown extends VCStatus("unknown")
case object Timeout extends VCStatus("timeout")
case object Cancelled extends VCStatus("cancelled")
+ case object Crashed extends VCStatus("crashed")
}
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index 701d08718..cffc4bae2 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -11,6 +11,18 @@ import leon.utils.DebugSectionSynthesis
import leon.utils.DebugSectionVerification
import leon.purescala.TypeOps
+import leon.purescala.Quantification._
+import purescala.Constructors._
+import purescala.ExprOps._
+import purescala.Expressions.Pattern
+import purescala.Extractors._
+import purescala.TypeOps._
+import purescala.Types._
+import purescala.Common._
+import purescala.Expressions._
+import purescala.Definitions._
+import leon.solvers.{ HenkinModel, Model, SolverFactory }
+
object VerificationReport {
/** If it can be computed, returns a user defined string for the given expression */
def userDefinedString(v: Expr, orElse: =>String)(ctx: LeonContext, program: Program): String = {
@@ -21,13 +33,19 @@ object VerificationReport {
case Some(fd) =>
//println("Found fd: " + fd.id.name)
val ste = new StringTracingEvaluator(ctx, program)
+ try {
val result = ste.eval(FunctionInvocation(fd.typed, Seq(v)))
+
result.result match {
- case Some((StringLiteral(res), _)) =>
+ case Some((StringLiteral(res), _)) if res != "" =>
res
case _ =>
orElse
}
+ } catch {
+ case e: evaluators.ContextualEvaluator#EvalError =>
+ orElse
+ }
case None =>
//println("Function to render " + v + " not found")
orElse
diff --git a/testcases/web/synthesis/22_String_List.scala b/testcases/web/synthesis/22_String_List.scala
new file mode 100644
index 000000000..089d57484
--- /dev/null
+++ b/testcases/web/synthesis/22_String_List.scala
@@ -0,0 +1,19 @@
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon.collection.ListOps._
+import leon.lang.synthesis._
+
+object ListsToString {
+
+ def allListsAreEmpty(t: List[Int]): Boolean = (t.isEmpty || t.tail.isEmpty || t.tail.tail.isEmpty || t.tail.head == 0) holds
+
+ def listToString(p : List[Int]): String = {
+ ???
+ } ensuring {
+ (res : String) => (p, res) passes {
+ case Cons(1, Cons(2, Nil())) =>
+ "[1, 2]"
+ }
+ }
+}
--
GitLab