diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-08 10:18:01 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-08 10:18:01 +0000 |
commit | afc984d28606e0c3c0254a26033f4a934eebd5b7 (patch) | |
tree | 5994303d8ed14150806c25b4627d54fdf1bb6195 | |
parent | 018d28f22253eb666044b3e2f5e6192b45fb7680 (diff) |
handle BitVectorSignExtend in pickler
-rw-r--r-- | src/expr/pickler.cpp | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/expr/pickler.cpp b/src/expr/pickler.cpp index 3d077502d..14477f3cd 100644 --- a/src/expr/pickler.cpp +++ b/src/expr/pickler.cpp @@ -233,6 +233,12 @@ void PicklerPrivate::toCaseConstant(TNode n) { toCaseString(k, asString); break; } + case kind::BITVECTOR_SIGN_EXTEND_OP: { + BitVectorSignExtend bvse = n.getConst<BitVectorSignExtend>(); + d_current << mkConstantHeader(k, 1); + d_current << mkBlockBody(bvse.signExtendAmount); + break; + } default: Unhandled(k); } @@ -371,6 +377,11 @@ Node PicklerPrivate::fromCaseConstant(Kind k, uint32_t constblocks) { BitVector bv(size, value); return d_nm->mkConst(bv); } + case kind::BITVECTOR_SIGN_EXTEND_OP: { + Block signExtendAmount = d_current.dequeue(); + BitVectorSignExtend bvse(signExtendAmount.d_body.d_data); + return d_nm->mkConst<BitVectorSignExtend>(bvse); + } default: Unhandled(k); } |