CVC3
2.4.1
|
#include <LFSCPrinter.h>
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) |
![]() | |
LFSCObj () | |
![]() | |
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< Expr > | d_user_assumptions |
RefPtr< LFSCConvert > | converter |
int | let_i |
CommonProofRules * | d_common_pf_rules |
ExprMap< int > | d_print_map |
ExprMap< bool > | d_print_visited_map |
Definition at line 7 of file LFSCPrinter.h.
LFSCPrinter::LFSCPrinter | ( | const Expr | pf_expr, |
Expr | qExpr, | ||
std::vector< Expr > | assumps, | ||
int | lfscm, | ||
CommonProofRules * | commonRules | ||
) |
Definition at line 4 of file LFSCPrinter.cpp.
References LFSCObj::cascade_expr(), converter, d_user_assumptions, Obj::initialize(), CVC3::Expr::isFalse(), let_i, NOT, and LFSCObj::printer.
|
private |
Definition at line 511 of file LFSCPrinter.cpp.
References CVC3::Expr::arity(), d_print_map, d_print_visited_map, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), and let_i.
Referenced by print_LFSC(), and set_print_expr().
|
private |
Definition at line 255 of file LFSCPrinter.cpp.
References CVC3::Expr::arity(), LFSCObj::cvc3_mimic, LFSCObj::d_terms, CVC3::DIVIDE, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::isRational(), CVC3::Expr::isRational(), CVC3::Expr::isVar(), ITE, kind_to_str(), CVC3::MULT, Obj::print_error(), print_rational(), print_rational_divide(), SKOLEM_VAR, LFSCObj::skolem_vars, and CVC3::UMINUS.
Referenced by print_LFSC().
|
private |
Definition at line 378 of file LFSCPrinter.cpp.
References CVC3::Expr::arity(), LFSCObj::cvc3_mimic, d_print_map, CVC3::DIVIDE, std::endl(), CVC3::Expr::getKids(), CVC3::Expr::getKind(), CVC3::Expr::getRational(), CVC3::isRational(), CVC3::Expr::isRational(), CVC3::Expr::isVar(), ITE, kind_to_str(), Obj::print_error(), print_formula_h(), print_rational(), print_rational_divide(), and CVC3::UMINUS.
Referenced by print_formula_h(), and print_terms().
|
private |
Definition at line 453 of file LFSCPrinter.cpp.
References d_print_map, CVC3::Expr::getKind(), is_eq_kind(), is_smt_kind(), CVC3::Expr::isAnd(), CVC3::Expr::isFalse(), CVC3::Expr::isIff(), CVC3::Expr::isImpl(), CVC3::Expr::isNot(), CVC3::Expr::isOr(), CVC3::Expr::isTrue(), ITE, kind_to_str(), and print_terms_h().
Referenced by print_formula(), and print_terms_h().
void LFSCPrinter::print_LFSC | ( | const Expr & | pf_expr | ) |
Definition at line 26 of file LFSCPrinter.cpp.
References CVC3::abs(), CVC3::ExprMap< Data >::begin(), LFSCObj::cascade_expr(), LFSCObj::collect_vars(), LFSCConvert::convert(), converter, LFSCObj::cvc3_mimic, LFSCObj::d_assump_map, LFSCObj::d_formulas, LFSCObj::d_formulas_printed, LFSCObj::d_pn, LFSCObj::d_pn_form, d_print_map, d_print_visited_map, LFSCObj::d_terms, LFSCObj::d_trusted, d_user_assumptions, LFSCObj::define_skolem_vars(), CVC3::ExprMap< Data >::empty(), CVC3::ExprMap< Data >::end(), std::endl(), LFSCConvert::getLFSCProof(), Obj::indentFlag, LFSCObj::input_preds, LFSCObj::input_vars, LFSCObj::isFormula(), kind_to_str(), LFSCObj::lfsc_mode, make_let_map(), LFSCObj::pntNeeded, LFSCProof::print(), print_formula(), print_poly_norm(), LFSCProof::print_structure(), print_terms(), and LFSCObj::queryM().
Referenced by CVC3::SearchEngineTheoremProducer::satProof().
|
inline |
Definition at line 33 of file LFSCPrinter.h.
References make_let_map().
Referenced by LFSCProofExpr::initialize().
|
inline |
Definition at line 35 of file LFSCPrinter.h.
References LFSCObj::isFormula(), print_formula(), and print_terms().
Referenced by LFSCProofExpr::print_pf().
|
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().
|
inline |
Definition at line 48 of file LFSCPrinter.h.
References LFSCObj::cascade_expr(), and print_terms_h().
Referenced by print_expr(), and print_LFSC().
|
private |
Definition at line 10 of file LFSCPrinter.h.
Referenced by LFSCPrinter(), and print_LFSC().
|
private |
Definition at line 12 of file LFSCPrinter.h.
Referenced by LFSCPrinter(), and print_LFSC().
|
private |
Definition at line 14 of file LFSCPrinter.h.
Referenced by LFSCPrinter(), and make_let_map().
|
private |
Definition at line 16 of file LFSCPrinter.h.
|
private |
Definition at line 18 of file LFSCPrinter.h.
Referenced by make_let_map(), print_formula_h(), print_LFSC(), and print_terms_h().
|
private |
Definition at line 19 of file LFSCPrinter.h.
Referenced by make_let_map(), and print_LFSC().