如何使用命令行运行数据记录 Z3答案

【问题标题】：How to run datalog in Z3 using commad line如何使用命令行运行数据记录 Z3
【发布时间】：2015-12-05 14:16:25
【问题描述】：

我尝试在 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，但是有错误消息：

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

谢谢。

【问题讨论】：

标签： z3 datalog

【解决方案1】：

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

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

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

【讨论】：