如何在Z3中声明混合数据类型的数组？
我正在使用 z3 的 python API，我的目标是能够推理包含两种数据之一的序列： 整数或我的自定义数据类型，除了类型之外没有任何属性。我读到有关“DeclareSort”的内容，这似乎意味着我们可以创建自定义类型。所以我按如下方式使用它：
ct = DeclareSort('CT')
CT = Const('CT', ct)
然后我尝试在我的类型和整数之间创建一个联合类型，如下所示：
u = Datatype('IntOrCT')
u.declare('IntV', ('int', IntSort()))
u.declare('CTV', ('ct', ct))
IntOrCT = u.create()
CTV = IntOrCT.CTV
IntV = IntOrCT.IntV
我现在尝试在数组中使用它们。但是，我无法将任何整数添加到数组中并得到： z3.z3types.Z3Exception: Z3 expression Expected
# X = Array('x', IntOrCT, IntOrCT)
# Store(X, 0, 4)
如果我将 IntOrCT 更改为 IntSort()，它将起作用。是否知道代码中可能缺少什么？或者我想在 z3 中做不到的事情？
I am using the python API for z3 and my goal is to be able to reason about sequences containing one of two kinds of data:
either an integer or my custom data type, which does not have any properties other than being a type. I read about 'DeclareSort' which seems to mean we can create a custom type. So I used it as follows:
ct = DeclareSort('CT')
CT = Const('CT', ct)
Then I tried to create a union type between my type and integers as follows:
u = Datatype('IntOrCT')
u.declare('IntV', ('int', IntSort()))
u.declare('CTV', ('ct', ct))
IntOrCT = u.create()
CTV = IntOrCT.CTV
IntV = IntOrCT.IntV
I am now trying to use them in an array. However, I cannot add any integers to my arrays and get: z3.z3types.Z3Exception: Z3 expression expected
# X = Array('x', IntOrCT, IntOrCT)
# Store(X, 0, 4)
If I change IntOrCT to IntSort(), it will work. Is there any idea what could be missing from the code? or is what I'm trying to do not possible in z3?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
您创建了一个由
IntOrCT索引的数组，存储IntOrCT值；所以你需要将你的索引和值包装在相应的构造函数中：当我运行这个时，我得到：
You created an array indexed by
IntOrCT, storingIntOrCTvalues; so you need to wrap your index and values in the corresponding constructors:When I run this, I get: