z3，z3py:是否有可能从本质上减少函数的搜索空间？
提问于 2015-09-02 07:52:05
我在推断一个函数( var1 )，我只关心当0 <= var1 <= 10和0 <= var <= 10，0 <= Function(var1) <= 10时这个函数的值。
约束函数搜索空间的一种常见方法(我猜)是类似于断言约束的方法，比如(在z3py中)：
for i in range(11):
solver.add(And(Function(i)>=0,Function(i)<=10))我的问题是:是否有更好的方法来限制函数的搜索空间？类似于自然设置这个函数的上/下界之类的东西？
我的直觉是:由于我对这个函数有很多其他的限制，我觉得如果我能自然地约束函数的搜索空间，那么求解者就可以自动避免许多不可能的分配，并且可以减少在推理上花费的时间。我不知道这是否有道理。
回答 2
Stack Overflow用户
回答已采纳
发布于 2015-09-07 19:34:53
Z3只支持简单类型。您基本上是在使用属性约束您的函数。您可以使用量化的断言对其进行编码。也就是说，断言
ForAll([x], Implies(And(0 <= x, x <= 10), And(0 <= F(x), F(x) <= 10)))对于F的每一次出现，都会实例化量词，而不是F域中的每个值。如果您的域很大，并且出现的次数很少，这将非常有帮助。另一方面，如果F在许多地方被使用(也是在搜索过程中实例化其他量词的结果)，那么预先说明界限将更便宜。
Stack Overflow用户
发布于 2015-09-29 12:16:25
我想到的一种方法是，我们可以通过将"IntSort“替换为"BitVecSort”作为输入和输出的排序来限制函数的域和范围。
假设我知道域是0,8，范围是0,127。然后我们可以将函数定义为
F = Function('F',BitVecSort(3),BitVecSort(7))页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/32357690
复制相关文章
点击加载更多
腾讯云开发者
