[SMT-LIB] consider inclusion of exponentiation in FixedSizeBitVectors

[Clark Barrett]

This seems like a reasonable suggestion.  If we add it, would any of you be
willing/able to provide a set of benchmarks using the new operator?

-Clark

On Wed, Apr 5, 2017 at 6:54 AM, Levent Erkok <erkokl at gmail.com> wrote:

> 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
> >
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>