CVC3  2.4.1
LFSCPrinter.h
Go to the documentation of this file.
1 #ifndef LFSC_PRINTER_H_
2 #define LFSC_PRINTER_H_
3 
4 #include "TReturn.h"
5 #include "LFSCConvert.h"
6 
7 class LFSCPrinter : public LFSCObj{
8 private:
9  //user assumptions
10  std::vector <Expr> d_user_assumptions;
11  //the converter object
13  //count for lets
14  int let_i;
15  //common proof rules (need this?)
17  //for printing formulas
20  //make the expr into possible let's
21  void make_let_map( const Expr& e );
22  //print the polynomial normalization
23  void print_poly_norm(const Expr& expr, std::ostream& s, bool pnRat = true, bool ratNeg = false );
24  void print_terms_h(const Expr& expr,std::ostream& s );
25  void print_formula_h(const Expr& clause, std::ostream& s );
26  public:
27  LFSCPrinter(const Expr pf_expr, Expr qExpr, std::vector<Expr> assumps, int lfscm, CommonProofRules* commonRules);
28 
29  //print the LFSC proof for the cvc3 proof
30  void print_LFSC(const Expr& pf_expr);
31 
32  //this is an expression that will be printed
33  void set_print_expr( const Expr& expr ) { make_let_map( expr ); }
34  //print expression
35  void print_expr(const Expr& expr, std::ostream& s){
36  if( isFormula( expr ) )
37  print_formula( expr, s );
38  else
39  print_terms( expr, s );
40  }
41  //print formula
42  void print_formula(const Expr& clause, std::ostream& s ){
43  //if( clause!=cascade_expr( clause, false ) )
44  // cout << "Warning: printing non-cascaded formula " << clause << std::endl;
45  print_formula_h( cascade_expr( clause ), s );
46  }
47  //print term
48  void print_terms(const Expr& expr,std::ostream& s ){
49  //if( expr!=cascade_expr( expr, false ) )
50  // cout << "Warning: printing non-cascaded term " << expr << std::endl;
51  print_terms_h( cascade_expr( expr ), s );
52  }
53 };
54 
55 
56 #endif
void print_formula(const Expr &clause, std::ostream &s)
Definition: LFSCPrinter.h:42
void print_terms(const Expr &expr, std::ostream &s)
Definition: LFSCPrinter.h:48
Data structure of expressions in CVC3.
Definition: expr.h:133
static Expr cascade_expr(const Expr &e)
Definition: LFSCObject.cpp:281
RefPtr< LFSCConvert > converter
Definition: LFSCPrinter.h:12
void print_expr(const Expr &expr, std::ostream &s)
Definition: LFSCPrinter.h:35
void print_LFSC(const Expr &pf_expr)
Definition: LFSCPrinter.cpp:26
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
Definition: LFSCPrinter.h:16
void set_print_expr(const Expr &expr)
Definition: LFSCPrinter.h:33
static bool isFormula(const Expr &e)
Definition: LFSCObject.cpp:514
std::vector< Expr > d_user_assumptions
Definition: LFSCPrinter.h:10
LFSCPrinter(const Expr pf_expr, Expr qExpr, std::vector< Expr > assumps, int lfscm, CommonProofRules *commonRules)
Definition: LFSCPrinter.cpp:4
ExprMap< bool > d_print_visited_map
Definition: LFSCPrinter.h:19
ExprMap< int > d_print_map
Definition: LFSCPrinter.h:18
void print_terms_h(const Expr &expr, std::ostream &s)
void print_formula_h(const Expr &clause, std::ostream &s)