CVC3  2.4.1
Util.cpp
Go to the documentation of this file.
1 #include "Util.h"
2 
3 bool Obj::errsInit = false;
4 ofstream Obj::errs;
5 bool Obj::indentFlag = false;
6 
7 // helper utility functions
8 void ajr_debug_print( const Expr& pf )
9 {
10  for( int a=0; a<pf.arity(); a++ )
11  {
12  cout << a << ": ";
13  pf[a].print();
14  }
15 }
16 
17 string kind_to_str(int knd ){
18 
19  string knd_str;
20  switch(knd){
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;
36  default:
37  {
38  knd_str="Unknown";
39  ostringstream ose;
40  ose << "WARNING: Unknown operator "<<knd;
41  Obj::print_error( ose.str().c_str(), cout );
42  }
43  }
44  return knd_str;
45 }
46 
47 bool is_eq_kind( int knd )
48 {
49  switch(knd){
50  case EQ:
51  case LE:
52  case LT:
53  case GE:
54  case GT:
55  case DISTINCT:return true;break;
56  }
57  return false;
58 }
59 
60 bool is_smt_kind( int knd )
61 {
62  return knd==EQ || knd==DISTINCT;
63 }
64 
65 //equation types ( a ~ b ) that are normalized to (b-a) ~' 0
66 bool is_opposite( int knd )
67 {
68  return ( knd==LE || knd==LT || knd==DISTINCT );
69 }
70 bool is_comparison( int knd )
71 {
72  return ( knd==LE || knd==LT || knd==GE || knd==GT );
73 }
74 
75 int get_not( int knd )
76 {
77  switch(knd){
78  case EQ: return DISTINCT; break;
79  case LE: return GT; break;
80  case LT: return GE; break;
81  case GE: return LT; break;
82  case GT: return LE; break;
83  case DISTINCT: return EQ; break;
84  }
85  return knd;
86 }
87 
88 //order in LFSC signature for rules when order does not matter (such as lra_add)
89 int get_knd_order( int knd )
90 {
91  switch(knd){
92  case EQ: return 0; break;
93  case GT: return 1; break;
94  case GE: return 2; break;
95  case DISTINCT: return 3; break;
96  }
97  return 4;
98 }
99 
100 int get_normalized( int knd, bool isnot )
101 {
102  if( isnot ) return get_normalized( get_not( knd ) );
103  switch(knd){
104  case LE: return GE; break;
105  case LT: return GT; break;
106  }
107  return knd;
108 }
109 
110 //should only be called on normalized ops
111 int get_knd_result( int knd1, int knd2 )
112 {
113  if( knd1==EQ )
114  return knd2;
115  if( knd2==EQ )
116  return knd1;
117  if( knd1!=DISTINCT && knd2!=DISTINCT ){
118  return ( knd1==GT || knd2==GT ) ? GT : GE;
119  }
120  ostringstream ose;
121  ose << "Unknown get_op_result. " << kind_to_str( knd1 ) << " " << kind_to_str( knd2 ) << std::endl;
122  Obj::print_error( ose.str().c_str(), cout );
123  return -1;
124 }
125 
126 // print helpers
127 void print_mpq(int num, int den, std::ostream& s )
128 {
129  if( num<0 )
130  s << "(~ ";
131  s << abs( num ) << "/" << den;
132  if( num<0 )
133  s << ")";
134 }
135 
136 void print_rational( const Rational& r, std::ostream& s )
137 {
138  //print_mpq( r.getNumerator().getInt(), r.getDenominator().getInt(), s );
139  if( r<0 )
140  s << "(~ " << -r;
141  else
142  s << r;
143  if( r.isInteger() )
144  s << "/1";
145  if( r<0 )
146  s << ")";
147 }
148 
149 void print_rational_divide( const Rational& n, const Rational& d, std::ostream& s )
150 {
151  //print_mpq( n.getNumerator().getInt(), d.getNumerator().getInt(), s );
152  if( n<0 )
153  s << "(~ " << -n << "/" << d << ")";
154  else
155  s << n << "/" << d;
156 }
157 
158 bool getRat( const Expr& e, Rational& r ){
159  if( e.isRational() ){
160  r = e.getRational();
161  return true;
162  }else if( e.getKind()==DIVIDE && e[0].isRational() && e[1].isRational() ){
163  r = e[0].getRational()/e[1].getRational();
164  return true;
165  }else if( e.getKind()==UMINUS ){
166  getRat( e[0], r );
167  r = -r;
168  return true;
169  }
170  return false;
171 }
172 
173 bool isFlat( const Expr& e ){
174  for( int a=0; a<e.arity(); a++ ){
175  if( e.getKind()==e[a].getKind() ){
176  if( e.arity()>=10 )
177  return false;
178  else if( !isFlat( e[a] ) )
179  return false;
180  }
181  }
182  return true;
183 }
184 
185 void make_flatten_expr_h( const Expr& e, Expr& pe, const Expr& pec, bool pecDef, int knd ){
186  //cout << "Trav " << e << std::endl;
187  if( e.getKind()==knd ){
188  make_flatten_expr_h( e[1], pe, pec, pecDef, knd );
189  if( e[0].getKind()==knd ){
190  make_flatten_expr_h( e[0], pe, pe, true, knd );
191  }else{
192  pe = Expr( knd, e[0], pe );
193  }
194  }else{
195  if( pecDef ){
196  pe = Expr( knd, e, pec );
197  }else{
198  pe = e;
199  }
200  }
201 }
202 
203 void make_flatten_expr( const Expr& e, Expr& pe, int knd ){
204  Expr pec;
205  make_flatten_expr_h( e, pe, pec, false, knd );
206 }
int arity() const
Definition: expr.h:1201
void print_rational(const Rational &r, std::ostream &s)
Definition: Util.cpp:136
static ofstream errs
Definition: Object.h:70
bool getRat(const Expr &e, Rational &r)
Definition: Util.cpp:158
Data structure of expressions in CVC3.
Definition: expr.h:133
bool isRational() const
Definition: expr.h:431
bool is_smt_kind(int knd)
Definition: Util.cpp:60
const Rational & getRational() const
Get the Rational value out of RATIONAL_EXPR.
Definition: expr.h:1135
Definition: kinds.h:66
bool isFlat(const Expr &e)
Definition: Util.cpp:173
void make_flatten_expr(const Expr &e, Expr &pe, int knd)
Definition: Util.cpp:203
bool is_eq_kind(int knd)
Definition: Util.cpp:47
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
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_normalized(int knd, bool isnot)
Definition: Util.cpp:100
static void print_error(const char *c, std::ostream &s)
Definition: Object.h:95
bool is_opposite(int knd)
Definition: Util.cpp:66
static bool errsInit
Definition: Object.h:69
void print(InputLanguage lang, bool dagify=true) const
Print the expression in the specified format.
Definition: expr.cpp:362
Definition: kinds.h:68
int getKind() const
Definition: expr.h:1168
T abs(T t)
Definition: cvc_util.h:53
void ajr_debug_print(const Expr &pf)
Definition: Util.cpp:8
int get_knd_order(int knd)
Definition: Util.cpp:89
string kind_to_str(int knd)
Definition: Util.cpp:17
void make_flatten_expr_h(const Expr &e, Expr &pe, const Expr &pec, bool pecDef, int knd)
Definition: Util.cpp:185
bool is_comparison(int knd)
Definition: Util.cpp:70
Definition: kinds.h:81
Definition: kinds.h:63
int get_knd_result(int knd1, int knd2)
Definition: Util.cpp:111
Definition: kinds.h:61
static bool indentFlag
Definition: Object.h:71
void print_rational_divide(const Rational &n, const Rational &d, std::ostream &s)
Definition: Util.cpp:149
Definition: kinds.h:67
Definition: kinds.h:70