1 /*++
2 Copyright (c) 2017 Arie Gurfinkel
3
4 Module Name:
5
6 factor_equivs.cpp
7
8 Abstract:
9 Factor equivalence classes out of an expression.
10
11 "Equivalence class structure" for objs. Uses a union_find structure internally.
12 Operations are :
13 -Declare a new equivalence class with a single element
14 -Merge two equivalence classes
15 -Retrieve whether two elements are in the same equivalence class
16 -Iterate on all the elements of the equivalence class of a given element
17 -Iterate on all equivalence classes (and then within them)
18
19 Author:
20
21 Julien Braine
22 Arie Gurfinkel
23
24 Revision History:
25
26 */
27
28 #include "ast/arith_decl_plugin.h"
29 #include "ast/for_each_expr.h"
30 #include "ast/ast_pp.h"
31 #include "ast/rewriter/expr_safe_replace.h"
32 #include "ast/rewriter/factor_equivs.h"
33
34 /**
35 Factors input vector v into equivalence classes and the rest
36 */
factor_eqs(expr_ref_vector & v,expr_equiv_class & equiv)37 void factor_eqs(expr_ref_vector &v, expr_equiv_class &equiv) {
38 ast_manager &m = v.get_manager();
39 arith_util arith(m);
40 expr *e1 = nullptr, *e2 = nullptr;
41
42 flatten_and(v);
43 unsigned j = 0;
44 for (unsigned i = 0; i < v.size(); ++i) {
45 if (m.is_eq(v.get(i), e1, e2)) {
46 if (arith.is_zero(e1)) {
47 std::swap(e1, e2);
48 }
49
50 // y + -1*x == 0
51 expr* a0 = nullptr, *a1 = nullptr, *x = nullptr;
52 if (arith.is_zero(e2) && arith.is_add(e1, a0, a1)) {
53 if (arith.is_times_minus_one(a1, x)) {
54 e1 = a0;
55 e2 = x;
56 }
57 else if (arith.is_times_minus_one(a0, x)) {
58 e1 = a1;
59 e2 = x;
60 }
61 }
62 equiv.merge(e1, e2);
63 }
64 else {
65 if (j < i) {
66 v[j] = v.get(i);
67 }
68 j++;
69 }
70 }
71 v.shrink(j);
72 }
73
74 /**
75 * Chooses a representative of an equivalence class
76 */
choose_rep(expr_equiv_class::eq_class & clazz,ast_manager & m)77 expr *choose_rep(expr_equiv_class::eq_class &clazz, ast_manager &m) {
78 expr *rep = nullptr;
79 unsigned rep_sz = 0, elem_sz;
80 for (expr *elem : clazz) {
81 if (!m.is_value(elem)) {
82 elem_sz = get_num_exprs(elem);
83 if (!rep || (rep && rep_sz > elem_sz)) {
84 rep = elem;
85 rep_sz = elem_sz;
86 }
87 }
88 }
89 TRACE("equiv",
90 tout << "Rep: " << mk_pp(rep, m) << "\n";
91 for (expr *el : clazz)
92 tout << mk_pp(el, m) << "\n";
93 tout << "RepEnd\n";);
94
95 return rep;
96 }
97
rewrite_eqs(expr_ref_vector & v,expr_equiv_class & equiv)98 void rewrite_eqs (expr_ref_vector &v, expr_equiv_class &equiv) {
99 ast_manager &m = v.m();
100 expr_safe_replace sub(m);
101 for (auto eq_class : equiv) {
102 expr *rep = choose_rep(eq_class, m);
103 for (expr *el : eq_class) {
104 if (el != rep) {
105 sub.insert (el, rep);
106 }
107 }
108 }
109 sub(v);
110 }
111
112
113 /**
114 * converts equivalence classes to equalities
115 */
equiv_to_expr(expr_equiv_class & equiv,expr_ref_vector & out)116 void equiv_to_expr(expr_equiv_class &equiv, expr_ref_vector &out) {
117 ast_manager &m = out.get_manager();
118 for (auto eq_class : equiv) {
119 expr *rep = choose_rep(eq_class, m);
120 SASSERT(rep);
121 for (expr *elem : eq_class) {
122 if (rep != elem) {
123 out.push_back (m.mk_eq (rep, elem));
124 }
125 }
126 }
127 }
128
129 /**
130 * expands equivalence classes to all derivable equalities
131 */
equiv_to_expr_full(expr_equiv_class & equiv,expr_ref_vector & out)132 bool equiv_to_expr_full(expr_equiv_class &equiv, expr_ref_vector &out) {
133 ast_manager &m = out.get_manager();
134 bool dirty = false;
135 for (auto eq_class : equiv) {
136 for (auto a = eq_class.begin(), end = eq_class.end(); a != end; ++a) {
137 expr_equiv_class::iterator b(a);
138 for (++b; b != end; ++b) {
139 out.push_back(m.mk_eq(*a, *b));
140 dirty = true;
141 }
142 }
143 }
144 return dirty;
145 }
146