Skip to content

Commit

Permalink
Z3 4.8.14
Browse files Browse the repository at this point in the history
  • Loading branch information
@mario-bucev
mario-bucev committed Jan 7, 2022
1 parent f086928 commit 51c6997
Show file tree
Hide file tree
Showing 22 changed files with 261 additions and 197 deletions.
14 changes: 7 additions & 7 deletions README.md
View file
Original file line number Diff line number Diff line change
@@ -1,25 +1,25 @@
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.12 and Scala 2.10, 2.11, 2.12, and 2.13.

[API documentation](https://epfl-lara.github.io/ScalaZ3/z3/index.html)
-------------------

Compiling ScalaZ3
-----------------

You should have Java and SBT 1.2.x installed.
You should have Java and SBT 1.5.x installed.

### Mac & Unix

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.12 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.12.jar`
and will contain the shared library dependencies.

For testing, run
Expand Down Expand Up @@ -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.12.jar` and will contain the shared library
dependencies.

#### Test your package.
Expand All @@ -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.12.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"
baseDirectory.value / "unmanaged" / s"scalaz3_${scalaBinaryVersion.value}-4.8.12.jar"
}
```

Expand Down
7 changes: 4 additions & 3 deletions build.sbt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,15 +3,15 @@ import ScalaZ3Build._
lazy val root = (project in file("."))
.settings(
name := "ScalaZ3",
version := "4.7.1",
version := "4.8.14",
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.13.6"),
libraryDependencies ++= Seq(
"org.scalatest" %% "scalatest" % "3.0.8" % "test"
),
Expand All @@ -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,
)
Expand Down
23 changes: 22 additions & 1 deletion project/Build.scala
View file
Original file line number Diff line number Diff line change
@@ -1,12 +1,15 @@
import sbt._
import sbt.Keys._
import org.eclipse.jgit.api._
import org.eclipse.jgit.treewalk.filter.PathFilter

import java.io.{FileInputStream, InputStream}
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.14"

lazy val PS = java.io.File.pathSeparator
lazy val DS = java.io.File.separator
Expand Down Expand Up @@ -124,6 +127,24 @@ object ScalaZ3Build {
.setName(z3SourceTag)
.call()

val diffs = Git.open(z3Path.asFile)
.diff()
.setPathFilter(PathFilter.create("src/api/"))
.call()
if (diffs.isEmpty) {
s.log.info(s"Applying mk_abs API patch...")
var is: InputStream = null
try {
is = new FileInputStream(new File("z3_mk_abs.patch"))
Git.open(z3Path.asFile)
.apply()
.setPatch(is)
.call()
} finally {
if (is != null) is.close()
}
}

val hashFile = z3Path / ".build-hash"

def computeHash(): String = {
Expand Down
51 changes: 21 additions & 30 deletions src/main/scala/z3/scala/Z3Context.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -236,7 +236,7 @@ sealed class Z3Context(val config: Map[String, String]) {

val (consFuns, unzippedOnce) = zipped.unzip
val (testFuns, selectorFunss) = unzippedOnce.unzip

(new Z3Sort(sort, this), consFuns, testFuns, selectorFunss)
}
}
Expand Down Expand Up @@ -265,15 +265,15 @@ sealed class Z3Context(val config: Map[String, String]) {
}

def mkIntConst(symbol: Z3Symbol) : Z3AST = {
mkConst(symbol, mkIntSort)
mkConst(symbol, mkIntSort())
}

def mkIntConst(s: String) : Z3AST = {
mkIntConst(mkStringSymbol(s))
}

def mkBoolConst(symbol: Z3Symbol) : Z3AST = {
mkConst(symbol, mkBoolSort)
mkConst(symbol, mkBoolSort())
}

def mkBoolConst(s: String) : Z3AST = {
Expand Down Expand Up @@ -301,11 +301,11 @@ sealed class Z3Context(val config: Map[String, String]) {
}

def mkFreshIntConst(prefix: String) : Z3AST = {
mkFreshConst(prefix, mkIntSort)
mkFreshConst(prefix, mkIntSort())
}

def mkFreshBoolConst(prefix: String) : Z3AST = {
mkFreshConst(prefix, mkBoolSort)
mkFreshConst(prefix, mkBoolSort())
}

def mkFreshFuncDecl(prefix: String, domainSorts: Seq[Z3Sort], rangeSort: Z3Sort) : Z3FuncDecl = {
Expand All @@ -328,7 +328,7 @@ sealed class Z3Context(val config: Map[String, String]) {
if(args.size == 0) {
throw new IllegalArgumentException("mkDistinct needs at least one argument")
} else if(args.size == 1) {
mkTrue
mkTrue()
} else {
new Z3AST(Native.mkDistinct(this.ptr, args.length, toPtrArray(args)), this)
}
Expand Down Expand Up @@ -444,6 +444,10 @@ sealed class Z3Context(val config: Map[String, String]) {
new Z3AST(Native.mkInt2real(this.ptr, ast.ptr), this)
}

def mkAbs(ast: Z3AST) : Z3AST = {
new Z3AST(Native.mkAbs(this.ptr, ast.ptr), this)
}

def mkReal2Int(ast: Z3AST) : Z3AST = {
new Z3AST(Native.mkReal2int(this.ptr, ast.ptr), this)
}
Expand Down Expand Up @@ -642,7 +646,7 @@ sealed class Z3Context(val config: Map[String, String]) {
def mkInt(value: Int, sort: Z3Sort) : Z3AST = {
new Z3AST(Native.mkInt(this.ptr, value, sort.ptr), this)
}

def mkReal(numerator: Int, denominator: Int) : Z3AST = {
new Z3AST(Native.mkReal(this.ptr, numerator, denominator), this)
}
Expand Down Expand Up @@ -875,6 +879,7 @@ sealed class Z3Context(val config: Map[String, String]) {
case OpUMinus => mkUnaryMinus(mkFreshConst("x", sorts(0)))
case OpMul => mkMul(sorts.map(mkFreshConst("x", _)) : _*)
case OpDiv => mkDiv(mkFreshConst("a", sorts(0)), mkFreshConst("b", sorts(1)))
case OpAbs => mkAbs(mkFreshConst("x", sorts(0)))
case _ => error("Unexpected decl kind " + op)
}

Expand Down Expand Up @@ -938,23 +943,23 @@ sealed class Z3Context(val config: Map[String, String]) {
}

def getIndexValue(ast: Z3AST) : Int = {
return Native.getIndexValue(this.ptr, ast.ptr)
Native.getIndexValue(this.ptr, ast.ptr)
}

def isQuantifierForall(ast: Z3AST) : Boolean = {
return Native.isQuantifierForall(this.ptr, ast.ptr)
Native.isQuantifierForall(this.ptr, ast.ptr)
}

def getQuantifierBody(ast: Z3AST) : Z3AST = {
return new Z3AST(Native.getQuantifierBody(this.ptr, ast.ptr), this)
new Z3AST(Native.getQuantifierBody(this.ptr, ast.ptr), this)
}

def getQuantifierBoundName(ast: Z3AST, i: Int) : Z3Symbol = {
return new Z3Symbol(Native.getQuantifierBoundName(this.ptr, ast.ptr, i), this)
new Z3Symbol(Native.getQuantifierBoundName(this.ptr, ast.ptr, i), this)
}

def getQuantifierNumBound(ast: Z3AST) : Int = {
return Native.getQuantifierNumBound(this.ptr, ast.ptr)
Native.getQuantifierNumBound(this.ptr, ast.ptr)
}

def getDeclKind(funcDecl: Z3FuncDecl) : Z3DeclKind = {
Expand Down Expand Up @@ -1024,22 +1029,8 @@ 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)
}
getFuncDecl(OpAbs, mkIntSort())
}

// Parser interface
Expand Down Expand Up @@ -1095,7 +1086,7 @@ sealed class Z3Context(val config: Map[String, String]) {
}

def simplifyAst(ast : Z3AST) : Z3AST = {
return new Z3AST(Native.simplify(this.ptr, ast.ptr), this);
new Z3AST(Native.simplify(this.ptr, ast.ptr), this);
}

def mkForAllConst(weight: Int, patterns: Seq[Z3Pattern], bounds: Seq[Z3AST], body: Z3AST) : Z3AST = mkQuantifierConst(true, weight, patterns, bounds, body)
Expand All @@ -1118,11 +1109,11 @@ sealed class Z3Context(val config: Map[String, String]) {
}

def mkTactic(name: String) : Z3Tactic = {
return new Z3Tactic(Native.mkTactic(this.ptr, name), this)
new Z3Tactic(Native.mkTactic(this.ptr, name), this)
}

def mkTacticAndThen(tactic1: Z3Tactic, tactic2: Z3Tactic) : Z3Tactic = {
return new Z3Tactic(Native.tacticAndThen(this.ptr, tactic1.ptr, tactic2.ptr), this)
new Z3Tactic(Native.tacticAndThen(this.ptr, tactic1.ptr, tactic2.ptr), this)
}

def mkSolver() : Z3Solver = {
Expand Down
98 changes: 50 additions & 48 deletions src/main/scala/z3/scala/Z3DeclKind.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,19 +37,20 @@ object OpToReal extends Z3DeclKind (Z3_decl_kind.Z3_OP_TO_REAL.toInt)
object OpToInt extends Z3DeclKind (Z3_decl_kind.Z3_OP_TO_INT.toInt)
object OpIsInt extends Z3DeclKind (Z3_decl_kind.Z3_OP_IS_INT.toInt)
object OpPower extends Z3DeclKind (Z3_decl_kind.Z3_OP_POWER.toInt) // NEW in ScalaZ3 3.0
object OpAbs extends Z3DeclKind (Z3_decl_kind.Z3_OP_ABS.toInt) // NEW in ScalaZ3 4.8.12

// Arrays & Sets
object OpStore extends Z3DeclKind (Z3_decl_kind.Z3_OP_STORE.toInt)
object OpSelect extends Z3DeclKind (Z3_decl_kind.Z3_OP_SELECT.toInt)
object OpConstArray extends Z3DeclKind (Z3_decl_kind.Z3_OP_CONST_ARRAY.toInt)
object OpArrayMap extends Z3DeclKind (Z3_decl_kind.Z3_OP_ARRAY_MAP.toInt)
object OpArrayDefault extends Z3DeclKind (Z3_decl_kind.Z3_OP_ARRAY_DEFAULT.toInt)
object OpSetUnion extends Z3DeclKind (Z3_decl_kind.Z3_OP_SET_UNION.toInt)
object OpSetIntersect extends Z3DeclKind (Z3_decl_kind.Z3_OP_SET_INTERSECT.toInt)
object OpStore extends Z3DeclKind (Z3_decl_kind.Z3_OP_STORE.toInt)
object OpSelect extends Z3DeclKind (Z3_decl_kind.Z3_OP_SELECT.toInt)
object OpConstArray extends Z3DeclKind (Z3_decl_kind.Z3_OP_CONST_ARRAY.toInt)
object OpArrayMap extends Z3DeclKind (Z3_decl_kind.Z3_OP_ARRAY_MAP.toInt)
object OpArrayDefault extends Z3DeclKind (Z3_decl_kind.Z3_OP_ARRAY_DEFAULT.toInt)
object OpSetUnion extends Z3DeclKind (Z3_decl_kind.Z3_OP_SET_UNION.toInt)
object OpSetIntersect extends Z3DeclKind (Z3_decl_kind.Z3_OP_SET_INTERSECT.toInt)
object OpSetDifference extends Z3DeclKind (Z3_decl_kind.Z3_OP_SET_DIFFERENCE.toInt)
object OpSetComplement extends Z3DeclKind (Z3_decl_kind.Z3_OP_SET_COMPLEMENT.toInt)
object OpSetSubset extends Z3DeclKind (Z3_decl_kind.Z3_OP_SET_SUBSET.toInt)
object OpAsArray extends Z3DeclKind (Z3_decl_kind.Z3_OP_AS_ARRAY.toInt)
object OpSetSubset extends Z3DeclKind (Z3_decl_kind.Z3_OP_SET_SUBSET.toInt)
object OpAsArray extends Z3DeclKind (Z3_decl_kind.Z3_OP_AS_ARRAY.toInt)
object OpArrayExt extends Z3DeclKind (Z3_decl_kind.Z3_OP_ARRAY_EXT.toInt) // NEW in ScalaZ3 3.0

// Bit-vectors
Expand Down Expand Up @@ -262,50 +263,51 @@ object Z3DeclKind {
}

def fromZ3(kind: Z3_decl_kind): Z3DeclKind = kind match {
case Z3_decl_kind.Z3_OP_TRUE => OpTrue
case Z3_decl_kind.Z3_OP_FALSE => OpFalse
case Z3_decl_kind.Z3_OP_EQ => OpEq
case Z3_decl_kind.Z3_OP_DISTINCT => OpDistinct
case Z3_decl_kind.Z3_OP_ITE => OpITE
case Z3_decl_kind.Z3_OP_AND => OpAnd
case Z3_decl_kind.Z3_OP_OR => OpOr
case Z3_decl_kind.Z3_OP_IFF => OpIff
case Z3_decl_kind.Z3_OP_XOR => OpXor
case Z3_decl_kind.Z3_OP_NOT => OpNot
case Z3_decl_kind.Z3_OP_IMPLIES => OpImplies
case Z3_decl_kind.Z3_OP_TRUE => OpTrue
case Z3_decl_kind.Z3_OP_FALSE => OpFalse
case Z3_decl_kind.Z3_OP_EQ => OpEq
case Z3_decl_kind.Z3_OP_DISTINCT => OpDistinct
case Z3_decl_kind.Z3_OP_ITE => OpITE
case Z3_decl_kind.Z3_OP_AND => OpAnd
case Z3_decl_kind.Z3_OP_OR => OpOr
case Z3_decl_kind.Z3_OP_IFF => OpIff
case Z3_decl_kind.Z3_OP_XOR => OpXor
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_ANUM => OpANum
case Z3_decl_kind.Z3_OP_AGNUM => OpAGNum
case Z3_decl_kind.Z3_OP_LE => OpLE
case Z3_decl_kind.Z3_OP_GE => OpGE
case Z3_decl_kind.Z3_OP_LT => OpLT
case Z3_decl_kind.Z3_OP_GT => OpGT
case Z3_decl_kind.Z3_OP_ADD => OpAdd
case Z3_decl_kind.Z3_OP_SUB => OpSub
case Z3_decl_kind.Z3_OP_UMINUS => OpUMinus
case Z3_decl_kind.Z3_OP_MUL => OpMul
case Z3_decl_kind.Z3_OP_DIV => OpDiv
case Z3_decl_kind.Z3_OP_IDIV => OpIDiv
case Z3_decl_kind.Z3_OP_REM => OpRem
case Z3_decl_kind.Z3_OP_MOD => OpMod
case Z3_decl_kind.Z3_OP_TO_REAL => OpToReal
case Z3_decl_kind.Z3_OP_TO_INT => OpToInt
case Z3_decl_kind.Z3_OP_IS_INT => OpIsInt
case Z3_decl_kind.Z3_OP_POWER => OpPower

case Z3_decl_kind.Z3_OP_STORE => OpStore
case Z3_decl_kind.Z3_OP_SELECT => OpSelect
case Z3_decl_kind.Z3_OP_CONST_ARRAY => OpConstArray
case Z3_decl_kind.Z3_OP_ANUM => OpANum
case Z3_decl_kind.Z3_OP_AGNUM => OpAGNum
case Z3_decl_kind.Z3_OP_LE => OpLE
case Z3_decl_kind.Z3_OP_GE => OpGE
case Z3_decl_kind.Z3_OP_LT => OpLT
case Z3_decl_kind.Z3_OP_GT => OpGT
case Z3_decl_kind.Z3_OP_ADD => OpAdd
case Z3_decl_kind.Z3_OP_SUB => OpSub
case Z3_decl_kind.Z3_OP_UMINUS => OpUMinus
case Z3_decl_kind.Z3_OP_MUL => OpMul
case Z3_decl_kind.Z3_OP_DIV => OpDiv
case Z3_decl_kind.Z3_OP_IDIV => OpIDiv
case Z3_decl_kind.Z3_OP_REM => OpRem
case Z3_decl_kind.Z3_OP_MOD => OpMod
case Z3_decl_kind.Z3_OP_TO_REAL => OpToReal
case Z3_decl_kind.Z3_OP_TO_INT => OpToInt
case Z3_decl_kind.Z3_OP_IS_INT => OpIsInt
case Z3_decl_kind.Z3_OP_POWER => OpPower
case Z3_decl_kind.Z3_OP_ABS => OpAbs

case Z3_decl_kind.Z3_OP_STORE => OpStore
case Z3_decl_kind.Z3_OP_SELECT => OpSelect
case Z3_decl_kind.Z3_OP_CONST_ARRAY => OpConstArray
case Z3_decl_kind.Z3_OP_ARRAY_MAP => OpArrayMap
case Z3_decl_kind.Z3_OP_ARRAY_DEFAULT => OpArrayDefault
case Z3_decl_kind.Z3_OP_SET_UNION => OpSetUnion
case Z3_decl_kind.Z3_OP_SET_INTERSECT => OpSetIntersect
case Z3_decl_kind.Z3_OP_SET_DIFFERENCE => OpSetDifference
case Z3_decl_kind.Z3_OP_SET_COMPLEMENT => OpSetComplement
case Z3_decl_kind.Z3_OP_SET_UNION => OpSetUnion
case Z3_decl_kind.Z3_OP_SET_INTERSECT => OpSetIntersect
case Z3_decl_kind.Z3_OP_SET_DIFFERENCE => OpSetDifference
case Z3_decl_kind.Z3_OP_SET_COMPLEMENT => OpSetComplement
case Z3_decl_kind.Z3_OP_SET_SUBSET => OpSetSubset
case Z3_decl_kind.Z3_OP_AS_ARRAY => OpAsArray
case Z3_decl_kind.Z3_OP_ARRAY_EXT => OpArrayExt
case Z3_decl_kind.Z3_OP_AS_ARRAY => OpAsArray
case Z3_decl_kind.Z3_OP_ARRAY_EXT => OpArrayExt

case Z3_decl_kind.Z3_OP_BNUM => OpBNum
case Z3_decl_kind.Z3_OP_BIT1 => OpBit1
Expand Down
Loading

0 comments on commit 51c6997

Please sign in to comment.