10 for(
int a=0; a<pf.
arity(); a++ )
21 case EQ: knd_str =
"=";
break;
22 case LE: knd_str =
"<=";
break;
23 case LT: knd_str =
"<";
break;
24 case GE: knd_str =
">=";
break;
25 case GT: knd_str =
">";
break;
26 case DISTINCT: knd_str =
"distinct";
break;
27 case PLUS: knd_str =
"+";
break;
28 case MINUS: knd_str =
"-";
break;
29 case MULT: knd_str =
"*";
break;
30 case AND: knd_str =
"and";
break;
31 case OR: knd_str =
"or";
break;
32 case NOT: knd_str =
"not";
break;
33 case ITE: knd_str =
"ite";
break;
34 case IFF: knd_str =
"iff";
break;
35 case UMINUS: knd_str =
"u-";
break;
40 ose <<
"WARNING: Unknown operator "<<knd;
72 return ( knd==
LE || knd==
LT || knd==
GE || knd==
GT );
79 case LE:
return GT;
break;
80 case LT:
return GE;
break;
81 case GE:
return LT;
break;
82 case GT:
return LE;
break;
92 case EQ:
return 0;
break;
93 case GT:
return 1;
break;
94 case GE:
return 2;
break;
104 case LE:
return GE;
break;
105 case LT:
return GT;
break;
118 return ( knd1==
GT || knd2==
GT ) ?
GT :
GE;
131 s <<
abs( num ) <<
"/" << den;
153 s <<
"(~ " << -n <<
"/" << d <<
")";
174 for(
int a=0; a<e.
arity(); a++ ){
178 else if( !
isFlat( e[a] ) )
189 if( e[0].getKind()==knd ){
192 pe =
Expr( knd, e[0], pe );
196 pe =
Expr( knd, e, pec );