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

[Clark Barrett]

That's right, because those three operators are not associative.

-Clark


On Sat, Jun 1, 2019 at 7:54 PM Aina Niemetz <aina.niemetz at gmail.com> wrote:

> That's my understanding, yes.
> I actually don't know why this is the case, though.
>
> On 6/1/19 7:46 PM, Trevor Hansen wrote:
> > 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
> > <mailto: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 <mailto:SMT-COMP at cs.nyu.edu>
> >     > https://cs.nyu.edu/mailman/listinfo/smt-comp
> >     >
> >
>
> _______________________________________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/smt-comp
>