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)

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 5c5b87f38dde49a56eb6ca4eaba9a178e616c0c3..00f2e944d6ce1de6525ac3d944fcd33904960d9f 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1886,7 +1886,8 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
       Kind lassocKind = CVC4::kind::UNDEFINED_KIND;
       if (args.size() >= 2)
       {
-        if (kind == CVC4::kind::INTS_DIVISION)
+        if (kind == CVC4::kind::INTS_DIVISION
+            || (kind == CVC4::kind::BITVECTOR_XNOR && PARSER_STATE->v2_6()))
         {
           // Builtin operators that are not tokenized, are left associative,
           // but not internally variadic must set this.

diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 171642c7e4dbfc8f86f2aa406a88072439a02fe9..7a3c3b0c312b8afc1c394309b7f38e9a92926613 100644 (file)
--- 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:

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 2c6acf69ca4b70d6a085fd239a26eee32468f8fb..97ca9a1be8ff2d664a052d15114ef7241712aa9c 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -534,6 +534,7 @@ set(regress_0_tests
   regress0/options/invalid_dump.smt2
   regress0/parallel-let.smt2
   regress0/parser/as.smt2
+  regress0/parser/bv_arity_smt2.6.smt2
   regress0/parser/constraint.smt2
   regress0/parser/declarefun-emptyset-uf.smt2
   regress0/parser/shadow_fun_symbol_all.smt2

diff --git a/test/regress/regress0/parser/bv_arity_smt2.6.smt2 b/test/regress/regress0/parser/bv_arity_smt2.6.smt2
new file mode 100644 (file)
index 0000000..437d80f
--- /dev/null
+++ b/test/regress/regress0/parser/bv_arity_smt2.6.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --strict-parsing
+(set-info :status unsat)
+(set-logic QF_BV)
+(declare-const x (_ BitVec 8))
+(declare-const y (_ BitVec 8))
+(declare-const z (_ BitVec 8))
+(assert (or (not (= (bvadd x y z) (bvadd (bvadd x y) z)))
+            (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)))))
+(check-sat)