CVC3  2.4.1
Public Member Functions | Static Public Member Functions | Private Attributes | List of all members
TReturn Class Reference

#include <TReturn.h>

Inheritance diagram for TReturn:
LFSCObj Obj

Public Member Functions

 TReturn (LFSCProof *lfsc_pf, std::vector< int > &L, std::vector< int > &Lused, Rational r, bool hasR, int pvY)
 
Rational mult_rational (TReturn *lhs)
 
void getL (std::vector< int > &lget, std::vector< int > &lgetu)
 
bool hasRational ()
 
Rational getRational ()
 
LFSCProofgetLFSCProof ()
 
int getProvesY ()
 
bool hasFv ()
 
- Public Member Functions inherited from LFSCObj
 LFSCObj ()
 
- Public Member Functions inherited from Obj
 Obj ()
 
virtual ~Obj ()
 
int GetRefCount ()
 get ref count More...
 
void Ref ()
 reference More...
 
void Unref ()
 unreference More...
 

Static Public Member Functions

static int normalize_tret (const Expr &pf1, TReturn *&t1, const Expr &pf2, TReturn *&t2, bool rev_pol=false)
 
static int normalize_tr (const Expr &pf1, TReturn *&t1, int y, bool rev_pol=false, bool printErr=true)
 
static void normalize_to_tf (const Expr &pf, TReturn *&t1, int y)
 
- Static Public Member Functions inherited from LFSCObj
static void initialize (const Expr &pf_expr, int lfscm)
 
- Static Public Member Functions inherited from Obj
static void print_error (const char *c, std::ostream &s)
 
static void print_warning (const char *c)
 
static void initialize ()
 

Private Attributes

RefPtr< LFSCProofd_lfsc_pf
 
std::vector< int > d_L
 
std::vector< int > d_L_used
 
Rational d_c
 
bool d_hasRt
 
int d_provesY
 
bool lcalced
 

Additional Inherited Members

- Protected Member Functions inherited from Obj
void indent (std::ostream &s, int ind=0)
 
- Static Protected Member Functions inherited from LFSCObj
static int getNumNodes (const Expr &pf, bool recount=false)
 
static Expr cascade_expr (const Expr &e)
 
static void define_skolem_vars (const Expr &e)
 
static bool isVar (const Expr &e)
 
static void collect_vars (const Expr &e, bool readPred=true)
 
static Expr queryElimNotNot (const Expr &expr)
 
static Expr queryAtomic (const Expr &expr, bool getBase=false)
 
static int queryM (const Expr &expr, bool add=true, bool trusted=false)
 
static int queryMt (const Expr &expr)
 
static int queryT (const Expr &e)
 
static bool getY (const Expr &e, Expr &pe, bool doIff=true, bool doLogic=true)
 
static bool isFormula (const Expr &e)
 
static bool can_pnorm (const Expr &e)
 
static bool what_is_proven (const Expr &pf, Expr &pe)
 
- Protected Attributes inherited from Obj
ostringstream oignore
 
int refCount
 
- Static Protected Attributes inherited from LFSCObj
static LFSCPrinterprinter
 
static int formula_i = 1
 
static int trusted_i = 1
 
static int term_i = 1
 
static int tnorm_i = 1
 
static int lfsc_mode
 
static bool debug_conv
 
static bool debug_var
 
static bool cvc3_mimic
 
static bool cvc3_mimic_input
 
static Rational nullRat
 
static ExprMap< int > nnode_map
 
static ExprMap< Exprcas_map
 
static ExprMap< Exprskolem_vars
 
static ExprMap< bool > temp_visited
 
static ExprMap< int > d_formulas
 
static ExprMap< int > d_trusted
 
static ExprMap< int > d_pn
 
static ExprMap< int > d_pn_form
 
static ExprMap< int > d_terms
 
static ExprMap< bool > input_vars
 
static ExprMap< bool > input_preds
 
static std::map< int, bool > pntNeeded
 
static ExprMap< bool > d_formulas_printed
 
