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

 LFSCPrinter (const Expr pf_expr, Expr qExpr, std::vector< Expr > assumps, int lfscm, CommonProofRules *commonRules)
void print_LFSC (const Expr &pf_expr)
void set_print_expr (const Expr &expr)
void print_expr (const Expr &expr, std::ostream &s)
void print_formula (const Expr &clause, std::ostream &s)
void print_terms (const Expr &expr, std::ostream &s)
- 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

Private Member Functions

void make_let_map (const Expr &e)
void print_poly_norm (const Expr &expr, std::ostream &s, bool pnRat=true, bool ratNeg=false)
void print_terms_h (const Expr &expr, std::ostream &s)
void print_formula_h (const Expr &clause, std::ostream &s)

Private Attributes

std::vector< Exprd_user_assumptions
RefPtr< LFSCConvertconverter
int let_i
CommonProofRulesd_common_pf_rules
ExprMap< int > d_print_map
ExprMap< bool > d_print_visited_map

Additional Inherited Members

- 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 ()
- 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)
- Static Protected Attributes inherited from LFSCObj
static LFSCPrinterprinter
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< Exprcas_map
static ExprMap< Exprskolem_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
- Static Protected Attributes inherited from Obj
static bool errsInit = false
static ofstream errs
static bool indentFlag = false

Detailed Description

Definition at line 7 of file LFSCPrinter.h.


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 LFSCObj::cascade_expr(), and print_formula_h().

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

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

Definition at line 48 of file LFSCPrinter.h.

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

Referenced by print_expr(), and print_LFSC().


Member Data Documentation

std::vector<Expr> LFSCPrinter::d_user_assumptions
private

Definition at line 10 of file LFSCPrinter.h.

Referenced by LFSCPrinter(), and print_LFSC().

RefPtr< LFSCConvert > LFSCPrinter::converter
private

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

CommonProofRules* LFSCPrinter::d_common_pf_rules
private

Definition at line 16 of file LFSCPrinter.h.

ExprMap<int> LFSCPrinter::d_print_map
private

Definition at line 18 of file LFSCPrinter.h.

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

ExprMap<bool> LFSCPrinter::d_print_visited_map
private

Definition at line 19 of file LFSCPrinter.h.

Referenced by make_let_map(), and print_LFSC().


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