I am building an inference engine that uses interval analysis to compute variable bounds. Efficiency is very important in my case:
- I cannot use SMT solvers
- I cannot afford full enumeration, since real programs may contain variables with large domains.
So far I am using a classic interval domain — but I am running into precision issues.
Example:
Assume: a*(a - 1) = 0 and b*(b - 1) = 0 ⇒ a, b ∈ {0,1}
Now consider:
out = (a + b) - a*bThe exact range ofoutis{0,1}, but interval analysis gives:
a + b ∈ [0,2] a * b ∈ [0,1] out ∈ [0,2] - [0,1] = [-1,2] The problem is that the analysis does not track how the values of a + b and a * b are correlated.
Could you please refer to techniques that could help me fix this problem in a way almost as cheap as plain intervals?
Is there perhaps a lightweight relational domain that is commonly used to keep such correlations and recover the tight [0,1] without sacrificing performance?
Or is that simply not possible without stepping into more expensive domains like octagons or polyhedra?
Any tips or references would be very helpful!
