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/theory/arith/theory_arith.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/theory/arith/theory_arith.cpp')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 13 |
1 files changed, 2 insertions, 11 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index d660cb4cd..1bd3277cd 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -1239,8 +1239,8 @@ Node TheoryArith::roundRobinBranch(){ Integer floor_d = d.floor(); Integer ceil_d = d.ceiling(); - Node leq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, mkIntegerNode(floor_d))); - Node geq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GEQ, var, mkIntegerNode(ceil_d))); + Node leq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, mkRationalNode(floor_d))); + Node geq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GEQ, var, mkRationalNode(ceil_d))); Node lem = NodeManager::currentNM()->mkNode(kind::OR, leq, geq); @@ -1436,9 +1436,6 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) { switch(n.getKind()) { - case kind::CONST_INTEGER: - return Rational(n.getConst<Integer>()); - case kind::CONST_RATIONAL: return n.getConst<Rational>(); @@ -1456,9 +1453,6 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) { case kind::MULT: { // 2+ args Assert(n.getNumChildren() == 2 && n[0].isConst()); DeltaRational value(1); - if (n[0].getKind() == kind::CONST_INTEGER) { - return getDeltaValue(n[1]) * n[0].getConst<Integer>(); - } if (n[0].getKind() == kind::CONST_RATIONAL) { return getDeltaValue(n[1]) * n[0].getConst<Rational>(); } @@ -1478,9 +1472,6 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) { if (n[1].getKind() == kind::CONST_RATIONAL) { return getDeltaValue(n[0]) / n[0].getConst<Rational>(); } - if (n[1].getKind() == kind::CONST_INTEGER) { - return getDeltaValue(n[0]) / n[0].getConst<Integer>(); - } Unreachable(); |