Skip to content

Commit

Permalink
Merge pull request #606 from informalsystems/dependabot/maven/io.gith…
Browse files Browse the repository at this point in the history 
…ub.tudo-aqua-z3-turnkey-4.8.10

- Bump z3-turnkey from 4.8.9 to 4.8.10
- Adapt types as needed to accommodate Z3Prover/z3#4832 (upcasting some types, and supplying some needed type params).
  • Loading branch information
Shon Feder authored Jul 7, 2021
2 parents 205a7d1 + 2ddf17d commit d5d7e1b
Show file tree
Hide file tree
Showing 3 changed files with 78 additions and 64 deletions.
2 changes: 1 addition & 1 deletion pom.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -136,7 +136,7 @@
<dependency>
<groupId>io.github.tudo-aqua</groupId>
<artifactId>z3-turnkey</artifactId>
<version>4.8.9</version>
<version>4.8.10</version>
</dependency>

<dependency>
Expand Down
4 changes: 2 additions & 2 deletions tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/SMTInterface.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ class SMTInterface {
* @param m_fun Wrapped function interpretation
* @param m_varSym Symbol used for variables
*/
private class FunWrapper(m_fun: FuncInterp, m_varSym: String) {
private class FunWrapper[R <: Sort](m_fun: FuncInterp[R], m_varSym: String) {

/** Return value for arguments outside the relevant subdomain. */
protected val m_default: Int = m_fun.getElse.asInstanceOf[IntNum].getInt
Expand All @@ -29,7 +29,7 @@ class SMTInterface {
* to the relevant subdomain.
*/
protected val m_map: Map[String, Int] =
(for { e: FuncInterp.Entry <- m_fun.getEntries } yield (
(for { e: FuncInterp.Entry[R] <- m_fun.getEntries } yield (
"%s_%s".format(m_varSym, e.getArgs.head),
e.getValue.asInstanceOf[IntNum].getInt
)).toMap
Expand Down
136 changes: 75 additions & 61 deletions tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -63,22 +63,27 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext {
* Since context operations may clear function declaration,
* we carry the context level in the map and clean the function declarations on pop.
*/
private val funDecls: mutable.Map[String, (FuncDecl, Int)] =
new mutable.HashMap[String, (FuncDecl, Int)]()
private val funDecls: mutable.Map[String, (FuncDecl[Sort], Int)] =
new mutable.HashMap[String, (FuncDecl[Sort], Int)]()

// The type of expressions of sorted elements.
// The wildcard type helps scalac resolve specious type mismatches of the form
// `Java-defined class Expr is invariant in type R`.
type ExprSort = Expr[Sort]

/**
* The calls to z3context.mkConst consume 20% of the running time, according to VisualVM.
* Let's cache the constants, if Z3 cannot do it well.
* Again, the cache carries the context level, to support push and pop.
*/
private val cellCache: mutable.Map[Int, (Expr, CellT, Int)] =
new mutable.HashMap[Int, (Expr, CellT, Int)]
private val cellCache: mutable.Map[Int, (ExprSort, CellT, Int)] =
new mutable.HashMap[Int, (ExprSort, CellT, Int)]

/**
* A cache for the in-relation between a set and its potential element.
*/
private val inCache: mutable.Map[(Int, Int), (Expr, Int)] =
new mutable.HashMap[(Int, Int), (Expr, Int)]
private val inCache: mutable.Map[(Int, Int), (ExprSort, Int)] =
new mutable.HashMap[(Int, Int), (ExprSort, Int)]

/**
* Sometimes, we lose a fresh arena in the rewriting rules. As this situation is very hard to debug,
Expand Down Expand Up @@ -132,9 +137,9 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext {
// which renders this step useless.
val z3expr =
if (cell.id == 0) {
z3context.mkEq(const, z3context.mkFalse())
z3context.mkEq(const, z3context.mkFalse().asInstanceOf[ExprSort])
} else {
z3context.mkEq(const, z3context.mkTrue())
z3context.mkEq(const, z3context.mkTrue().asInstanceOf[ExprSort])
}

log(s"(assert $z3expr)")
Expand All @@ -154,13 +159,13 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext {
log(s"(declare-const $name Bool)")
nBoolConsts += 1
val const = z3context.mkConst(name, z3context.getBoolSort)
inCache += ((set.id, elem.id) -> (const, level))
inCache += ((set.id, elem.id) -> ((const.asInstanceOf[ExprSort], level)))

_metrics = _metrics.addNConsts(1)
}
}

private def getInPred(setId: Int, elemId: Int): Expr = {
private def getInPred(setId: Int, elemId: Int): ExprSort = {
inCache.get((setId, elemId)) match {
case None =>
val setT = cellCache(setId)._2
Expand Down Expand Up @@ -216,20 +221,17 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext {
def evalGroundExpr(ex: TlaEx): TlaEx = {
val (smtEx, _) = toExpr(ex)
val z3expr = z3solver.getModel.eval(smtEx, true)
z3expr match {
case b: BoolExpr =>
val isTrue = b.getBoolValue.equals(Z3_lbool.Z3_L_TRUE)
ValEx(if (isTrue) TlaBool(true) else TlaBool(false)) // in undefined case, just return false

case i: IntNum =>
ValEx(TlaInt(i.getBigInteger))

case _ =>
if (z3expr.isConst && z3expr.getSort.getName.toString.startsWith("Cell_")) {
NameEx(z3expr.toString)
} else {
flushAndThrow(new SmtEncodingException(s"SMT $id: Expected an integer or Boolean, found: $z3expr", ex))
}
if (z3expr.isBool) {
val isTrue = z3expr.getBoolValue.equals(Z3_lbool.Z3_L_TRUE)
ValEx(if (isTrue) TlaBool(true) else TlaBool(false)) // in undefined case, just return false
} else if (z3expr.isIntNum) {
ValEx(TlaInt(z3expr.asInstanceOf[IntNum].getBigInteger))
} else {
if (z3expr.isConst && z3expr.getSort.getName.toString.startsWith("Cell_")) {
NameEx(z3expr.toString)
} else {
flushAndThrow(new SmtEncodingException(s"SMT $id: Expected an integer or Boolean, found: $z3expr", ex))
}
}
}

Expand Down Expand Up @@ -413,28 +415,28 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext {
}
}

private def toExpr(ex: TlaEx): (Expr, Long) = {
private def toExpr(ex: TlaEx): (ExprSort, Long) = {
simplifier.simplifyShallow(ex) match {
case NameEx(name) =>
val nm = cellCache(ArenaCell.idFromName(name))._1 // the cached cell
(nm, 1)

case ValEx(TlaBool(false)) =>
val bool = z3context.mkFalse()
(bool, 1)
(bool.asInstanceOf[ExprSort], 1)

case ValEx(TlaBool(true)) =>
val bool = z3context.mkTrue()
(bool, 1)
(bool.asInstanceOf[ExprSort], 1)

case ValEx(TlaInt(num)) =>
if (num.isValidLong) {
val int = z3context.mkInt(num.toLong)
(int, 1)
(int.asInstanceOf[ExprSort], 1)
} else {
// support big integers, issue #450
val n = z3context.mkInt(num.toString())
(n, 1)
(n.asInstanceOf[ExprSort], 1)
}

case OperEx(oper: TlaArithOper, lex, rex) =>
Expand All @@ -449,45 +451,45 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext {
if (ArenaCell.isValidName(lname) && ArenaCell.isValidName(rname)) {
// just comparing cells
val eq = z3context.mkEq(cellCache(ArenaCell.idFromName(lname))._1, cellCache(ArenaCell.idFromName(rname))._1)
(eq, 1)
(eq.asInstanceOf[ExprSort], 1)
} else {
// comparing integers and Boolean to cells, Booleans to Booleans, and Integers to Integers
val (le, ln) = toExpr(lhs)
val (re, rn) = toExpr(rhs)
val eq = toEqExpr(le, re)
(eq, 1 + ln + rn)
val eq = toEqExpr(le.asInstanceOf[Expr[Sort]], re.asInstanceOf[Expr[Sort]])
(eq.asInstanceOf[ExprSort], 1 + ln + rn)
}

case OperEx(TlaOper.eq, lhs, rhs) =>
val (le, ln) = toExpr(lhs)
val (re, rn) = toExpr(rhs)
val eq = toEqExpr(le, re)
(eq, 1 + ln + rn)
(eq.asInstanceOf[ExprSort], 1 + ln + rn)

case OperEx(TlaOper.ne, lhs, rhs) =>
val (eq, n) = toExpr(OperEx(TlaOper.eq, lhs, rhs))
(z3context.mkNot(eq.asInstanceOf[BoolExpr]), 1 + n)
(z3context.mkNot(eq.asInstanceOf[BoolExpr]).asInstanceOf[ExprSort], 1 + n)

case OperEx(ApalacheOper.distinct, args @ _*) =>
val (es, ns) = (args map toExpr).unzip
val distinct = z3context.mkDistinct(es: _*)
(distinct,
(distinct.asInstanceOf[ExprSort],
ns.foldLeft(1L) {
_ + _
})

case OperEx(TlaBoolOper.and, args @ _*) =>
val (es, ns) = (args map toExpr).unzip
val and = z3context.mkAnd(es.map(_.asInstanceOf[BoolExpr]): _*)
(and,
(and.asInstanceOf[ExprSort],
ns.foldLeft(1L) {
_ + _
})

case OperEx(TlaBoolOper.or, args @ _*) =>
val (es, ns) = (args map toExpr).unzip
val or = z3context.mkOr(es.map(_.asInstanceOf[BoolExpr]): _*)
(or,
(or.asInstanceOf[ExprSort],
ns.foldLeft(1L) {
_ + _
})
Expand All @@ -496,13 +498,13 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext {
val (lhsZ3, ln) = toExpr(lhs)
val (rhsZ3, rn) = toExpr(rhs)
val imp = z3context.mkImplies(lhsZ3.asInstanceOf[BoolExpr], rhsZ3.asInstanceOf[BoolExpr])
(imp, 1 + ln + rn)
(imp.asInstanceOf[ExprSort], 1 + ln + rn)

case OperEx(TlaBoolOper.equiv, lhs, rhs) =>
val (lhsZ3, ln) = toExpr(lhs)
val (rhsZ3, rn) = toExpr(rhs)
val equiv = z3context.mkEq(lhsZ3.asInstanceOf[BoolExpr], rhsZ3.asInstanceOf[BoolExpr])
(equiv, 1 + ln + rn)
(equiv.asInstanceOf[ExprSort], 1 + ln + rn)

case OperEx(TlaControlOper.ifThenElse, cond, thenExpr, elseExpr) =>
val (boolCond, cn) = toExpr(cond)
Expand All @@ -514,12 +516,12 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext {
case OperEx(TlaBoolOper.not, e) =>
val (exZ3, n) = toExpr(e)
val not = z3context.mkNot(exZ3.asInstanceOf[BoolExpr])
(not, 1 + n)
(not.asInstanceOf[ExprSort], 1 + n)

case OperEx(TlaSetOper.notin, elem, set) =>
val (e, n) = toExpr(OperEx(TlaSetOper.in, elem, set))
val not = z3context.mkNot(e.asInstanceOf[BoolExpr])
(not, 1 + n)
(not.asInstanceOf[ExprSort], 1 + n)

case OperEx(TlaSetOper.in, NameEx(elemName), NameEx(setName)) =>
val setId = ArenaCell.idFromName(setName)
Expand All @@ -535,20 +537,20 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext {
}
}

private def toEqExpr(le: Expr, re: Expr) = {
private def toEqExpr[R <: Sort](le: Expr[R], re: Expr[R]) = {
(le, re) match {
case (_: BoolExpr, _: BoolExpr) | (_: IntExpr, _: IntExpr) =>
z3context.mkEq(le, re)

case (_: IntExpr, _: Expr) =>
case (_: IntExpr, _: Expr[R]) =>
// comparing an integer constant and a cell of integer type, which is declared as integer
z3context.mkEq(le, re)

case (_: Expr, _: IntExpr) =>
case (_: Expr[R], _: IntExpr) =>
// comparing an integer constant and a cell of integer type, which is declared as integer
z3context.mkEq(le, re)

case (_: Expr, _: Expr) =>
case (_: Expr[R], _: Expr[R]) =>
// comparing a cell constant against a function application
z3context.mkEq(le, re)

Expand All @@ -557,63 +559,75 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext {
}
}

private def toArithExpr(ex: TlaEx): (Expr, Long) = {
def mkBinEx(ctor: (ArithExpr, ArithExpr) => Expr, left: TlaEx, right: TlaEx): (Expr, Long) = {
// Workaround for impedence bitween with Java Generics and Scala parametric types
// See, e.g., https://stackoverflow.com/a/16430462/1187277
private def mkArithCmp(ctor: (Expr[ArithSort], Expr[ArithSort]) => BoolExpr)(a: ExprSort, b: ExprSort): ExprSort = {
ctor(a.asInstanceOf[Expr[ArithSort]], b.asInstanceOf[Expr[ArithSort]]).asInstanceOf[ExprSort]
}

private def mkArithOp(ctor: (Expr[ArithSort], Expr[ArithSort]) => ArithExpr[ArithSort])(a: ExprSort,
b: ExprSort): ExprSort = {
ctor(a.asInstanceOf[Expr[ArithSort]], b.asInstanceOf[Expr[ArithSort]]).asInstanceOf[ExprSort]
}

private def toArithExpr(ex: TlaEx): (ExprSort, Long) = {

def mkBinEx(ctor: (ExprSort, ExprSort) => ExprSort, left: TlaEx, right: TlaEx): (ExprSort, Long) = {
val (le, ln) = toArithExpr(left)
val (re, rn) = toArithExpr(right)
val z3ex = ctor(le.asInstanceOf[ArithExpr], re.asInstanceOf[ArithExpr])
val z3ex = ctor(le, re)
(z3ex, 1 + ln + rn)
}

ex match {
case ValEx(TlaInt(num)) =>
if (num.isValidLong) {
val n = z3context.mkInt(num.toLong)
(n, 1)
(n.asInstanceOf[ExprSort], 1)
} else {
// support big integers, issue #450
val n = z3context.mkInt(num.toString())
(n, 1)
(n.asInstanceOf[ExprSort], 1)
}

case NameEx(name) =>
val n = z3context.mkIntConst(name) // TODO: incompatible sorts?
(n, 1)
(n.asInstanceOf[ExprSort], 1)

case OperEx(TlaArithOper.lt, left, right) =>
mkBinEx(z3context.mkLt, left, right)
mkBinEx(mkArithCmp(z3context.mkLt), left, right)

case OperEx(TlaArithOper.le, left, right) =>
mkBinEx(z3context.mkLe, left, right)
mkBinEx(mkArithCmp(z3context.mkLe), left, right)

case OperEx(TlaArithOper.gt, left, right) =>
mkBinEx(z3context.mkGt, left, right)
mkBinEx(mkArithCmp(z3context.mkGt), left, right)

case OperEx(TlaArithOper.ge, left, right) =>
mkBinEx(z3context.mkGe, left, right)
mkBinEx(mkArithCmp(z3context.mkGe), left, right)

case OperEx(TlaArithOper.plus, left, right) =>
mkBinEx({ case (l, r) => z3context.mkAdd(l, r) }, left, right)
mkBinEx(mkArithOp((l, r) => z3context.mkAdd(l, r)), left, right)

case OperEx(TlaArithOper.minus, left, right) =>
mkBinEx({ case (l, r) => z3context.mkSub(l, r) }, left, right)
mkBinEx(mkArithOp((l, r) => z3context.mkSub(l, r)), left, right)

case OperEx(TlaArithOper.mult, left, right) =>
mkBinEx({ case (l, r) => z3context.mkMul(l, r) }, left, right)
mkBinEx(mkArithOp((l, r) => z3context.mkMul(l, r)), left, right)

case OperEx(TlaArithOper.div, left, right) =>
mkBinEx(z3context.mkDiv, left, right)
mkBinEx(mkArithOp(z3context.mkDiv), left, right)

case OperEx(TlaArithOper.mod, left, right) =>
val (le, ln) = toArithExpr(left)
val (re, rn) = toArithExpr(right)
val mod = z3context.mkMod(le.asInstanceOf[IntExpr], re.asInstanceOf[IntExpr])
(mod, 1 + ln + rn)
(mod.asInstanceOf[ExprSort], 1 + ln + rn)

case OperEx(TlaArithOper.uminus, subex) =>
val (e, n) = toArithExpr(subex)
val minus = z3context.mkUnaryMinus(e.asInstanceOf[IntExpr])
(minus, 1 + n)
(minus.asInstanceOf[ExprSort], 1 + n)

case OperEx(TlaControlOper.ifThenElse, cond, thenExpr, elseExpr) =>
val (boolCond, cn) = toExpr(cond)
Expand Down

0 comments on commit d5d7e1b

Please sign in to comment.