SMT strict mode now disallows N-ary use of concat, bvadd, bvmul, bvand, bvor, and...

diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 55a06a8e30c2bd83a08445f5e6d8c7076af40308..da68f334c12ef4de210b9d5c0dc80f9145f2a8fc 100644 (file)
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -139,6 +139,28 @@ public:
     this->Parser::checkDeclaration(name, check, type, ss.str());
   }
 
+  void checkOperator(Kind kind, unsigned numArgs) throw(ParserException) {
+    Parser::checkOperator(kind, numArgs);
+    // strict SMT-LIB mode enables extra checks for some bitvector operators
+    // 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_PLUS:
+        if(numArgs != 2) {
+          parseError("Operator requires exact 2 arguments in strict SMT-LIB compliance mode: " + kindToString(kind));
+        }
+        break;
+      default:
+        break; /* no problem */
+      }
+    }
+  }
+
 private:
 
   void addArithmeticOperators();