From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Fri, 8 Jun 2012 10:18:01 +0000 (+0000)
Subject: handle BitVectorSignExtend in pickler
X-Git-Tag: cvc5-1.0.0~8104
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=afc984d28606e0c3c0254a26033f4a934eebd5b7;p=cvc5.git

handle BitVectorSignExtend in pickler
---

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