CVC3
2.4.1
|
#include <TReturn.h>
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().
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 | ||
) |
Definition at line 37 of file TReturn.cpp.
Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCConvert::make_let_proof(), LFSCConvert::do_bso(), normalize_tr(), and normalize_to_tf().
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::get().
Referenced by LFSCConvert::convert(), LFSCConvert::cvc3_to_lfsc(), LFSCConvert::do_bso(), normalize_tr(), and normalize_to_tf().
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_tret(), normalize_tr(), and normalize_to_tf().
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 getProvesY(), LFSCObj::debug_conv, std::endl(), 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 getLFSCProof(), LFSCProof::getChOp(), getL(), getProvesY(), LFSCObj::debug_conv, std::endl(), LFSCObj::what_is_proven(), LFSCObj::queryElimNotNot(), CVC3::Expr::isIff(), IFF, CVC3::Expr::isImpl(), IMPLIES, LFSCObj::queryAtomic(), TReturn(), LFSCClausify::Make(), LFSCObj::nullRat, LFSCObj::can_pnorm(), LFSCLraPoly::Make(), getRational(), hasRational(), is_eq_kind(), CVC3::Expr::getKind(), normalize_to_tf(), LFSCProofExpr::Make(), LFSCProofGeneric::Make(), RefPtr::get(), NOT, LFSCPfVar::Make(), LFSCObj::queryM(), CVC3::abs(), LFSCProofGeneric::MakeStr(), CVC3::Expr::isFalse(), CVC3::Expr::isTrue(), Obj::print_error(), LFSCLraAdd::Make(), get_normalized(), LFSCLraContra::Make(), is_comparison(), CVC3::GT, DISTINCT, LFSCObj::printer, LFSCPrinter::print_formula(), LFSCLraMulC::Make(), LFSCLraSub::Make(), EQ, LFSCAssume::Make(), and LFSCProof::setChOp().
Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCConvert::do_bso(), and normalize_tret().
Definition at line 423 of file TReturn.cpp.
References getLFSCProof(), LFSCProof::getChOp(), getProvesY(), std::endl(), Obj::print_error(), getL(), LFSCProof::AsLFSCLraPoly(), TReturn(), LFSCProof::getChild(), LFSCObj::nullRat, LFSCObj::queryAtomic(), LFSCObj::queryM(), CVC3::Expr::getKind(), LFSCPfVar::Make(), CVC3::abs(), NOT, LFSCLraPoly::Make(), RefPtr::get(), LFSCLraContra::Make(), LFSCLraAdd::Make(), get_normalized(), is_comparison(), CVC3::GT, DISTINCT, LFSCAssume::Make(), and LFSCProof::setChOp().
Referenced by normalize_tr().
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] |
std::vector<int> TReturn::d_L_used [private] |
Rational TReturn::d_c [private] |
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] |