[SMT-LIB] new bitvector theories/logics

[Domagoj Babic]

Hi,

On 5/11/07, Clark Barrett <barrett at cs.nyu.edu> wrote:
> If you look at the files I posted, you'll see that these operators have already
> been renamed as you suggested.  I would appreciate it if you would take a
> careful look at the summary in QF_BV.smt and let me know if you have any
> additional feedback.

Oops, sorry about missing that. I thought that all the changes were
summarized in your email.

I checked the operators. bvcomp is very useful, because it will allow me
to simplify my sf2smt translator. However, I don't see what's the rationale
behind bvredor and bvredand:

bvredor(x) = bvnot(bvcomp(x, 0))
bvredand(x) = bvcomp(x, -1)

also, bvnand and bvxnor are very trivial to synthetize.

IMHO, the small additional convenience of having these 'syntactic
sugars' does not justify the additional complexity.



I experimented with different encodings in Calysto, and found out that a
small set of operators is much better because it also promotes common
subexpression elimination (CSE). For instance, in SW you can frequently
see cases like:

x = a bvand b
y = bvnot(a bvand b)

One possible encoding is:
x = a bvand b
y = a bvnand b

but it becomes much harder to eliminate the common subexpression. If on
the other hand, you force people to use a minimalistic (but expressive
enough!) set of operators, CSE becomes trivial.

How much does CSE matter?

In some cases a lot:
Try bit-blasting a*b /= b*a. Without CSE, it scales up to 11 bits with a
top-notch solver, on a fast machine. On the other hand, if you run CSE,
you get x=a*b, x /= x, which is solved faster than the clock resolution
even for 64-bit variables - a simple optimization that gives exponential
speedup.

So, I suggest elimination of 'syntactic sugars' in order to simplify the
parsing and to promote CSE.


Regards,
    Domagoj Babic