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 );
void print_rational(const Rational &r, std::ostream &s)
bool getRat(const Expr &e, Rational &r)
Data structure of expressions in CVC3.
bool is_smt_kind(int knd)
const Rational & getRational() const
Get the Rational value out of RATIONAL_EXPR.
bool isFlat(const Expr &e)
void make_flatten_expr(const Expr &e, Expr &pe, int knd)
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
void print_mpq(int num, int den, std::ostream &s)
int get_normalized(int knd, bool isnot)
static void print_error(const char *c, std::ostream &s)
bool is_opposite(int knd)
void print(InputLanguage lang, bool dagify=true) const
Print the expression in the specified format.
void ajr_debug_print(const Expr &pf)
int get_knd_order(int knd)
string kind_to_str(int knd)
void make_flatten_expr_h(const Expr &e, Expr &pe, const Expr &pec, bool pecDef, int knd)
bool is_comparison(int knd)
int get_knd_result(int knd1, int knd2)
void print_rational_divide(const Rational &n, const Rational &d, std::ostream &s)