使用 SMTLib for z3 的 Datalog 中的循环关系 [英] Cyclic relation in Datalog using SMTLib for z3

问题描述

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

I would like to express this problem in the SMTLib Format and evaluate it using 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) ).

My question is how to write the rule (or query) which detect the existence of a cycle in the relation path (this rule in basic datalog : :- path(x,y), path(y,x) ).

推荐答案

教程Levent Erkok其实指出包含所有正确的信息(我认为).既不了解 Datalog 也不了解 Z3 的修复点功能，我仍然能够拼凑出以下内容:

The tutorial Levent Erkok pointed out actually contains all the right information (I think). Knowing neither Datalog nor Z3's fixpoint features, I was still able to piece together the following:

(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 nightly 报告sat，说明有循环，但是unsat如果去掉E-rules中的任何一个.

Z3 4.8.0 nightly reports sat, indicating that there is a cycle, but unsat if any of the E-rules is removed.

我不得不使用整数而不是字符串，因为(我的版本)Z3 中止并出现错误 Rule 在规则 P-1 中包含无限排序 如果使用字符串.

I had to use ints instead of strings, though, since (my version of) Z3 aborts with the error Rule contains infinite sorts in rule P-1 if strings are used.

这篇关于使用 SMTLib for z3 的 Datalog 中的循环关系的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！