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

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())。在这种情况下我该怎么办？

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

Answer 1

我的处境和您一样，但我会尽力回答您的问题。

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

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

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