Improve factor equalities

src/ast/factor_equivs.cpp

@@ -27,7 +27,9 @@ Revision History:
 
 #include "ast/factor_equivs.h"
 #include "ast/arith_decl_plugin.h"
-
+#include "ast/for_each_expr.h"
+#include "ast/ast_pp.h"
+#include "ast/rewriter/expr_safe_replace.h"
 /**
    Factors input vector v into equivalence classes and the rest
  */
@@ -68,19 +70,52 @@ void factor_eqs(expr_ref_vector &v, expr_equiv_class &equiv) {
     v.shrink(j);
 }
 
+/**
+ * Chooses a representative of an equivalence class
+ */
+expr *choose_rep(expr_equiv_class::eq_class &clazz, ast_manager &m) {
+    expr *rep = nullptr;
+    unsigned rep_sz, elem_sz;
+    for (expr *elem : clazz) {
+        if (!m.is_value(elem)) {
+            elem_sz = get_num_exprs(elem);
+            if (!rep || (rep && rep_sz > elem_sz)) {
+                rep = elem;
+                rep_sz = elem_sz;
+            }
+        }
+    }
+    TRACE("equiv",
+          tout << "Rep: " << mk_pp(rep, m) << "\n";
+          for (expr *el : clazz)
+              tout << mk_pp(el, m) << "\n";
+          tout << "RepEnd\n";);
+
+    return rep;
+}
+
+void rewrite_eqs (expr_ref_vector &v, expr_equiv_class &equiv) {
+    ast_manager &m = v.m();
+    expr_safe_replace sub(m);
+    for (auto eq_class : equiv) {
+        expr *rep = choose_rep(eq_class, m);
+        for (expr *el : eq_class) {
+            if (el != rep) {
+                sub.insert (el, rep);
+            }
+        }
+    }
+    sub(v);
+}
+
+
 /**
  * converts equivalence classes to equalities
  */
 void equiv_to_expr(expr_equiv_class &equiv, expr_ref_vector &out) {
     ast_manager &m = out.get_manager();
     for (auto eq_class : equiv) {
-        expr *rep = nullptr;
+        expr *rep = choose_rep(eq_class, m);
-        for (expr *elem : eq_class) {
-            if (!m.is_value(elem)) {
-                rep = elem;
-                break;
-            }
-        }
         SASSERT(rep);
         for (expr *elem : eq_class) {
             if (rep != elem) {

src/ast/factor_equivs.h

@@ -60,6 +60,8 @@ public:
 
     obj_equiv_class(Manager& m) : m_to_obj(m) {}
 
+    Manager &m() const {return m_to_obj.m();}
+
     void add_elem(OBJ*o) {
         SASSERT(!m_to_int.find(o));
         add_elem_impl(o);
@@ -169,6 +171,11 @@ typedef obj_equiv_class<expr, ast_manager> expr_equiv_class;
  *  Factors input vector v into equivalence classes and the rest
  */
 void factor_eqs(expr_ref_vector &v, expr_equiv_class &equiv);
+/**
+ * Rewrite expressions in v by choosing a representative from the
+ * equivalence class.
+ */
+void rewrite_eqs(expr_ref_vector &v, expr_equiv_class &equiv);
 /**
  * converts equivalence classes to equalities
  */