From 8f67715239c208585a2b75f28799d6f2f7b054f2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Wed, 20 Jan 2016 21:14:00 +0100
Subject: [PATCH] Support for string literals in compilation unit (enumeration
solver) Added missing strings in enumeration. Better error messages when
tests fail.
---
src/main/scala/leon/codegen/CompilationUnit.scala | 3 +++
src/main/scala/leon/datagen/VanuatooDataGen.scala | 3 ++-
src/test/scala/leon/integration/solvers/SolversSuite.scala | 6 +++---
3 files changed, 8 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 93c8c6d02..26f976c09 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -177,6 +177,9 @@ class CompilationUnit(val ctx: LeonContext,
case FractionalLiteral(n, d) =>
new runtime.Rational(n.toString, d.toString)
+
+ case StringLiteral(v) =>
+ new java.lang.String(v)
case GenericValue(tp, id) =>
e
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index 8b4846a33..b82dc6a0f 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -58,6 +58,8 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
def stringConstructor(s: String) = strings(s)
+ lazy val stubValues = ints.values ++ bigInts.values ++ booleans.values ++ chars.values ++ rationals.values ++ strings.values
+
def cPattern(c: Constructor[Expr, TypeTree], args: Seq[VPattern[Expr, TypeTree]]) = {
ConstructorPattern[Expr, TypeTree](c, args)
}
@@ -307,7 +309,6 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
None
})
- val stubValues = ints.values ++ bigInts.values ++ booleans.values ++ chars.values ++ rationals.values
val gen = new StubGenerator[Expr, TypeTree](stubValues.toSeq,
Some(getConstructors _),
treatEmptyStubsAsChildless = true)
diff --git a/src/test/scala/leon/integration/solvers/SolversSuite.scala b/src/test/scala/leon/integration/solvers/SolversSuite.scala
index 24ebf3591..d568e471f 100644
--- a/src/test/scala/leon/integration/solvers/SolversSuite.scala
+++ b/src/test/scala/leon/integration/solvers/SolversSuite.scala
@@ -72,13 +72,13 @@ class SolversSuite extends LeonTestSuiteWithProgram {
val model = solver.getModel
for (v <- vs) {
if (model.isDefinedAt(v.id)) {
- assert(model(v.id).getType === v.getType, "Extracting value of type "+v.getType)
+ assert(model(v.id).getType === v.getType, s"Solver $solver - Extracting value of type "+v.getType)
} else {
- fail("Model does not contain "+v.id+" of type "+v.getType)
+ fail(s"Solver $solver - Model does not contain "+v.id.uniqueName+" of type "+v.getType)
}
}
case _ =>
- fail("Constraint "+cnstr.asString+" is unsat!?")
+ fail(s"Solver $solver - Constraint "+cnstr.asString+" is unsat!?")
}
} finally {
solver.free()
--
GitLab