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

[Clark Barrett]

That is a good point Trevor.  We should consider allowing concat operators
to take more than two arguments as well.

-Clark


On Sun, Jun 2, 2019 at 7:06 PM Trevor Hansen <trev_abroad at yahoo.com> wrote:

> Thanks for the explanation Clarke,
>
> Not related to this year's competition. But is it correct that concat is
> the only associative operation in QF_BV that doesn't allow >2 operands?
>
> cvc4, boolector, and z3, all parse 3-operand concat. But Mathsat and STP
> don't.
>
> (set-info :smt-lib-version 2.6)
> (set-logic QF_BV)
> (declare-fun x () (_ BitVec 3))
> (declare-fun y () (_ BitVec 3))
> (declare-fun z () (_ BitVec 3))
> (assert (= (concat x y z  )  (_ bv0 9) ) )
> (check-sat)
>
> Thanks again,
> Trev.
>
>
> On Sun, Jun 2, 2019 at 1:23 PM Clark Barrett <barrett at cs.stanford.edu>
> wrote:
>
>> 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
>> >
>> _______________________________________________
>> SMT-COMP mailing list
>> SMT-COMP at cs.nyu.edu
>> https://cs.nyu.edu/mailman/listinfo/smt-comp
>>
>