CVC3  2.4.1
Public Member Functions | Static Public Member Functions | Private Attributes
TReturn Class Reference

#include <TReturn.h>

Inheritance diagram for TReturn:
LFSCObj Obj

List of all members.

Public Member Functions

Static Public Member Functions

Private Attributes


Constructor & Destructor Documentation

TReturn::TReturn ( LFSCProof lfsc_pf,
std::vector< int > &  L,
std::vector< int > &  Lused,
Rational  r,
bool  hasR,
int  pvY 
)

Definition at line 8 of file TReturn.cpp.

References d_hasRt, d_L, d_L_used, std::endl(), and lcalced.

Referenced by normalize_tr(), and normalize_to_tf().


Member Function Documentation

Rational TReturn::mult_rational ( TReturn lhs)

Definition at line 24 of file TReturn.cpp.

References hasRational(), mult_rational(), and d_c.

Referenced by LFSCConvert::cvc3_to_lfsc(), and mult_rational().

void TReturn::getL ( std::vector< int > &  lget,
std::vector< int > &  lgetu 
)
bool TReturn::hasRational ( ) [inline]

Definition at line 35 of file TReturn.h.

References d_hasRt.

Referenced by LFSCConvert::cvc3_to_lfsc(), mult_rational(), and normalize_tr().

Rational TReturn::getRational ( ) [inline]

Definition at line 36 of file TReturn.h.

References d_c.

Referenced by LFSCConvert::cvc3_to_lfsc(), and normalize_tr().

LFSCProof* TReturn::getLFSCProof ( ) [inline]
int TReturn::getProvesY ( ) [inline]
bool TReturn::hasFv ( ) [inline]

Definition at line 39 of file TReturn.h.

References d_L_used.

int TReturn::normalize_tret ( const Expr pf1,
TReturn *&  t1,
const Expr pf2,
TReturn *&  t2,
bool  rev_pol = false 
) [static]
int TReturn::normalize_tr ( const Expr pf1,
TReturn *&  t1,
int  y,
bool  rev_pol = false,
bool  printErr = true 
) [static]
void TReturn::normalize_to_tf ( const Expr pf,
TReturn *&  t1,
int  y 
) [static]

Member Data Documentation

Definition at line 14 of file TReturn.h.

Referenced by getLFSCProof().

std::vector<int> TReturn::d_L [private]

Definition at line 16 of file TReturn.h.

Referenced by TReturn(), and getL().

Definition at line 18 of file TReturn.h.

Referenced by TReturn(), getL(), and hasFv().

Definition at line 20 of file TReturn.h.

Referenced by mult_rational(), and getRational().

bool TReturn::d_hasRt [private]

Definition at line 21 of file TReturn.h.

Referenced by TReturn(), and hasRational().

int TReturn::d_provesY [private]

Definition at line 28 of file TReturn.h.

Referenced by getProvesY().

bool TReturn::lcalced [private]

Definition at line 29 of file TReturn.h.

Referenced by TReturn().


The documentation for this class was generated from the following files: