【发布时间】：2021-09-07 17:32:45
【问题描述】：
我目前正在为一小部分 Python 构建一个符号执行引擎。这个子集支持的最复杂的数据结构是任意嵌套的元组，也就是说，你可以写像x = (1, 2, (3, 4), 5)这样的东西。在我的 SE 引擎中，所有值都表示为 z3 对象。昨天，我尝试在 z3 中为这些嵌套元组建模时遇到了很困难的事情。
我尝试了什么：
- 数组。问题：数组就是数组，也就是说，它们跨越一个矩形空间，这不适合我的元组。
- 序列。我喜欢序列数据类型；但是，它不支持嵌套。例如，你不能写
z3.Concat(z3.Unit(z3.IntVal(1)), z3.Unit(z3.Concat(z3.Unit(z3.IntVal(2)), z3.Unit(z3.IntVal(3)))))，这会引发z3.z3types.Z3Exception: b"Sort of function 'seq.++' does not match the declared type. Given domain: (Seq Int) (Seq (Seq Int))" - 列表。然而，列表只有一个类型
T，我只能将其实例化为List或，例如Int。据我所知，z3 中没有联合类型或通用超级排序之类的东西。 - 未解释的函数。我认为应该可以引入带有排序
Tuple的函数tuple，甚至为不同的参数长度和排序重载它。但是，我不知道如何提取tuple(1, 2, 3)的元素，因为该表达式不是递归定义的。
我会感谢 z3 / SMT 专家的帮助！
提前非常感谢！
元组数据类型：“抽象”索引和元组的问题
我还尝试了@alias 提出的想法，为元组定义数据类型。这工作得很好，但有一个问题：如果元组或索引不是具体的，即是（包含）变量的（表达式），我如何对元组元素的访问进行建模？
例如，我可以将 2 元组的整数定义为：
Tup_II = z3.Datatype('Tuple_II')
Tup_II.declare('tuple', ('fst', z3.IntSort()), ('snd', z3.IntSort()))
Tup_II = Tup_II.create()
a_tuple = Tup_II.tuple(z3.IntVal(1), z3.IntVal(2))
print(a_tuple) # tuple(1, 2)
tuple_concrete_access = z3.simplify(Tup_II.fst(a_tuple))
print(tuple_concrete_access) # 1
没关系。我还可以通过嵌入 Tup_II 数据类型在顶部定义嵌套元组：
Tup_IT = z3.Datatype('Tuple_IT')
Tup_IT.declare('tuple', ('fst', z3.IntSort()), ('snd', Tup_II))
Tup_IT = Tup_IT.create()
another_tuple = Tup_IT.tuple(z3.IntVal(0), a_tuple)
print(another_tuple) # tuple(0, tuple(1, 2))
但是要访问一个元素，我需要知道索引是 0 还是 1 才能选择正确的访问器 (fst, snd) .
我试图从序列类型的行为中获得灵感：
int_seq = z3.Concat(z3.Unit(z3.IntVal(1)), z3.Unit(z3.IntVal(2)))
print(int_seq) # Concat(Unit(1), Unit(2))
concrete_access = z3.simplify(int_seq[z3.IntVal(0)])
print(concrete_access) # 1
concrete_access_2 = z3.simplify(int_seq[z3.IntVal(2)])
x = z3.Int("x")
abstract_access = z3.simplify(int_seq[x])
print(abstract_access)
# If(And(x >= 0, Not(2 <= x)),
# seq.nth_i(Concat(Unit(1), Unit(2)), x),
# seq.nth_u(Concat(Unit(1), Unit(2)), x))
所以一个想法是定义一个Tuple_II.nth 函数。但是，如果我们有一个像 Tup_IT 这样由不同类型的元素组成的元组，我该如何定义这个函数的目标域呢？例如，
target_sort = # ???
tup_IT_nth = z3.Function("Tuple_IT.nth", z3.IntSort(), Tup_II, target_sort)
因此，我需要某种超级类型的int 和Tup_II：与列表相同的问题。
有什么想法吗？ :)
我想要的：创建元组类型的实用函数
只是假设我可以解决getter函数的排序问题；然后我写了一个很好的实用函数，创建了在存在抽象索引的情况下处理元组所需的所有东西：
def create_tuple_type(*sorts: z3.SortRef) -> \
Tuple[z3.Datatype, Dict[int, z3.FuncDeclRef], z3.FuncDeclRef, z3.BoolRef]:
"""
DOES NOT YET WORK WITH NESTED TUPLES!
Example:
>>> tuple_II, accessors, getter, axioms = create_tuple_type(z3.IntSort(), z3.IntSort())
>>>
>>> a_tuple = tuple_II.tuple(z3.IntVal(1), z3.IntVal(2))
>>>
>>> print(z3.simplify(accessors[0](a_tuple))) # 1
>>> print(z3.simplify(getter(a_tuple, z3.IntVal(0)))) # Tuple_II.nth(tuple(1, 2), 0)
>>>
>>> s = z3.Solver()
>>> s.set("timeout", 1000)
>>> s.add(z3.Not(z3.Implies(axioms, z3.IntVal(1) == getter(a_tuple, z3.IntVal(0)))))
>>> assert s.check() == z3.unsat # proved!
>>>
>>> s = z3.Solver()
>>> s.set("timeout", 1000)
>>> s.add(z3.Not(z3.Implies(axioms, z3.IntVal(0) == getter(a_tuple, z3.IntVal(0)))))
>>> assert s.check() == z3.unknown # not proved!
:param sorts: The argument sorts for the tuple type
:return: The new tuple type along with
accessor functions,
a generic accessor function,
and axioms for the generic accessor
"""
dt_name = "Tuple_" + "".join([str(sort)[0] for sort in sorts])
datatype = z3.Datatype(dt_name)
datatype.declare('tuple', *{f"get_{i}": sort for i, sort in enumerate(sorts)}.items())
datatype = datatype.create()
accessors = {i: getattr(datatype, f"get_{i}") for i in range(len(sorts))}
target_sort = z3.IntSort() # ??? <-- What to do here?
get = z3.Function(f"{dt_name}.nth", datatype, z3.IntSort(), target_sort)
get_in_range = z3.Function(f"{dt_name}.nth_i", datatype, z3.IntSort(), target_sort)
get_not_in_range = z3.Function(f"{dt_name}.nth_u", datatype, z3.IntSort(), target_sort)
x = z3.Int("x")
t = z3.Const("t", datatype)
axiom_1 = z3.ForAll(
[t, x],
get(t, x) == z3.If(
z3.And(x >= z3.IntVal(0), x < z3.IntVal(len(sorts))),
get_in_range(t, x),
get_not_in_range(t, x)
)
)
axiom_2 = None
for idx in range(len(sorts)):
axiom = get_in_range(t, z3.IntVal(idx)) == accessors[idx](t)
if axiom_2 is None:
axiom_2 = axiom
continue
axiom_2 = z3.And(axiom_2, axiom)
axiom_2 = z3.ForAll([t], axiom_2)
return datatype, accessors, get, z3.And(axiom_1, axiom_2)
问题在于target_sort 的声明与# ??? <-- What to do here? 注释。
【问题讨论】：
标签： tuples z3 smt z3py smt-lib