z3、z3py:是否可以从本质上减少Function的搜索空间? [英] z3, z3py: Is it possible to intrinsically reduce the search space of Function?

问题描述

我正在推断一个 Function(var1) 并且我只关心这个函数的值，当 0 <= var1 <= 10 并且我知道，当 0 <= var <= 10, 0 <=函数(var1) <= 10.

I am inferring a Function(var1) and I only care about the values of this function when 0 <= var1 <= 10 and I know, when 0 <= var <= 10, 0 <= Function(var1) <= 10.

(我猜)限制函数搜索空间的一种常见方法是像(在 z3py 中)断言约束一样:

A common way (I guess) to constrain the search space of the Function is something like asserting constraints like (in z3py):

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

我的问题是:有没有更好的方法来限制函数的搜索空间?像设置这个函数的上界/下界一样吗?

My question is that: is there a better way so that I can constrain the search space of Function? Something like setting upperbound/lowerbound of this Function by nature?

我的直觉是:由于我对这个 Function 有很多其他的约束，我觉得如果我能自然地约束 Function 的搜索空间，求解器可能会自动避免许多不可能的分配，并且花费在推断可能会减少.我不确定这是否有意义.

My intuitions are that: since I have a lot other constraints for this Function, I feel like if I could constrain the search space of Function by nature, many impossible assignment might be automatically avoided by the solver, and the time spent on the inference might be reduced. I am not sure if this makes sense.

推荐答案

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

Z3 only supports simple types. You are basically constraining your function using a property. You could encode this using a quantified assertion. That is, assert that

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

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

The quantifier gets instantiated for each occurrence of F, as opposed to each value in the domain of F. This helps a lot if your domain is huge and the number of occurrences is small. On the other hand if F gets used in many places (also as a consequence of instantiating other quantifiers during search), then stating the bounds up front will be cheaper.

这篇关于z3、z3py:是否可以从本质上减少Function的搜索空间?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！