Added string support in smtlib interface

Added more documentation

build.sbt

@@ -143,7 +143,7 @@ def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${versi
 
 lazy val bonsai      = ghProject("git://github.com/colder/bonsai.git",     "0fec9f97f4220fa94b1f3f305f2e8b76a3cd1539")
 
-lazy val scalaSmtLib = ghProject("git://github.com/regb/scala-smtlib.git", "3b6ef4992b6af15d08a7320fd12202f35e97b905")
+lazy val scalaSmtLib = ghProject("git://github.com/MikaelMayer/scala-smtlib.git", "8ef13ef3294ab823aed0bad40678f507b1fe63e2")
 
 lazy val root = (project in file(".")).
   configs(RegressionTest, IsabelleTest, IntegrTest).

src/main/scala/leon/solvers/EnumerationSolver.scala

@@ -48,6 +48,7 @@ class EnumerationSolver(val context: LeonContext, val program: Program) extends
 
   private var model = Model.empty
 
+  /** @inheritdoc */
   def check: Option[Boolean] = {
     val timer = context.timers.solvers.enum.check.start()
     val res = try {
@@ -78,6 +79,7 @@ class EnumerationSolver(val context: LeonContext, val program: Program) extends
     res
   }
 
+  /** @inheritdoc */
   def getModel: Model = {
     model
   }

src/main/scala/leon/solvers/Solver.scala

@@ -23,7 +23,9 @@ trait Solver extends Interruptible {
     assertCnstr(Not(vc.condition))
   }
 
+  /** Returns Some(true) if it found a satisfying model, Some(false) if no model exists, and None otherwise */
   def check: Option[Boolean]
+  /** Returns the model if it exists */
   def getModel: Model
   def getResultSolver: Option[Solver] = Some(this)
 

src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala

@@ -26,6 +26,7 @@ import _root_.smtlib.parser.Terms.{
 }
 import _root_.smtlib.parser.CommandsResponses.{ Error => ErrorResponse, _ }
 import _root_.smtlib.theories._
+import _root_.smtlib.theories.experimental._
 import _root_.smtlib.interpreters.ProcessInterpreter
 
 trait SMTLIBTarget extends Interruptible {
@@ -233,6 +234,7 @@ trait SMTLIBTarget extends Interruptible {
         case RealType    => Reals.RealSort()
         case Int32Type   => FixedSizeBitVectors.BitVectorSort(32)
         case CharType    => FixedSizeBitVectors.BitVectorSort(32)
+        case StringType  => Strings.StringSort()
 
         case RawArrayType(from, to) =>
           Sort(SMTIdentifier(SSymbol("Array")), Seq(declareSort(from), declareSort(to)))
@@ -356,6 +358,9 @@ trait SMTLIBTarget extends Interruptible {
       case FractionalLiteral(n, d)   => Reals.Div(Reals.NumeralLit(n), Reals.NumeralLit(d))
       case CharLiteral(c)            => FixedSizeBitVectors.BitVectorLit(Hexadecimal.fromInt(c.toInt))
       case BooleanLiteral(v)         => Core.BoolConst(v)
+      case StringLiteral(v)          =>
+        declareSort(StringType)
+        Strings.StringLit(v)
       case Let(b, d, e) =>
         val id = id2sym(b)
         val value = toSMT(d)
@@ -586,6 +591,12 @@ trait SMTLIBTarget extends Interruptible {
       case RealMinus(a, b)           => Reals.Sub(toSMT(a), toSMT(b))
       case RealTimes(a, b)           => Reals.Mul(toSMT(a), toSMT(b))
       case RealDivision(a, b)        => Reals.Div(toSMT(a), toSMT(b))
+      
+      case StringLength(a)           => Strings.Length(toSMT(a))
+      case StringConcat(a, b)        => Strings.Concat(toSMT(a), toSMT(b))
+      case SubString(a, start, Plus(start2, length)) if start == start2  =>
+                                        Strings.Substring(toSMT(a),toSMT(start),toSMT(length))
+      case SubString(a, start, end)  => Strings.Substring(toSMT(a),toSMT(start),toSMT(Minus(end, start)))
 
       case And(sub)                  => Core.And(sub.map(toSMT): _*)
       case Or(sub)                   => Core.Or(sub.map(toSMT): _*)
@@ -641,6 +652,31 @@ trait SMTLIBTarget extends Interruptible {
 
       case (SNumeral(n), Some(RealType)) =>
         FractionalLiteral(n, 1)
+      
+      case (SString(v), Some(StringType)) =>
+        StringLiteral(v)
+        
+      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 (FunctionApplication(SimpleSymbol(SSymbol("ite")), Seq(cond, thenn, elze)), t) =>
         IfExpr(

src/main/scala/leon/utils/IncrementalSet.scala

@@ -6,6 +6,7 @@ import scala.collection.mutable.{Stack, Set => MSet}
 import scala.collection.mutable.Builder
 import scala.collection.{Iterable, IterableLike, GenSet}
 
+/** A stack of mutable sets with a set-like API and methods to push and pop */
 class IncrementalSet[A] extends IncrementalState
                         with Iterable[A]
                         with IterableLike[A, Set[A]]
@@ -14,32 +15,41 @@ class IncrementalSet[A] extends IncrementalState
   private[this] val stack = new Stack[MSet[A]]()
   override def repr = stack.flatten.toSet
 
+  /** Removes all the elements */
   override def clear(): Unit = {
     stack.clear()
   }
 
+  /** Removes all the elements and creates a new set */
   def reset(): Unit = {
     clear()
     push()
   }
 
+  /** Creates one more set level */
   def push(): Unit = {
     stack.push(MSet())
   }
 
+  /** Removes one set level */
   def pop(): Unit = {
     stack.pop()
   }
 
+  /** Returns true if the set contains elem */
   def apply(elem: A) = repr.contains(elem)
+  /** Returns true if the set contains elem */
   def contains(elem: A) = repr.contains(elem)
 
+  /** Returns an iterator over all the elements */
   def iterator = stack.flatten.iterator
+  /** Add an element to the head set */
   def += (elem: A) = { stack.head += elem; this }
+  /** Removes an element from all stacked sets */
   def -= (elem: A) = { stack.foreach(_ -= elem); this }
 
   override def newBuilder = new scala.collection.mutable.SetBuilder(Set.empty[A])
   def result = this
 
-  push()
+  push() // By default, creates a new empty mutable set ready to add elements to it.
 }