#include <LFSCPrinter.h>
Inherits LFSCObj.
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)
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
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 | ||
| ) |
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.
Member Function Documentation
| void LFSCPrinter::make_let_map | ( | const Expr & | e | ) | [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().
| 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(), 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().
| void LFSCPrinter::print_terms_h | ( | const Expr & | expr, |
| std::ostream & | s | ||
| ) | [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().
| 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::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(), 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(), Obj::indentFlag, LFSCObj::input_preds, LFSCObj::input_vars, LFSCObj::isFormula(), kind_to_str(), LFSCObj::lfsc_mode, make_let_map(), LFSCObj::pntNeeded, print_formula(), print_poly_norm(), print_terms(), and LFSCObj::queryM().
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 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:
