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

#include <TReturn.h>

Inherits LFSCObj.

Collaboration diagram for TReturn:
Collaboration graph

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 ()
 
LFSCProof * getLFSCProof ()
 
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
 
void Ref ()
 reference
 
void Unref ()
 unreference
 

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< LFSCProof > d_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 LFSCPrinter * printer
 
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< Expr > cas_map
 
static ExprMap< Expr > skolem_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
 

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 
)

Definition at line 37 of file TReturn.cpp.

References d_L, and d_L_used.

Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCConvert::do_bso(), LFSCConvert::make_let_proof(), normalize_to_tf(), and normalize_tr().

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

Definition at line 37 of file TReturn.h.

References d_lfsc_pf, and RefPtr< T >::get().

Referenced by LFSCConvert::convert(), LFSCConvert::cvc3_to_lfsc(), LFSCConvert::do_bso(), normalize_to_tf(), and normalize_tr().

int TReturn::getProvesY ( )
inline

Definition at line 38 of file TReturn.h.

References d_provesY.

Referenced by LFSCConvert::convert(), LFSCConvert::cvc3_to_lfsc(), LFSCConvert::do_bso(), normalize_to_tf(), normalize_tr(), and normalize_tret().

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

Definition at line 84 of file TReturn.cpp.

References LFSCObj::debug_conv, std::endl(), getProvesY(), normalize_tr(), and Obj::print_error().

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

int TReturn::normalize_tr ( const Expr &  pf1,
TReturn *&  t1,
int  y,
bool  rev_pol = false,
bool  printErr = true 
)
static

Definition at line 125 of file TReturn.cpp.

References CVC3::abs(), LFSCObj::can_pnorm(), LFSCObj::debug_conv, DISTINCT, std::endl(), EQ, RefPtr< T >::get(), get_normalized(), LFSCProof::getChOp(), CVC3::Expr::getKind(), getL(), getLFSCProof(), getProvesY(), getRational(), CVC3::GT, hasRational(), IFF, IMPLIES, is_comparison(), is_eq_kind(), CVC3::Expr::isFalse(), CVC3::Expr::isIff(), CVC3::Expr::isImpl(), CVC3::Expr::isTrue(), LFSCProofExpr::Make(), LFSCLraAdd::Make(), LFSCPfVar::Make(), LFSCLraMulC::Make(), LFSCClausify::Make(), LFSCProofGeneric::Make(), LFSCAssume::Make(), LFSCLraSub::Make(), LFSCLraPoly::Make(), LFSCLraContra::Make(), LFSCProofGeneric::MakeStr(), normalize_to_tf(), NOT, LFSCObj::nullRat, Obj::print_error(), LFSCPrinter::print_formula(), LFSCObj::printer, LFSCObj::queryAtomic(), LFSCObj::queryElimNotNot(), LFSCObj::queryM(), LFSCProof::setChOp(), TReturn(), and LFSCObj::what_is_proven().

Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCConvert::do_bso(), and normalize_tret().

void TReturn::normalize_to_tf ( const Expr &  pf,
TReturn *&  t1,
int  y 
)
static

Definition at line 423 of file TReturn.cpp.

References CVC3::abs(), LFSCProof::AsLFSCLraPoly(), DISTINCT, std::endl(), RefPtr< T >::get(), get_normalized(), LFSCProof::getChild(), LFSCProof::getChOp(), CVC3::Expr::getKind(), getL(), getLFSCProof(), getProvesY(), CVC3::GT, is_comparison(), LFSCLraAdd::Make(), LFSCPfVar::Make(), LFSCAssume::Make(), LFSCLraPoly::Make(), LFSCLraContra::Make(), NOT, LFSCObj::nullRat, Obj::print_error(), LFSCObj::queryAtomic(), LFSCObj::queryM(), LFSCProof::setChOp(), and TReturn().

Referenced by normalize_tr().

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:
Generated on Thu May 16 2013 13:25:17 for CVC3 by   doxygen 1.8.2