[SMT-COMP] Incremental QF_BV, addition with >2 operands
Trevor Hansen
trev_abroad at yahoo.com
Sun Jun 2 22:06:15 EDT 2019
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
>
More information about the SMT-COMP
mailing list