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

1 files changed, 22 insertions, 0 deletions

diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 55a06a8e3..da68f334c 100644
--- 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();