在z3中实现GDL的尝试

Question

我正在尝试使用Language中的z3实现一些GDL c#，而且我几乎被困在了起始块中。

基本上，我想从下面的gdl开始非常简单

(role you) 
(init (state 0))

(<= (legal you proceed)
(true (state 0)))

(<= (next (state 1))
(does you proceed))

(<= terminal
(true (state 1)))

(<= (goal you 100))

然后询问哪一个“法律”是可满足的(在这个设计的例子中，只有一个合法的，在信息状态下是可满足的)。

看一下z3示例，看起来我需要创建一个定点

Fixedpoint fp = ctx.MkFixedpoint();

然后当我想加入

(role you)

我会做

            Sort domain=?;
            Sort range=?;
            FuncDecl pred = ctx.MkFuncDecl("role", domain, range);
            uint you = 1;
            fp.AddFact(pred, you);

但我不知道域应该是未解释的排序还是其他什么(枚举排序？)。我不知道如何得到‘范围’，或者符号'you‘是否可以用整数来表示。

Answer 1

这是一个值得研究的有趣问题。对于Z3的上下文，应该记住以下几点：

1. 定点引擎(此时有几个后端)不处理未解释的排序或未解释的函数。您应该只使用有限域排序(布尔值、位向量、枚举排序)、线性算法以及某种程度上的递归数据类型排序。对于角色的概念，枚举排序似乎是一个更好的匹配。例如，player_x和player_y是两个不同的实体。
2. 对于GDL，请考虑是否将GDL直接嵌入到Datalog (没有否定)。然后把这些写成霍恩子句，例如，霍恩子句就是不动点引擎所称的“规则”。

由于GDL包含几个内置操作，next、目标值、终端和init具有特殊的解释，而对GDL中的规则的解释并不直接对应于一组角子句(例如，据我所知，"next“是同步的)，首先使用一个过渡系统理解GDL语义，更新状态变量向量，然后从过渡系统中提取角子句(在http://rise4fun.com/Z3Py/tutorial/fixedpoints上给出了将过渡系统转换为角子句的一个例子)，然后使用霍恩子句/规则写下转换系统。