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.

diff --git a/NEWS b/NEWS
index 93a7cc61541eb9233bd777856e74876d32041b52..682b9ce757ba18d564a738480e5fd4245c2ea56d 100644 (file)
--- a/NEWS
+++ b/NEWS
@@ -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 08beec35a6a145806a9f16138a524d7ccdf8f214..6ed8855e4f9355c3d94b67a7ac15f2d0b721f38d 100644 (file)
--- 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 437d80f5692af21d5e682e3b9154e8dde65be3f8..c8b159f3bc28ef424ed41eec67695e39d5b1349f 100644 (file)
--- 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)