21 #ifndef _cvc3__include__theory_arith_old_h_
22 #define _cvc3__include__theory_arith_old_h_
49 friend std::ostream&
operator<<(std::ostream& os,
const FreeConst& fc);
75 friend std::ostream&
operator<<(std::ostream& os,
const Ineq& ineq);
140 void dfs(
const Expr& e1, std::vector<Expr>& output_list);
147 void selectLargest(
const std::vector<Expr>& v1, std::vector<Expr>& v2);
150 void selectSmallest( std::vector<Expr>& v1, std::vector<Expr>& v2);
271 bool isStale(
const Ineq& ineq);
302 std::set<Expr>& cache);
338 bool enumerate,
bool computeSize);
528 if (
k >= 0)
return q;
663 return (
q < r.
q || (
q == r.
q &&
k <= r.
k));
675 FatalAssert(
false,
"EpsRational::operator <=, what kind of number is this????");
704 FatalAssert(
false,
"EpsRational::toString, what kind of number is this????");
706 return "hm, what am I?";
730 void getEdgeTheorems(
const Expr& x,
const Expr& y,
const EdgeInfo& edgeInfo, std::vector<Theorem>& outputTheorems);
953 void tryPropagate(
const Expr& x,
const Expr& y,
const DifferenceLogicGraph::EdgeInfo& x_y_edge,
int kind);