29 print_warning(
"Warning: printing out lambda abstracted proof more than once");
30 #ifdef IGNORE_PRINT_MULTI_LAMBDA
51 print_warning(
"ERROR: printing out lambda abstracted proof more than once" );
52 #ifdef IGNORE_PRINT_MULTI_LAMBDA
70 void LFSCProof::calcL( std::vector< int >& lget, std::vector< int >& lgetu ){
107 #ifdef PRINT_MAJOR_METHODS
108 cout <<
";[M] CNF " << reason <<
" " << pos <<
std::endl;
128 ostringstream oss1, oss2;
130 for(
int a=(form.
arity()-2); a>=0; a-- ){
131 int m1 =
queryM( form[a] );
132 oss1 <<
"(or_elim_1 _ _ ";
133 oss1 << ( m1<0 ?
"(not_not_intro _ " :
"" );
134 oss1 <<
"@v" <<
abs( m1 );
135 oss1 << ( m1<0 ?
") " :
" " );
141 for(
int a=0; a<(form.
arity()-1); a++ ){
153 for(
int a=0; a<form.
arity(); a++ ){
154 if( a<(form.
arity()-1))
155 os1 <<
"(and_intro _ _ ";
157 if( a<(form.
arity()-1)){
162 os2 <<
" @v" <<
abs(m) <<
")";
165 for(
int a=0; a<form.
arity(); a++ ){
171 std::vector< Expr > assumes;
176 os1 <<
"(and_intro _ _ ";
177 os1 <<
"@v" <<
abs(
queryM( curr[0] ) ) <<
" ";
179 assumes.push_back( curr[0] );
182 os2 <<
" @v" <<
abs(m) <<
")";
184 for(
int a=0; a<(int)assumes.size(); a++ ){
206 os <<
"(impl_elim _ _ @v" <<
abs( m1 ) <<
" @v" <<
abs( m ) <<
")";
225 os <<
"(ite_elim_2" << (m1<0 ?
"n" :
"" );
226 os <<
" _ _ _ @v" <<
abs( m1 ) <<
" @v" <<
abs( m ) <<
")";
236 os <<
"(not_ite_elim_2 _ _ _ @v" << (m1<0 ?
"n" :
"" );
237 os <<
abs( m1 ) <<
" @v" <<
abs( m ) <<
")";
248 os <<
"(not_ite_elim_1 _ _ _ @v" <<
abs( m1 ) <<
" @v" <<
abs( m ) <<
")";
260 os <<
" _ _ _ @v" <<
abs( m1 ) <<
" @v" <<
abs( m ) <<
")";
270 os <<
"(not_ite_elim_3 _ _ _ @v" <<
abs( m2 ) <<
" @v" <<
abs( m ) <<
")";
282 os <<
" _ _ _ @v" <<
abs( m2 ) <<
" @v" <<
abs( m ) <<
")";
300 os <<
"(not_iff_elim_1 _ _ @v" <<
abs( m1 ) <<
" @v" <<
abs( m ) <<
")";
310 os <<
"(not_iff_elim_2 _ _ @v" <<
abs( m1 ) <<
" @v" <<
abs( m ) <<
")";
320 os <<
"(impl_elim _ _ @v" <<
abs( m1 ) <<
"(iff_elim_1 _ _ @v" <<
abs( m ) <<
"))";
331 os <<
"(impl_elim _ _ @v" <<
abs( m2 ) <<
"(iff_elim_2 _ _ @v" <<
abs( m ) <<
"))";
343 ostringstream os1, os2;
344 if( form[pos].isNot() )
345 os1 <<
"(not_not_elim _ ";
346 os1 <<
"(or_elim" << ( (pos==form.
arity()) ?
"_end" :
"" );
347 os1 <<
" _ _ " << pos <<
" ";
349 if( form[pos].isNot() )
367 ose <<
"CNF, " << reason <<
" unknown position = " << pos <<
std::endl;
376 ostringstream os1, os2;
377 os1 <<
"(not_not_elim _ ";
386 ostringstream os1, os2;
389 for(
int a=0; a<numHoles; a++ )
400 for(
int a=0; a<n; a++ ){
404 print_error(
"WARNING: and elim out of range", cout );
409 ostringstream os1, os2;
411 if( n==form.
arity()-1 )
413 os1 <<
" _ _ " << n <<
" ";