尝试使用 query
关键字提出定点查询时,我收到"未知排序"错误。 例如,定点教程中的以下示例,在 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)
返回:
(error "line 9 column 13: unknown sort 'mc'")
当我从命令行运行它时。 我使用从 Linux 上的 github 存储库编译的 Z3 版本 4.4.2。我的命令行是:z3 -smt2 example.smt
是否需要设置一些编译标志才能启用此功能?
我最近将"query"的格式更改为仅使用谓词。本教程必须更新。
(declare-rel q (Int Int))
(rule (=> (and (mc m n) (< n 91)) (q m n)))
(query q :print-certificate true)