Z3，创建数据structure/class，使用数据类型

Question

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

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 文档中使用的术语可能与 OO 编程语言中常用的术语（如 Java、Python）略有不同？我真的很难掌握一些术语和例子...

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

Answer 1

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

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

Answer 2

数据类型是一种可以有多个构造函数的结构：像树（叶或分支），或列表（nil，或 cons），或任何其他一般树状结构。

根据您的描述，您似乎实际上不需要数据类型，而是直接记录值。（术语令人困惑。OO 人称之为数据类型的东西大部分时间只是一个 struct/record，而函数式编程或 SMT 人称之为数据类型的东西要丰富得多，有许多像列表一样递归的构造函数。这是不幸的是，但是你学过一次并且很容易记住的东西。）

显然，没有一种适合所有人的尺寸；而且您的问题描述相当模糊。但我猜你想表示一些 Variable 的概念，它具有关联的固定名称、大小和某种初始化字段。您想要的只是一个 Python class ，您可以在其中依靠灵活的类型将其用作具体变量，或用作 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)

我使用 class 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>

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

希望对您有所帮助！

Z3，创建数据structure/class，使用数据类型

Z3, create data structure/class, using Datatype

python

arrays

data-structures

z3

z3py