0

我有这种树数据类型，我希望能够在其中上下移动。但实际上，任何结构都可以工作，只要我能得到一个节点的父/左子/右子。

Tree = Datatype('Tree')
Tree.declare('nil')
Tree.declare('node', ('label', IntSort()), ('left', Tree), ('up', Tree), ('right', Tree))
Tree = Tree.create()

但我不知道如何填充数据结构......我以为我可以一次创建一个节点，如下所示，但这似乎是错误的方式。

trees = [Const('t' + str(i), Tree) for i in range(3)]
Tree.up(trees[0]) = Tree.nil
Tree.left(trees[0]) = trees[1]
Tree.right(trees[0]) = trees[2]
Tree.up(trees[1]) = trees[0]
Tree.up(trees[2]) = trees[0]

谢谢你的帮助。

4

1 回答 1

2

我感觉您对此类数据结构的工作方式有些误解。Z3 的语言，因此也是 Z3py 的语言，是一阶逻辑（模理论）的语言，其中只存在假设/事实。命令式编程语言的主要区别之一是，您没有破坏性更新*，即您无法更新实体的值。

在您的代码中，您尝试通过本质上操作指针（例如，通过（尝试的）赋值）以命令式的方式构建数据结构

Tree.up(trees[0]) = Tree.nil

您可能想到的是“trees[0].up指向nil”。但是，由于破坏性更新不是一阶语言的一部分，因此您必须“考虑功能性”，即“假设up(trees[0]) == nil”。添加这样的假设可以如下完成（在rise4fun上在线）：

s = Solver()

s.add(
  Tree.up(trees[0]) == Tree.nil,
  Tree.left(trees[0]) == trees[1],
  Tree.right(trees[0]) == trees[2],
  Tree.up(trees[1]) == trees[0],
  Tree.up(trees[2]) == trees[0]
)

print s.check() # sat -> your constraints are satisfiable

没有破坏性更新的结果是您无法以命令式编程语言的典型方式修改数据结构。有了这样的更新，就可以修改树trees[1].up.left != trees[1]，例如，通过赋值trees[1].up.left = trees[2](for trees[1] != trees[2])。但是，如果添加相应的假设

s.add(
  trees[1] != trees[2],
  Tree.left(Tree.up(trees[1])) == trees[2]
)

print s.check() # unsat

您会发现您的约束不再可满足，因为新旧假设相互矛盾。


顺便说一句，您对Tree数据类型的定义可以假设Tree.up(nil) == someTree. 假设t1 != t2是一棵树的叶子 和left(t1) == right(t1) == nil和 类似，那么如果和t2，你就会有矛盾。不过，我不知道如何在 Z3 级别上防止这种情况发生。up(nil) == t1up(nil) == t2


* 破坏性更新可以作为语法糖添加，因为它们可以通过所谓的传递转换变成假设。例如，这是在中间验证语言Boogie中完成的。

于 2013-06-11T09:28:22.830 回答