Scala^Z3 (Z3 Version 3.2) and parsesmtlib2string(...) not working

While trying to implement a test using parsesmtlib2string I hit an error:

println("Hello World!");
var smtlib2String = ""
smtlib2String += "(declare-fun x () bool)" + "\n"
smtlib2String += "(declare-fun y () bool)" + "\n"
sm开发者_Python百科tlib2String += "(assert (= x y))" + "\n"
smtlib2String += "(assert (= x true))" + "\n"
//  smtlib2String += "(check-sat)" + "\n"
//  smtlib2String += "(model)" + "\n"
smtlib2String += "(exit)" + "\n"

val cfg = new Z3Config
val z3 = new Z3Context(cfg)

z3.parseSMTLIB2String(smtlib2String)

When uncommenting "Check-sat" I get "unknown". When uncommenting "model" I get "unsupported".

Using F# with Z3 3.2 it would just give me a Term back, but in Scala the return type is Unit. I looked through the Z3-C API but didn't find a good example on how to use ist.

So, what is the best way to get a model using smtlib2string?

Btw: Using Scala^Z3 and building a Z3AST works just fine and I can get a model using .checkAndGetModel(). The SMT-LIB2 Code above works fine with the F# .NET parsesmtlib2string method.

Using one of "getSMTLIBFormulas, getSMTLIBAssumptions, getSMTLIBDecls, getSMTLIBSorts" yields "Error: parser (data) is not available".

Using "getSMTLIBError.size" yields "0".

The parseSMTLIB2[...] methods should indeed have returned a Z3AST, thanks for reporting the problem. This is fixed in scalaz3-3.2.b.jar. Now regarding the use of the SMT-LIB 2 parser, I'm myself new to this, so Leo should perhaps confirm, but my understanding is that you should only use it to parse formulas, not to issue commands such as (check-sat).

Here is an example that works for me:

import z3.scala._
val smtlib2String = """
  (declare-fun x () bool)
  (declare-fun y () bool)
  (assert (= x y))
  (assert (= x true))"""

val ctx = new Z3Context("MODEL" -> true)
val assertions = ctx.parseSMTLIB2String(smtlib2String)
println(assertions) // prints "(and (= x y) (= x true))"
ctx.assertCnstr(assertions)
println(ctx.checkAndGetModel._1) // prints "Some(true)", i.e. SAT

Now if you want to programmatically recover the model for x, my understanding is that the only way to do it is to create a symbol for x before parsing and to pass it to the parser, using the overloaded definition of the parseSMTLIB2[...] method. Here is how you do it:

val ctx = new Z3Context("MODEL" -> true)
val xSym = ctx.mkStringSymbol("x") // should be the same symbol as in the SMT-LIB string
val assertions = ctx.parseSMTLIB2String(smtlib2String, Map(xSym -> ctx.mkBoolSort), Map.empty)
ctx.assertCnstr(assertions)
val model = ctx.checkAndGetModel._2
val xTree = ctx.mkConst(xSym, ctx.mkBoolSort) // need a tree to evaluate using the model
println(model.evalAs[Boolean](xTree)) // prints "Some(true)"

Hope this helps.

(Again, there may be a simpler way to do this, but I'm not aware of it. The parsing methods are directly bound to their C equivalent and the only example I could find doesn't show much.)