Added string conversion utilities when converting from String to String$0

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())))))
+  }
+}

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
     }