Cross-build for Scala 2.13.0

README.md

@@ -1,7 +1,7 @@
-ScalaZ3 for Scala 2.10, 2.11, and 2.12
-======================================
+ScalaZ3
+=======
 
-This is ScalaZ3 for Z3 4.7.1 and Scala 2.10, 2.11, and 2.12.
+This is ScalaZ3 for Z3 4.7.1 and Scala 2.10, 2.11, 2.12, and 2.13.
 
 Compiling ScalaZ3
 -----------------
@@ -14,7 +14,7 @@ Run
 
     sbt +package
 
-to compile Z3 4.7.1 and cross-compile ScalaZ3 for Scala 2.10, 2.11 and 2.12.
+to compile Z3 4.7.1 and cross-compile ScalaZ3 for Scala 2.10, 2.11, 2.12 and 2.13.
 
 The JAR files will be in `target/scala-2.XX/scalaz3_2.XX-4.7.1.jar`
 and will contain the shared library dependencies.
@@ -74,13 +74,13 @@ Using ScalaZ3
 
 ### On a single operating system / architecture
 
-Create a folder named `unmanaged` at the same level as your `build.sbt` file, and copy the JAR file in `target/scala-2.XX/scalaz3_2.XX-3.0.jar` into it.
+Create a folder named `unmanaged` at the same level as your `build.sbt` file, and copy the JAR file in `target/scala-2.XX/scalaz3_2.XX-4.7.1.jar` into it.
 
 Then add, the following lines to your `build.sbt` file:
 
 ```scala
 unmanagedJars in Compile += {
-  baseDirectory.value / "unmanaged" / s"scalaz3_${scalaBinaryVersion.value}-3.0.jar"
+  baseDirectory.value / "unmanaged" / s"scalaz3_${scalaBinaryVersion.value}-4.7.1.jar"
 }
 ```
 
