CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
search
LFSCLraProof.cpp
Go to the documentation of this file.
1
#include "
LFSCLraProof.h
"
2
3
//LFSCLraAdd ...
4
5
void
LFSCLraAdd::print_pf
( std::ostream& s,
int
ind )
6
{
7
s<<
"(lra_add_"
;
8
s <<
kind_to_str
(
d_op1
);
9
s <<
"_"
;
10
s <<
kind_to_str
(
d_op2
);
11
s <<
" _ _ _ "
;
12
d_children
[0]->
print
(s, ind+1);
13
s<<
" "
;
14
d_children
[1]->
print
(s, ind+1);
15
s<<
")"
;
16
}
17
LFSCProof
*
LFSCLraAdd::Make
(
LFSCProof
* pf1,
LFSCProof
* pf2,
int
op1,
int
op2)
18
{
19
if
( pf1->
isTrivial
() )
20
return
pf2;
21
else
if
( pf2->
isTrivial
() )
22
return
pf1;
23
else
{
24
op1 = pf1->
checkOp
()!=-1 ? pf1->
checkOp
() : op1;
25
op2 = pf2->
checkOp
()!=-1 ? pf2->
checkOp
() : op2;
26
if
(
get_knd_order
( op1 )>
get_knd_order
( op2 ) )
27
return
Make
( pf2, pf1, op2, op1 );
28
else
29
return
new
LFSCLraAdd
( pf1, pf2, op1, op2 );
30
}
31
}
32
33
// LFSCLraAxiom ...
34
35
RefPtr< LFSCProof >
LFSCLraAxiom::eq
;
36
37
LFSCProof
*
LFSCLraAxiom::MakeEq
(){
38
if
( !
eq
.
get
() ){
39
eq
=
new
LFSCLraAxiom
(
EQ
);
40
}
41
return
eq
.
get
();
42
}
43
44
void
LFSCLraAxiom::print_pf
( std::ostream& s,
int
ind )
45
{
46
s<<
"(lra_axiom_"
<<
kind_to_str
(
d_op
);
47
if
(
d_op
!=
EQ
){
48
s <<
" "
;
49
print_rational
(
d_r
, s );
50
}
51
s<<
")"
;
52
}
53
54
//LFSCLraMulC ...
55
56
void
LFSCLraMulC::print_pf
( std::ostream& s,
int
ind )
57
{
58
s <<
"(lra_mul_c_"
<<
kind_to_str
(
d_op
)<<
" _ _ "
;
59
print_rational
(
d_r
, s );
60
s <<
" "
;
61
d_pf
->
print
( s, ind+1 );
62
s <<
")"
;
63
}
64
65
LFSCProof
*
LFSCLraMulC::Make
(
LFSCProof
* pf,
Rational
r,
int
op)
66
{
67
if
( pf->
isTrivial
() || r==1 )
68
return
pf;
69
else
if
( pf->
AsLFSCLraMulC
() ){
70
Rational
rt = r*pf->
AsLFSCLraMulC
()->
d_r
;
71
if
( rt==1 )
72
return
pf->
AsLFSCLraMulC
()->
d_pf
.
get
();
73
else
74
return
new
LFSCLraMulC
( pf->
AsLFSCLraMulC
()->
d_pf
.
get
(), rt, op );
75
}
else
76
return
new
LFSCLraMulC
( pf, r, op );
77
}
78
79
//LFSCLraSub ...
80
81
void
LFSCLraSub::print_pf
( std::ostream& s,
int
ind ){
82
s <<
"(lra_sub_"
<<
kind_to_str
(
d_op1
)<<
"_"
<<
kind_to_str
(
d_op2
)<<
" _ _ _ "
;
83
d_children
[0]->
print
(s, ind+1);
84
s <<
" "
;
85
d_children
[1]->
print
(s, ind+1);
86
s <<
")"
;
87
}
88
89
LFSCProof
*
LFSCLraSub::Make
(
LFSCProof
* pf1,
LFSCProof
* pf2,
int
op1,
int
op2){
90
if
( pf2->
isTrivial
() )
91
return
pf1;
92
else
if
( pf1->
isTrivial
() ){
93
Rational
r =
Rational
( -1 );
94
return
LFSCLraMulC::Make
( pf2, r, op2 );
95
}
else
96
return
new
LFSCLraSub
( pf1, pf2, op1, op2 );
97
}
98
99
//LFSCLraPoly ...
100
101
void
LFSCLraPoly::print_pf
( std::ostream& s,
int
ind ){
102
if
(
d_var
<0 ){
103
s <<
"(lra_not_"
<<
kind_to_str
(
get_normalized
(
d_op
));
104
s <<
"_to_"
<<
kind_to_str
(
get_normalized
(
get_not
(
d_op
) ));
105
s <<
" _ _"
;
106
}
107
s <<
" (poly_form"
;
108
if
(
d_var
<0 )
109
s <<
"_not"
;
110
s <<
" _ _ @pn"
<<
abs
(
d_var
) <<
" "
;
111
d_pf
->
print
( s, ind );
112
s <<
")"
;
113
if
(
d_var
<0 )
114
s <<
")"
;
115
}
116
117
LFSCProof
*
LFSCLraPoly::Make
(
const
Expr
& e,
LFSCProof
* p )
118
{
119
Expr
e1 =
queryAtomic
( e );
120
Expr
eb =
queryAtomic
( e,
true
);
121
if
(
is_eq_kind
( e1.
getKind
() ) )
122
{
123
int
m =
queryM
( e );
124
//get the required term that is needed to normalize
125
Expr
et;
126
if
(
is_opposite
( eb.
getKind
() ) )
127
et =
Expr
(
MINUS
, eb[1], eb[0] );
128
else
129
et =
Expr
(
MINUS
, eb[0], eb[1] );
130
131
//et.print();
132
133
//get the polynomial normalization proof number
134
int
valT =
queryMt
( et );
135
//store it in d_pn_form (this will setup the proper pn*)
136
d_pn_form
[eb] = valT;
137
138
p =
LFSCLraPoly::Make
( p, m, eb.
getKind
() );
139
p->
setChOp
(
get_normalized
( e1.
getKind
() ) );
140
return
p;
141
//if( m<0 )
142
//{
143
// os << "(lra_not_" << kind_to_str(get_normalized( eb.getKind() ));
144
// os << "_to_" << kind_to_str(get_normalized( get_not( eb.getKind() ) ));
145
// os << " _ _";
146
// os2 << ")";
147
//}
148
//os << " (poly_form";
149
//if( m<0 )
150
// os << "_not";
151
//os << " _ _ @pn" << abs( m ) << " ";
152
//os2 << ")";
153
}
154
else
155
{
156
ostringstream ose;
157
ose <<
"ERROR:make_polynomial_proof: Trying to make non-atomic "
<< e1 <<
" "
<< e.
isNot
() <<
std::endl
;
158
ose << e <<
std::endl
;
159
print_error
( ose.str().c_str(), cout );
160
return
NULL;
161
}
162
}
Generated on Sat Aug 3 2013 07:58:27 for CVC3 by
1.8.4