CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
search
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
12
RefPtr< LFSCConvert >
converter
;
13
//count for lets
14
int
let_i
;
15
//common proof rules (need this?)
16
CommonProofRules
*
d_common_pf_rules
;
17
//for printing formulas
18
ExprMap<int>
d_print_map
;
19
ExprMap<bool>
d_print_visited_map
;
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
Generated on Sat May 18 2013 12:01:25 for CVC3 by
1.8.3.1