1 /*++
2 Copyright (c) 2020 Microsoft Corporation
3
4 Module Name:
5
6 value_sweep.cpp
7
8 Author:
9
10 Nikolaj Bjorner 2020-04-25
11
12 --*/
13
14 #include "ast/for_each_expr.h"
15 #include "ast/ast_pp.h"
16 #include "ast/rewriter/value_sweep.h"
17
value_sweep(ast_manager & m)18 value_sweep::value_sweep(ast_manager& m):
19 m(m),
20 m_gen(m),
21 m_rec(m),
22 m_dt(m),
23 m_rewrite(m),
24 m_values(m),
25 m_args(m),
26 m_pinned(m),
27 m_rounds(10),
28 m_range(20),
29 m_qhead(0)
30 {}
31
set_value_core(expr * e,expr * v)32 void value_sweep::set_value_core(expr* e, expr* v) {
33 m_values.reserve(e->get_id() + 1);
34 m_values[e->get_id()] = v;
35 }
36
set_value(expr * e,expr * v)37 void value_sweep::set_value(expr* e, expr* v) {
38 if (!is_reducible(e) || m_dt.is_accessor(e)) {
39 set_value_core(e, v);
40 m_pinned.push_back(e);
41 }
42 }
43
reset_values()44 void value_sweep::reset_values() {
45 m_values.reset();
46 m_pinned.reset();
47 }
48
get_value(expr * e) const49 expr* value_sweep::get_value(expr* e) const {
50 if (m.is_value(e))
51 return e;
52 if (m_values.size() <= e->get_id())
53 return nullptr;
54 return m_values[e->get_id()];
55 }
56
unassign(unsigned sz)57 void value_sweep::unassign(unsigned sz) {
58 for (unsigned i = m_queue.size(); i-- > sz; ) {
59 expr* e = m_queue[i];
60 m_values[e->get_id()] = nullptr;
61 }
62 m_queue.shrink(sz);
63 m_qhead = sz;
64 }
65
assign_next_value()66 bool value_sweep::assign_next_value() {
67 for (; m_vhead < m_vars.size(); ) {
68 expr* v = m_vars[m_vhead];
69 ++m_vhead;
70 if (!get_value(v)) {
71 unsigned index = m_rand() % m_range;
72 expr_ref val = m_gen.get_value(v->get_sort(), index);
73 set_value_core(v, val);
74 m_queue.push_back(v);
75 return true;
76 }
77 }
78 return false;
79 }
80
is_reducible(expr * e) const81 bool value_sweep::is_reducible(expr* e) const {
82 if (!is_app(e))
83 return false;
84 app* a = to_app(e);
85 return
86 m_rec.is_defined(a) ||
87 a->get_family_id() == m_dt.get_family_id() ||
88 a->get_family_id() == m.get_basic_family_id();
89 }
90
all_args_have_values(app * p) const91 bool value_sweep::all_args_have_values(app* p) const {
92 for (expr* arg : *p) {
93 if (!get_value(arg))
94 return false;
95 }
96 return true;
97 }
98
propagate_values()99 void value_sweep::propagate_values() {
100 for (; m_qhead < m_queue.size(); ++m_qhead) {
101 expr* e = m_queue[m_qhead];
102 for (app* p : m_parents[e->get_id()]) {
103 if (get_value(p))
104 continue;
105 if (!is_reducible(p))
106 continue;
107 if (!all_args_have_values(p))
108 continue;
109 m_args.reset();
110 for (expr* arg : *p)
111 m_args.push_back(get_value(arg));
112 expr_ref new_value(m.mk_app(p->get_decl(), m_args), m);
113 m_rewrite(new_value);
114 TRACE("value_sweep", tout << "propagate " << mk_pp(p, m) << " " << new_value << "\n";);
115 set_value_core(p, new_value);
116 m_queue.push_back(p);
117 }
118 }
119 }
120
init(expr_ref_vector const & terms)121 void value_sweep::init(expr_ref_vector const& terms) {
122 m_parents.reset();
123 m_queue.reset();
124 m_vars.reset();
125 m_qhead = 0;
126 m_vhead = 0;
127 for (expr* t : subterms::ground(terms)) {
128 m_parents.reserve(t->get_id() + 1);
129 if (get_value(t))
130 m_queue.push_back(t);
131 else if (!is_reducible(t))
132 m_vars.push_back(t);
133 }
134 for (expr* t : subterms::ground(terms)) {
135 if (!is_app(t))
136 continue;
137 for (expr* arg : *to_app(t)) {
138 m_parents[arg->get_id()].push_back(to_app(t));
139 }
140 }
141 }
142
operator ()(expr_ref_vector const & terms,vector<expr_ref_vector> & values)143 void value_sweep::operator()(expr_ref_vector const& terms,
144 vector<expr_ref_vector>& values) {
145
146 unsigned qhead0 = m_queue.size();
147 init(terms);
148 propagate_values();
149 unsigned qhead = m_queue.size();
150 for (unsigned i = 0; i < m_rounds; ++i) {
151 m_vhead = 0;
152 while (assign_next_value()) {
153 propagate_values();
154 }
155 expr_ref_vector vec(m);
156 for (expr* t : terms) {
157 vec.push_back(get_value(t));
158 }
159 values.push_back(vec);
160 unassign(qhead);
161 }
162 unassign(qhead0);
163 }
164