@@ -92,7 +92,7 @@ Make sure to name the resulting JAR files as `scalaz3-[osName]-[osArch]-[scalaBi
 
 - `[osName]` is one of: `mac`, `win`, `unix`.
 - `[osArch]` corresponds to `System.getProperty("sun.arch.data.model")`, ie. `x64`, `fds`, etc.
-- `[scalaBinaryVersion]` is one of: `2.11`, `2.12`, `2.13`.
+- `[scalaBinaryVersion]` is one of: `2.10`, `2.11`, `2.12`, `2.13`.
 
 Create a folder named `unmanaged` at the same level as your `build.sbt` file, and copy the aforementioned JAR files into it.
 

build.sbt

@@ -11,9 +11,9 @@ lazy val root = (project in file("."))
       "-feature",
     ),
     scalaVersion := "2.12.8",
-    crossScalaVersions := Seq("2.10.7", "2.11.12", "2.12.8"),
+    crossScalaVersions := Seq("2.10.7", "2.11.12", "2.12.8", "2.13.0"),
     libraryDependencies ++= Seq(
-      "org.scalatest" %% "scalatest" % "3.0.7" % "test"
+      "org.scalatest" %% "scalatest" % "3.0.8" % "test"
     ),
     libraryDependencies ++= {
       CrossVersion.partialVersion(scalaVersion.value) match {

src/main/scala/z3/scala/Z3Context.scala

@@ -41,7 +41,8 @@ sealed class Z3Context(val config: Map[String, String]) {
   val optimizerQueue = new Z3RefCountQueue[Z3Optimizer]
   val tacticQueue    = new Z3RefCountQueue[Z3Tactic]
 
-  def this(params: (String,Any)*) = this(Map[String, Any](params : _*).mapValues(_.toString))
+  def this(params: (String, Any)*) =
+    this(params.map { case (s, a) => (s, a.toString) }.toMap)
 
   private var deleted : Boolean = false
   override def finalize() : Unit = {
@@ -219,7 +220,7 @@ sealed class Z3Context(val config: Map[String, String]) {
 
     consListList.foreach(cl => Native.delConstructorList(this.ptr, cl))
 
-    for((sort, consLst) <- (newSorts zip consScalaList)) yield {
+    for((sort, consLst) <- (newSorts.toIndexedSeq zip consScalaList)) yield {
       val zipped = for (cons <- consLst) yield {
         val consFunPtr = new Native.LongPtr()
         val testFunPtr = new Native.LongPtr()
@@ -484,7 +485,7 @@ sealed class Z3Context(val config: Map[String, String]) {
     val sz = sorts.size
     val consPtr = new Native.LongPtr()
     val projFuns = new Array[Long](sz)
-    val fieldNames = sorts.map(s => mkFreshStringSymbol(name + "-field")).toArray
+    val fieldNames = sorts.map(s => mkFreshStringSymbol(s"$name-field")).toArray
     val sortPtr = Native.mkTupleSort(this.ptr, name.ptr, sz, fieldNames.map(_.ptr), sorts.map(_.ptr).toArray, consPtr, projFuns)
     val newSort = new Z3Sort(sortPtr, this)
     val consFuncDecl = new Z3FuncDecl(consPtr.value, sz, this)

src/test/scala/z3/scala/Abs.scala

@@ -27,9 +27,9 @@ class Abs extends FunSuite with Matchers {
     result should equal(Some(true))
 
     val array2Ev = model.eval(array2)
-    array2Ev should be ('defined)
+    array2Ev should be (Symbol("defined"))
     val array2Val = model.getArrayValue(array2Ev.get)
-    array2Val should be ('defined)
+    array2Val should be (Symbol("defined"))
     val (valueMap, default) = array2Val.get
     valueMap(z3.mkInt(0, is)) should equal (z3.mkInt(1, is))
     valueMap(z3.mkInt(1, is)) should equal (z3.mkInt(0, is))

src/test/scala/z3/scala/Arrays.scala

@@ -32,11 +32,11 @@ class Arrays extends FunSuite with Matchers {
     result should equal(Some(true))
 
     val array1Evaluated = model.eval(array1)
-    array1Evaluated should be ('defined)
+    array1Evaluated should be (Symbol("defined"))
     array1Evaluated match {
       case Some(ae) =>
         val array1Val = model.getArrayValue(ae)
-        array1Val should be ('defined)
+        array1Val should be (Symbol("defined"))
         //println("When evaluated, array1 is: " + array1Val)
         array1Val match {
           case Some((valueMap,default)) =>
@@ -47,11 +47,11 @@ class Arrays extends FunSuite with Matchers {
     }
 
     val array2Evaluated = model.eval(array2)
-    array2Evaluated should be ('defined)
+    array2Evaluated should be (Symbol("defined"))
     array2Evaluated match {
       case Some(ae) => {
         val array2Val = model.getArrayValue(ae)
-        array2Val should be ('defined)
+        array2Val should be (Symbol("defined"))
         //println("When evaluated, array2 is: " + array2Val)
         array2Val match {
           case Some((valueMap,default)) => {

src/test/scala/z3/scala/Quantifiers.scala

@@ -36,8 +36,8 @@ class Quantifiers extends FunSuite with Matchers {
      * (declare-fun array-of (Type) Type)
      */
     val typeSort = z3.mkUninterpretedSort("Type")
-    val subtype = z3.mkFuncDecl("subtype", List[Z3Sort](typeSort, typeSort).toArray, z3.mkBoolSort)
-    val arrayOf = z3.mkFuncDecl("array-of", List[Z3Sort](typeSort).toArray, typeSort)
+    val subtype = z3.mkFuncDecl("subtype", List[Z3Sort](typeSort, typeSort).toIndexedSeq, z3.mkBoolSort)
+    val arrayOf = z3.mkFuncDecl("array-of", List[Z3Sort](typeSort).toIndexedSeq, typeSort)
 
     val syms @ List(xSym, ySym, zSym) = List("x", "y", "z").map(z3.mkSymbol(_))
     val consts @ List(x, y, z) = syms.map(sym => z3.mkConst(sym, typeSort))

src/test/scala/z3/scala/Sequences.scala

@@ -21,8 +21,8 @@ class Sequences extends FunSuite with Matchers {
     val s1eval = model.eval(s1)
     val s2eval = model.eval(s2)
 
-    s1eval should be ('defined)
-    s2eval should be ('defined)
+    s1eval should be (Symbol("defined"))
+    s2eval should be (Symbol("defined"))
   }
 
   test("Different head") {
@@ -61,7 +61,7 @@ class Sequences extends FunSuite with Matchers {
     val s1eval = model.eval(s1)
     val s2eval = model.eval(s2)
 
-    s1eval should be ('defined)
-    s2eval should be ('defined)
+    s1eval should be (Symbol("defined"))
+    s2eval should be (Symbol("defined"))
   }
 }

src/test/scala/z3/scala/Sets.scala

@@ -20,14 +20,14 @@ class Sets extends FunSuite with Matchers {
 
     val s1eval = model.eval(s1)
     val s2eval = model.eval(s2)
-    s1eval should be ('defined)
-    s2eval should be ('defined)
+    s1eval should be (Symbol("defined"))
+    s2eval should be (Symbol("defined"))
     (s1eval,s2eval) match {
       case (Some(se1), Some(se2)) =>
         val s1val = model.getSetValue(se1)
         val s2val = model.getSetValue(se2)
-        s1val should be ('defined)
-        s2val should be ('defined)
+        s1val should be (Symbol("defined"))
+        s2val should be (Symbol("defined"))
         s1val should not equal (s2val)
         //println("Set values :" + s1val + ", " + s2val)
       case _ =>