z3、z3py：是否可以从本质上减少 Function 的搜索空间？答案

【问题标题】：z3, z3py: Is it possible to intrinsically reduce the search space of Function?z3、z3py：是否可以从本质上减少 Function 的搜索空间？
【发布时间】：2015-09-02 15:52:05
【问题描述】：

我在推断一个 Function(var1)，我只关心这个函数的值，当 0

约束函数搜索空间的一种常用方法（我猜）类似于断言约束，例如（在 z3py 中）：

for i in range(11):
  solver.add(And(Function(i)>=0,Function(i)<=10))

我的问题是：有没有更好的方法可以限制函数的搜索空间？类似于设置这个函数的上限/下限？

我的直觉是：由于我对这个函数有很多其他的约束，我觉得如果我能自然地约束函数的搜索空间，许多不可能的赋值可能会被求解器自动避免，并且花费在推理可能会减少。我不确定这是否有意义。

【问题讨论】：

标签： z3 smt z3py

【解决方案1】：

Z3 只支持简单类型。您基本上是在使用属性来限制您的功能。您可以使用量化的断言对其进行编码。那是，断言

   ForAll([x], Implies(And(0 <= x, x <= 10), And(0 <= F(x), F(x) <= 10)))

每次出现 F 时都会实例化量词，而不是每次出现 F 的域中的值。如果您的域很大并且出现次数很少，这将很有帮助。另一方面，如果 F 在许多地方使用（也是在搜索期间实例化其他量词的结果），那么预先说明边界会更便宜。

【讨论】：

是的，看来只有这两种方法可以实现我的目标。我正在我的项目中实施无量词，因为它更便宜。谢谢，尼古拉！

【解决方案2】：

我想到的一种方法是，我们可以通过将“IntSort”替换为“BitVecSort”作为输入和输出的排序来限制函数的域和范围。

假设我知道域是 [0,8] 并且范围是 [0,127]。然后我们可以将函数定义为

F = Function('F',BitVecSort(3),BitVecSort(7))

【讨论】：