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.

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.

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.

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.

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).

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

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