diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-04 15:21:52 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-04 15:21:52 -0400 |
commit | 468f1afc7546ad47dc8aac097aa738c374acdc82 (patch) | |
tree | 9de12a88e58d448da2752f021be9681965c7c978 /src/parser/smt2 | |
parent | dbdc83268d75b205198cbad5d60397de28705c65 (diff) |
SMT strict mode now disallows N-ary use of concat, bvadd, bvmul, bvand, bvor, and bvxor.
Diffstat (limited to 'src/parser/smt2')
-rw-r--r-- | src/parser/smt2/smt2.h | 22 |
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(); |