Z3，使用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文档中使用的术语可能与通常在面向对象编程语言中使用的术语略有不同。我真的很难掌握一些术语和例子……
*一个更棘手的部分，如何在z3数组中存储这种变量？例如，我想使用z3约束求解在大小大于10的数组中查找变量对象的索引。
回答 2
Stack Overflow用户
发布于 2020-01-29 00:47:54
数据类型是一种可以具有多个构造函数的结构:如树(叶子或分支)、列表(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>这给了我一个很好的模型，它满足了我指定的所有约束。
希望这能有所帮助！
Stack Overflow用户
发布于 2020-01-28 17:46:20
我的情况和你一样，但我会尽我所能回答你的问题。
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 listahttps://stackoverflow.com/questions/59940869
复制相似问题
腾讯云开发者
