Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Z3 4.8.14 #80

Merged
merged 1 commit into from
Mar 5, 2022
Merged

Z3 4.8.14 #80

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 7 additions & 7 deletions README.md
View file
Open in desktop
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.14 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.14 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.14.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.14.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.14.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.14.jar"
}
```

Expand Down
7 changes: 4 additions & 3 deletions build.sbt
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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("""
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For what it's worth, given the mkAbs helper you added below it should be possible to make this marginally less hacky by avoiding the parsing. I had to do something similar to get a handle to the built-in if-then-else function here: https://github.com/epfl-lara/inox/blob/2f402f9bf9541cc061558e525fdd53efa5f86a87/src/main/scala/inox/solvers/z3/Z3Native.scala#L478

(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
Open in desktop
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