z3 - bddbddb 中的非循环关系

Question

我正在使用 Z3 评估使用 bddbddb 格式 ( http://bddbddb.sourceforge.net/ ) 编写的数据记录程序。

如何以 bddbddb 格式表达关系是非循环的这一事实？

我的意思是数据记录中的这样一条规则

：- 相对（X，Y），相对（Y，X）。