Make bv{add,mul,and,or,xor,xnor} left-associative (#2955)
authorAndres Noetzli <andres.noetzli@gmail.com>
Tue, 16 Apr 2019 19:11:37 +0000 (12:11 -0700)
committerMathias Preiner <mathias.preiner@gmail.com>
Tue, 16 Apr 2019 19:11:37 +0000 (12:11 -0700)
commit2f7131c81078a964a4043ef79186cdcf91951974
tree14fe132462c8be51f19578448033acd3f08b7eff
parenta47b722aa31cdd036f83425b2a805e6a572a974b
Make bv{add,mul,and,or,xor,xnor} left-associative (#2955)

The most recent version of SMT-LIB defines bv{add,mul,and,or,xor,xnor}
[0, 1] as left-associative. CVC4 treats all but bvxnor as having
variable arity anyway but the arity check was too strict when using
`--strict-parsing`.  This commit changes the strict parsing check. For
bvxnor, it adds code to the parser that expands an application of bvxnor
into multiple applications of a binary bvxnor if needed.

References:
[0] http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml (bvand,
bvor, bvadd, bvmul)
[1] http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV (bvxor, bvxnor)
src/parser/smt2/Smt2.g
src/parser/smt2/smt2.h
test/regress/CMakeLists.txt
test/regress/regress0/parser/bv_arity_smt2.6.smt2 [new file with mode: 0644]