From 1e27a99ea2198dc7a060ff99500f110d1d8db569 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Wed, 20 Jan 2016 14:40:23 +0100
Subject: [PATCH] Removed unused construction of string functions for z3
---
.../leon/solvers/smtlib/SMTLIBZ3Target.scala | 23 -------------------
1 file changed, 23 deletions(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
index af88e4cfa..be9844a31 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
@@ -140,29 +140,6 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
case t => unsupported(t, "Cannot extract string")
}
- /*case (Strings.Length(a), _) =>
- val aa = fromSMT(a)
- StringLength(aa)
-
- case (Strings.Concat(a, b, c @ _*), _) =>
- val aa = fromSMT(a)
- val bb = fromSMT(b)
- (StringConcat(aa, bb) /: c.map(fromSMT(_))) {
- case (s, cc) => StringConcat(s, cc)
- }
-
- case (Strings.Substring(s, start, offset), _) =>
- val ss = fromSMT(s)
- val tt = fromSMT(start)
- val oo = fromSMT(offset)
- oo match {
- case Minus(otherEnd, `tt`) => SubString(ss, tt, otherEnd)
- case _ => SubString(ss, tt, Plus(tt, oo))
- }
-
- case (Strings.At(a, b), _) => fromSMT(Strings.Substring(a, b, SNumeral(1)))
-*/
-
case _ =>
super.fromSMT(t, otpe)
}
--
GitLab