CVC3  2.4.1
Public Member Functions | Public Attributes | List of all members
CVC3::TheoryArithNew::ExprBoundInfo Struct Reference

Public Member Functions

 ExprBoundInfo (const EpsRational &bound, const Expr &e)
 
 ExprBoundInfo ()
 
bool operator< (const ExprBoundInfo &bI) const
 

Public Attributes

EpsRational bound
 
Expr e
 

Detailed Description

The structure necessaty to hold the bounds on expressions (for theory propagation).

Definition at line 574 of file theory_arith_new.h.

Constructor & Destructor Documentation

CVC3::TheoryArithNew::ExprBoundInfo::ExprBoundInfo ( const EpsRational bound,
const Expr e 
)
inline

Constructor

Definition at line 581 of file theory_arith_new.h.

CVC3::TheoryArithNew::ExprBoundInfo::ExprBoundInfo ( )
inline

The empty constructor for the map

Definition at line 584 of file theory_arith_new.h.

Member Function Documentation

bool CVC3::TheoryArithNew::ExprBoundInfo::operator< ( const ExprBoundInfo bI) const
inline

The comparator, just if we need it. Compares first by expressions then by bounds

Definition at line 589 of file theory_arith_new.h.

References bound, e, CVC3::Expr::getKind(), and CVC3::LE.

Member Data Documentation

EpsRational CVC3::TheoryArithNew::ExprBoundInfo::bound

The bound itself

Definition at line 576 of file theory_arith_new.h.

Referenced by operator<().

Expr CVC3::TheoryArithNew::ExprBoundInfo::e

The assertion theoreem of the bound

Definition at line 578 of file theory_arith_new.h.

Referenced by operator<().


The documentation for this struct was generated from the following file: