CVC3
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