6 d_user_assumptions(assumps),
7 d_common_pf_rules(commonRules){
32 cout <<
"(check " <<
endl;
60 cout<<
"(% "<<(*v).first<<
" var_real"<<
endl;
66 cout<<
"(% "<<(*v).first<<
" formula"<<
endl;
115 while( j2 != j2end ){
121 cout <<
"@f" << val <<
" ";
124 cout <<
"@x" << val <<
" ";
140 cout<<
"(% @F"<<m<<
" (th_holds ";
151 cout <<
"(% @T" << (*j).second <<
" (th_holds ";
158 cout <<
"(: bottom" <<
endl;
190 cout <<
"(decl_atom ";
196 cout<<
" (\\ @b"<<(*j).second<<
" (\\ @a"<<(*j).second<<
endl;
203 cout <<
"(decl_term_atom ";
205 cout<<
" (\\ @bt"<<(*j).second<<
" (\\ @at"<<(*j).second<<
endl;
220 cout <<
"(pn_let _ _ ";
223 cout <<
"(\\ @pnt" << (*j).second <<
endl;
232 cout <<
"(poly_norm_" <<
kind_to_str( (*j).first.getKind() ) <<
" _ _ _ @pnt";
234 cout << (*j).second <<
" ";
246 lambda_pf->
print( cout );
251 cout << cparen.str() <<
endl;
257 if(expr.
arity()==2 ){
259 ostringstream cparen;
261 for(
int a=0; a<2; a++ ){
277 s<<
"c_" << ( a==0 ?
"L" :
"R" );
289 ose <<
"ERROR: Multiplying by non-constant " << expr;
312 print_error(
"ERROR: Pn Dividing by non-constant", s );
329 s <<
"(pn_u- _ _ _ ";
343 bool success =
false;
349 s <<
"(pn_var_atom _ _ @at" << val <<
")";
354 ose <<
"Trying to pn_var_atom a non-atomized skolem var " << expr;
361 s <<
"(pn_var_atom _ _ @at" << val <<
")";
364 ose <<
"Trying to pn_var_atom a non-atomized ITE " << expr;
367 }
else if(expr.
isVar()){
368 s<<
"(pn_var "<<expr<<
")";
372 ose<<
"ERROR printing polynomial norm for "<<expr;
386 }
else if(expr.
isVar()){
387 s<<
"(a_var_real "<<expr<<
")";
388 }
else if(expr.
arity()==2 ){
395 print_error(
"ERROR: Dividing by non constant", s );
423 cout <<
"cannot determine rational " << expr <<
endl;
431 }
else if(expr.
arity()>2){
433 vector<Expr> kids = expr.
getKids();
434 vector<Expr>::iterator i = kids.begin(), iend= kids.end();
442 for(
int j=0; j<expr.
arity();j++){
448 os <<
"ERROR printing term "<<expr<<
" "<<expr.
arity();
457 }
else if(clause.
isNot()){
461 }
else if(clause.
isOr()){
467 }
else if(clause.
isAnd()){
473 }
else if(clause.
isImpl()){
479 }
else if(clause.
isIff()){
504 }
else if( clause.
isTrue() ){
513 for(
int a=0; a<(int)e.
arity(); a++ ){