[SMT-LIB] new bitvector theories/logics

[Clark Barrett]

> I checked the operators. bvcomp is very useful, because it will allow me
> to simplify my sf2smt translator.

Great.

> 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.

The rationale is that these operators exist in high-level languages like
verilog and so it makes it easier for someone to translate to our language if
we support the same set of operators.  We want to make it as easy as possible
for people to create benchmarks in the language (and we want the benchmarks to
capture as closely as possible the original setting of the problem).  It's true
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.

As for performance and CSE, I think this is more of an implementation issue
rather than a logical issue.  I would expect that people implementing bitvector
systems would compile down to a small set of core operators for performance
reasons, but I don't think it's necessary to choose a particular set of core
operators at the logical level.