在 Z3Py 中创建变量、对和集合

Question

这是一个关于使用 Python API 到 Z3 (Z3Py) 的三部分问题。

我以为我知道常量和变量之间的区别，但显然不是。我在想我可以声明一种类型并实例化这种类型的变量，如下所示：
```
Node, (a1,a2,a3) = EnumSort('Node', ['a1','a2','a3'])
n1 = Node('n1') # c.f. x = Int('x')
```
但是 python 抛出一个异常说你不能 "call Node"。唯一似乎有效的方法是声明 n1 一个常量
```
Node, (a1,a2,a3) = EnumSort('Node', ['a1','a2','a3'])
n1 = Const('n1',Node)
```
但我对此感到困惑，因为我认为 a1、a2、a3 是常量。也许 n1 是一个符号常量，但我将如何声明一个实际变量？
如何创建常量集？我尝试从一个空集开始并添加到它，但这不起作用
```
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这个不行returns无解。另一方面用
替换第 3 行
```
nodes = Const('nodes',SetSort(Node))
```
现在过于宽松，允许 Z3 将节点解释为满足公式所需的任何节点集。如何只创建集合 {a1}?
除了必须通过看起来有点麻烦的数据类型声明之外，是否有一种简单的方法来创建对？例如
```
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 不会修改 set 参数。它只是创建一个新的。所以，只需给它一个名字并像这样使用它：

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 使用其各自宿主语言的功能.

在 Z3Py 中创建变量、对和集合

Creating variables, pairs, and sets in Z3Py

z3

z3py

声明枚举

插入集合

结对工作