1

我正在尝试在 c# 中使用 z3 实现一些 GDL http://en.wikipedia.org/wiki/Game_Description_Language，但我几乎陷入了起步阶段。

本质上，我想从以下 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);

但我不知道域应该是未解释的排序还是其他（枚举排序？）。我不确定如何获得“范围”或符号“你”是否只能用整数表示。

4

1 回答 1

2

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

  1. 定点引擎（此时有几个后端）不处理未解释的排序或未解释的函数。你真的应该只使用有限域排序（布尔、位向量、枚举排序）、线性算术和在某种程度上递归数据类型排序。对于角色的概念，枚举排序似乎更合适。例如， player_x 和 player_y 是两个不同的实体。
  2. 对于 GDL，考虑是否存在将 GDL 直接嵌入到 Datalog（没有否定）。然后将这些写成 Horn 子句，例如，Horn 子句就是定点引擎所称的“规则”。

由于 GDL 包含几个内置操作，next、goal、terminal 和 init，它们具有特殊的解释，并且 GDL 中的规则解释不直接对应于一组 Horn 子句（例如，据我所知，“next ” 是同步的）首先使用转换系统来理解 GDL 语义可能是最容易的，它更新状态变量的向量，然后从转换系统中提取 Horn 子句（将转换系统转换为 Horn 子句的示例在http： //rise4fun.com/Z3Py/tutorial/fixedpoints）然后使用 Horn 子句/规则写下转换系统。

于 2013-08-01T17:02:13.963 回答