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/arith_utilities.h | |
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/arith_utilities.h')
-rw-r--r-- | src/theory/arith/arith_utilities.h | 38 |
1 files changed, 0 insertions, 38 deletions
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index af32c3f87..fb669cce4 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -41,50 +41,12 @@ inline Node mkRationalNode(const Rational& q){ return NodeManager::currentNM()->mkConst<Rational>(q); } -inline Node mkIntegerNode(const Integer& z){ - return NodeManager::currentNM()->mkConst<Integer>(z); -} - inline Node mkBoolNode(bool b){ return NodeManager::currentNM()->mkConst<bool>(b); } -inline Rational coerceToRational(TNode constant){ - switch(constant.getKind()){ - case kind::CONST_INTEGER: - { - Rational q(constant.getConst<Integer>()); - return q; - } - case kind::CONST_RATIONAL: - return constant.getConst<Rational>(); - default: - Unreachable(); - } - Rational unreachable(0,0); - return unreachable; -} - -inline Node coerceToRationalNode(TNode constant){ - switch(constant.getKind()){ - case kind::CONST_INTEGER: - { - Rational q(constant.getConst<Integer>()); - Node n = mkRationalNode(q); - return n; - } - case kind::CONST_RATIONAL: - return constant; - default: - Unreachable(); - } - return Node::null(); -} - - - /** \f$ k \in {LT, LEQ, EQ, GEQ, GT} \f$ */ inline bool isRelationOperator(Kind k){ using namespace kind; |