- English only

# Lab for Automated Reasoning and Analysis LARA

# Examples of Using Z3 with Scala

Compiling and running the following examples requires that you obtain z3.jar, `libz3.so`

(from Microsoft Research), and use Scala 2.8. The best way to figure out which functions to use is probably to read through the C API once, then through the Scala API, then looking at examples, and finally, contacting us.

## Testing your setup

## *nix Systems

Once you have the required files, try our your setup with the Scala interpreter. Note that you have to make sure that `libz3.so`

is in the dynamically-loaded library path (`LD_LIBRARY_PATH`

in Unix-like systems). You can run `scala`

as follows:

LD_LIBRARY_PATH=${Z3_LIB_PATH} scala -classpath scalaz3.jar

where `${Z3_LIB_PATH}`

is the directory where you keep `libz3.so`

. (Alternatively, export `LD_LIBRARY_PATH`

once and for all.) Then, try the following:

scala> z3.scala.version

it should print something like:

res0: String = Z3 3.2 (build 0, rev. 0), ScalaZ3 3.2.b

If you have an older version of Z3, go get the latest.

## Windows

~~Make sure you have all required files installed and available in the path, including the Microsoft Visual C++ 2010 Redistributable Package. The instructions are otherwise similar as above.~~

As of ScalaZ3 3.2.a, there are no additional dependencies for the Windows version.

## Solving integer constraints

The following program reads one integer from the command line and converts that number of seconds into hours, minutes and remaining seconds. Fails if the total is more than a day.

import z3.scala._ object SecondsToTime { def main(args : Array[String]) = { val totSecs = args(0).toInt val cfg = new Z3Config("MODEL" -> true) // required if you plan to query models of satisfiable constraints val z3 = new Z3Context(cfg) // prepares the integer sort and three constants (the "unknowns") val i = z3.mkIntSort val h = z3.mkConst(z3.mkStringSymbol("h"), i) val m = z3.mkConst(z3.mkStringSymbol("m"), i) val s = z3.mkConst(z3.mkStringSymbol("s"), i) // builds a constant integer value from the CL arg. val t = z3.mkInt(totSecs, i) // more integer constants val z = z3.mkInt(0, i) val sx = z3.mkInt(60, i) // builds the constraint h*3600 + m * 60 + s == totSecs val cs1 = z3.mkEq( z3.mkAdd( z3.mkMul(z3.mkInt(3600, i), h), z3.mkMul(sx, m), s), t) // more constraints val cs2 = z3.mkAnd(z3.mkGE(h, z), z3.mkLT(h, z3.mkInt(24, i))) val cs3 = z3.mkAnd(z3.mkGE(m, z), z3.mkLT(m, sx)) val cs4 = z3.mkAnd(z3.mkGE(s, z), z3.mkLT(s, sx)) // pushes the constraints to the Z3 context z3.assertCnstr(z3.mkAnd(cs1, cs2, cs3, cs4)) // attempting to solve the constraints, and reading the result z3.checkAndGetModel match { case (None, _) => println("Z3 failed. The reason is: " + z3.getSearchFailure.message) case (Some(false), _) => println("Unsat.") case (Some(true), model) => { println("h: " + model.evalAsInt(h)) println("m: " + model.evalAsInt(m)) println("s: " + model.evalAsInt(s)) model.delete } } z3.delete } }

You can compile it simply by running

scalac -cp scalaz3.jar SecondsToTime.scala

and run it with

LD_LIBRARY_PATH=${Z3_LIB_PATH} scala -cp scalaz3.jar SecondsToTime 12345

for instance.

This should print:

h: Some(3) m: Some(25) s: Some(45)

Now if you try to run it with 123456 instead, you'll get

Unsat.

because the number of seconds exceeds one day.

## Using Quantifiers

The following program uses a quantifier to specify the Fibonacci function and “compute” some values for it.

import z3.scala._ object Fibonacci { def main(args : Array[String]) : Unit = { val config = new Z3Config("MODEL" -> true) val z3 = new Z3Context(config) toggleWarningMessages(true) val intSort = z3.mkIntSort // declares a function symbol of type int->int val fibonacci = z3.mkFreshFuncDecl("fib", List(intSort), intSort) val fib0 = z3.mkEq(fibonacci(z3.mkInt(0, intSort)), z3.mkInt(0, intSort)) // fib(0) = 0 val fib1 = z3.mkEq(fibonacci(z3.mkInt(1, intSort)), z3.mkInt(1, intSort)) // fib(1) = 1 // FORALL x . x > 1 ==> fib(x) = fib(x-1) + fib(x-2) val boundVar = z3.mkBound(0, intSort) val pattern: Z3Pattern = z3.mkPattern(fibonacci(boundVar)) val axiomTree = z3.mkImplies( z3.mkGT(boundVar, z3.mkInt(1, intSort)), z3.mkEq( fibonacci(boundVar), z3.mkAdd( fibonacci(z3.mkSub(boundVar, z3.mkInt(1, intSort))), fibonacci(z3.mkSub(boundVar, z3.mkInt(2, intSort)))) ) ) val someName: Z3Symbol = z3.mkIntSymbol(0) val fibN = z3.mkForAll(0, List(pattern), List((someName, intSort)), axiomTree) // just printing the axioms println("fib0 ::: " + fib0) println("fib1 ::: " + fib1) println("fibN ::: " + fibN) z3.assertCnstr(fib0) z3.assertCnstr(fib1) z3.assertCnstr(fibN) val x = z3.mkConst(z3.mkStringSymbol("v"), intSort) val query = z3.mkEq(x, fibonacci(z3.mkInt(5, intSort))) println("Query ::: " + query) z3.assertCnstr(query) val (answer, model) = z3.checkAndGetModel println("fibonacci(5) = ?") answer match { case Some(true) => println("there's a solution: " + model) case Some(false) => println("no solution") case _ => { println("Failure reason: " + z3.getSearchFailure.message) println("Here's a model anyway : " + model) } } z3.delete } }

Compiling and executing should give you

... Query ::: (= v (fib!0 5)) fibonacci(5) = ? Failure reason: Logical context contains universal quantifiers Here's a model anyway : v -> 5 fib!0 -> { 0 -> 0 1 -> 1 5 -> 5 4 -> 3 3 -> 2 2 -> 1 else -> 1 }

Note that Z3 does not say `sat`

, because of the universally-quantified axiom (it would have to build an infinite model, to be “really sure”). It gives a candidate model, though. The candidate model does not satisfy the universal axiom (because in its interpretation, fib(6) = 1, for instance), but note that it's enough to get you the result that you wanted (fib is correct up to the required value).

## Using Algebraic Data Types

More to come later. Contact us if you're can't wait and/or figure it out by looking at the API.

## Writing Theory Plugins

More to come later. Contact us if you're can't wait and/or figure it out by looking at the API.