|
Adds an option to do "bitwise" comparisons in the lazy IAND solver. Instead of creating an exact match for the value of a term using a sum, this would lazily fix groups of bits using integer extracts (divs and mods) when the abstract and concrete values differ at those bits.
For example, with a 1-bit granularity, you might learn a lemma like:
((_ iand 4) x y), value = 1
actual (2, 3) = 2
bv-value = #b0001
bv-actual (#b0010, #b0011) = #b0010
IAndSolver::Lemma: (let ((_let_1 ((_ iand 4) x y)))
(and (and true
(= (mod _let_1 2) (ite (and (= (mod x 2) 1) (= (mod y 2) 1)) 1 0)))
(= (mod (div _let_1 2) 2) (ite (and (= (mod (div x 2) 2) 1) (= (mod (div y 2) 2) 1)) 1 0))))
; BITWISE_REFINE
which is just forcing the bottom two bits of the iand operator result to implement bitwise-AND semantics.
|
