Z3，使用dataType创建数据结构/类 [英] Z3, create data structure/class, using Datatype

问题描述

可以创建一个数据结构，该数据结构包含与以下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等面向对象编程语言中常用的术语略有不同？我真的很难掌握其中的一些术语和例子...

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

推荐答案

数据类型是一种可以有多个构造函数的结构：如树(叶子或树枝)、列表(空或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>

这为我提供了一个满足我指定的所有约束的很好的模型。

希望能有所帮助！

这篇关于Z3，使用dataType创建数据结构/类的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！