diff options
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; |