267 for(
int a=1; a<pf.
arity(); a++ ){
293 }
else if( e.
arity()==1 ){
295 }
else if( e.
arity()>0 ){
297 for(
int a=e.
arity()-2; a>=0; a-- ){
324 ose <<
"Unexpected non-discharged assumption " << ce;
330 for(
int a=1; a<e.
arity(); a++ ){
350 for(
int a=0; a<e.
arity(); a++ ){
375 }
else if( e[0].isFalse() ){
379 return Expr(
get_not( e[0].getKind() ), e[0][1], e[0][0] );
400 print_error(
"WARNING: uninitialized e in query", cout );
406 return val*(neg ? -1 : 1 );
423 os <<
"ERROR: cannot make polynomial normalization for " << ce <<
std::endl;
463 ose <<
"Can't pnorm " << ea[0] <<
" " << ea[1] <<
std::endl;
473 if(
getY( e[1], pe2,
false ) ){
490 if(
getY( e[1], pe2,
false,
false ) ){
491 if(
getY( e[0], pe1,
false,
false ) ){
549 pe =
Expr(
EQ, pf[1], pf[2] );
562 pe =
Expr(
IFF, pf[1], pf[3] );
572 pe =
Expr(
EQ, pf[2], pf[4] );
577 pe =
Expr(
EQ, pf[3], pf[2] );
586 pe =
Expr(
IFF, pf[1], pf[2] );
595 if( pf[1].getKind()==
UMINUS ){
596 pe =
Expr(
EQ, pf[1], pf[2] );
598 }
else if( pf[1].getKind()==
NOT ){
599 pe =
Expr(
IFF, pf[1], pf[2] );
611 pe =
Expr( ( pf[1].getKind()==
LE && pf[2].getKind()==
LE ) ?
LE :
LT, pf[1][0], pf[2][1] );
615 pe =
Expr(
EQ, pf[2][0], pf[2][1]);
620 if( pf[1].getKind()==
AND || pf[1].getKind()==
OR || pf[1].getKind()==
IFF ||
is_eq_kind( pf[1].getKind() ) ||
622 pe =
Expr(
IFF, pf[1], pf[2] );
624 }
else if( pf[1].getKind()==
ITE || pf[1].getKind()==
PLUS || pf[1].getKind()==
MINUS || pf[1].getKind()==
MULT ){
625 pe =
Expr(
EQ, pf[1], pf[2] );
669 pe =
Expr(
IFF, pf[1], pf[1] );
671 pe =
Expr(
EQ, pf[1], pf[1] );
700 pe =
Expr(
IFF, pf[1],
Expr(
get_not( pf[1][0].getKind() ), pf[1][0][0], pf[1][0][1] ) );
771 if(pf[1] == e_false){
776 if(pf[1].isNot() && pf[1][0] == pf[2]){
777 pe = e.
iffExpr(pf[2].negate());
786 if(pf[2] == e_false){
791 if(pf[2].isNot() && pf[2][0] == pf[1]){
792 pe = e.
iffExpr(pf[1].negate());
811 ose <<
"What_is_proven, unknown: (" <<
d_rules[pf[0]] <<
"): " << pf[0];