"unknown sort" 定点查询错误

Question

我在尝试使用 query 关键字进行定点查询时收到 "unknown sort" 错误。比如下面这个来自定点教程的例子，在Z3的网络版中效果很好，

(declare-rel mc (Int Int))
(declare-var n Int)
(declare-var m Int)
(declare-var p Int)

(rule (=> (> m 100) (mc m (- m 10))))
(rule (=> (and (<= m 100) (mc (+ m 11) p) (mc p n)) (mc m n)))

(query (and (mc m n) (< n 91))
 :print-certificate true)

returns:

(error "line 9 column 13: unknown sort 'mc'")

当我从命令行运行时。我使用从 Linux 上的 github 存储库编译的 Z3 版本 4.4.2。我的命令行是：z3 -smt2 example.smt

是否需要设置一些编译标志才能启用此功能？

Answer 1

我最近更改了 "query" 的格式以仅使用谓词。教程要更新了。

 (declare-rel q (Int Int))
 (rule (=> (and (mc m n) (< n 91)) (q m n)))
 (query q :print-certificate true)

"unknown sort" 定点查询错误

"unknown sort" error in fixed point queries

z3

z3-fixedpoint