diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-10-08 16:00:58 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-10-08 16:00:58 +0000 |
| commit | ef83f6744c1dcd1d5a90ea279cf77530d6de5b31 (patch) | |
| tree | bf27aabf5e77da2d8ba6e29f3002c33950c0cc61 | |
| parent | 292f98a5649d6f282e1e2d4c53fb76127196488a (diff) | |
fix SMT-LIBv2 compliance mode for bitvectors (was completely broken; didn't allow use of any BV ops
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 40 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.h | 2 |
2 files changed, 42 insertions, 0 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 45caf94a8..695d154e1 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -45,6 +45,45 @@ void Smt2::addArithmeticOperators() { addOperator(kind::GEQ); } +void Smt2::addBitvectorOperators() { + addOperator(kind::BITVECTOR_CONCAT); + addOperator(kind::BITVECTOR_AND); + addOperator(kind::BITVECTOR_OR); + addOperator(kind::BITVECTOR_XOR); + addOperator(kind::BITVECTOR_NOT); + addOperator(kind::BITVECTOR_NAND); + addOperator(kind::BITVECTOR_NOR); + addOperator(kind::BITVECTOR_XNOR); + addOperator(kind::BITVECTOR_COMP); + addOperator(kind::BITVECTOR_MULT); + addOperator(kind::BITVECTOR_PLUS); + addOperator(kind::BITVECTOR_SUB); + addOperator(kind::BITVECTOR_NEG); + addOperator(kind::BITVECTOR_UDIV); + addOperator(kind::BITVECTOR_UREM); + addOperator(kind::BITVECTOR_SDIV); + addOperator(kind::BITVECTOR_SREM); + addOperator(kind::BITVECTOR_SMOD); + addOperator(kind::BITVECTOR_SHL); + addOperator(kind::BITVECTOR_LSHR); + addOperator(kind::BITVECTOR_ASHR); + addOperator(kind::BITVECTOR_ULT); + addOperator(kind::BITVECTOR_ULE); + addOperator(kind::BITVECTOR_UGT); + addOperator(kind::BITVECTOR_UGE); + addOperator(kind::BITVECTOR_SLT); + addOperator(kind::BITVECTOR_SLE); + addOperator(kind::BITVECTOR_SGT); + addOperator(kind::BITVECTOR_SGE); + addOperator(kind::BITVECTOR_BITOF); + addOperator(kind::BITVECTOR_EXTRACT); + addOperator(kind::BITVECTOR_REPEAT); + addOperator(kind::BITVECTOR_ZERO_EXTEND); + addOperator(kind::BITVECTOR_SIGN_EXTEND); + addOperator(kind::BITVECTOR_ROTATE_LEFT); + addOperator(kind::BITVECTOR_ROTATE_RIGHT); +} + void Smt2::addTheory(Theory theory) { switch(theory) { case THEORY_CORE: @@ -82,6 +121,7 @@ void Smt2::addTheory(Theory theory) { break; case THEORY_BITVECTORS: + addBitvectorOperators(); break; case THEORY_QUANTIFIERS: diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 72310b5a4..48942265a 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -91,6 +91,8 @@ private: void addArithmeticOperators(); + void addBitvectorOperators(); + };/* class Smt2 */ }/* CVC4::parser namespace */ |