[SMT-LIB] new bitvector theories/logics

[Domagoj Babic]

Hi Clark,

> that operators like bvredor and bvredand are quite simple to synthesize once
> you have bvcomp, but it's also trivial for an implementation system to treat
> them as macros, so I don't see this as a real disadvantage.

Ok, as you wish.



I've updated sf2smt and smt2sf tools. Please try to translate the
benchmarks, and
let me know if there are any problems.

BTW, I found that bvcomp is not as useful as I hoped it to be, because
it solves only
one problem: a <=> (b <=> c), while for other cases, like (a <=> (b =>
c)), I still
need to hack conversion from bool to bv1, and the other way around.
So, at the end,
I left the conversion as I initially wrote it...

Domagoj Babic