[SMT-LIB] consider inclusion of exponentiation in FixedSizeBitVectors

[Levent Erkok]

I would like this as well. Currently, in the Haskell interface for SMTLib,
I'm using a repeated squaring of the base and the bit-blasting of the
exponent technique: For each set bit in the exponent, you iterate the
squaring of the base according to its position and multiply all those
factors. While this works and is relatively easy to write in Haskell (
https://github.com/LeventErkok/sbv/blob/master/Data/SBV/BitVectors/Model.hs#L549-L556),
it generates rather long terms with lots of multiplication. (Though no
axiomatization is needed, it comes out as a chain of "ite" calls and
multiplies.) It would be nice if solvers naively supported it.

-Levent.

On Wed, Apr 5, 2017 at 12:48 AM, Florian Schanda <florian.schanda at altran.com
> wrote:

> On Wednesday 05 Apr 2017 07:04:38 Yannick Moy wrote:
> > Is it planned to include exponentiation in FixedSizeBitVectors theory?
> > Currently, we're using an uninterpreted function with an axiomatization
> for
> > it, which leads to poor performance (typically all such goals end up not
> > being proved). It seems that provers that support FixedSizeBitVectors
> > natively could also support exponentiation.
>
> We've actually had support for this in Riposte, but it was fairly slow.
> Martin, can you remember how we did this?
>
> But yeah, I'd like to +1 this, it would be good for SPARK 2014.
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>