Z3，创建数据结构/类，使用 Datatype

Question

也许创建一个包含与以下 Python 类相同信息的数据结构。

class Variable:
    def __init__(self):
        self.name = "v1"  #str
        self.size = 10    #int
        self.initialized = True    #bool

拥有三个不同类型的不同字段。

如果字段类型相同，例如“str”，我可以使用z3.Array('a', StringSort(), StringSort())。有点像映射一样使用它。

在python代码中显示的字段类型不同的情况下，我该怎么办？

我查看了Datatype，并阅读了 z3py 指南中关于他们如何创建List 的示例。但是，我无法完全理解到底发生了什么。我认为 z3 文档中使用的术语可能与 Java、Python 等 OO 编程语言中常用的术语略有不同？我很难掌握一些术语和示例...

*** 更棘手的部分，如何将这种变量存储在 z3 数组中？ 比如我想在一个大小> 10的数组中找到一个变量对象的索引，使用z3约束求解。

Answer 1

数据类型是一种可以具有多个构造函数的结构：例如树（叶子或分支），或列表（nil 或 cons），或任何其他通常类似于树的结构。

从您的描述看来，您实际上并不想要一个数据类型，而是一个直接的记录值。 （术语令人困惑。OO人们称之为数据类型的东西大多数时候只是一个结构/记录，而函数式编程或SMT人们称之为数据类型的东西更丰富，有许多像列表一样递归的构造函数。这很不幸，但是你学过一次就很容易记住的东西。）

显然，没有一种尺寸适合所有人；而且您的问题描述相当模糊。但我猜你想代表Variable 的一些概念，它具有关联的固定名称、大小和某种类型的初始化字段。您想要的只是一个 Python 类，您可以在其中依靠灵活的类型将其用作具体变量或 z3 可以操作的符号变量。基于此，我倾向于像这样编写您的问题：

from z3 import *

class Variable:
    def __init__(self, nm):
        self.name        = nm
        self.size        = Int(nm + '_size')
        self.initialized = Bool(nm + '_initialized')

    def __str__(self):
        return "<Name: %s, Size: %s, Initialized: %s>" % (self.name, self.size, self.initialized)

# Helper function to grab a variable from a z3 model
def getVar(m, v):
    var             = Variable(v.name)
    var.size        = m[v.size]
    var.initialized = m[v.initialized]
    return var

# Declare a few vars
myVar1 = Variable('myVar1')
myVar2 = Variable('myVar2')

# Add some constraints
s = Solver()

s.add(myVar1.size == 12)
s.add(myVar2.initialized == True);
s.add(myVar1.size > myVar2.size)
s.add(myVar1.initialized == Not(myVar2.initialized))

# Get a satisfying model
if s.check() == sat:
    m = s.model()
    print getVar(m, myVar1)
    print getVar(m, myVar2)

我使用 Variable 类来表示一个常规值，就像在 Python 中一样，也可以存储符号大小（通过 Int(nm + '_size')）和符号初始化信息（通过 Bool(nm + '_initialized')）。语法可能看起来有点混乱，但如果你通过程序，我相信你会看到逻辑。函数getVar 是一个助手，用于在调用check 后获取这些变量之一的值，以访问模型值。

我在程序中添加了一些约束以使其变得有趣；显然，这是您将编写原始问题的部分。当我运行这个程序时，我得到：

$ python a.py
<Name: myVar1, Size: 12, Initialized: False>
<Name: myVar2, Size: 11, Initialized: True>

这给了我一个很好的模型来满足我指定的所有约束。

希望有帮助！

Answer 2

我的情况和你一样，但我会尽力回答你的问题。

I could just use z3.Array('a', StringSort(), StringSort()). What do I do in this kind of situation?

是的，您应该实现它，但请记住，Z3（和 SMT 中）中的数组是无限大小的，如果您想要一个固定数组，您可以：

vec = IntVector('vec', 10)

尊重你的另一个问题，我和你的情况类似，因为我在正确理解 Z3 方面遇到了很多困难。如果您在 Haskell 中工作，我会调整列表（尝试做更多的理解）

def funList(sort):
    List = Datatype('List')
    #Constructor insert: (Int, List) -> List
    List.declare('insert', ('head', sort), ('tail', List)) 
    List.declare('nil') #declaración de nil, así permito la opción de tener una lista vacía
    return List.create() #creo la lista