diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-09-25 18:08:08 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-25 18:08:08 -0700 |
| commit | 160a3f55bf4dbfdbc1385ce4898c62b1fd3a8c78 (patch) | |
| tree | 3f56f693cf842a099911ec9cb3bedbda688d4951 | |
| parent | c59345b93b2ecf3552f5205b312c262a1ae5eab8 (diff) | |
Restrict bvxnor to only allow two operands (was n-ary). (#5138)
Bit-vector operator bvxnor was previously mistakenly marked as
left-assoicative in SMT-LIB. This has recently been corrected in
SMT-LIB. We now restrict bvxnor to only allow two operands in order to
avoid confusion about the semantics, since the behavior of n-ary
operands to bvxnor is now undefined in SMT-LIB.
| -rw-r--r-- | NEWS | 5 | ||||
| -rw-r--r-- | src/api/cvc4cpp.cpp | 2 | ||||
| -rw-r--r-- | test/regress/regress0/parser/bv_arity_smt2.6.smt2 | 3 |
3 files changed, 7 insertions, 3 deletions
@@ -29,6 +29,11 @@ Changes: SMT-LIB 2.6 semantics. * The `competition` build type includes the dependencies used for SMT-COMP by default. Note that this makes this build type produce GPL-licensed binaries. +* Bit-vector operator bvxnor was previously mistakenly marked as + left-assoicative in SMT-LIB. This has recently been corrected in SMT-LIB. We + now restrict bvxnor to only allow two operands in order to avoid confusion + about the semantics, since the behavior of n-ary operands to bvxnor is now + undefined in SMT-LIB. Changes since 1.7 diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 08beec35a..6ed8855e4 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -3145,7 +3145,7 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const if (echildren.size() > 2) { if (kind == INTS_DIVISION || kind == XOR || kind == MINUS - || kind == DIVISION || kind == BITVECTOR_XNOR || kind == HO_APPLY) + || kind == DIVISION || kind == HO_APPLY) { // left-associative, but CVC4 internally only supports 2 args res = d_exprMgr->mkLeftAssociative(k, echildren); diff --git a/test/regress/regress0/parser/bv_arity_smt2.6.smt2 b/test/regress/regress0/parser/bv_arity_smt2.6.smt2 index 437d80f56..c8b159f3b 100644 --- a/test/regress/regress0/parser/bv_arity_smt2.6.smt2 +++ b/test/regress/regress0/parser/bv_arity_smt2.6.smt2 @@ -8,6 +8,5 @@ (not (= (bvmul x y z) (bvmul (bvmul x y) z))) (not (= (bvand x y z) (bvand (bvand x y) z))) (not (= (bvor x y z) (bvor (bvor x y) z))) - (not (= (bvxor x y z) (bvxor (bvxor x y) z))) - (not (= (bvxnor x y z) (bvxnor (bvxnor x y) z))))) + (not (= (bvxor x y z) (bvxor (bvxor x y) z))))) (check-sat) |