From d814fca700f52c77a623a5e81a22ba54764fca7e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <a-mikmay@microsoft.com>
Date: Mon, 19 Oct 2015 18:54:36 +0200
Subject: [PATCH] Leon now supports strings for compilation phase.
---
src/main/scala/leon/frontends/scalac/CodeExtraction.scala | 1 -
src/main/scala/leon/purescala/Extractors.scala | 7 +++++++
testcases/stringrender/runTests.sh | 4 ++--
3 files changed, 9 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 1c4f19bf6..ea5318e4b 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1486,7 +1486,6 @@ trait CodeExtraction extends ASTExtractors {
Implies(extractTree(lhs), extractTree(rhs)).setPos(current.pos)
case c @ ExCall(rec, sym, tps, args) =>
- println("Parsing call:" + c)
val rrec = rec match {
case t if (defsToDefs contains sym) && !isMethod(sym) =>
null
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index abe8dbe1a..0a6971eb3 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -27,6 +27,10 @@ object Extractors {
Some((Seq(t), (es: Seq[Expr]) => RealUMinus(es.head)))
case BVNot(t) =>
Some((Seq(t), (es: Seq[Expr]) => BVNot(es.head)))
+ case StringLength(t) =>
+ Some((Seq(t), (es: Seq[Expr]) => StringLength(es.head)))
+ case ToString(t) =>
+ Some((Seq(t), (es: Seq[Expr]) => ToString(es.head)))
case SetCardinality(t) =>
Some((Seq(t), (es: Seq[Expr]) => SetCardinality(es.head)))
case CaseClassSelector(cd, e, sel) =>
@@ -120,6 +124,8 @@ object Extractors {
Some(Seq(t1, t2), (es: Seq[Expr]) => times(es(0), es(1)))
case RealDivision(t1, t2) =>
Some(Seq(t1, t2), (es: Seq[Expr]) => RealDivision(es(0), es(1)))
+ case StringConcat(t1, t2) =>
+ Some(Seq(t1, t2), (es: Seq[Expr]) => StringConcat(es(0), es(1)))
case ElementOfSet(t1, t2) =>
Some(Seq(t1, t2), (es: Seq[Expr]) => ElementOfSet(es(0), es(1)))
case SubsetOf(t1, t2) =>
@@ -156,6 +162,7 @@ object Extractors {
case CaseClass(cd, args) => Some((args, CaseClass(cd, _)))
case And(args) => Some((args, and))
case Or(args) => Some((args, or))
+ case SubString(t1, a, b) => Some((t1::a::b::Nil, es => SubString(es(0), es(1), es(2))))
case FiniteSet(els, base) =>
Some((els.toSeq, els => FiniteSet(els.toSet, base)))
case FiniteMap(args, f, t) => {
diff --git a/testcases/stringrender/runTests.sh b/testcases/stringrender/runTests.sh
index ec8439754..92ab18023 100644
--- a/testcases/stringrender/runTests.sh
+++ b/testcases/stringrender/runTests.sh
@@ -15,12 +15,12 @@ echo "################################" >> $summaryLog
echo "# Category, File, function, p.S, fuS, foS, Tms, Fms, Rms, verif?" >> $summaryLog
#All benchmarks:
-./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairUnWrapped testcases/stringrender/IntWrapperRender.scala | tee -a $fullLog
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairUnwrapped testcases/stringrender/IntWrapperRender.scala | tee -a $fullLog
./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairNameChangedPrefix testcases/stringrender/IntWrapperRender.scala | tee -a $fullLog
./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairNameChangedSuffix testcases/stringrender/IntWrapperRender.scala | tee -a $fullLog
./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairDuplicate testcases/stringrender/IntWrapperRender.scala | tee -a $fullLog
-./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairUnWrapped testcases/stringrender/TupleWrapperRender.scala | tee -a $fullLog
+./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairUnwrapped testcases/stringrender/TupleWrapperRender.scala | tee -a $fullLog
./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairNameChangedPrefix testcases/stringrender/TupleWrapperRender.scala | tee -a $fullLog
./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairNameChangedSuffix testcases/stringrender/TupleWrapperRender.scala | tee -a $fullLog
./leon --stringrender --timeout=30 --solvers=fairz3,enum --functions=repairDuplicate testcases/stringrender/TupleWrapperRender.scala | tee -a $fullLog
--
GitLab