CVC3  2.4.1
Public Member Functions | Private Member Functions | Private Attributes
LFSCPrinter Class Reference

#include <LFSCPrinter.h>

Inheritance diagram for LFSCPrinter:
LFSCObj Obj

List of all members.

Public Member Functions

Private Member Functions

Private Attributes


Constructor & Destructor Documentation

LFSCPrinter::LFSCPrinter ( const Expr  pf_expr,
Expr  qExpr,
std::vector< Expr assumps,
int  lfscm,
CommonProofRules commonRules 
)

Member Function Documentation

void LFSCPrinter::make_let_map ( const Expr e) [private]
void LFSCPrinter::print_poly_norm ( const Expr expr,
std::ostream s,
bool  pnRat = true,
bool  ratNeg = false 
) [private]
void LFSCPrinter::print_terms_h ( const Expr expr,
std::ostream s 
) [private]
void LFSCPrinter::print_formula_h ( const Expr clause,
std::ostream s 
) [private]
void LFSCPrinter::print_LFSC ( const Expr pf_expr)
void LFSCPrinter::set_print_expr ( const Expr expr) [inline]

Definition at line 33 of file LFSCPrinter.h.

References make_let_map().

Referenced by LFSCProofExpr::initialize().

void LFSCPrinter::print_expr ( const Expr expr,
std::ostream s 
) [inline]

Definition at line 35 of file LFSCPrinter.h.

References LFSCObj::isFormula(), print_formula(), and print_terms().

Referenced by LFSCProofExpr::print_pf().

void LFSCPrinter::print_formula ( const Expr clause,
std::ostream s 
) [inline]

Definition at line 42 of file LFSCPrinter.h.

References print_formula_h(), and LFSCObj::cascade_expr().

Referenced by print_LFSC(), print_expr(), and TReturn::normalize_tr().

void LFSCPrinter::print_terms ( const Expr expr,
std::ostream s 
) [inline]

Definition at line 48 of file LFSCPrinter.h.

References print_terms_h(), and LFSCObj::cascade_expr().

Referenced by print_LFSC(), and print_expr().


Member Data Documentation

Definition at line 10 of file LFSCPrinter.h.

Referenced by LFSCPrinter(), and print_LFSC().

Definition at line 12 of file LFSCPrinter.h.

Referenced by LFSCPrinter(), and print_LFSC().

int LFSCPrinter::let_i [private]

Definition at line 14 of file LFSCPrinter.h.

Referenced by LFSCPrinter(), and make_let_map().

Definition at line 16 of file LFSCPrinter.h.

Definition at line 18 of file LFSCPrinter.h.

Referenced by print_LFSC(), print_terms_h(), print_formula_h(), and make_let_map().

Definition at line 19 of file LFSCPrinter.h.

Referenced by print_LFSC(), and make_let_map().


The documentation for this class was generated from the following files: