|
CVC3
|
00001 #ifndef UTIL_H_ 00002 #define UTIL_H_ 00003 00004 #include "Object.h" 00005 00006 // helper utility functions 00007 void ajr_debug_print( const Expr& pf ); 00008 string kind_to_str(int knd ); 00009 bool is_eq_kind( int knd ); 00010 bool is_smt_kind( int knd ); 00011 00012 //equation types ( a ~ b ) that are normalized to (b-a) ~' 0 00013 bool is_opposite( int knd ); 00014 bool is_comparison( int knd ); 00015 int get_not( int knd ); 00016 00017 //order in LFSC signature for rules when order does not matter (such as lra_add) 00018 int get_knd_order( int knd ); 00019 int get_normalized( int knd, bool isnot = false ); 00020 00021 //should only be called on normalized ops 00022 int get_knd_result( int knd1, int knd2 ); 00023 00024 //print helpers 00025 void print_mpq(int num, int den, std::ostream& s ); 00026 void print_rational( const Rational& r, std::ostream& s ); 00027 void print_rational_divide( const Rational& n, const Rational& d, std::ostream& s ); 00028 00029 bool getRat( const Expr& e, Rational& r ); 00030 bool isFlat( const Expr& e ); 00031 void make_flatten_expr( const Expr& e, Expr& pe, int knd ); 00032 00033 #endif
1.7.3