| 301 | namespace IR { |
| 302 | |
| 303 | expr float_refined(const expr &a, const expr &b) { |
| 304 | EGraph g; |
| 305 | unsigned na = g.get(a); |
| 306 | unsigned nb = g.get(b); |
| 307 | #ifdef DEBUG_FMF |
| 308 | cout << "Before saturate:\n" << g << "Roots: " << na << " / " << nb << "\n\n"; |
| 309 | #endif |
| 310 | |
| 311 | if (na == nb) |
| 312 | return true; |
| 313 | |
| 314 | g.saturate(); |
| 315 | |
| 316 | na = g.root(na); |
| 317 | nb = g.root(nb); |
| 318 | #ifdef DEBUG_FMF |
| 319 | cout << "After saturate:\n" << g << "Roots: " << na << " / " << nb << "\n\n"; |
| 320 | #endif |
| 321 | if (na == nb) |
| 322 | return true; |
| 323 | |
| 324 | #ifdef DEBUG_FMF |
| 325 | cout << "Expr A: " << g.smtOf(na) << "\n\nExpr B: " << g.smtOf(nb) << "\n\n"; |
| 326 | #endif |
| 327 | |
| 328 | return g.smtOf(na) == g.smtOf(nb); |
| 329 | } |
| 330 | |
| 331 | } |