z3 - 如何使用命令行在 Z3 中运行数据记录

Question

我尝试在 Z3（版本：4.3.2）中运行数据记录文件（test.dl，来自http://rise4fun.com/Z3/tutorialcontent/fixedpoints#h21），如下所示。

(set-option :fixedpoint.engine datalog)
(define-sort s () (_ BitVec 3))
(declare-rel edge (s s))
(declare-rel path (s s))
(declare-var a s)
(declare-var b s)
(declare-var c s)

(rule (=> (edge a b) (path a b)))
(rule (=> (and (path a b) (path b c)) (path a c)))

(rule (edge #b001 #b010))
(rule (edge #b001 #b011))
(rule (edge #b010 #b100))

(query (path #b001 #b100))
(query (path #b011 #b100))
(query (path #b001 b)
  :print-answer true)

使用命令z3 test.dl，但有错误消息：

有人可以帮助如何运行数据记录文件吗？

谢谢。

Answer 1

此文件的输入格式是 SMT2，而不是 Datalog。即使您想运行 Datalog 引擎，该文件也不是 Datalog 格式，因此解析器会为您提供您看到的错误。

使用该命令运行 Z3z3 -smt2 test.dl是成功的，因为这会强制 Z3 使用 SMT2 解析器而不是 Datalog 解析器。或者，将文件重命名为test.smt2并运行z3 test.smt2作品。

这两个命令都产生了我认为是预期的输出 sat unsat sat (or (= (:var 0) #b011) (= (:var 0) #b010) (= (:var 0) #b100))