1

Z3 モデルの一部として返されたセット オブジェクトを印刷/表示できませんでした。次の例を考えてみましょう (F# の場合)。

let ctx:Context = new Context()
let ASort = ctx.MkEnumSort("S",[| "A"; "B"; "C"|])
let ASetSort = ctx.MkSetSort(ASort)
let xs = ctx.MkConst("xs",ASetSort)
let p = mkPredDecl ctx ("p",[|ASetSort|])
let px = ctx.MkApp(p,xs) :?> BoolExpr
let s = ctx.MkSolver()
s.Assert (ctx.MkAnd(px, ctx.MkNot(ctx.MkEq(xs,ctx.MkEmptySet(ASort)))))
assert (s.Check() = Status.SATISFIABLE)
let xs_interp = s.Model.Eval(xs)
xs_interp

ソルバーはセットを返します (この場合はシングルトン セット {A} ですが、問題ではありません)。実際に印刷する方法がわかりませんでした。標準的なToString()方法は単に配列であると言い、モデルを表示すると、クエリ関数を使用してセットが内部的に表現されていることがわかります。私は次のことを試しました

let foo xs x =
  let mem= ctx.MkSetMembership(x,xs_interp) :?> BoolExpr
  s.Assert mem
  s.Check()= Status.SATISFIABLE
Array.filter (foo xs) ASort.Consts

不格好なだけでなく、機能しません。セットのクエリ関数表現を調べることができると思いますが、Z3 のセットの表現が変更されてコードが壊れてしまうと、あまり良くないように思えます。API に欠けているものはありますか? ToString() メソッドを変更して、セットの内容を実際に出力することはできますか?

4

1 に答える 1