1 /*++
2 Copyright (c) 2014 Microsoft Corporation
3
4 Module Name:
5
6 bvsls_opt_engine.cpp
7
8 Abstract:
9
10 Optimization extensions to bvsls
11
12 Author:
13
14 Christoph (cwinter) 2014-03-28
15
16 Notes:
17
18 --*/
19 #include "ast/normal_forms/nnf.h"
20 #include "tactic/sls/bvsls_opt_engine.h"
21
bvsls_opt_engine(ast_manager & m,params_ref const & p)22 bvsls_opt_engine::bvsls_opt_engine(ast_manager & m, params_ref const & p) :
23 sls_engine(m, p),
24 m_hard_tracker(sls_engine::m_tracker),
25 m_obj_tracker(m, m_bv_util, m_mpz_manager, m_powers),
26 m_obj_evaluator(m, m_bv_util, m_obj_tracker, m_mpz_manager, m_powers)
27 {
28 m_best_model = alloc(model, m);
29 }
30
~bvsls_opt_engine()31 bvsls_opt_engine::~bvsls_opt_engine()
32 {
33 }
34
optimize(expr_ref const & objective,model_ref initial_model,bool _maximize)35 bvsls_opt_engine::optimization_result bvsls_opt_engine::optimize(
36 expr_ref const & objective,
37 model_ref initial_model,
38 bool _maximize)
39 {
40 SASSERT(m_bv_util.is_bv(objective));
41 TRACE("sls_opt", tout << "objective: " << (_maximize?"maximize":"minimize") << " " <<
42 mk_ismt2_pp(objective, m()) << std::endl;);
43 m_hard_tracker.initialize(m_assertions);
44 setup_opt_tracker(objective, _maximize);
45
46 if (initial_model.get() != nullptr) {
47 TRACE("sls_opt", tout << "Initial model provided: " << std::endl;
48 for (unsigned i = 0; i < initial_model->get_num_constants(); i++) {
49 func_decl * fd = initial_model->get_constant(i);
50 expr * val = initial_model->get_const_interp(fd);
51 tout << fd->get_name() << " := " << mk_ismt2_pp(val, m()) << std::endl;
52 });
53 m_hard_tracker.set_model(initial_model);
54 m_evaluator.update_all();
55 }
56
57 optimization_result res(m_manager);
58 lbool is_sat = m_hard_tracker.is_sat() ? l_true : l_undef;
59
60 TRACE("sls_opt", tout << "initial model is sat? " << is_sat << std::endl;);
61
62 for (m_stats.m_restarts = 0;
63 m_stats.m_restarts < m_max_restarts;
64 m_stats.m_restarts++)
65 {
66 mpz old_best;
67 m_mpz_manager.set(old_best, m_best_model_score);
68
69 if (is_sat != l_true) {
70 do {
71 checkpoint();
72
73 IF_VERBOSE(1, verbose_stream() << "Satisfying... restarts left:" << (m_max_restarts - m_stats.m_restarts) << std::endl;);
74 is_sat = search();
75
76 if (is_sat == l_undef)
77 m_hard_tracker.randomize(m_assertions);
78 }
79 while (is_sat != l_true &&
80 m_stats.m_restarts++ < m_max_restarts);
81 }
82
83 if (is_sat == l_true) {
84 IF_VERBOSE(1, verbose_stream() << "Optimizing... restarts left:" << (m_max_restarts - m_stats.m_restarts) << std::endl;);
85 res.is_sat = l_true;
86 m_obj_tracker.set_model(m_hard_tracker.get_model());
87 m_obj_evaluator.update_all();
88 expr_ref local_best = maximize();
89 if ((_maximize && m_mpz_manager.gt(m_best_model_score, old_best)) ||
90 (!_maximize && m_mpz_manager.lt(m_best_model_score, old_best)))
91 {
92 res.optimum = local_best;
93 }
94 }
95
96 m_hard_tracker.randomize(m_assertions);
97 m_evaluator.update_all();
98 is_sat = m_hard_tracker.is_sat() ? l_true : l_undef;
99 }
100
101 TRACE("sls_opt", tout << "sat: " << res.is_sat << "; optimum: " << mk_ismt2_pp(res.optimum, m()) << std::endl;);
102
103 return res;
104 }
105
setup_opt_tracker(expr_ref const & objective,bool _max)106 void bvsls_opt_engine::setup_opt_tracker(expr_ref const & objective, bool _max)
107 {
108 expr_ref obj(m_manager);
109 obj = objective;
110 if (!_max)
111 obj = m_bv_util.mk_bv_neg(objective);
112
113 m_obj_e = obj.get();
114 m_obj_bv_sz = m_bv_util.get_bv_size(m_obj_e);
115 ptr_vector<expr> objs;
116 objs.push_back(m_obj_e);
117 m_obj_tracker.initialize(objs);
118 }
119
maximize()120 expr_ref bvsls_opt_engine::maximize()
121 {
122 SASSERT(m_hard_tracker.is_sat());
123
124 TRACE("sls_opt", tout << "Initial opt model:" << std::endl; m_obj_tracker.show_model(tout););
125
126 mpz score, old_score, max_score, new_value;
127 unsigned new_const = (unsigned)-1, new_bit = 0;
128 ptr_vector<func_decl> consts = m_obj_tracker.get_constants();
129 move_type move;
130 m_mpz_manager.set(score, top_score());
131 m_mpz_manager.set(max_score, m_powers(m_obj_bv_sz)); m_mpz_manager.dec(max_score);
132
133 IF_VERBOSE(10, verbose_stream() << "Initial score: " << m_mpz_manager.to_string(score) << std::endl;);
134
135 save_model(score);
136
137 while (m_mpz_manager.lt(score, max_score) && check_restart(m_stats.m_moves))
138 {
139 checkpoint();
140 m_stats.m_moves++;
141 m_mpz_manager.set(old_score, score);
142 new_const = (unsigned)-1;
143
144 mpz score(0);
145 m_mpz_manager.set(score,
146 find_best_move(consts, score, new_const, new_value, new_bit, move, max_score, m_obj_e));
147
148 if (new_const == static_cast<unsigned>(-1)) {
149 m_mpz_manager.set(score, old_score);
150 if (m_mpz_manager.gt(score, m_best_model_score))
151 save_model(score);
152 if (!randomize_wrt_hard()) {
153 // Can't improve and can't randomize; can't do anything other than bail out.
154 TRACE("sls_opt", tout << "Got stuck; bailing out." << std::endl;);
155 IF_VERBOSE(10, verbose_stream() << "No local improvements possible." << std::endl;);
156 goto bailout;
157 }
158 m_mpz_manager.set(score, top_score());
159 }
160 else {
161 m_stats.m_moves++;
162 TRACE("sls_opt", tout << "New optimum: " << m_mpz_manager.to_string(score) << std::endl;);
163 IF_VERBOSE(10, verbose_stream() << "New optimum: " << m_mpz_manager.to_string(score) << std::endl;);
164 func_decl * fd = consts[new_const];
165 incremental_score(fd, new_value);
166 m_obj_evaluator.update(fd, new_value);
167 m_mpz_manager.set(score, top_score());
168 }
169 }
170
171 bailout:
172 m_mpz_manager.del(new_value);
173
174 expr_ref res(m_manager);
175 res = m_bv_util.mk_numeral(m_best_model_score, m_obj_bv_sz);
176 return res;
177 }
178
save_model(mpz const & score)179 void bvsls_opt_engine::save_model(mpz const & score) {
180 model_ref mdl = m_hard_tracker.get_model();
181 model_ref obj_mdl = m_obj_tracker.get_model();
182
183 for (unsigned i = 0; i < obj_mdl->get_num_constants(); i++) {
184 func_decl * fd = obj_mdl->get_constant(i);
185 expr * val = obj_mdl->get_const_interp(fd);
186 if (mdl->has_interpretation(fd)) {
187 if (mdl->get_const_interp(fd) != val)
188 TRACE("sls_opt", tout << "model disagreement on " << fd->get_name() << ": " <<
189 mk_ismt2_pp(val, m()) << " != " << mk_ismt2_pp(mdl->get_const_interp(fd), m()) << std::endl;);
190 SASSERT(mdl->get_const_interp(fd) == val);
191 }
192 else
193 mdl->register_decl(fd, val);
194 }
195
196 m_best_model = mdl;
197 m_mpz_manager.set(m_best_model_score, score);
198 }
199
200 // checks whether the score outcome of a given move is better than the previous score
what_if(func_decl * fd,const unsigned & fd_inx,const mpz & temp,mpz & best_score,unsigned & best_const,mpz & best_value)201 bool bvsls_opt_engine::what_if(
202 func_decl * fd,
203 const unsigned & fd_inx,
204 const mpz & temp,
205 mpz & best_score,
206 unsigned & best_const,
207 mpz & best_value)
208 {
209 #if _EARLY_PRUNE_
210 double r = incremental_score_prune(fd, temp);
211 #else
212 double r = incremental_score(fd, temp);
213 #endif
214
215 if (r >= 1.0 && m_hard_tracker.is_sat()) {
216 m_obj_evaluator.update(fd, temp);
217 mpz cur_best(0);
218 m_mpz_manager.set(cur_best, top_score());
219
220 TRACE("sls_whatif", tout << "WHAT IF " << fd->get_name() << " WERE " << m_mpz_manager.to_string(temp) <<
221 " --> " << r << "; score=" << m_mpz_manager.to_string(cur_best) << std::endl;);
222
223 if (m_mpz_manager.gt(cur_best, best_score)) {
224 m_mpz_manager.set(best_score, cur_best);
225 best_const = fd_inx;
226 m_mpz_manager.set(best_value, temp);
227 return true;
228 }
229 }
230 else
231 {
232 TRACE("sls_whatif_failed", tout << "WHAT IF " << fd->get_name() << " WERE " << m_mpz_manager.to_string(temp) <<
233 " --> unsatisfied hard constraints" << std::endl;);
234 }
235
236 return false;
237 }
238
find_best_move(ptr_vector<func_decl> & to_evaluate,mpz & score,unsigned & best_const,mpz & best_value,unsigned & new_bit,move_type & move,mpz const & max_score,expr * objective)239 mpz bvsls_opt_engine::find_best_move(
240 ptr_vector<func_decl> & to_evaluate,
241 mpz & score,
242 unsigned & best_const,
243 mpz & best_value,
244 unsigned & new_bit,
245 move_type & move,
246 mpz const & max_score,
247 expr * objective)
248 {
249 mpz old_value, temp;
250 #if _USE_MUL3_ || _USE_UNARY_MINUS_
251 mpz temp2;
252 #endif
253 unsigned bv_sz;
254 mpz new_score;
255 m_mpz_manager.set(new_score, score);
256
257 for (unsigned i = 0; i < to_evaluate.size() && m_mpz_manager.lt(new_score, max_score); i++) {
258 func_decl * fd = to_evaluate[i];
259 sort * srt = fd->get_range();
260 bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt);
261 m_mpz_manager.set(old_value, m_obj_tracker.get_value(fd));
262
263 // first try to flip every bit
264 for (unsigned j = 0; j < bv_sz && m_mpz_manager.lt(new_score, max_score); j++) {
265 // What would happen if we flipped bit #i ?
266 mk_flip(srt, old_value, j, temp);
267
268 if (what_if(fd, i, temp, new_score, best_const, best_value)) {
269 new_bit = j;
270 move = MV_FLIP;
271 }
272 }
273
274 if (m_bv_util.is_bv_sort(srt) && bv_sz > 1) {
275 #if _USE_ADDSUB_
276 if (!m_mpz_manager.is_even(old_value)) {
277 // for odd values, try +1
278 mk_inc(bv_sz, old_value, temp);
279 if (what_if(fd, i, temp, new_score, best_const, best_value))
280 move = MV_INC;
281 }
282 else {
283 // for even values, try -1
284 mk_dec(bv_sz, old_value, temp);
285 if (what_if(fd, i, temp, new_score, best_const, best_value))
286 move = MV_DEC;
287 }
288 #endif
289 // try inverting
290 mk_inv(bv_sz, old_value, temp);
291 if (what_if(fd, i, temp, new_score, best_const, best_value))
292 move = MV_INV;
293
294 #if _USE_UNARY_MINUS_
295 mk_inc(bv_sz, temp, temp2);
296 if (what_if(fd, i, temp2, new_score, best_const, best_value))
297 move = MV_UMIN;
298 #endif
299
300 #if _USE_MUL2DIV2_
301 // try multiplication by 2
302 mk_mul2(bv_sz, old_value, temp);
303 if (what_if(fd, i, temp, new_score, best_const, best_value))
304 move = MV_MUL2;
305
306 #if _USE_MUL3_
307 // try multiplication by 3
308 mk_add(bv_sz, old_value, temp, temp2);
309 if (what_if(fd, i, temp2, new_score, best_const, best_value))
310 move = MV_MUL3;
311 #endif
312
313 // try division by 2
314 mk_div2(bv_sz, old_value, temp);
315 if (what_if(fd, i, temp, new_score, best_const, best_value))
316 move = MV_DIV2;
317 #endif
318 }
319
320 // reset to what it was before
321 //double check =
322 incremental_score(fd, old_value);
323 m_obj_evaluator.update(fd, old_value);
324 }
325
326 m_mpz_manager.del(old_value);
327 m_mpz_manager.del(temp);
328 #if _USE_MUL3_
329 m_mpz_manager.del(temp2);
330 #endif
331
332 return new_score;
333 }
334
randomize_wrt_hard()335 bool bvsls_opt_engine::randomize_wrt_hard() {
336 ptr_vector<func_decl> consts = m_obj_tracker.get_constants();
337 unsigned csz = consts.size();
338 unsigned retry_count = csz;
339
340 while (retry_count-- > 0)
341 {
342
343 unsigned ri = (m_obj_tracker.get_random_uint((csz < 16) ? 4 : (csz < 256) ? 8 : (csz < 4096) ? 12 : (csz < 65536) ? 16 : 32)) % csz;
344 func_decl * random_fd = consts[ri]; // Random constant
345
346 mpz random_val; // random value.
347 m_mpz_manager.set(random_val, m_obj_tracker.get_random(random_fd->get_range()));
348
349 mpz old_value;
350 m_mpz_manager.set(old_value, m_obj_tracker.get_value(random_fd));
351
352 if (!m_mpz_manager.eq(random_val, old_value)) {
353 m_evaluator.update(random_fd, random_val);
354
355 if (m_hard_tracker.is_sat()) {
356 TRACE("sls_opt", tout << "Randomizing " << random_fd->get_name() << " to " <<
357 m_mpz_manager.to_string(random_val) << std::endl;);
358 m_obj_evaluator.update(random_fd, random_val);
359 return true;
360 }
361 else
362 m_evaluator.update(random_fd, old_value);
363 }
364 }
365
366 return false;
367 }
368