使用 SMTLib for z3 的 Datalog 中的循环关系

Question

我想用 SMTLib 格式表达这个问题，并使用 Z3 进行评估。

edge("som1","som3").
edge("som2","som4").
edge("som4","som1").
edge("som3","som4").
path(x,y) :- edge(x,y). % x and y are strings
path(x,z) :- edge(x,y), path(y,z).
:- path(x,y), path(y,x). %cyclic path.

我的问题是如何编写检测关系路径中是否存在循环的规则（或查询）（基本数据日志中的此规则：:- path(x,y), path(y,x)）。

Answer 1

Levent Erkok 指出的教程实际上包含所有正确的信息（我认为）。既不了解 Datalog 也不了解 Z3 的定点功能，我仍然能够拼凑以下内容：

(set-option :fixedpoint.engine datalog) 
(define-sort s () Int) 

(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)) P-1)
(rule (=> (and (path a b) (path b c)) (path a c)) P-2)

(rule (edge 1 2) E-1)
(rule (edge 2 3) E-2)
(rule (edge 3 1) E-3)

(declare-rel cycle (s))
(rule (=> (path a a) (cycle a)))
(query cycle :print-answer true)

Z3 4.8.0每晚报sat，表示有循环，但是unsat如果有E-rules被去掉的话。

不过，我不得不使用整数而不是字符串，因为如果使用字符串，（我的版本）Z3 会中止并出现错误 Rule contains infinite sorts in rule P-1。