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

[Aina Niemetz]

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
>     >
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 488 bytes
Desc: OpenPGP digital signature
URL: </pipermail/smt-comp/attachments/20190601/7e1cdb9a/attachment.asc>