CVC3
2.4.1
|
#include <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::printer, CVC3::Expr::isFalse(), d_user_assumptions, LFSCObj::cascade_expr(), NOT, Obj::initialize(), let_i, and converter.
void LFSCPrinter::make_let_map | ( | const Expr & | e | ) | [private] |
Definition at line 511 of file LFSCPrinter.cpp.
References CVC3::Expr::arity(), d_print_visited_map, CVC3::ExprMap::find(), CVC3::ExprMap::end(), d_print_map, and let_i.
Referenced by print_LFSC(), and set_print_expr().
void LFSCPrinter::print_poly_norm | ( | const Expr & | expr, |
std::ostream & | s, | ||
bool | pnRat = true , |
||
bool | ratNeg = false |
||
) | [private] |
Definition at line 255 of file LFSCPrinter.cpp.
References CVC3::Expr::arity(), CVC3::Expr::getKind(), CVC3::MULT, CVC3::UMINUS, LFSCObj::cvc3_mimic, CVC3::Expr::isRational(), CVC3::DIVIDE, Obj::print_error(), CVC3::isRational(), CVC3::Expr::getRational(), print_rational_divide(), kind_to_str(), print_rational(), SKOLEM_VAR, LFSCObj::skolem_vars, CVC3::ExprMap::find(), CVC3::ExprMap::end(), LFSCObj::d_terms, ITE, and CVC3::Expr::isVar().
Referenced by print_LFSC().
void LFSCPrinter::print_terms_h | ( | const Expr & | expr, |
std::ostream & | s | ||
) | [private] |
Definition at line 378 of file LFSCPrinter.cpp.
References d_print_map, CVC3::Expr::isRational(), print_rational(), CVC3::Expr::getRational(), CVC3::Expr::isVar(), CVC3::Expr::arity(), CVC3::Expr::getKind(), CVC3::DIVIDE, CVC3::isRational(), print_rational_divide(), Obj::print_error(), kind_to_str(), ITE, print_formula_h(), CVC3::UMINUS, LFSCObj::cvc3_mimic, std::endl(), and CVC3::Expr::getKids().
Referenced by print_formula_h(), and print_terms().
void LFSCPrinter::print_formula_h | ( | const Expr & | clause, |
std::ostream & | s | ||
) | [private] |
Definition at line 453 of file LFSCPrinter.cpp.
References d_print_map, CVC3::Expr::isNot(), CVC3::Expr::isOr(), CVC3::Expr::isAnd(), CVC3::Expr::isImpl(), CVC3::Expr::isIff(), CVC3::Expr::getKind(), ITE, is_eq_kind(), kind_to_str(), is_smt_kind(), print_terms_h(), CVC3::Expr::isFalse(), and CVC3::Expr::isTrue().
Referenced by print_terms_h(), and print_formula().
void LFSCPrinter::print_LFSC | ( | const Expr & | pf_expr | ) |
Definition at line 26 of file LFSCPrinter.cpp.
References std::endl(), d_user_assumptions, LFSCObj::cascade_expr(), LFSCObj::queryM(), LFSCObj::d_assump_map, LFSCObj::collect_vars(), LFSCObj::input_vars, CVC3::ExprMap::begin(), CVC3::ExprMap::end(), LFSCObj::input_preds, LFSCObj::define_skolem_vars(), converter, make_let_map(), LFSCObj::d_trusted, LFSCObj::d_formulas_printed, d_print_visited_map, d_print_map, LFSCObj::isFormula(), print_formula(), print_terms(), CVC3::ExprMap::empty(), LFSCObj::d_formulas, LFSCObj::d_terms, LFSCObj::d_pn_form, LFSCObj::pntNeeded, LFSCObj::d_pn, LFSCObj::cvc3_mimic, print_poly_norm(), kind_to_str(), CVC3::abs(), LFSCObj::lfsc_mode, and Obj::indentFlag.
Referenced by CVC3::SearchEngineTheoremProducer::satProof().
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().
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 print_LFSC(), print_terms_h(), print_formula_h(), and make_let_map().
ExprMap<bool> LFSCPrinter::d_print_visited_map [private] |
Definition at line 19 of file LFSCPrinter.h.
Referenced by print_LFSC(), and make_let_map().