CVC3
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