diff options
author | Tim King <taking@cs.nyu.edu> | 2012-05-15 19:01:19 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-05-15 19:01:19 +0000 |
commit | 488ae3f42d9d3e06978e11a42d1d47e76072f797 (patch) | |
tree | f466859889ceee9947e20d695fd35f99065277f8 /src/expr/pickler.cpp | |
parent | fe2088f892af594765fc50d8cc9f2b4f87286b7c (diff) |
This commit removes the CONST_INTEGER kind from nodes. This code comes from the branch arithmetic/remove_const_int.
Diffstat (limited to 'src/expr/pickler.cpp')
-rw-r--r-- | src/expr/pickler.cpp | 22 |
1 files changed, 5 insertions, 17 deletions
diff --git a/src/expr/pickler.cpp b/src/expr/pickler.cpp index f09c552d1..3d077502d 100644 --- a/src/expr/pickler.cpp +++ b/src/expr/pickler.cpp @@ -207,17 +207,11 @@ void PicklerPrivate::toCaseConstant(TNode n) { d_current << mkConstantHeader(k, 1); d_current << mkBlockBody(n.getConst<bool>()); break; - case kind::CONST_INTEGER: case kind::CONST_RATIONAL: { std::string asString; - if(k == kind::CONST_INTEGER) { - const Integer& i = n.getConst<Integer>(); - asString = i.toString(16); - } else { - Assert(k == kind::CONST_RATIONAL); - const Rational& q = n.getConst<Rational>(); - asString = q.toString(16); - } + Assert(k == kind::CONST_RATIONAL); + const Rational& q = n.getConst<Rational>(); + asString = q.toString(16); toCaseString(k, asString); break; } @@ -357,16 +351,10 @@ Node PicklerPrivate::fromCaseConstant(Kind k, uint32_t constblocks) { bool b= val.d_body.d_data; return d_nm->mkConst<bool>(b); } - case kind::CONST_INTEGER: case kind::CONST_RATIONAL: { std::string s = fromCaseString(constblocks); - if(k == kind::CONST_INTEGER) { - Integer i(s, 16); - return d_nm->mkConst<Integer>(i); - } else { - Rational q(s, 16); - return d_nm->mkConst<Rational>(q); - } + Rational q(s, 16); + return d_nm->mkConst<Rational>(q); } case kind::BITVECTOR_EXTRACT_OP: { Block high = d_current.dequeue(); |