时间戳

首页 > 解决方案 > Creating variables, pairs, and sets in Z3Py

z3 - Creating variables, pairs, and sets in Z3Py

问题描述

this is a three part question on the use of the Python API to Z3 (Z3Py).

  1. I thought I knew the difference between a constant and a variable but apparently not. I was thinking I could declare a sort and instantiate a variable of that sort as follows:

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

    But python throws an exception saying that you can't "call Node". The only thing that seems to work is to declare n1 a constant

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

    but I'm baffled at this since I would think that a1,a2,a3 are the constants. Perhaps n1 is a symbolic constant, but how would I declare an actual variable?

  2. How to create a constant set? I tried starting with an empty set and adding to it but that doesn't work

    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)])

    But this doesn't work Z3 returns no solution. On the other hand replacing the 3rd line with

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

    is now too permissive, allowing Z3 to interpret nodes as any set of nodes that's needed to satisfy the formula. How do I create just the set {a1}?

  3. Is there an easy way to create pairs, other than having to go through the datatype declaration which seems a bit cumbersome? eg

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

标签： z3z3py

解决方案

声明枚举

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)

这将创建 set {a1, a2}。

作为一个经验法则，API 试图始终保持功能性，即不对现有变量进行破坏性更新，而是您可以从旧值中创建新值。

使用对

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

推荐阅读