z3, z3py: 是否可以从本质上减少函数的搜索 space？
z3, z3py: Is it possible to intrinsically reduce the search space of Function?
我正在推断一个函数 (var1)，我只关心当 0 <= var1 <= 10 时这个函数的值，我知道，当 0 <= var <= 10, 0 <= Function(var1 ) <= 10.
限制函数搜索 space 的一种常见方法（我猜）类似于断言约束，例如（在 z3py 中）：
for i in range(11):
solver.add(And(Function(i)>=0,Function(i)<=10))
我的问题是：有没有更好的方法来限制函数的搜索space？像设置这个函数的 upperbound/lowerbound 一样吗？
我的直觉是：因为我对这个函数有很多其他约束，我觉得如果我能从本质上约束函数的搜索 space，求解器可能会自动避免许多不可能的赋值，推理所花费的时间可能会减少。我不确定这是否有意义。
Z3 只支持简单类型。您基本上是使用 属性 来限制您的功能。您可以使用量化断言对此进行编码。那是，
断言
ForAll([x], Implies(And(0 <= x, x <= 10), And(0 <= F(x), F(x) <= 10)))
每次出现 F 都会实例化量词，而不是每次出现
F 域中的值。如果您的域很大且出现次数很少，这将有很大帮助。另一方面，如果 F 在许多地方使用（也是在搜索过程中实例化其他量词的结果），那么预先说明界限会更便宜。
我想到的一种方法是，我们可以通过将 "IntSort" 作为输入和输出的排序替换为 "BitVecSort" 来限制函数的域和范围。
假设我知道域是[0,8]，范围是[0,127]。然后我们可以将函数定义为
F = Function('F',BitVecSort(3),BitVecSort(7))
我正在推断一个函数 (var1)，我只关心当 0 <= var1 <= 10 时这个函数的值，我知道，当 0 <= var <= 10, 0 <= Function(var1 ) <= 10.
限制函数搜索 space 的一种常见方法（我猜）类似于断言约束，例如（在 z3py 中）：
for i in range(11):
solver.add(And(Function(i)>=0,Function(i)<=10))
我的问题是：有没有更好的方法来限制函数的搜索space？像设置这个函数的 upperbound/lowerbound 一样吗？
我的直觉是：因为我对这个函数有很多其他约束，我觉得如果我能从本质上约束函数的搜索 space，求解器可能会自动避免许多不可能的赋值，推理所花费的时间可能会减少。我不确定这是否有意义。
Z3 只支持简单类型。您基本上是使用 属性 来限制您的功能。您可以使用量化断言对此进行编码。那是， 断言
ForAll([x], Implies(And(0 <= x, x <= 10), And(0 <= F(x), F(x) <= 10)))
每次出现 F 都会实例化量词，而不是每次出现 F 域中的值。如果您的域很大且出现次数很少，这将有很大帮助。另一方面，如果 F 在许多地方使用（也是在搜索过程中实例化其他量词的结果），那么预先说明界限会更便宜。
我想到的一种方法是，我们可以通过将 "IntSort" 作为输入和输出的排序替换为 "BitVecSort" 来限制函数的域和范围。
假设我知道域是[0,8]，范围是[0,127]。然后我们可以将函数定义为
F = Function('F',BitVecSort(3),BitVecSort(7))