21 #ifndef _cvc3__include__theory_arith_new_h_
22 #define _cvc3__include__theory_arith_new_h_
62 friend std::ostream&
operator<<(std::ostream& os,
const FreeConst& fc);
87 friend std::ostream&
operator<<(std::ostream& os,
const Ineq& ineq);
128 void selectLargest(
const std::vector<Expr>& v1, std::vector<Expr>& v2);
131 void selectSmallest( std::vector<Expr>& v1, std::vector<Expr>& v2);
195 bool isStale(
const Ineq& ineq);
218 std::set<Expr>& cache);
251 bool enumerate,
bool computeSize);
327 if (
k >= 0)
return q;
444 return (
q < r.
q || (
q == r.
q &&
k <= r.
k));
456 FatalAssert(
false,
"EpsRational::operator <=, what kind of number is this????");
485 FatalAssert(
false,
"EpsRational::toString, what kind of number is this????");
487 return "hm, what am I?";
555 std::cout << expr1 <<
" @ " << expr2 <<
std::endl;
558 if (expr1[1] == expr2[1])
566 return expr1[1] < expr2[1];
600 return e[1] < bI.
e[1];