From 2f7131c81078a964a4043ef79186cdcf91951974 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 16 Apr 2019 12:11:37 -0700
Subject: 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)
---
 src/parser/smt2/Smt2.g |  3 ++-
 src/parser/smt2/smt2.h | 20 +++++++++++++++-----
 2 files changed, 17 insertions(+), 6 deletions(-)

(limited to 'src/parser/smt2')

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 5c5b87f38..00f2e944d 100644
--- 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 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:
-- 
cgit v1.2.3