2

parsesmtlib2string を使用してテストを実装しようとすると、エラーが発生しました。

println("Hello World!");
var smtlib2String = ""
smtlib2String += "(declare-fun x () bool)" + "\n"
smtlib2String += "(declare-fun y () bool)" + "\n"
smtlib2String += "(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)

「Check-sat」のコメントを外すと、「unknown」と表示されます。「モデル」のコメントを外すと、「サポートされていません」と表示されます。

Z3 3.2 で F# を使用すると Term が返されますが、Scala では戻り値の型は Unit です。Z3-C API を調べましたが、ist の使用方法に関する適切な例が見つかりませんでした。

では、smtlib2string を使用してモデルを取得する最良の方法は何でしょうか?

ところで: Scala^Z3 を使用して Z3AST をビルドすると問題なく動作し、.checkAndGetModel() を使用してモデルを取得できます。上記の SMT-LIB2 コードは、F# .NET parsesmtlib2string メソッドで正常に動作します。

「getSMTLIBFormulas、getSMTLIBAssumptions、getSMTLIBDecls、getSMTLIBSorts」のいずれかを使用すると、「エラー: パーサー (データ) が利用できません」というメッセージが表示されます。

「getSMTLIBError.size」を使用すると「0」になります。

4

1 に答える 1

2

問題を報告してくれてparseSMTLIB2[...]ありがとう。Z3ASTこれはscalaz3-3.2.b.jarで修正されています。SMT-LIB 2 パーサーの使用に関しては、私自身が初めてなので、おそらく Leo が確認する必要がありますが、私の理解では、SMT-LIB 2 パーサーは数式を解析するためだけに使用し、(check-sat).

これは私のために働く例です：

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

のモデルをプログラムで回復したい場合x、私の理解では、それを行う唯一の方法は、メソッドのオーバーロードされた定義を使用して、解析x 前にparseSMTLIB2[...]のシンボルを作成し、それをパーサーに渡すことです。方法は次のとおりです。

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

お役に立てれば。

(繰り返しますが、これを行うためのより簡単な方法があるかもしれませんが、私はそれを認識していません。解析メソッドは C の同等物に直接バインドされており、私が見つけた唯一の例はあまり示していません。)

于 2011-09-26T14:15:20.853 に答える