Cleanup of arithmetic, and some new utility functions for the coming fcsimplex code.

1 files changed, 0 insertions, 53 deletions

diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index c7f511a98..76210fc7c 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -168,59 +168,6 @@ inline int deltaCoeff(Kind k){
   }
 }
 
-
-// template <bool selectLeft>
-// inline TNode getSide(TNode assertion, Kind simpleKind){
-//   switch(simpleKind){
-//   case kind::LT:
-//   case kind::GT:
-//   case kind::DISTINCT:
-//     return selectLeft ? (assertion[0])[0] : (assertion[0])[1];
-//   case kind::LEQ:
-//   case kind::GEQ:
-//   case kind::EQUAL:
-//     return selectLeft ? assertion[0] : assertion[1];
-//   default:
-//     Unreachable();
-//     return TNode::null();
-//   }
-// }
-
-// inline DeltaRational determineRightConstant(TNode assertion, Kind simpleKind){
-//   TNode right = getSide<false>(assertion, simpleKind);
-
-//   Assert(right.getKind() == kind::CONST_RATIONAL);
-//   const Rational& noninf = right.getConst<Rational>();
-
-//   Rational inf = Rational(Integer(deltaCoeff(simpleKind)));
-//   return DeltaRational(noninf, inf);
-// }
-
-// inline DeltaRational asDeltaRational(TNode n){
-//   Kind simp = simplifiedKind(n);
-//   return determineRightConstant(n, simp);
-// }
-
-//  /**
-//   * Takes two nodes with exactly 2 children,
-//   * the second child of both are of kind CONST_RATIONAL,
-//   * and compares value of the two children.
-//   * This is for comparing inequality nodes.
-//   *   RightHandRationalLT((<= x 50), (< x 75)) == true
-//   */
-// struct RightHandRationalLT
-// {
-//   bool operator()(TNode s1, TNode s2) const
-//   {
-//     TNode rh1 = s1[1];
-//     TNode rh2 = s2[1];
-//     const Rational& c1 = rh1.getConst<Rational>();
-//     const Rational& c2 = rh2.getConst<Rational>();
-//     int cmpRes = c1.cmp(c2);
-//     return cmpRes < 0;
-//   }
-// };
-
 inline Node negateConjunctionAsClause(TNode conjunction){
   Assert(conjunction.getKind() == kind::AND);
   NodeBuilder<> orBuilder(kind::OR);