From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Sat, 26 Sep 2020 01:08:08 +0000 (-0700)
Subject: Restrict bvxnor to only allow two operands (was n-ary). (#5138)
X-Git-Tag: cvc5-1.0.0~2806
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=160a3f55bf4dbfdbc1385ce4898c62b1fd3a8c78;p=cvc5.git

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 93a7cc615..682b9ce75 100644
--- 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 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)