z3 - 在 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 不返回任何解决方案。另一方面，将第 3 行替换为

   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 函数不会修改 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 接口(interface)正是这样做的，以提供更容易使用各自宿主语言特性的 API。