From 858dc1b6a24438a2033bc292992fca36ac62d929 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Thu, 14 Apr 2016 16:48:46 +0200
Subject: [PATCH] Added string conversion utilities when converting from String
to String$0
---
library/theories/String.scala | 42 +++++++++++++++++++
.../leon/solvers/theories/StringEncoder.scala | 22 ++++++++++
2 files changed, 64 insertions(+)
diff --git a/library/theories/String.scala b/library/theories/String.scala
index 85e4d90c7..8cfced9d8 100644
--- a/library/theories/String.scala
+++ b/library/theories/String.scala
@@ -30,3 +30,45 @@ sealed abstract class String {
case class StringCons(head: Char, tail: String) extends String
case class StringNil() extends String
+
+@library
+object String {
+ def fromChar(i: Char): String = {
+ StringCons(i, StringNil())
+ }
+
+ def fromBigInt(i: BigInt): String =
+ if(i < 0) StringCons('-', fromBigInt(-i))
+ else if(i == BigInt(0)) StringCons('0', StringNil())
+ else if(i == BigInt(1)) StringCons('1', StringNil())
+ else if(i == BigInt(2)) StringCons('2', StringNil())
+ else if(i == BigInt(3)) StringCons('3', StringNil())
+ else if(i == BigInt(4)) StringCons('4', StringNil())
+ else if(i == BigInt(5)) StringCons('5', StringNil())
+ else if(i == BigInt(6)) StringCons('6', StringNil())
+ else if(i == BigInt(7)) StringCons('7', StringNil())
+ else if(i == BigInt(8)) StringCons('8', StringNil())
+ else if(i == BigInt(9)) StringCons('9', StringNil())
+ else fromBigInt(i / 10).concat(fromBigInt(i % 10))
+
+ def fromInt(i: Int): String = i match {
+ case -2147483648 => StringCons('-', StringCons('2', fromInt(147483648)))
+ case i if i < 0 => StringCons('-', fromInt(-i))
+ case 0 => StringCons('0', StringNil())
+ case 1 => StringCons('1', StringNil())
+ case 2 => StringCons('2', StringNil())
+ case 3 => StringCons('3', StringNil())
+ case 4 => StringCons('4', StringNil())
+ case 5 => StringCons('5', StringNil())
+ case 6 => StringCons('6', StringNil())
+ case 7 => StringCons('7', StringNil())
+ case 8 => StringCons('8', StringNil())
+ case 9 => StringCons('9', StringNil())
+ case i => fromInt(i / 10).concat(fromInt(i % 10))
+ }
+
+ def fromBoolean(b: Boolean): String = {
+ if(b) StringCons('t', StringCons('r', StringCons('u', StringCons('e', StringNil()))))
+ else StringCons('f', StringCons('a', StringCons('l', StringCons('s', StringCons('e', StringNil())))))
+ }
+}
diff --git a/src/main/scala/leon/solvers/theories/StringEncoder.scala b/src/main/scala/leon/solvers/theories/StringEncoder.scala
index 051981440..02293fab3 100644
--- a/src/main/scala/leon/solvers/theories/StringEncoder.scala
+++ b/src/main/scala/leon/solvers/theories/StringEncoder.scala
@@ -22,6 +22,12 @@ class StringEncoder(ctx: LeonContext, p: Program) extends TheoryEncoder {
val Drop = p.library.lookupUnique[FunDef]("leon.theories.String.drop").typed
val Slice = p.library.lookupUnique[FunDef]("leon.theories.String.slice").typed
val Concat = p.library.lookupUnique[FunDef]("leon.theories.String.concat").typed
+
+ val FromInt = p.library.lookupUnique[FunDef]("leon.theories.String.fromInt").typed
+ val FromChar = p.library.lookupUnique[FunDef]("leon.theories.String.fromChar").typed
+ val FromBoolean = p.library.lookupUnique[FunDef]("leon.theories.String.fromBoolean").typed
+ val FromBigInt = p.library.lookupUnique[FunDef]("leon.theories.String.fromBigInt").typed
+
private val stringBijection = new Bijection[String, Expr]()
@@ -48,6 +54,14 @@ class StringEncoder(ctx: LeonContext, p: Program) extends TheoryEncoder {
Some(FunctionInvocation(Take, Seq(FunctionInvocation(Drop, Seq(transform(a), transform(start))), transform(length))).copiedFrom(e))
case SubString(a, start, end) =>
Some(FunctionInvocation(Slice, Seq(transform(a), transform(start), transform(end))).copiedFrom(e))
+ case Int32ToString(a) =>
+ Some(FunctionInvocation(FromInt, Seq(transform(a))).copiedFrom(e))
+ case IntegerToString(a) =>
+ Some(FunctionInvocation(FromBigInt, Seq(transform(a))).copiedFrom(e))
+ case CharToString(a) =>
+ Some(FunctionInvocation(FromChar, Seq(transform(a))).copiedFrom(e))
+ case BooleanToString(a) =>
+ Some(FunctionInvocation(FromBoolean, Seq(transform(a))).copiedFrom(e))
case _ => None
}
@@ -85,6 +99,14 @@ class StringEncoder(ctx: LeonContext, p: Program) extends TheoryEncoder {
case FunctionInvocation(Drop, Seq(a, count)) =>
val ra = transform(a)
Some(SubString(ra, transform(count), StringLength(ra)).copiedFrom(e))
+ case FunctionInvocation(FromInt, Seq(a)) =>
+ Some(Int32ToString(transform(a)).copiedFrom(e))
+ case FunctionInvocation(FromBigInt, Seq(a)) =>
+ Some(IntegerToString(transform(a)).copiedFrom(e))
+ case FunctionInvocation(FromChar, Seq(a)) =>
+ Some(CharToString(transform(a)).copiedFrom(e))
+ case FunctionInvocation(FromBoolean, Seq(a)) =>
+ Some(BooleanToString(transform(a)).copiedFrom(e))
case _ => None
}
--
GitLab