Z3 get-answer 返回不支持答案

【问题标题】：Z3 get-answer returns unsupportedZ3 get-answer 返回不支持
【发布时间】：2013-11-05 20:04:33
【问题描述】：

我正在使用 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、I1 和 err。有没有办法以 SMTLIB2 格式获得相同的内容？谢谢。

【问题讨论】：

啊...get-answer 不是 SMTLIB2 的一部分。我错误地认为它是，因为它是 Z3Py 的一部分。
顺便说一句，declare-rel、rule 和 query 也不属于 SMTLIB2。这些是 Z3 特定的命令，用于使用 Z3 中可用的定点引擎。

标签： z3 z3-fixedpoint

【解决方案1】：

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

【讨论】：