在 Z3Py 中创建变量、对和集

Question

这是一个由三部分组成的问题，涉及 Z3 (Z3Py) 的 Python API 的使用。

1. 我以为我知道常量和变量之间的区别，但显然不知道。我想我可以声明一种排序并实例化该排序的变量，如下所示：

   Node, (a1,a2,a3) = EnumSort('Node', ['a1','a2','a3'])
   n1 = Node('n1') # c.f. x = Int('x')
   

   但是 python 抛出一个异常，说你不能“调用 Node”。似乎唯一有效的是声明n1一个常量

   Node, (a1,a2,a3) = EnumSort('Node', ['a1','a2','a3'])
   n1 = Const('n1',Node)
   

   但我对此感到困惑，因为我认为 a1,a2,a3 是常数。也许 n1 是一个符号常量，但我如何声明一个实际变量？

2. 如何创建常量集？我尝试从一个空集开始并添加到其中，但这不起作用

   Node, (a1,a2,a3) = EnumSort('Node', ['a1','a2','a3'])
   n1 = Const('n1',Node)
   nodes = EmptySet(Node)
   SetAdd(nodes, a1) #<-- want to create a set {a1}
   solve([IsMember(n1,nodes)])
   

   但这不起作用 Z3 没有返回任何解决方案。另一方面，将第三行替换为

   nodes = Const('nodes',SetSort(Node))
   

   现在过于宽松，允许 Z3 将节点解释为满足公式所需的任何节点集。如何只创建集合 {a1}？

3. 除了看起来有点麻烦的数据类型声明之外，是否有一种简单的方法来创建对？例如

   Edge = Datatype('Edge')
   Edge.declare('pr', ('fst', Node), ('snd',Node))
   Edge.create()
   edge1 = Edge.pr(a1,a2)
   

Answer 1

声明枚举

Const正如您所发现的那样，这是正确的声明方式。这确实有点误导，但实际上所有符号变量都是这样创建的。例如，你可以说：

 a = Const('a', IntSort())

这相当于说

a = Int('a')

只是后者看起来更好，但实际上它只是 z3 人们定义的一个函数，它的功能与前者的功能相同。如果您喜欢该语法，可以执行以下操作：

NodeSort, (a1,a2,a3) = EnumSort('Node', ['a1','a2','a3'])

def Node(nm):
    return Const(nm, NodeSort)

现在你可以说：

 n1 = Node ('n1')

我想这就是你的意图。

插入到集合中

你走在正确的道路上；但请记住，该函数SetAdd不会修改设置的参数。它只是创建一个新的。因此，只需给它一个名称并像这样使用它：

emptyNodes = EmptySet(Node)
myNodes = SetAdd(emptyNodes, a1)
solve([IsMember(n1,myNodes)])

或者，您可以简单地替换：

mySet = SetAdd(SetAdd(EmptySet(Node), a1), a2)

这将创建集合{a1, a2}.

根据经验，API 尝试始终发挥作用，即不对现有变量进行破坏性更新，而是从旧值中创建新值。

结对工作

这是唯一的办法。但是没有什么可以阻止您定义自己的函数来简化此任务，就像我们Node在第一部分中对函数所做的那样。毕竟，z3py 本质上是 Python 库，z3 人员做了很多工作来使其变得更好，但您也可以使用 Python 的全部功能来简化您的生活。事实上，其他语言（Scala、Haskell、O'Caml 等）的 z3 的许多其他接口正是这样做的，以便使用各自宿主语言的功能提供更容易使用的 API。