diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-04-16 12:11:37 -0700 |
---|---|---|
committer | Mathias Preiner <mathias.preiner@gmail.com> | 2019-04-16 12:11:37 -0700 |
commit | 2f7131c81078a964a4043ef79186cdcf91951974 (patch) | |
tree | 14fe132462c8be51f19578448033acd3f08b7eff /src/parser/smt2/smt2.h | |
parent | a47b722aa31cdd036f83425b2a805e6a572a974b (diff) |
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)
Diffstat (limited to 'src/parser/smt2/smt2.h')
-rw-r--r-- | src/parser/smt2/smt2.h | 20 |
1 files changed, 15 insertions, 5 deletions
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 171642c7e..7a3c3b0c3 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -319,15 +319,25 @@ private: // that CVC4 permits as N-ary but the standard requires is binary if(strictModeEnabled()) { switch(kind) { - case kind::BITVECTOR_CONCAT: case kind::BITVECTOR_AND: - case kind::BITVECTOR_OR: - case kind::BITVECTOR_XOR: case kind::BITVECTOR_MULT: + case kind::BITVECTOR_OR: case kind::BITVECTOR_PLUS: + case kind::BITVECTOR_XOR: + if (numArgs != 2 && !v2_6()) + { + parseError( + "Operator requires exactly 2 arguments in strict SMT-LIB " + "compliance mode (for versions <2.6): " + + kindToString(kind)); + } + break; + case kind::BITVECTOR_CONCAT: if(numArgs != 2) { - parseError("Operator requires exact 2 arguments in strict SMT-LIB " - "compliance mode: " + kindToString(kind)); + parseError( + "Operator requires exactly 2 arguments in strict SMT-LIB " + "compliance mode: " + + kindToString(kind)); } break; default: |