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.
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?
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 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)))
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.
One way that I think of is that we can probably restrict the domain and range of function by replacing "IntSort" as the sort for input and output with "BitVecSort".
Suppose I know the domain is [0,8] and range is [0,127]. Then we could define function as
F = Function('F',BitVecSort(3),BitVecSort(7))
