CVC3  2.4.1
Util.h
Go to the documentation of this file.
1 #ifndef UTIL_H_
2 #define UTIL_H_
3 
4 #include "Object.h"
5 
6 // helper utility functions
7 void ajr_debug_print( const Expr& pf );
8 string kind_to_str(int knd );
9 bool is_eq_kind( int knd );
10 bool is_smt_kind( int knd );
11 
12 //equation types ( a ~ b ) that are normalized to (b-a) ~' 0
13 bool is_opposite( int knd );
14 bool is_comparison( int knd );
15 int get_not( int knd );
16 
17 //order in LFSC signature for rules when order does not matter (such as lra_add)
18 int get_knd_order( int knd );
19 int get_normalized( int knd, bool isnot = false );
20 
21 //should only be called on normalized ops
22 int get_knd_result( int knd1, int knd2 );
23 
24 //print helpers
25 void print_mpq(int num, int den, std::ostream& s );
26 void print_rational( const Rational& r, std::ostream& s );
27 void print_rational_divide( const Rational& n, const Rational& d, std::ostream& s );
28 
29 bool getRat( const Expr& e, Rational& r );
30 bool isFlat( const Expr& e );
31 void make_flatten_expr( const Expr& e, Expr& pe, int knd );
32 
33 #endif
bool getRat(const Expr &e, Rational &r)
Definition: Util.cpp:158
Data structure of expressions in CVC3.
Definition: expr.h:133
bool is_comparison(int knd)
Definition: Util.cpp:70
void print_rational_divide(const Rational &n, const Rational &d, std::ostream &s)
Definition: Util.cpp:149
bool is_smt_kind(int knd)
Definition: Util.cpp:60
int get_normalized(int knd, bool isnot=false)
Definition: Util.cpp:100
void ajr_debug_print(const Expr &pf)
Definition: Util.cpp:8
string kind_to_str(int knd)
Definition: Util.cpp:17
bool is_opposite(int knd)
Definition: Util.cpp:66
void make_flatten_expr(const Expr &e, Expr &pe, int knd)
Definition: Util.cpp:203
int get_not(int knd)
Definition: Util.cpp:75
void print_mpq(int num, int den, std::ostream &s)
Definition: Util.cpp:127
int get_knd_result(int knd1, int knd2)
Definition: Util.cpp:111
int get_knd_order(int knd)
Definition: Util.cpp:89
bool is_eq_kind(int knd)
Definition: Util.cpp:47
bool isFlat(const Expr &e)
Definition: Util.cpp:173
void print_rational(const Rational &r, std::ostream &s)
Definition: Util.cpp:136