1 #ifndef LFSC_PRINTER_H_
2 #define LFSC_PRINTER_H_
23 void print_poly_norm(
const Expr& expr, std::ostream& s,
bool pnRat =
true,
bool ratNeg =
false );
void print_formula(const Expr &clause, std::ostream &s)
void print_terms(const Expr &expr, std::ostream &s)
Data structure of expressions in CVC3.
static Expr cascade_expr(const Expr &e)
RefPtr< LFSCConvert > converter
void print_expr(const Expr &expr, std::ostream &s)
void print_LFSC(const Expr &pf_expr)
void make_let_map(const Expr &e)
void print_poly_norm(const Expr &expr, std::ostream &s, bool pnRat=true, bool ratNeg=false)
CommonProofRules * d_common_pf_rules
void set_print_expr(const Expr &expr)
static bool isFormula(const Expr &e)
std::vector< Expr > d_user_assumptions
LFSCPrinter(const Expr pf_expr, Expr qExpr, std::vector< Expr > assumps, int lfscm, CommonProofRules *commonRules)
ExprMap< bool > d_print_visited_map
ExprMap< int > d_print_map
void print_terms_h(const Expr &expr, std::ostream &s)
void print_formula_h(const Expr &clause, std::ostream &s)