1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 sls_score_tracker.h 7 8 Abstract: 9 10 Score and value tracking module for SLS 11 12 Author: 13 14 Christoph (cwinter) 2012-02-29 15 16 Notes: 17 18 --*/ 19 20 #pragma once 21 22 #include<math.h> 23 #include "ast/for_each_expr.h" 24 #include "ast/ast_smt2_pp.h" 25 #include "ast/bv_decl_plugin.h" 26 #include "model/model.h" 27 28 #include "tactic/sls/sls_params.hpp" 29 #include "tactic/sls/sls_powers.h" 30 31 class sls_tracker { 32 ast_manager & m_manager; 33 unsynch_mpz_manager & m_mpz_manager; 34 bv_util & m_bv_util; 35 powers & m_powers; 36 random_gen m_rng; 37 unsigned m_random_bits; 38 unsigned m_random_bits_cnt; 39 mpz m_zero, m_one, m_two; 40 41 struct value_score { value_scorevalue_score42 value_score() : m(nullptr), value(unsynch_mpz_manager::mk_z(0)), score(0.0), score_prune(0.0), has_pos_occ(0), has_neg_occ(0), distance(0), touched(1) {}; 43 value_score(value_score&&) noexcept = default; ~value_scorevalue_score44 ~value_score() { if (m) m->del(value); } 45 value_score& operator=(value_score&&) = default; 46 unsynch_mpz_manager * m; 47 mpz value; 48 double score; 49 double score_prune; 50 unsigned has_pos_occ; 51 unsigned has_neg_occ; 52 unsigned distance; // max distance from any root 53 unsigned touched; 54 }; 55 56 public: 57 typedef obj_map<func_decl, expr* > entry_point_type; 58 59 private: 60 typedef obj_map<expr, value_score> scores_type; 61 typedef obj_map<expr, ptr_vector<expr> > uplinks_type; 62 typedef obj_map<expr, ptr_vector<func_decl> > occ_type; 63 obj_hashtable<expr> m_top_expr; 64 scores_type m_scores; 65 uplinks_type m_uplinks; 66 entry_point_type m_entry_points; 67 ptr_vector<func_decl> m_constants; 68 ptr_vector<func_decl> m_temp_constants; 69 occ_type m_constants_occ; 70 unsigned m_last_pos; 71 unsigned m_walksat; 72 unsigned m_ucb; 73 double m_ucb_constant; 74 unsigned m_ucb_init; 75 double m_ucb_forget; 76 double m_ucb_noise; 77 unsigned m_touched; 78 double m_scale_unsat; 79 unsigned m_paws_init; 80 obj_map<expr, unsigned> m_where_false; 81 expr** m_list_false; 82 unsigned m_track_unsat; 83 obj_map<expr, unsigned> m_weights; 84 double m_top_sum; 85 obj_hashtable<expr> m_temp_seen; 86 87 public: sls_tracker(ast_manager & m,bv_util & bvu,unsynch_mpz_manager & mm,powers & p)88 sls_tracker(ast_manager & m, bv_util & bvu, unsynch_mpz_manager & mm, powers & p) : 89 m_manager(m), 90 m_mpz_manager(mm), 91 m_bv_util(bvu), 92 m_powers(p), 93 m_random_bits_cnt(0), 94 m_zero(m_mpz_manager.mk_z(0)), 95 m_one(m_mpz_manager.mk_z(1)), 96 m_two(m_mpz_manager.mk_z(2)) { 97 } 98 ~sls_tracker()99 ~sls_tracker() { 100 m_mpz_manager.del(m_zero); 101 m_mpz_manager.del(m_one); 102 m_mpz_manager.del(m_two); 103 } 104 updt_params(params_ref const & _p)105 void updt_params(params_ref const & _p) { 106 sls_params p(_p); 107 m_walksat = p.walksat(); 108 m_ucb = p.walksat_ucb(); 109 m_ucb_constant = p.walksat_ucb_constant(); 110 m_ucb_init = p.walksat_ucb_init(); 111 m_ucb_forget = p.walksat_ucb_forget(); 112 m_ucb_noise = p.walksat_ucb_noise(); 113 m_scale_unsat = p.scale_unsat(); 114 m_paws_init = p.paws_init(); 115 // Andreas: track_unsat is currently disabled because I cannot guarantee that it is not buggy. 116 // If you want to use it, you will also need to change comments in the assertion selection. 117 m_track_unsat = 0;//p.track_unsat(); 118 } 119 120 /* Andreas: Tried to give some measure for the formula size by the following two methods but both are not used currently. 121 unsigned get_formula_size() { 122 return m_scores.size(); 123 } 124 125 double get_avg_bw(goal_ref const & g) { 126 double sum = 0.0; 127 unsigned count = 0; 128 129 for (unsigned i = 0; i < g->size(); i++) 130 { 131 m_temp_constants.reset(); 132 ptr_vector<func_decl> const & this_decls = m_constants_occ.find(g->form(i)); 133 unsigned sz = this_decls.size(); 134 for (unsigned i = 0; i < sz; i++) { 135 func_decl * fd = this_decls[i]; 136 m_temp_constants.push_back(fd); 137 sort * srt = fd->get_range(); 138 sum += (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt); 139 count++; 140 } 141 } 142 143 return sum / count; 144 }*/ 145 adapt_top_sum(expr * e,double add,double sub)146 inline void adapt_top_sum(expr * e, double add, double sub) { 147 m_top_sum += m_weights.find(e) * (add - sub); 148 } 149 set_top_sum(double new_score)150 inline void set_top_sum(double new_score) { 151 m_top_sum = new_score; 152 } 153 get_top_sum()154 inline double get_top_sum() { 155 return m_top_sum; 156 } 157 get_top_exprs()158 inline obj_hashtable<expr> const & get_top_exprs() { 159 return m_top_expr; 160 } 161 is_sat()162 inline bool is_sat() { 163 for (obj_hashtable<expr>::iterator it = m_top_expr.begin(); 164 it != m_top_expr.end(); 165 it++) 166 if (!m_mpz_manager.is_one(get_value(*it))) 167 return false; 168 return true; 169 } 170 set_value(expr * n,const mpz & r)171 inline void set_value(expr * n, const mpz & r) { 172 SASSERT(m_scores.contains(n)); 173 m_mpz_manager.set(m_scores.find(n).value, r); 174 } 175 set_value(func_decl * fd,const mpz & r)176 inline void set_value(func_decl * fd, const mpz & r) { 177 SASSERT(m_entry_points.contains(fd)); 178 expr * ep = get_entry_point(fd); 179 set_value(ep, r); 180 } 181 get_value(expr * n)182 inline mpz & get_value(expr * n) { 183 SASSERT(m_scores.contains(n)); 184 return m_scores.find(n).value; 185 } 186 get_value(func_decl * fd)187 inline mpz & get_value(func_decl * fd) { 188 SASSERT(m_entry_points.contains(fd)); 189 expr * ep = get_entry_point(fd); 190 return get_value(ep); 191 } 192 set_score(expr * n,double score)193 inline void set_score(expr * n, double score) { 194 SASSERT(m_scores.contains(n)); 195 m_scores.find(n).score = score; 196 } 197 set_score(func_decl * fd,double score)198 inline void set_score(func_decl * fd, double score) { 199 SASSERT(m_entry_points.contains(fd)); 200 expr * ep = get_entry_point(fd); 201 set_score(ep, score); 202 } 203 get_score(expr * n)204 inline double & get_score(expr * n) { 205 SASSERT(m_scores.contains(n)); 206 return m_scores.find(n).score; 207 } 208 get_score(func_decl * fd)209 inline double & get_score(func_decl * fd) { 210 SASSERT(m_entry_points.contains(fd)); 211 expr * ep = get_entry_point(fd); 212 return get_score(ep); 213 } 214 set_score_prune(expr * n,double score)215 inline void set_score_prune(expr * n, double score) { 216 SASSERT(m_scores.contains(n)); 217 m_scores.find(n).score_prune = score; 218 } 219 get_score_prune(expr * n)220 inline double & get_score_prune(expr * n) { 221 SASSERT(m_scores.contains(n)); 222 return m_scores.find(n).score_prune; 223 } 224 has_pos_occ(expr * n)225 inline unsigned has_pos_occ(expr * n) { 226 SASSERT(m_scores.contains(n)); 227 return m_scores.find(n).has_pos_occ; 228 } 229 has_neg_occ(expr * n)230 inline unsigned has_neg_occ(expr * n) { 231 SASSERT(m_scores.contains(n)); 232 return m_scores.find(n).has_neg_occ; 233 } 234 get_distance(expr * n)235 inline unsigned get_distance(expr * n) { 236 SASSERT(m_scores.contains(n)); 237 return m_scores.find(n).distance; 238 } 239 set_distance(expr * n,unsigned d)240 inline void set_distance(expr * n, unsigned d) { 241 SASSERT(m_scores.contains(n)); 242 m_scores.find(n).distance = d; 243 } 244 get_entry_point(func_decl * fd)245 inline expr * get_entry_point(func_decl * fd) { 246 SASSERT(m_entry_points.contains(fd)); 247 return m_entry_points.find(fd); 248 } 249 get_entry_points()250 inline entry_point_type const & get_entry_points() { 251 return m_entry_points; 252 } 253 has_uplinks(expr * n)254 inline bool has_uplinks(expr * n) { 255 return m_uplinks.contains(n); 256 } 257 is_top_expr(expr * n)258 inline bool is_top_expr(expr * n) { 259 return m_top_expr.contains(n); 260 } 261 get_uplinks(expr * n)262 inline ptr_vector<expr> & get_uplinks(expr * n) { 263 SASSERT(m_uplinks.contains(n)); 264 return m_uplinks.find(n); 265 } 266 ucb_forget(ptr_vector<expr> & as)267 inline void ucb_forget(ptr_vector<expr> & as) { 268 if (m_ucb_forget < 1.0) 269 { 270 expr * e; 271 unsigned touched_old, touched_new; 272 273 for (unsigned i = 0; i < as.size(); i++) 274 { 275 e = as[i]; 276 touched_old = m_scores.find(e).touched; 277 touched_new = (unsigned)((touched_old - 1) * m_ucb_forget + 1); 278 m_scores.find(e).touched = touched_new; 279 m_touched += touched_new - touched_old; 280 } 281 } 282 } 283 initialize(app * n)284 void initialize(app * n) { 285 // Build score table 286 if (!m_scores.contains(n)) { 287 value_score vs; 288 vs.m = & m_mpz_manager; 289 m_scores.insert(n, std::move(vs)); 290 } 291 292 // Update uplinks 293 unsigned na = n->get_num_args(); 294 for (unsigned i = 0; i < na; i++) { 295 expr * c = n->get_arg(i); 296 m_uplinks.insert_if_not_there(c, ptr_vector<expr>()).push_back(n); 297 } 298 299 func_decl * d = n->get_decl(); 300 301 if (n->get_num_args() == 0) { 302 if (d->get_family_id() != null_family_id) { 303 // Interpreted constant 304 mpz t; 305 value2mpz(n, t); 306 set_value(n, t); 307 m_mpz_manager.del(t); 308 } 309 else { 310 // Uninterpreted constant 311 m_entry_points.insert_if_not_there(d, n); 312 m_constants.push_back(d); 313 } 314 } 315 } 316 317 struct init_proc { 318 ast_manager & m_manager; 319 sls_tracker & m_tracker; 320 init_procinit_proc321 init_proc(ast_manager & m, sls_tracker & tracker): 322 m_manager(m), 323 m_tracker(tracker) { 324 } 325 operatorinit_proc326 void operator()(var * n) {} 327 operatorinit_proc328 void operator()(quantifier * n) {} 329 operatorinit_proc330 void operator()(app * n) { 331 m_tracker.initialize(n); 332 } 333 }; 334 335 struct find_func_decls_proc { 336 ast_manager & m_manager; 337 ptr_vector<func_decl> & m_occs; 338 find_func_decls_procfind_func_decls_proc339 find_func_decls_proc (ast_manager & m, ptr_vector<func_decl> & occs): 340 m_manager(m), 341 m_occs(occs) { 342 } 343 operatorfind_func_decls_proc344 void operator()(var * n) {} 345 operatorfind_func_decls_proc346 void operator()(quantifier * n) {} 347 operatorfind_func_decls_proc348 void operator()(app * n) { 349 if (n->get_num_args() != 0) 350 return; 351 func_decl * d = n->get_decl(); 352 if (d->get_family_id() != null_family_id) 353 return; 354 m_occs.push_back(d); 355 } 356 }; 357 calculate_expr_distances(ptr_vector<expr> const & as)358 void calculate_expr_distances(ptr_vector<expr> const & as) { 359 // precondition: m_scores is set up. 360 unsigned sz = as.size(); 361 ptr_vector<app> stack; 362 for (unsigned i = 0; i < sz; i++) 363 stack.push_back(to_app(as[i])); 364 while (!stack.empty()) { 365 app * cur = stack.back(); 366 stack.pop_back(); 367 368 unsigned d = get_distance(cur); 369 370 for (unsigned i = 0; i < cur->get_num_args(); i++) { 371 app * child = to_app(cur->get_arg(i)); 372 unsigned d_child = get_distance(child); 373 if (d >= d_child) { 374 set_distance(child, d+1); 375 stack.push_back(child); 376 } 377 } 378 } 379 } 380 381 /* Andreas: Used this at some point to have values for the non-top-level expressions. 382 However, it did not give better performance but even cause some additional m/o - is not used currently. 383 void initialize_recursive(init_proc proc, expr_mark visited, expr * e) { 384 if (m_manager.is_and(e) || m_manager.is_or(e)) { 385 app * a = to_app(e); 386 expr * const * args = a->get_args(); 387 unsigned int sz = a->get_num_args(); 388 for (unsigned int i = 0; i < sz; i++) { 389 expr * q = args[i]; 390 initialize_recursive(proc, visited, q); 391 } 392 } 393 for_each_expr(proc, visited, e); 394 } 395 396 void initialize_recursive(expr * e) { 397 if (m_manager.is_and(e) || m_manager.is_or(e)) { 398 app * a = to_app(e); 399 expr * const * args = a->get_args(); 400 unsigned int sz = a->get_num_args(); 401 for (unsigned int i = 0; i < sz; i++) { 402 expr * q = args[i]; 403 initialize_recursive(q); 404 } 405 } 406 ptr_vector<func_decl> t; 407 m_constants_occ.insert_if_not_there(e, t); 408 find_func_decls_proc ffd_proc(m_manager, m_constants_occ.find(e)); 409 expr_fast_mark1 visited; 410 quick_for_each_expr(ffd_proc, visited, e); 411 }*/ 412 initialize(ptr_vector<expr> const & as)413 void initialize(ptr_vector<expr> const & as) { 414 init_proc proc(m_manager, *this); 415 expr_mark visited; 416 unsigned sz = as.size(); 417 for (unsigned i = 0; i < sz; i++) { 418 expr * e = as[i]; 419 if (!m_top_expr.contains(e)) 420 m_top_expr.insert(e); 421 for_each_expr(proc, visited, e); 422 } 423 424 visited.reset(); 425 426 for (unsigned i = 0; i < sz; i++) { 427 expr * e = as[i]; 428 ptr_vector<func_decl> t; 429 m_constants_occ.insert_if_not_there(e, t); 430 find_func_decls_proc ffd_proc(m_manager, m_constants_occ.find(e)); 431 expr_fast_mark1 visited; 432 quick_for_each_expr(ffd_proc, visited, e); 433 } 434 435 calculate_expr_distances(as); 436 437 TRACE("sls", tout << "Initial model:" << std::endl; show_model(tout); ); 438 439 if (m_track_unsat) 440 { 441 m_list_false = new expr*[sz]; 442 for (unsigned i = 0; i < sz; i++) 443 { 444 if (m_mpz_manager.eq(get_value(as[i]), m_zero)) 445 break_assertion(as[i]); 446 } 447 } 448 449 m_temp_seen.reset(); 450 for (unsigned i = 0; i < sz; i++) 451 { 452 expr * e = as[i]; 453 454 // initialize weights 455 if (!m_weights.contains(e)) 456 m_weights.insert(e, m_paws_init); 457 458 // positive/negative occurrences used for early pruning 459 setup_occs(as[i]); 460 } 461 462 // initialize ucb total touched value (individual ones are always initialized to 1) 463 m_touched = m_ucb_init ? as.size() : 1; 464 } 465 increase_weight(expr * e)466 void increase_weight(expr * e) 467 { 468 m_weights.find(e)++; 469 } 470 decrease_weight(expr * e)471 void decrease_weight(expr * e) 472 { 473 unsigned old_weight = m_weights.find(e); 474 m_weights.find(e) = old_weight > m_paws_init ? old_weight - 1 : m_paws_init; 475 } 476 get_weight(expr * e)477 unsigned get_weight(expr * e) 478 { 479 return m_weights.find(e); 480 } 481 make_assertion(expr * e)482 void make_assertion(expr * e) 483 { 484 if (m_track_unsat) 485 { 486 if (m_where_false.contains(e)) 487 { 488 unsigned pos = m_where_false.find(e); 489 m_where_false.erase(e); 490 if (pos != m_where_false.size()) 491 { 492 expr * q = m_list_false[m_where_false.size()]; 493 m_list_false[pos] = q; 494 m_where_false.find(q) = pos; 495 } 496 } 497 } 498 } 499 break_assertion(expr * e)500 void break_assertion(expr * e) 501 { 502 if (m_track_unsat) 503 { 504 if (!m_where_false.contains(e)) 505 { 506 unsigned pos = m_where_false.size(); 507 m_list_false[pos] = e; 508 m_where_false.insert(e, pos); 509 } 510 } 511 } 512 show_model(std::ostream & out)513 void show_model(std::ostream & out) { 514 unsigned sz = get_num_constants(); 515 for (unsigned i = 0; i < sz; i++) { 516 func_decl * fd = get_constant(i); 517 out << fd->get_name() << " = " << m_mpz_manager.to_string(get_value(fd)) << std::endl; 518 } 519 } 520 set_model(model_ref const & mdl)521 void set_model(model_ref const & mdl) { 522 for (unsigned i = 0; i < mdl->get_num_constants(); i++) { 523 func_decl * fd = mdl->get_constant(i); 524 expr * val = mdl->get_const_interp(fd); 525 if (m_entry_points.contains(fd)) { 526 if (m_manager.is_bool(val)) { 527 set_value(fd, m_manager.is_true(val) ? m_mpz_manager.mk_z(1) : m_mpz_manager.mk_z(0)); 528 } 529 else if (m_bv_util.is_numeral(val)) { 530 rational r_val; 531 unsigned bv_sz; 532 m_bv_util.is_numeral(val, r_val, bv_sz); 533 const mpq& q = r_val.to_mpq(); 534 SASSERT(m_mpz_manager.is_one(q.denominator())); 535 set_value(fd, q.numerator()); 536 } 537 else 538 NOT_IMPLEMENTED_YET(); 539 } 540 } 541 } 542 get_model()543 model_ref get_model() { 544 model_ref res = alloc(model, m_manager); 545 unsigned sz = get_num_constants(); 546 for (unsigned i = 0; i < sz; i++) { 547 func_decl * fd = get_constant(i); 548 res->register_decl(fd, mpz2value(fd->get_range(), get_value(fd))); 549 } 550 return res; 551 } 552 get_num_constants()553 unsigned get_num_constants() { 554 return m_constants.size(); 555 } 556 get_constants()557 ptr_vector<func_decl> & get_constants() { 558 return m_constants; 559 } 560 get_constant(unsigned i)561 func_decl * get_constant(unsigned i) { 562 return m_constants[i]; 563 } 564 set_random_seed(unsigned s)565 void set_random_seed(unsigned s) { 566 m_rng.set_seed(s); 567 } 568 get_random_bv(sort * s)569 mpz get_random_bv(sort * s) { 570 SASSERT(m_bv_util.is_bv_sort(s)); 571 unsigned bv_size = m_bv_util.get_bv_size(s); 572 mpz r; m_mpz_manager.set(r, 0); 573 574 mpz temp; 575 do 576 { 577 m_mpz_manager.mul(r, m_two, temp); 578 m_mpz_manager.add(temp, get_random_bool(), r); 579 } while (--bv_size > 0); 580 m_mpz_manager.del(temp); 581 582 return r; 583 } 584 get_random_bool()585 mpz & get_random_bool() { 586 if (m_random_bits_cnt == 0) { 587 m_random_bits = m_rng(); 588 m_random_bits_cnt = 15; // random_gen produces 15 bits of randomness. 589 } 590 591 bool val = (m_random_bits & 0x01) != 0; 592 m_random_bits = m_random_bits >> 1; 593 m_random_bits_cnt--; 594 595 return (val) ? m_one : m_zero; 596 } 597 get_random_uint(unsigned bits)598 unsigned get_random_uint(unsigned bits) { 599 if (m_random_bits_cnt == 0) { 600 m_random_bits = m_rng(); 601 m_random_bits_cnt = 15; // random_gen produces 15 bits of randomness. 602 } 603 604 unsigned val = 0; 605 while (bits-- > 0) { 606 if ((m_random_bits & 0x01) != 0) val++; 607 val <<= 1; 608 m_random_bits >>= 1; 609 m_random_bits_cnt--; 610 611 if (m_random_bits_cnt == 0) { 612 m_random_bits = m_rng(); 613 m_random_bits_cnt = 15; // random_gen produces 15 bits of randomness. 614 } 615 } 616 617 return val; 618 } 619 get_random(sort * s)620 mpz get_random(sort * s) { 621 if (m_bv_util.is_bv_sort(s)) 622 return get_random_bv(s); 623 else if (m_manager.is_bool(s)) 624 return m_mpz_manager.dup(get_random_bool()); 625 else { 626 NOT_IMPLEMENTED_YET(); // This only works for bit-vectors for now. 627 return get_random_bv(nullptr); 628 } 629 } 630 randomize(ptr_vector<expr> const & as)631 void randomize(ptr_vector<expr> const & as) { 632 TRACE("sls", tout << "Abandoned model:" << std::endl; show_model(tout); ); 633 634 for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); it++) { 635 func_decl * fd = it->m_key; 636 sort * s = fd->get_range(); 637 mpz temp = get_random(s); 638 set_value(it->m_value, temp); 639 m_mpz_manager.del(temp); 640 } 641 642 TRACE("sls", tout << "Randomized model:" << std::endl; show_model(tout); ); 643 } 644 reset(ptr_vector<expr> const & as)645 void reset(ptr_vector<expr> const & as) { 646 TRACE("sls", tout << "Abandoned model:" << std::endl; show_model(tout); ); 647 648 for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); it++) { 649 set_value(it->m_value, m_zero); 650 } 651 } 652 653 void setup_occs(expr * n, bool negated = false) { 654 if (m_manager.is_bool(n)) 655 { 656 if (m_manager.is_and(n) || m_manager.is_or(n)) 657 { 658 SASSERT(!negated); 659 app * a = to_app(n); 660 expr * const * args = a->get_args(); 661 for (unsigned i = 0; i < a->get_num_args(); i++) 662 { 663 expr * child = args[i]; 664 if (!m_temp_seen.contains(child)) 665 { 666 setup_occs(child, false); 667 m_temp_seen.insert(child); 668 } 669 } 670 } 671 else if (m_manager.is_not(n)) 672 { 673 SASSERT(!negated); 674 app * a = to_app(n); 675 SASSERT(a->get_num_args() == 1); 676 expr * child = a->get_arg(0); 677 SASSERT(!m_manager.is_and(child) && !m_manager.is_or(child)); 678 setup_occs(child, true); 679 } 680 else 681 { 682 if (negated) 683 m_scores.find(n).has_neg_occ = 1; 684 else 685 m_scores.find(n).has_pos_occ = 1; 686 } 687 } 688 else if (m_bv_util.is_bv(n)) { 689 /* CMW: I need this for optimization. Safe to ignore? */ 690 } 691 else 692 NOT_IMPLEMENTED_YET(); 693 } 694 695 double score_bool(expr * n, bool negated = false) { 696 TRACE("sls_score", tout << ((negated)?"NEG ":"") << "BOOL: " << mk_ismt2_pp(n, m_manager) << std::endl; ); 697 698 double res = 0.0; 699 700 if (is_uninterp_const(n)) { 701 const mpz & r = get_value(n); 702 if (negated) 703 res = (m_mpz_manager.is_one(r)) ? 0.0 : 1.0; 704 else 705 res = (m_mpz_manager.is_one(r)) ? 1.0 : 0.0; 706 } 707 else if (m_manager.is_and(n)) { 708 SASSERT(!negated); 709 app * a = to_app(n); 710 expr * const * args = a->get_args(); 711 /* Andreas: Seems to have no effect. But maybe you want to try it again at some point. 712 double sum = 0.0; 713 for (unsigned i = 0; i < a->get_num_args(); i++) 714 sum += get_score(args[i]); 715 res = sum / (double) a->get_num_args(); */ 716 double min = 1.0; 717 for (unsigned i = 0; i < a->get_num_args(); i++) { 718 double cur = get_score(args[i]); 719 if (cur < min) min = cur; 720 } 721 res = min; 722 } 723 else if (m_manager.is_or(n)) { 724 SASSERT(!negated); 725 app * a = to_app(n); 726 expr * const * args = a->get_args(); 727 double max = 0.0; 728 for (unsigned i = 0; i < a->get_num_args(); i++) { 729 double cur = get_score(args[i]); 730 if (cur > max) max = cur; 731 } 732 res = max; 733 } 734 else if (m_manager.is_ite(n)) { 735 SASSERT(!negated); 736 app * a = to_app(n); 737 SASSERT(a->get_num_args() == 3); 738 const mpz & cond = get_value(a->get_arg(0)); 739 double s_t = get_score(a->get_arg(1)); 740 double s_f = get_score(a->get_arg(2)); 741 res = (m_mpz_manager.is_one(cond)) ? s_t : s_f; 742 } 743 else if (m_manager.is_eq(n) || m_manager.is_iff(n)) { 744 app * a = to_app(n); 745 SASSERT(a->get_num_args() == 2); 746 expr * arg0 = a->get_arg(0); 747 expr * arg1 = a->get_arg(1); 748 const mpz & v0 = get_value(arg0); 749 const mpz & v1 = get_value(arg1); 750 751 if (negated) { 752 res = (m_mpz_manager.eq(v0, v1)) ? 0.0 : 1.0; 753 TRACE("sls_score", tout << "V0 = " << m_mpz_manager.to_string(v0) << " ; V1 = " << 754 m_mpz_manager.to_string(v1) << std::endl; ); 755 } 756 else if (m_manager.is_bool(arg0)) { 757 res = m_mpz_manager.eq(v0, v1) ? 1.0 : 0.0; 758 TRACE("sls_score", tout << "V0 = " << m_mpz_manager.to_string(v0) << " ; V1 = " << 759 m_mpz_manager.to_string(v1) << std::endl; ); 760 } 761 else if (m_bv_util.is_bv(arg0)) { 762 mpz diff, diff_m1; 763 m_mpz_manager.bitwise_xor(v0, v1, diff); 764 unsigned hamming_distance = 0; 765 unsigned bv_sz = m_bv_util.get_bv_size(arg0); 766 // unweighted hamming distance 767 while (!m_mpz_manager.is_zero(diff)) { 768 if (!m_mpz_manager.is_even(diff)) { 769 hamming_distance++; 770 } 771 m_mpz_manager.machine_div(diff, m_two, diff); 772 } 773 res = 1.0 - (hamming_distance / (double) bv_sz); 774 TRACE("sls_score", tout << "V0 = " << m_mpz_manager.to_string(v0) << " ; V1 = " << 775 m_mpz_manager.to_string(v1) << " ; HD = " << hamming_distance << 776 " ; SZ = " << bv_sz << std::endl; ); 777 m_mpz_manager.del(diff); 778 m_mpz_manager.del(diff_m1); 779 } 780 else 781 NOT_IMPLEMENTED_YET(); 782 } 783 else if (m_bv_util.is_bv_ule(n)) { // x <= y 784 app * a = to_app(n); 785 SASSERT(a->get_num_args() == 2); 786 const mpz & x = get_value(a->get_arg(0)); 787 const mpz & y = get_value(a->get_arg(1)); 788 int bv_sz = m_bv_util.get_bv_size(a->get_decl()->get_domain()[0]); 789 790 if (negated) { 791 if (m_mpz_manager.gt(x, y)) 792 res = 1.0; 793 else { 794 mpz diff; 795 m_mpz_manager.sub(y, x, diff); 796 m_mpz_manager.inc(diff); 797 rational n(diff); 798 n /= rational(m_powers(bv_sz)); 799 double dbl = n.get_double(); 800 // In extreme cases, n is 0.9999 but to_double returns something > 1.0 801 res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; 802 m_mpz_manager.del(diff); 803 } 804 } 805 else { 806 if (m_mpz_manager.le(x, y)) 807 res = 1.0; 808 else { 809 mpz diff; 810 m_mpz_manager.sub(x, y, diff); 811 rational n(diff); 812 n /= rational(m_powers(bv_sz)); 813 double dbl = n.get_double(); 814 res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; 815 m_mpz_manager.del(diff); 816 } 817 } 818 TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " << 819 m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; ); 820 } 821 else if (m_bv_util.is_bv_sle(n)) { // x <= y 822 app * a = to_app(n); 823 SASSERT(a->get_num_args() == 2); 824 mpz x; m_mpz_manager.set(x, get_value(a->get_arg(0))); 825 mpz y; m_mpz_manager.set(y, get_value(a->get_arg(1))); 826 unsigned bv_sz = m_bv_util.get_bv_size(a->get_decl()->get_domain()[0]); 827 const mpz & p = m_powers(bv_sz); 828 const mpz & p_half = m_powers(bv_sz-1); 829 if (x >= p_half) { m_mpz_manager.sub(x, p, x); } 830 if (y >= p_half) { m_mpz_manager.sub(y, p, y); } 831 832 if (negated) { 833 if (x > y) 834 res = 1.0; 835 else { 836 mpz diff; 837 m_mpz_manager.sub(y, x, diff); 838 m_mpz_manager.inc(diff); 839 rational n(diff); 840 n /= p; 841 double dbl = n.get_double(); 842 res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; 843 m_mpz_manager.del(diff); 844 } 845 TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " << 846 m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; ); 847 } 848 else { 849 if (x <= y) 850 res = 1.0; 851 else { 852 mpz diff; 853 m_mpz_manager.sub(x, y, diff); 854 SASSERT(!m_mpz_manager.is_neg(diff)); 855 rational n(diff); 856 n /= p; 857 double dbl = n.get_double(); 858 res = (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl; 859 m_mpz_manager.del(diff); 860 } 861 TRACE("sls_score", tout << "x = " << m_mpz_manager.to_string(x) << " ; y = " << 862 m_mpz_manager.to_string(y) << " ; SZ = " << bv_sz << std::endl; ); 863 } 864 m_mpz_manager.del(x); 865 m_mpz_manager.del(y); 866 } 867 else if (m_manager.is_not(n)) { 868 SASSERT(!negated); 869 app * a = to_app(n); 870 SASSERT(a->get_num_args() == 1); 871 expr * child = a->get_arg(0); 872 // Precondition: Assertion set is in NNF. 873 // Also: careful about the unsat assertion scaling further down. 874 if (m_manager.is_and(child) || m_manager.is_or(child)) 875 NOT_IMPLEMENTED_YET(); 876 res = score_bool(child, true); 877 } 878 else if (m_manager.is_distinct(n)) { 879 app * a = to_app(n); 880 unsigned pairs = 0, distinct_pairs = 0; 881 unsigned sz = a->get_num_args(); 882 for (unsigned i = 0; i < sz; i++) { 883 for (unsigned j = i+1; j < sz; j++) { 884 // pair i/j 885 const mpz & v0 = get_value(a->get_arg(0)); 886 const mpz & v1 = get_value(a->get_arg(1)); 887 pairs++; 888 if (v0 != v1) 889 distinct_pairs++; 890 } 891 } 892 res = (distinct_pairs/(double)pairs); 893 if (negated) res = 1.0 - res; 894 } 895 else 896 NOT_IMPLEMENTED_YET(); 897 898 SASSERT(res >= 0.0 && res <= 1.0); 899 900 app * a = to_app(n); 901 family_id afid = a->get_family_id(); 902 903 if (afid == m_bv_util.get_family_id()) 904 if (res < 1.0) res *= m_scale_unsat; 905 906 TRACE("sls_score", tout << "SCORE = " << res << std::endl; ); 907 return res; 908 } 909 score_bv(expr * n)910 double score_bv(expr * n) { 911 return 0.0; // a bv-expr is always scored as 0.0; we won't use those scores. 912 } 913 value2mpz(expr * n,mpz & result)914 void value2mpz(expr * n, mpz & result) { 915 m_mpz_manager.set(result, m_zero); 916 917 if (m_manager.is_bool(n)) { 918 m_mpz_manager.set(result, m_manager.is_true(n) ? m_one : m_zero); 919 } 920 else if (m_bv_util.is_bv(n)) { 921 unsigned bv_sz = m_bv_util.get_bv_size(n); 922 rational q; 923 if (!m_bv_util.is_numeral(n, q, bv_sz)) 924 NOT_IMPLEMENTED_YET(); 925 const mpq& temp = q.to_mpq(); 926 SASSERT(m_mpz_manager.is_one(temp.denominator())); 927 m_mpz_manager.set(result, temp.numerator()); 928 } 929 else 930 NOT_IMPLEMENTED_YET(); 931 } 932 mpz2value(sort * s,const mpz & r)933 expr_ref mpz2value(sort * s, const mpz & r) { 934 expr_ref res(m_manager); 935 if (m_manager.is_bool(s)) 936 res = (m_mpz_manager.is_zero(r)) ? m_manager.mk_false() : m_manager.mk_true(); 937 else if (m_bv_util.is_bv_sort(s)) { 938 rational rat(r); 939 res = m_bv_util.mk_numeral(rat, s); 940 } 941 else 942 NOT_IMPLEMENTED_YET(); 943 return res; 944 } 945 score(expr * n)946 double score(expr * n) { 947 if (m_manager.is_bool(n)) 948 return score_bool(n); 949 else if (m_bv_util.is_bv(n)) 950 return score_bv(n); 951 else { 952 NOT_IMPLEMENTED_YET(); 953 return 0; 954 } 955 } 956 get_constants(expr * e)957 ptr_vector<func_decl> & get_constants(expr * e) { 958 ptr_vector<func_decl> const & this_decls = m_constants_occ.find(e); 959 unsigned sz = this_decls.size(); 960 for (unsigned i = 0; i < sz; i++) { 961 func_decl * fd = this_decls[i]; 962 if (!m_temp_constants.contains(fd)) 963 m_temp_constants.push_back(fd); 964 } 965 return m_temp_constants; 966 } 967 get_unsat_constants_gsat(ptr_vector<expr> const & as)968 ptr_vector<func_decl> & get_unsat_constants_gsat(ptr_vector<expr> const & as) { 969 unsigned sz = as.size(); 970 if (sz == 1) { 971 if (m_mpz_manager.neq(get_value(as[0]), m_one)) 972 return get_constants(); 973 } 974 975 m_temp_constants.reset(); 976 977 for (unsigned i = 0; i < sz; i++) { 978 expr * q = as[i]; 979 if (m_mpz_manager.eq(get_value(q), m_one)) 980 continue; 981 ptr_vector<func_decl> const & this_decls = m_constants_occ.find(q); 982 unsigned sz2 = this_decls.size(); 983 for (unsigned j = 0; j < sz2; j++) { 984 func_decl * fd = this_decls[j]; 985 if (!m_temp_constants.contains(fd)) 986 m_temp_constants.push_back(fd); 987 } 988 } 989 return m_temp_constants; 990 } 991 get_unsat_constants_walksat(expr * e)992 ptr_vector<func_decl> & get_unsat_constants_walksat(expr * e) { 993 if (!e || !m_temp_constants.empty()) 994 return m_temp_constants; 995 ptr_vector<func_decl> const & this_decls = m_constants_occ.find(e); 996 unsigned sz = this_decls.size(); 997 for (unsigned j = 0; j < sz; j++) { 998 func_decl * fd = this_decls[j]; 999 if (!m_temp_constants.contains(fd)) 1000 m_temp_constants.push_back(fd); 1001 } 1002 return m_temp_constants; 1003 } 1004 get_unsat_constants(ptr_vector<expr> const & as)1005 ptr_vector<func_decl> & get_unsat_constants(ptr_vector<expr> const & as) { 1006 if (m_walksat) 1007 { 1008 expr * e = get_unsat_assertion(as); 1009 1010 if (!e) 1011 { 1012 m_temp_constants.reset(); 1013 return m_temp_constants; 1014 } 1015 1016 return get_unsat_constants_walksat(e); 1017 } 1018 else 1019 return get_unsat_constants_gsat(as); 1020 } 1021 get_unsat_assertion(ptr_vector<expr> const & as)1022 expr * get_unsat_assertion(ptr_vector<expr> const & as) { 1023 unsigned sz = as.size(); 1024 if (sz == 1) { 1025 if (m_mpz_manager.neq(get_value(as[0]), m_one)) 1026 return as[0]; 1027 else 1028 return nullptr; 1029 } 1030 m_temp_constants.reset(); 1031 1032 unsigned pos = -1; 1033 if (m_ucb) 1034 { 1035 double max = -1.0; 1036 // Andreas: Commented things here might be used for track_unsat data structures as done in SLS for SAT. But seems to have no benefit. 1037 /* for (unsigned i = 0; i < m_where_false.size(); i++) { 1038 expr * e = m_list_false[i]; */ 1039 for (unsigned i = 0; i < sz; i++) { 1040 expr * e = as[i]; 1041 if (m_mpz_manager.neq(get_value(e), m_one)) 1042 { 1043 value_score & vscore = m_scores.find(e); 1044 // Andreas: Select the assertion with the greatest ucb score. Potentially add some noise. 1045 // double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched); 1046 double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched) + m_ucb_noise * get_random_uint(8); 1047 if (q > max) { max = q; pos = i; } 1048 } 1049 } 1050 if (pos == static_cast<unsigned>(-1)) 1051 return nullptr; 1052 1053 m_touched++; 1054 m_scores.find(as[pos]).touched++; 1055 // Andreas: Also part of track_unsat data structures. Additionally disable the previous line! 1056 /* m_last_pos = pos; 1057 m_scores.find(m_list_false[pos]).touched++; 1058 return m_list_false[pos]; */ 1059 } 1060 else 1061 { 1062 // Andreas: The track_unsat data structures for random assertion selection. 1063 /* sz = m_where_false.size(); 1064 if (sz == 0) 1065 return 0; 1066 return m_list_false[get_random_uint(16) % sz]; */ 1067 1068 unsigned cnt_unsat = 0; 1069 for (unsigned i = 0; i < sz; i++) 1070 if (m_mpz_manager.neq(get_value(as[i]), m_one) && (get_random_uint(16) % ++cnt_unsat == 0)) pos = i; 1071 if (pos == static_cast<unsigned>(-1)) 1072 return nullptr; 1073 } 1074 1075 m_last_pos = pos; 1076 return as[pos]; 1077 } 1078 get_new_unsat_assertion(ptr_vector<expr> const & as)1079 expr * get_new_unsat_assertion(ptr_vector<expr> const & as) { 1080 unsigned sz = as.size(); 1081 if (sz == 1) 1082 return nullptr; 1083 m_temp_constants.reset(); 1084 1085 unsigned cnt_unsat = 0, pos = -1; 1086 for (unsigned i = 0; i < sz; i++) 1087 if ((i != m_last_pos) && m_mpz_manager.neq(get_value(as[i]), m_one) && (get_random_uint(16) % ++cnt_unsat == 0)) pos = i; 1088 1089 if (pos == static_cast<unsigned>(-1)) 1090 return nullptr; 1091 return as[pos]; 1092 } 1093 }; 1094 1095