CVC3
|
#include <TReturn.h>
Inherits LFSCObj.
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 () |
![]() | |
LFSCObj () | |
![]() | |
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 void | initialize (const Expr &pf_expr, int lfscm) |
![]() | |
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 |
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().
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.
Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCConvert::do_bso(), LFSCConvert::make_let_proof(), normalize_to_tf(), and normalize_tr().
|
inline |
Definition at line 35 of file TReturn.h.
References d_hasRt.
Referenced by LFSCConvert::cvc3_to_lfsc(), mult_rational(), and normalize_tr().
|
inline |
Definition at line 36 of file TReturn.h.
References d_c.
Referenced by LFSCConvert::cvc3_to_lfsc(), and normalize_tr().
|
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().
|
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().
|
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().
|
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().
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().
Definition at line 14 of file TReturn.h.
Referenced by getLFSCProof().
|
private |
|
private |
|
private |
Definition at line 20 of file TReturn.h.
Referenced by getRational(), and mult_rational().
|
private |
Definition at line 21 of file TReturn.h.
Referenced by hasRational(), and TReturn().
|
private |
Definition at line 28 of file TReturn.h.
Referenced by getProvesY().