TReturn Class Reference

#include <TReturn.h>

Inherits LFSCObj.

Collaboration diagram for TReturn:

List of all members.

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 ()

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)

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

---

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(), LFSCAssume::Make(), LFSCLraSub::Make(), LFSCLraMulC::Make(), LFSCLraContra::Make(), LFSCLraAdd::Make(), LFSCPfVar::Make(), LFSCProofGeneric::Make(), LFSCProofExpr::Make(), LFSCLraPoly::Make(), LFSCClausify::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(), LFSCAssume::Make(), LFSCLraAdd::Make(), LFSCLraContra::Make(), LFSCLraPoly::Make(), LFSCPfVar::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:

• TReturn.h
• TReturn.cpp