From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 4 Jun 2014 19:21:52 +0000 (-0400)
Subject: SMT strict mode now disallows N-ary use of concat, bvadd, bvmul, bvand, bvor, and... 
X-Git-Tag: cvc5-1.0.0~6862
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=468f1afc7546ad47dc8aac097aa738c374acdc82;p=cvc5.git

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

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();