z3 - Z3 get-answer 返回不支持

Question

我正在使用 Z3 中的定点引擎来编码几个通用号角公式。查询结果是不满意的。在 Z3Py 中，使用 get_answer() 将估值返回给未解释的关系。但是，在 SMTLIB2 格式中，get-answer 返回unsupported. 这是我的程序：

(declare-var x Int)
(declare-var y Int)

(declare-rel I (Int) interval_relation)
(declare-rel I1 (Int) interval_relation)
(declare-rel err (Int) interval_relation)

(rule (=> (= x 0) (I x) ))
(rule (=> (and (= y (+ x 1)) (I x) ) (I1 y) ))
(rule (=> (and (> y 2) (I1 y)) (err y) ))

(query (err y)
    :engine pdr
:use-farkas true
:print-answer true
)
(get-answer)

我使用 Z3 得到的输出version 4.3.2是：

unsat
unsupported
; get-answer

在 Z3Py 中，创建一个定点上下文，fp=Fixedpoint()然后执行print fp.get_answer()会将估值返回到I和。有没有办法以 SMTLIB2 格式获得相同的内容？谢谢。I1err

Answer 1

评论部分基本上回答了这个问题。“查询”的 SMT-LIB2 扩展采用您的示例所示的属性。事实上 :print-answer 相当于得到答案。