为什么这个 Z3 查询失败答案

【问题标题】：Why is this Z3 query failing为什么这个 Z3 查询失败
【发布时间】：2015-03-10 00:54:08
【问题描述】：

我正在试验 Z3，尤其是 muZ，但是有些查询失败了，我不明白为什么。比如这个蕴涵的定义

(declare-rel imp (Bool Bool))
(declare-var post Bool)

(rule (imp false post))
(rule (=> (imp true post) post))

(query (imp true false) :print-certificate true)

给出错误(error "query failed: Illegal head. The head predicate needs to be uninterpreted and registered (as recursive) (= (:var 0) true)")

更大的示例，使用相同结构定义的许多参数按预期工作。此外，通过删除第二条规则，我得到了错误ERROR: certificates are not supported for datalog，这让我怀疑由于某种原因这个问题被错误地解释为datalog，而更大的问题被解释为fixedpoints。

是什么导致此查询失败？

【问题讨论】：

标签： z3

【解决方案1】：

格式形式规则通常假定规则的头部有未解释的谓词。第二条规则的头部有一个绑定变量。

如果您将非命题特征添加到数据记录规则中，例如算术，定点引擎将寻求调度理解这些特征的引擎。您可以通过指定 (set-option :fixedpoint.engine 'engine-name') 来控制引擎，其中 'engine-name' 是 datalog/duality/pdr 等。对证书和答案的支持因引擎而异。

【讨论】：