diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-04-18 19:08:11 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-04-18 19:08:11 +0000 |
| commit | d1ba1ccd5a3c55ba7a0e63b33fd921642e44752d (patch) | |
| tree | f3d22cdd12076a488dff2e9176dd1f619c731902 /src/parser/cvc/Cvc.g | |
| parent | 267858307741675cb78e829270e619f57cf21a27 (diff) | |
more work on CVC language
Diffstat (limited to 'src/parser/cvc/Cvc.g')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 25 |
1 files changed, 17 insertions, 8 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 96a8346b0..30866eddb 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -597,7 +597,7 @@ arrayType[CVC4::Type& t] Type t2; } : baseType[t] - | ARRAY_TOK baseType[t] OF_TOK baseType[t2] + | ARRAY_TOK bitvectorType[t] OF_TOK bitvectorType[t2] { t = EXPR_MANAGER->mkArrayType(t, t2); } ; @@ -927,10 +927,14 @@ bvUminusTerm[CVC4::Expr& f] { f = MK_EXPR(CVC4::kind::BITVECTOR_LSHR, f, f2); } | SX_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); - f = MK_EXPR(MK_CONST(BitVectorSignExtend(k)), f); } + unsigned n = BitVectorType(f.getType()).getSize(); + // sign extension in TheoryBitVector is defined as in SMT-LIBv2 + f = MK_EXPR(MK_CONST(BitVectorSignExtend(k - n)), f); } | BVZEROEXTEND_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); - f = MK_EXPR(MK_CONST(BitVectorSignExtend(k)), f); } + unsigned n = BitVectorType(f.getType()).getSize(); + // also zero extension + f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k - n)), f); } | BVREPEAT_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); f = MK_EXPR(MK_CONST(BitVectorRepeat(k)), f); } @@ -945,14 +949,19 @@ bvUminusTerm[CVC4::Expr& f] bvShiftTerm[CVC4::Expr& f] @init { - std::vector<CVC4::Expr> expressions; - std::vector<unsigned> operators; - unsigned op; + bool left = false; } : bvComparison[f] - ( ( LEFTSHIFT_TOK | RIGHTSHIFT_TOK) INTEGER_LITERAL + ( (LEFTSHIFT_TOK { left = true; } | RIGHTSHIFT_TOK) INTEGER_LITERAL { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); - f = MK_EXPR(MK_CONST(BitVectorRotateLeft(k)), f); } + if(left) { + f = MK_EXPR(kind::BITVECTOR_CONCAT, f, MK_CONST(BitVector(k))); + } else { + unsigned n = BitVectorType(f.getType()).getSize(); + f = MK_EXPR(kind::BITVECTOR_CONCAT, MK_CONST(BitVector(k)), + MK_EXPR(MK_CONST(BitVectorExtract(n - 1, k)), f)); + } + } )? ; |