Definition at line 533 of file theory_arith_new.h.
CVC3::TheoryArithNew::BoundInfo::BoundInfo | ( | const EpsRational & | bound, | |
const Theorem & | thm | |||
) | [inline] |
Constructor
Definition at line 540 of file theory_arith_new.h.
CVC3::TheoryArithNew::BoundInfo::BoundInfo | ( | ) | [inline] |
The empty constructor for the map
Definition at line 543 of file theory_arith_new.h.
CVC3::TheoryArithNew::BoundInfo::BoundInfo | ( | const EpsRational & | bound, | |
const Theorem & | thm | |||
) | [inline] |
Constructor
Definition at line 544 of file theory_arith_new.mine.h.
CVC3::TheoryArithNew::BoundInfo::BoundInfo | ( | ) | [inline] |
The empty constructor for the map
Definition at line 547 of file theory_arith_new.mine.h.
bool CVC3::TheoryArithNew::BoundInfo::operator< | ( | const BoundInfo & | bI | ) | const [inline] |
The comparator, just if we need it. Compares first by expressions then by bounds
Definition at line 548 of file theory_arith_new.h.
References bound, std::endl(), CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), CVC3::Theorem::isRewrite(), CVC3::LE, and theorem.
bool CVC3::TheoryArithNew::BoundInfo::operator< | ( | const BoundInfo & | bI | ) | const [inline] |
The comparator, just if we need it. Compares first by expressions then by bounds
Definition at line 552 of file theory_arith_new.mine.h.
References bound, std::endl(), CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), CVC3::Theorem::isRewrite(), CVC3::LE, and theorem.
The assertion theoreem of the bound
Definition at line 537 of file theory_arith_new.h.
Referenced by operator<().