diff --git a/.gitignore b/.gitignore index f6f3f9f..1d08515 100644 --- a/.gitignore +++ b/.gitignore @@ -28,3 +28,7 @@ z3/* # IDEA project files .idea/* *.iml + +# VSCode and metals +.metals +.vscode diff --git a/README.md b/README.md index 20a1dd4..16a0e67 100644 --- a/README.md +++ b/README.md @@ -1,7 +1,7 @@ ScalaZ3 ![Build status](http://laraquad4.epfl.ch:9000/epfl-lara/ScalaZ3/status/master) ======= -This is ScalaZ3 for Z3 4.7.1 and Scala 2.10, 2.11, 2.12, and 2.13. +This is ScalaZ3 for Z3 4.8.10 and Scala 2.10, 2.11, 2.12, and 2.13. [API documentation](https://epfl-lara.github.io/ScalaZ3/z3/index.html) ------------------- @@ -17,9 +17,9 @@ Run sbt +package -to compile Z3 4.7.1 and cross-compile ScalaZ3 for Scala 2.10, 2.11, 2.12 and 2.13. +to compile Z3 4.8.10 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` +The JAR files will be in `target/scala-2.XX/scalaz3_2.XX-4.8.10.jar` and will contain the shared library dependencies. For testing, run @@ -57,7 +57,7 @@ Now navigate to the scalaz3 folder and type: sbt +package -The JAR files will be in `target/scala-2.XX/scalaz3_2.XX-4.7.1.jar` and will contain the shared library +The JAR files will be in `target/scala-2.XX/scalaz3_2.XX-4.8.10.jar` and will contain the shared library dependencies. #### Test your package. @@ -77,13 +77,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-4.7.1.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.8.10.jar` into it. Then add, the following lines to your `build.sbt` file: ```scala -Compile / unmanagedJars += { - baseDirectory.value / "unmanaged" / s"scalaz3_${scalaBinaryVersion.value}-4.7.1.jar" +unmanagedJars in Compile += { + baseDirectory.value / "unmanaged" / s"scalaz3_${scalaBinaryVersion.value}-4.8.10.jar" } ``` diff --git a/build.sbt b/build.sbt index 9af358d..c24178b 100644 --- a/build.sbt +++ b/build.sbt @@ -3,15 +3,15 @@ import ScalaZ3Build._ lazy val root = (project in file(".")) .settings( name := "ScalaZ3", - version := "4.7.1", + version := "4.8.10", organization := "ch.epfl.lara", scalacOptions ++= Seq( "-deprecation", "-unchecked", "-feature", ), - scalaVersion := "2.12.8", - crossScalaVersions := Seq("2.10.7", "2.11.12", "2.12.8", "2.13.0"), + scalaVersion := "2.12.13", + crossScalaVersions := Seq("2.10.7", "2.11.12", "2.12.8", "2.12.13", "2.13.5"), libraryDependencies ++= Seq( "org.scalatest" %% "scalatest" % "3.0.8" % "test" ), @@ -31,6 +31,7 @@ lazy val root = (project in file(".")) Compile / compile := ((Compile / compile) dependsOn checksumTask).value, Test / test := ((Test / test) dependsOn (Compile / Keys.`package`)).value, Test / compile := ((Test / compile) dependsOn (Compile / Keys.`package`)).value, + Test / testOnly := ((Test / testOnly) dependsOn (Compile / Keys.`package`)).evaluated, Test / internalDependencyClasspath := testClasspath.value, Compile / packageBin / mappings := newMappingsTask.value, ) diff --git a/project/Build.scala b/project/Build.scala index 3a011d9..2cd755e 100644 --- a/project/Build.scala +++ b/project/Build.scala @@ -6,7 +6,7 @@ import scala.sys.process._ object ScalaZ3Build { lazy val z3SourceRepo = "https://github.com/Z3Prover/z3.git" - lazy val z3SourceTag = "z3-4.7.1" + lazy val z3SourceTag = "z3-4.8.10" lazy val PS = java.io.File.pathSeparator lazy val DS = java.io.File.separator diff --git a/src/main/scala/z3/scala/Z3Context.scala b/src/main/scala/z3/scala/Z3Context.scala index edd2ec5..b2e952c 100644 --- a/src/main/scala/z3/scala/Z3Context.scala +++ b/src/main/scala/z3/scala/Z3Context.scala @@ -1024,24 +1024,6 @@ sealed class Z3Context(val config: Map[String, String]) { res } - // XXX: this is a HUGE hack to get around the fact that the Z3 api doesn't - // provide a handle to the absolute value function. - def getAbsFuncDecl(): Z3FuncDecl = { - val ast = parseSMTLIB2String(""" - (declare-fun x () Int) - (declare-fun y () Int) - (assert (= y (abs x))) - """) - - getASTKind(ast) match { - case Z3AppAST(_, Seq(_, absAst)) => getASTKind(absAst) match { - case Z3AppAST(decl, _) => decl - case c => error("Unexpected ast kind " + c) - } - case c => error("Unexpected ast kind " + c) - } - } - // Parser interface private def parseSMTLIB2(file: Boolean, str: String) : Z3AST = { if(file) { diff --git a/src/main/scala/z3/scala/Z3Optimizer.scala b/src/main/scala/z3/scala/Z3Optimizer.scala index be342b5..047ff31 100644 --- a/src/main/scala/z3/scala/Z3Optimizer.scala +++ b/src/main/scala/z3/scala/Z3Optimizer.scala @@ -67,7 +67,7 @@ class Z3Optimizer private[z3](val ptr: Long, val context: Z3Context) extends Z3O private[this] var lastResult: Option[Boolean] = None def check(): Option[Boolean] = { - val res = i2ob(Native.optimizeCheck(context.ptr, this.ptr)) + val res = i2ob(Native.optimizeCheck(context.ptr, this.ptr, 0, null)) lastResult = res res } diff --git a/src/test/scala/z3/scala/Abs.scala b/src/test/scala/z3/scala/Abs.scala deleted file mode 100644 index c33d418..0000000 --- a/src/test/scala/z3/scala/Abs.scala +++ /dev/null @@ -1,38 +0,0 @@ -package z3.scala - -import org.scalatest.{FunSuite, Matchers} - -class Abs extends FunSuite with Matchers { - - test("array-map absolute value") { - val z3 = new Z3Context("MODEL" -> true) - - val is = z3.mkIntSort - val intArraySort = z3.mkArraySort(is, is) - val array1 = z3.mkFreshConst("arr", intArraySort) - val array2 = z3.mkFreshConst("arr", intArraySort) - - val abs = z3.getAbsFuncDecl() - - val solver = z3.mkSolver - - solver.assertCnstr(z3.mkEq(z3.mkSelect(array1, z3.mkInt(0, is)), z3.mkInt(1, is))) - solver.assertCnstr(z3.mkEq(z3.mkSelect(array1, z3.mkInt(1, is)), z3.mkInt(0, is))) - solver.assertCnstr(z3.mkEq(z3.mkSelect(array1, z3.mkInt(2, is)), z3.mkInt(-1, is))) - - solver.assertCnstr(z3.mkEq(array2, z3.mkArrayMap(abs, array1))) - - val (result, model) = solver.checkAndGetModel - - result should equal(Some(true)) - - val array2Ev = model.eval(array2) - array2Ev should be (Symbol("defined")) - val array2Val = model.getArrayValue(array2Ev.get) - 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)) - valueMap(z3.mkInt(2, is)) should equal (z3.mkInt(1, is)) - } -}