interpretation [3,2]. For the purpose of the memo we assume a xed bit-with w 2 N+. A bit vector variable is seen as an integer variable with possible values 0::(2w 1). Addition a +w b is de ned as (a + b) mod 2w. Two types of comparisons are de ned: unsigned a u b and signed a s b. The unsigned is standard integer comparison, i.e., a u b , a b. The signed uses the two's complement representation for signed numbers. Hence, we have a s b , s(a) s(b), where s(a) , a < 2w 1 ? a : a 2w. Consider a conjunction V1::m :(ai bi) ^ Vm+1::n(ai bi), where ai bi is one of the following forms with x a bit-vector variable and c1; c2 constants.
2. c1 3. c1 +w x 4. x s c1 5. c1 s x 1. c1 +w x u c2 +w x u c2 +w x
u c2
Problem: Decide whether the input has a solution and if it has, determine if it is unique.
We show that every constraint of the form above can be represented as a positive or negative interval constraint. We write [a ; b] and v[a ; b] for the positive and negative interval ranging from a to b inclusively, respectively. Hence, [a ; b] for 0 a; b < 2w denotes the set of values from a to b and v[a ; b] the values v with (0 v < a) _ (b < v < 2w). Observe that [a ; b] [ v[a ; b] = [0 ; 2w 1]. For a > b, it holds that [a ; b] = ; and v[a ; b] = [0 ; 2w 1]. 1 The algorithm is a generalization of a standard solution to \The Interval Point Cover Problem".
Algorithm 1: Compute bounds
input : Set of intervals I 1 P f[a ; b] j [a ; b] 2 Ig 2 l P = ; ? 0 : min fa j [a ; b] 2 P g 3 h P = ; ? 2w 1 : max fb j [a ; b] 2 P g 4 N fv[a ; b] j v[a ; b] 2 Ig 5 N sort N by rst element 6 p; l0; h0 l; l; l 1 7 for v[a ; b] 2 N [ v[2w ; 2w] do 8 if p > h then break 9 if b < p then continue 10 if p < a then 11 if h0 > l0 then l0 p 12 h0 a 1 13 p 3.1 Implementation and Redundancies Algorithm 1 can be implemented in a straightforward fashion. Positive intervals do not need to be explicitly stored. Rather, we maintain a lower and upper bound L and U , respectively. These are updated with every new positive interval. These bounds let us also simplify negative intervals. An interval v[a ; b] with a L is simpli ed to [b + 1 ; 2w 1]. Analogously, v[a ; b] with b u is simpli ed to [0 ; a 1].
Maintaining the upper and lower bounds lets us quickly detect if a new interval is redundant. A positive interval [a ; b] is redundant if L a ^ b U and a negative interval v[a ; b] is redundant if a > U _ b < L. Note that such detection of redundancies depends on the order of processing the intervals. 4
To measure the e ect of the individual simpli cations we construct several
examples. (
We generated 100 random instances for 32-bit numbers for each example and applied the standard bit-blasting technique in Z3 on them. Table 2 overviews the number of con icts in the SAT solver.
Examples (
The comparison shows that the biggest saving are in the case of unsatis able constraints and constraints that lead to unique solution. In the case of redundant intervals, however, the results do not indicate improvement. 5
This memo shows how a system of inequalities over one variable and no multiplication can be represented as a set of positive and negative intervals. Naturally, such intervals are closed under negation, admit a polynomial satis ability check and check for solution uniqueness. Preliminary evaluation suggests that such analysis enables signi cant speedups. In the future we plan to integrate this analysis into Z3 and investigate how could improve bit-vector solving by approximating solutions as intervals.