Update Z3 to version 4.7.1

Author: romac

README.md

@@ -1,26 +1,22 @@
 ScalaZ3 for Scala 2.10, 2.11, and 2.12
 ======================================
 
-This is ScalaZ3 for Z3 4.5.0 and Scala 2.10, 2.11, and 2.12.
-
-ScalaZ3 for Z3 version 4.3.2 can be found in the branch `Z3-4.3.2`.
-
-Switch to the branch `2.9.x` for Scala 2.9 support (Z3 version 4.3.2).
+This is ScalaZ3 for Z3 4.7.1 and Scala 2.10, 2.11, and 2.12.
 
 Compiling ScalaZ3
 -----------------
 
-You should have Java and SBT 0.13.x installed.
+You should have Java and SBT 1.2.x installed.
 
 ### Mac & Unix
 
 Run
 
     sbt +package
-    
-to compile Z3 4.5.0 and cross-compile ScalaZ3 for Scala 2.10, 2.11 and 2.12.
 
-The JAR files will be in `target/scala-2.XX/scalaz3_2.XX-3.0.jar`
+to compile Z3 4.7.1 and cross-compile ScalaZ3 for Scala 2.10, 2.11 and 2.12.
+
+The JAR files will be in `target/scala-2.XX/scalaz3_2.XX-4.7.1.jar`
 and will contain the shared library dependencies.
 
 For testing, run
@@ -58,7 +54,7 @@ Now navigate to the scalaz3 folder and type:
 
     sbt +package
 
-The JAR files will be in `target/scala-2.XX/scalaz3_2.XX-3.0.jar` and will contain the shared library
+The JAR files will be in `target/scala-2.XX/scalaz3_2.XX-4.7.1.jar` and will contain the shared library
 dependencies.
 
 #### Test your package.

build.sbt

