CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
search
LFSCObject.h
Go to the documentation of this file.
1
#ifndef LFSC_OBJ_H_
2
#define LFSC_OBJ_H_
3
4
#include "
Object.h
"
5
#include "
Util.h
"
6
7
class
LFSCPrinter
;
8
9
class
LFSCObj
:
public
Obj
10
{
11
public
:
12
LFSCObj
(){}
13
static
void
initialize
(
const
Expr
& pf_expr,
int
lfscm );
14
protected
:
15
//the printer object
16
static
LFSCPrinter
*
printer
;
17
//counters
18
static
int
formula_i
;
19
static
int
trusted_i
;
20
static
int
term_i
;
21
static
int
tnorm_i
;
22
//options for the conversion
23
static
int
lfsc_mode
;
24
static
bool
debug_conv
;
25
static
bool
debug_var
;
26
static
bool
cvc3_mimic
;
27
static
bool
cvc3_mimic_input
;
28
//null rational
29
static
Rational
nullRat
;
30
//get number of nodes
31
static
ExprMap< int >
nnode_map
;
32
static
int
getNumNodes
(
const
Expr
& pf,
bool
recount =
false
);
33
//cascade expr
34
static
ExprMap< Expr >
cas_map
;
35
static
Expr
cascade_expr
(
const
Expr
& e );
36
//skolem variables
37
static
ExprMap< Expr >
skolem_vars
;
//with the expr they point to
38
static
ExprMap< bool >
temp_visited
;
39
static
void
define_skolem_vars
(
const
Expr
& e );
40
//is variable
41
static
bool
isVar
(
const
Expr
& e );
42
//collect free variables
43
static
void
collect_vars
(
const
Expr
& e,
bool
readPred =
true
);
44
protected
:
45
// this is actually the M map <formula, int> where M = {v_i -> non-negated formula}
46
static
ExprMap<int>
d_formulas
;
47
//trusted formulas
48
static
ExprMap<int>
d_trusted
;
49
// this is the M_t map <term, int> where M_t = { v_i -> term }
50
static
ExprMap<int>
d_pn
;
51
//this is the equations that will use the d_pn map. They are mapped to the index of the pn_i they will use
52
static
ExprMap<int>
d_pn_form
;
53
//similar to m, but with terms
54
static
ExprMap<int>
d_terms
;
55
//input variables
56
static
ExprMap<bool>
input_vars
;
57
//input predicates
58
static
ExprMap<bool>
input_preds
;
59
//pnt that are needed to print
60
static
std::map< int, bool >
pntNeeded
;
61
//atoms that must be printed
62
static
ExprMap<bool>
d_formulas_printed
;
63
//original proof expression
64
static
Expr
d_pf_expr
;
65
//assumptions
66
static
ExprMap<bool>
d_assump_map
;
67
protected
:
68
//eliminate not not
69
static
Expr
queryElimNotNot
(
const
Expr
& expr);
70
//get base will get you the base formula, i.e. ~( a = b ) returns ( a = b )
71
//get base = false will get you the equivalent atomic, i.e. ~( a = b ) returns ( b != a )
72
static
Expr
queryAtomic
(
const
Expr
& expr,
bool
getBase =
false
);
73
//returns a integer v, +v means M( v ) = expr, -v means M( v ) = expr', where expr := NOT expr'
74
//add is whether or not to add it to M, or just query
75
static
int
queryM
(
const
Expr
& expr,
bool
add =
true
,
bool
trusted =
false
);
76
//returns an integer v, where M_t( v ) = expr
77
static
int
queryMt
(
const
Expr
& expr);
78
//similar to m, but this time it is with terms
79
static
int
queryT
(
const
Expr
& e );
80
//get Y
81
static
bool
getY
(
const
Expr
& e,
Expr
& pe,
bool
doIff =
true
,
bool
doLogic =
true
);
82
//is this expr a formula
83
static
bool
isFormula
(
const
Expr
& e );
84
//can this expr be polynomial normalized
85
static
bool
can_pnorm
(
const
Expr
& e );
86
//what is proven
87
static
bool
what_is_proven
(
const
Expr
& pf,
Expr
& pe );
88
protected
:
89
// differentiate between variables and rules
90
static
ExprMap<bool>
d_rules
;
91
// boolean resultion rules
92
static
Expr
d_bool_res_str
;
93
static
Expr
d_assump_str
;
94
// arithmetic rules
95
static
Expr
d_iff_mp_str
;
96
static
Expr
d_impl_mp_str
;
97
static
Expr
d_iff_trans_str
;
98
static
Expr
d_real_shadow_str
;
99
static
Expr
d_cycle_conflict_str
;
100
static
Expr
d_real_shadow_eq_str
;
101
static
Expr
d_basic_subst_op_str
;
102
static
Expr
d_mult_ineqn_str
;
103
static
Expr
d_right_minus_left_str
;
104
static
Expr
d_eq_trans_str
;
105
static
Expr
d_eq_symm_str
;
106
static
Expr
d_canon_plus_str
;
107
static
Expr
d_refl_str
;
108
static
Expr
d_cnf_convert_str
;
109
static
Expr
d_learned_clause_str
;
110
static
Expr
d_minus_to_plus_str
;
111
static
Expr
d_plus_predicate_str
;
112
static
Expr
d_negated_inequality_str
;
113
static
Expr
d_flip_inequality_str
;
114
static
Expr
d_optimized_subst_op_str
;
115
static
Expr
d_iff_true_elim_str
;
116
static
Expr
d_basic_subst_op1_str
;
117
static
Expr
d_basic_subst_op0_str
;
118
static
Expr
d_canon_mult_str
;
119
static
Expr
d_canon_invert_divide_str
;
120
static
Expr
d_iff_true_str
;
121
static
Expr
d_mult_eqn_str
;
122
static
Expr
d_rewrite_eq_symm_str
;
123
static
Expr
d_implyWeakerInequality_str
;
124
static
Expr
d_implyWeakerInequalityDiffLogic_str
;
125
static
Expr
d_imp_mp_str
;
126
static
Expr
d_rewrite_implies_str
;
127
static
Expr
d_rewrite_or_str
;
128
static
Expr
d_rewrite_and_str
;
129
static
Expr
d_rewrite_iff_symm_str
;
130
static
Expr
d_iff_not_false_str
;
131
static
Expr
d_iff_false_str
;
132
static
Expr
d_iff_false_elim_str
;
133
static
Expr
d_not_to_iff_str
;
134
static
Expr
d_not_not_elim_str
;
135
static
Expr
d_const_predicate_str
;
136
static
Expr
d_rewrite_not_not_str
;
137
static
Expr
d_rewrite_not_true_str
;
138
static
Expr
d_rewrite_not_false_str
;
139
static
Expr
d_if_lift_rule_str
;
140
static
Expr
d_CNFITE_str
;
141
static
Expr
d_var_intro_str
;
142
static
Expr
d_int_const_eq_str
;
143
static
Expr
d_rewrite_eq_refl_str
;
144
static
Expr
d_iff_symm_str
;
145
static
Expr
d_rewrite_iff_str
;
146
static
Expr
d_implyNegatedInequality_str
;
147
static
Expr
d_uminus_to_mult_str
;
148
static
Expr
d_lessThan_To_LE_rhs_rwr_str
;
149
static
Expr
d_rewrite_ite_same_str
;
150
static
Expr
d_andE_str
;
151
static
Expr
d_implyEqualities_str
;
152
static
Expr
d_addInequalities_str
;
153
//CNF rules
154
static
Expr
d_CNF_str
;
155
static
Expr
d_cnf_add_unit_str
;
156
static
Expr
d_minisat_proof_str
;
157
//reasons for CNF
158
static
Expr
d_or_final_s
;
159
static
Expr
d_and_final_s
;
160
static
Expr
d_ite_s
;
161
static
Expr
d_iff_s
;
162
static
Expr
d_imp_s
;
163
static
Expr
d_or_mid_s
;
164
static
Expr
d_and_mid_s
;
165
};
166
167
#endif
Generated on Sun Aug 5 2012 13:18:43 for CVC3 by
1.8.1.2