[SMT-COMP] Fwd: Incremental QF_BV, addition with >2 operands

[Trevor Hansen]

Thanks Aina,

I didn't notice that.

Am I correct in understanding that bvnand, bvnor and bvcomp each must have
two operands?

Trev.


On Sun, Jun 2, 2019 at 11:47 AM Aina Niemetz <aina.niemetz at gmail.com> wrote:

> Hi Trevor,
>
> since 2017 (SMT-LIB 2.6), bvadd is left-associative, as is bvor, bvand,
> bvmul, bvxor and bvxnor:
>
> http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml
> http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV
>
> So, yes, this is allowed.
>
> Cheers,
> Aina
>
>
> On 6/1/19 6:40 PM, Trevor Hansen wrote:
> > In the incremental QF_BV benchmarks, The
> >
> /20170501-Heizmann-UltimateAutomizer/jain_5_true-unreach-call_true-no-overflow.i.smt2
> > benchmark has additions with >2 operands.
> >
> > For example:
> >
> > (set-info :smt-lib-version 2.6)
> > (set-logic QF_BV)
> > (declare-fun c_main_~x~4 () (_ BitVec 32))
> > (declare-fun c_main_~y~4 () (_ BitVec 32))
> > (assert
> > (distinct
> > (bvadd
> >   c_main_~y~4
> >   c_main_~x~4
> >   (_ bv4294967266 32)
> > )
> > (_ bv0 32)
> > )
> > )
> > (check-sat)
> >
> > This example is parsed and solved by z3, mathsat, boolector, yices2, and
> > cvc4. So addition with >2 operands has wide support.
> >
> > The solvers I'm involved with don't parse it. Although it's easy for me
> to
> > change that.
> >
> > Am I confused, are >2 operands allowed?
> > Even if they are currently not allowed, is the use so widespread they
> > should be allowed?
> >
> > Thanks,
> > Trev.
> > _______________________________________________
> > SMT-COMP mailing list
> > SMT-COMP at cs.nyu.edu
> > https://cs.nyu.edu/mailman/listinfo/smt-comp
> >
>
>