@@ -3,7 +3,7 @@ import ScalaZ3Build._
 lazy val root = (project in file("."))
   .settings(
     name := "ScalaZ3",
-    version := "4.0",
+    version := "4.7.1",
     organization := "ch.epfl.lara",
     scalacOptions ++= Seq(
       "-deprecation",

project/Build.scala

@@ -5,6 +5,9 @@ import scala.sys.process._
 
 object ScalaZ3Build {
 
+  lazy val z3SourceRepo = "https://github.com/Z3Prover/z3.git"
+  lazy val z3SourceTag  = "z3-4.7.1"
+
   lazy val PS = java.io.File.pathSeparator
   lazy val DS = java.io.File.separator
 
@@ -32,9 +35,6 @@ object ScalaZ3Build {
   lazy val jdkMacIncludePath  = jdkIncludePath / "darwin"
   lazy val jdkWinIncludePath  = jdkIncludePath / "win32"
 
-  lazy val z3SourceRepo = "https://github.com/Z3Prover/z3.git"
-  lazy val z3SourceTag = "z3-4.6.0"
-
   lazy val osInf: String = Option(System.getProperty("os.name")).getOrElse("")
 
   lazy val osArch: String = {
@@ -112,7 +112,7 @@ object ScalaZ3Build {
     val s = streams.value
 
     if (!z3Path.asFile.exists) {
-      s.log.info("Cloning Z3 source repository ...")
+      s.log.info(s"Cloning Z3 source repository to $z3Path...")
       Git.cloneRepository()
         .setDirectory(z3Path.asFile)
         .setURI(z3SourceRepo)

src/main/scala/z3/scala/Z3DeclKind.scala

@@ -17,7 +17,6 @@ object OpXor      extends Z3DeclKind (Z3_decl_kind.Z3_OP_XOR.toInt)
 object OpNot      extends Z3DeclKind (Z3_decl_kind.Z3_OP_NOT.toInt)
 object OpImplies  extends Z3DeclKind (Z3_decl_kind.Z3_OP_IMPLIES.toInt)
 object OpOEq      extends Z3DeclKind (Z3_decl_kind.Z3_OP_OEQ.toInt)      // NEW in ScalaZ3 3.0
-object OpInterp   extends Z3DeclKind (Z3_decl_kind.Z3_OP_INTERP.toInt)   // NEW in ScalaZ3 3.0
 
 // Arithmetic
 object OpANum   extends Z3DeclKind (Z3_decl_kind.Z3_OP_ANUM.toInt)
@@ -126,7 +125,6 @@ object OpPrNotOrElim        extends Z3DeclKind (Z3_decl_kind.Z3_OP_PR_NOT_OR_ELI
 object OpPrRewrite          extends Z3DeclKind (Z3_decl_kind.Z3_OP_PR_REWRITE.toInt)           // NEW in ScalaZ3 3.0
 object OpPrRewriteStar      extends Z3DeclKind (Z3_decl_kind.Z3_OP_PR_REWRITE_STAR.toInt)      // NEW in ScalaZ3 3.0
 object OpPrPullQuant        extends Z3DeclKind (Z3_decl_kind.Z3_OP_PR_PULL_QUANT.toInt)        // NEW in ScalaZ3 3.0
-object OpPrPullQuantStar    extends Z3DeclKind (Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR.toInt)   // NEW in ScalaZ3 3.0
 object OpPrPushQuant        extends Z3DeclKind (Z3_decl_kind.Z3_OP_PR_PUSH_QUANT.toInt)        // NEW in ScalaZ3 3.0
 object OpPrElimUnusedVars   extends Z3DeclKind (Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS.toInt)  // NEW in ScalaZ3 3.0
 object OpPrDER              extends Z3DeclKind (Z3_decl_kind.Z3_OP_PR_DER.toInt)               // NEW in ScalaZ3 3.0
@@ -143,8 +141,6 @@ object OpPrApplyDef         extends Z3DeclKind (Z3_decl_kind.Z3_OP_PR_APPLY_DEF.
 object OpPrIffOEq           extends Z3DeclKind (Z3_decl_kind.Z3_OP_PR_IFF_OEQ.toInt)           // NEW in ScalaZ3 3.0
 object OpPrNNFPos           extends Z3DeclKind (Z3_decl_kind.Z3_OP_PR_NNF_POS.toInt)           // NEW in ScalaZ3 3.0
 object OpPrNNFNeg           extends Z3DeclKind (Z3_decl_kind.Z3_OP_PR_NNF_NEG.toInt)           // NEW in ScalaZ3 3.0
-object OpPrNNFStar          extends Z3DeclKind (Z3_decl_kind.Z3_OP_PR_NNF_STAR.toInt)          // NEW in ScalaZ3 3.0
-object OpPrCNFStar          extends Z3DeclKind (Z3_decl_kind.Z3_OP_PR_CNF_STAR.toInt)          // NEW in ScalaZ3 3.0
 object OpPrSkolemize        extends Z3DeclKind (Z3_decl_kind.Z3_OP_PR_SKOLEMIZE.toInt)         // NEW in ScalaZ3 3.0
 object OpPrModusPonensOEq   extends Z3DeclKind (Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ.toInt)  // NEW in ScalaZ3 3.0
 object OpPrThLemma          extends Z3DeclKind (Z3_decl_kind.Z3_OP_PR_TH_LEMMA.toInt)          // NEW in ScalaZ3 3.0
@@ -278,7 +274,6 @@ object Z3DeclKind {
     case Z3_decl_kind.Z3_OP_NOT => OpNot 
     case Z3_decl_kind.Z3_OP_IMPLIES => OpImplies 
     case Z3_decl_kind.Z3_OP_OEQ => OpOEq
-    case Z3_decl_kind.Z3_OP_INTERP => OpInterp
 
     case Z3_decl_kind.Z3_OP_ANUM => OpANum 
     case Z3_decl_kind.Z3_OP_AGNUM => OpAGNum 
@@ -383,7 +378,6 @@ object Z3DeclKind {
     case Z3_decl_kind.Z3_OP_PR_REWRITE => OpPrRewrite
     case Z3_decl_kind.Z3_OP_PR_REWRITE_STAR => OpPrRewriteStar
     case Z3_decl_kind.Z3_OP_PR_PULL_QUANT => OpPrPullQuant
-    case Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR => OpPrPullQuantStar
     case Z3_decl_kind.Z3_OP_PR_PUSH_QUANT => OpPrPushQuant
     case Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS => OpPrElimUnusedVars
     case Z3_decl_kind.Z3_OP_PR_DER => OpPrDER
@@ -400,8 +394,6 @@ object Z3DeclKind {
     case Z3_decl_kind.Z3_OP_PR_IFF_OEQ => OpPrIffOEq
     case Z3_decl_kind.Z3_OP_PR_NNF_POS => OpPrNNFPos
     case Z3_decl_kind.Z3_OP_PR_NNF_NEG => OpPrNNFNeg
-    case Z3_decl_kind.Z3_OP_PR_NNF_STAR => OpPrNNFStar
-    case Z3_decl_kind.Z3_OP_PR_CNF_STAR => OpPrCNFStar
     case Z3_decl_kind.Z3_OP_PR_SKOLEMIZE => OpPrSkolemize
     case Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ => OpPrModusPonensOEq
     case Z3_decl_kind.Z3_OP_PR_TH_LEMMA => OpPrThLemma