static Expr d_pf_expr
 
static ExprMap< bool > d_assump_map
 
static ExprMap< bool > d_rules
 
static Expr d_bool_res_str
 
static Expr d_assump_str
 
static Expr d_iff_mp_str
 
static Expr d_impl_mp_str
 
static Expr d_iff_trans_str
 
static Expr d_real_shadow_str
 
static Expr d_cycle_conflict_str
 
static Expr d_real_shadow_eq_str
 
static Expr d_basic_subst_op_str
 
static Expr d_mult_ineqn_str
 
static Expr d_right_minus_left_str
 
static Expr d_eq_trans_str
 
static Expr d_eq_symm_str
 
static Expr d_canon_plus_str
 
static Expr d_refl_str
 
static Expr d_cnf_convert_str
 
static Expr d_learned_clause_str
 
static Expr d_minus_to_plus_str
 
static Expr d_plus_predicate_str
 
static Expr d_negated_inequality_str
 
static Expr d_flip_inequality_str
 
static Expr d_optimized_subst_op_str
 
static Expr d_iff_true_elim_str
 
static Expr d_basic_subst_op1_str
 
static Expr d_basic_subst_op0_str
 
static Expr d_canon_mult_str
 
static Expr d_canon_invert_divide_str
 
static Expr d_iff_true_str
 
static Expr d_mult_eqn_str
 
static Expr d_rewrite_eq_symm_str
 
static Expr d_implyWeakerInequality_str
 
static Expr d_implyWeakerInequalityDiffLogic_str
 
static Expr d_imp_mp_str
 
static Expr d_rewrite_implies_str
 
static Expr d_rewrite_or_str
 
static Expr d_rewrite_and_str
 
static Expr d_rewrite_iff_symm_str
 
static Expr d_iff_not_false_str
 
static Expr d_iff_false_str
 
static Expr d_iff_false_elim_str
 
static Expr d_not_to_iff_str
 
static Expr d_not_not_elim_str
 
static Expr d_const_predicate_str
 
static Expr d_rewrite_not_not_str
 
static Expr d_rewrite_not_true_str
 
static Expr d_rewrite_not_false_str
 
static Expr d_if_lift_rule_str
 
static Expr d_CNFITE_str
 
static Expr d_var_intro_str
 
static Expr d_int_const_eq_str
 
static Expr d_rewrite_eq_refl_str
 
static Expr d_iff_symm_str
 
static Expr d_rewrite_iff_str
 
static Expr d_implyNegatedInequality_str
 
static Expr d_uminus_to_mult_str
 
static Expr d_lessThan_To_LE_rhs_rwr_str
 
static Expr d_rewrite_ite_same_str
 
static Expr d_andE_str
 
static Expr d_implyEqualities_str
 
static Expr d_addInequalities_str
 
static Expr d_CNF_str
 
static Expr d_cnf_add_unit_str
 
static Expr d_minisat_proof_str
 
static Expr d_or_final_s
 
static Expr d_and_final_s
 
static Expr d_ite_s
 
static Expr d_iff_s
 
static Expr d_imp_s
 
static Expr d_or_mid_s
 
static Expr d_and_mid_s
 
- Static Protected Attributes inherited from Obj
static bool errsInit = false
 
static ofstream errs
 
static bool indentFlag = false
 

Detailed Description

Definition at line 11 of file TReturn.h.

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_to_tf(), and normalize_tr().

Member Function Documentation

Rational TReturn::mult_rational ( TReturn lhs)

Definition at line 24 of file TReturn.cpp.

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

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

RefPtr< LFSCProof > TReturn::d_lfsc_pf
private

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 getL(), and TReturn().

std::vector<int> TReturn::d_L_used
private

Definition at line 18 of file TReturn.h.

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

Rational TReturn::d_c
private

Definition at line 20 of file TReturn.h.

Referenced by getRational(), and mult_rational().

bool TReturn::d_hasRt
private

Definition at line 21 of file TReturn.h.

Referenced by hasRational(), and TReturn().

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: