9 d_lfsc_pf(lfsc_pf), d_c( r ), d_provesY(pvY){
11 for(
int a=0; a<(int)L.size(); a++ )
12 d_L.push_back( L[a] );
13 for(
int a=0; a<(int)Lused.size(); a++ )
16 #ifdef DEBUG_MEM_STATS
17 static int counter = 0;
19 cout <<
"make a tret " << counter <<
std::endl;
37 void TReturn::getL( std::vector< int >& lget, std::vector< int >& lgetu ){
39 std::vector< int >::iterator i;
40 for(
int a=0; a<(int)
d_L.size(); a++ ){
41 i = std::find( lget.begin(), lget.end(),
d_L[a] );
43 lget.push_back(
d_L[a] );
46 for(
int a=0; a<(int)
d_L_used.size(); a++ ){
47 i = std::find( lgetu.begin(), lgetu.end(),
d_L_used[a] );
56 void TReturn::calcL( std::vector< int >& lget, std::vector< int >& lgetu ){
63 std::vector< int >::iterator i;
64 for(
int a=0; a<(int)
d_L.size(); a++ ){
65 i = std::find( lget.begin(), lget.end(),
d_L[a] );
67 lget.push_back(
d_L[a] );
70 for(
int a=0; a<(int)
d_L_used.size(); a++ ){
71 i = std::find( lgetu.begin(), lgetu.end(),
d_L_used[a] );
114 os << pf1[0] <<
" " << pf2[0] <<
std::endl;
130 std::vector< int > emptyL;
131 std::vector< int > emptyLUsed;
132 t1->
getL( emptyL, emptyLUsed );
137 cout <<
"normalizing tr " << t1->
getProvesY() <<
" to " << y <<
" rev_pol = " << rev_pol <<
std::endl;
181 }
else if( e[0]==e[1] ){
182 ostringstream os1, os2;
187 emptyL, emptyLUsed,
nullRat,
false, 0 );
190 #ifdef PRINT_MAJOR_METHODS
191 cout <<
";[M]: Normalize 1 to 0, iff" <<
std::endl;
197 ostringstream os1, os2;
198 os1 <<
"(" << ( e[0].
getKind()==
NOT ?
"not_to_iff" :
"iff_not_false" );
202 emptyL, emptyLUsed,
nullRat,
false, 0 );
204 else if( e[1].isTrue() )
207 ostringstream os1, os2;
208 os1 <<
"(iff_true _ ";
211 emptyL, emptyLUsed,
nullRat,
false, 0 );
226 ostringstream os1, os2, os3, os4;
227 os1 <<
"(impl_elim _ _ ";
228 os2 <<
"(impl_intro _ _ (\\ @V0 (iff_intro _ _ ";
231 std::vector< RefPtr< LFSCProof > > pfs;
233 pfs.push_back( ti1->getLFSCProof() );
234 pfs.push_back( ti2->getLFSCProof() );
235 std::vector< string > strs;
236 strs.push_back( os1.str() );
237 strs.push_back( os2.str() );
238 strs.push_back( os3.str() );
239 strs.push_back( os4.str() );
253 ostringstream os1, os2;
254 os1 <<
"(iff_elim_1 _ _ ";
272 int val1 =
queryM( e[0] );
273 int val2 =
queryM( e[1] );
279 os <<
"(impl_refl_atom" << (val1<0 ?
"_not" :
"" );
280 os <<
" _ _ @a" <<
abs( val1 ) <<
")";
283 emptyL, emptyLUsed,
nullRat,
false, 2 );
287 #ifdef PRINT_MAJOR_METHODS
288 cout <<
";[M]: Normalize 1 to 2, iff/impl double logical iff" <<
std::endl;
292 ose <<
"Warning: normalize logical atoms, not equal ";
297 os <<
"impl_refl_" << ( eatom2.
isFalse() ?
"false" :
"true" );
299 emptyL, emptyLUsed,
nullRat,
false, 2 );
301 else if( eatom2.
isTrue() )
304 ostringstream oss1, oss2;
305 oss1 <<
"(iff_true_impl _ ";
308 emptyL, emptyLUsed,
nullRat,
false, 2 );
312 #ifdef PRINT_MAJOR_METHODS
324 ostringstream oss1, oss2;
327 oss1 <<
"(impl_intro";
328 oss1 <<
" _ _ (\\ @v" <<
abs( val1 ) <<
" ";
329 oss1 <<
"(bottom_elim ";
337 t1 =
new TReturn( p.get(), emptyL, emptyLUsed,
nullRat,
false, 2 );
342 #ifdef PRINT_MAJOR_METHODS
347 ostringstream os1, os2;
350 os1 <<
"(impl_intro";
352 os1 <<
"@v" <<
abs( val1 ) <<
" ";
384 t1 =
new TReturn( p.get(), emptyL, emptyLUsed,
nullRat,
false, 2 );
389 ose <<
"NTret 12 could not handle " << eatom1 <<
" " << eatom2;
405 ose <<
"proven_expr = " << e <<
std::endl;
412 #ifdef IGNORE_NORMALIZE
431 std::vector< int > emptyL;
432 std::vector< int > emptyLUsed;
433 t1->
getL( emptyL, emptyLUsed );
437 #ifdef PRINT_MAJOR_METHODS
438 cout <<
";[M]: Normalize 1 to " << y <<
", simplify case" <<
std::endl;
445 #ifdef PRINT_MAJOR_METHODS
446 cout <<
";[M]: Normalize 1 to " << y <<
", iff/impl, atom" <<
std::endl;
473 t1 =
new TReturn( p.get(), emptyL, emptyLUsed,
nullRat,
false, y );