Levent Erkok指出的教程实际上包含了所有正确的信息(我认为(。我既不知道Datalog也不知道Z3的固定点功能，仍然能够拼凑出以下内容：
我想用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)(。
(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，表示存在循环，但如果删除了任何E-规则，则报告unsat。
不过，我不得不使用int而不是字符串，因为如果使用字符串，(我的版本(Z3将中止并返回错误Rule contains infinite sorts in rule P-1。