From 3bc31b6603ce4e8ca47cf890cb98325ed3de5969 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 31 Mar 2014 17:41:34 +0100 Subject: [PATCH 1/2] bvsls integration with opt::wmaxsmt Signed-off-by: Christoph M. Wintersteiger --- src/opt/weighted_maxsat.cpp | 40 ++-- src/tactic/sls/bvsls_opt_engine.cpp | 308 +++++++++++++++++++++++++--- src/tactic/sls/bvsls_opt_engine.h | 31 ++- src/tactic/sls/sls_evaluator.h | 8 + src/tactic/sls/sls_tracker.h | 38 ++++ 5 files changed, 385 insertions(+), 40 deletions(-) diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 5cf69b16b..9789f8b87 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -306,13 +306,13 @@ namespace opt { expr_dependency_ref core(m); goal_ref_buffer result; model_converter_ref model_converter; - (*simplify)(g, result, model_converter, pc, core); + (*simplify)(g, result, model_converter, pc, core); SASSERT(result.size() == 1); goal* r = result[0]; for (unsigned i = 0; i < r->size(); ++i) { m_bvsls.assert_expr(r->form(i)); - } - + } + m_lower = m_upper = rational::zero(); for (unsigned i = 0; i < m_soft.size(); ++i) { @@ -336,20 +336,28 @@ namespace opt { objective = bv.mk_bv_add(objective, es[i].get()); } } - // TBD: can we set an initial model on m_bvsls? - bvsls_opt_engine::optimization_result res = m_bvsls.optimize(objective); - switch(res.is_sat) { - case l_true: { - unsigned bv_size = 0; - // TBD: m_bvsls.get_model(m_model); - VERIFY(bv.is_numeral(res.optimum, m_lower, bv_size)); - break; + lbool is_sat = s.check_sat_core(0, 0); + if (is_sat == l_true) { + updt_model(s); + // TBD: can we set an initial model on m_bvsls? + // CMW: Yes, see next line. + bvsls_opt_engine::optimization_result res = m_bvsls.optimize(objective, m_model, true); + switch (res.is_sat) { + case l_true: { + unsigned bv_size = 0; + m_bvsls.get_model(m_model); + VERIFY(bv.is_numeral(res.optimum, m_lower, bv_size)); + break; + } + case l_false: + case l_undef: + break; + } + return res.is_sat; } - case l_false: - case l_undef: - break; - } - return res.is_sat; + else + return is_sat; + } /** diff --git a/src/tactic/sls/bvsls_opt_engine.cpp b/src/tactic/sls/bvsls_opt_engine.cpp index 2afdce295..cad496fd0 100644 --- a/src/tactic/sls/bvsls_opt_engine.cpp +++ b/src/tactic/sls/bvsls_opt_engine.cpp @@ -16,54 +16,316 @@ Author: Notes: --*/ +#include "nnf.h" #include "bvsls_opt_engine.h" bvsls_opt_engine::bvsls_opt_engine(ast_manager & m, params_ref const & p) : - sls_engine(m, p) + sls_engine(m, p), + m_hard_tracker(sls_engine::m_tracker), + m_obj_tracker(m, m_bv_util, m_mpz_manager, m_powers), + m_obj_evaluator(m, m_bv_util, m_obj_tracker, m_mpz_manager, m_powers) { + m_best_model = alloc(model, m); } bvsls_opt_engine::~bvsls_opt_engine() { } -bvsls_opt_engine::optimization_result bvsls_opt_engine::optimize(expr_ref const & objective) +bvsls_opt_engine::optimization_result bvsls_opt_engine::optimize( + expr_ref const & objective, + model_ref initial_model, + bool _maximize) { SASSERT(m_bv_util.is_bv(objective)); - m_tracker.initialize(m_assertions); - m_restart_limit = _RESTART_LIMIT_; + TRACE("sls_opt", tout << "objective: " << (_maximize?"maximize":"minimize") << " " << + mk_ismt2_pp(objective, m()) << std::endl;); + m_hard_tracker.initialize(m_assertions); + m_restart_limit = _RESTART_LIMIT_; + + if (initial_model.get() != 0) { + TRACE("sls_opt", tout << "Initial model provided: " << std::endl; + for (unsigned i = 0; i < initial_model->get_num_constants(); i++) { + func_decl * fd = initial_model->get_constant(i); + expr * val = initial_model->get_const_interp(fd); + tout << fd->get_name() << " := " << mk_ismt2_pp(val, m()) << std::endl; + }); + m_hard_tracker.set_model(initial_model); + } optimization_result res(m_manager); - do { - checkpoint(); + res.is_sat = m_hard_tracker.is_sat() ? l_true : l_undef; - IF_VERBOSE(1, verbose_stream() << "Optimizing... restarts left:" << (m_max_restarts - m_stats.m_restarts) << std::endl; ); - res.is_sat = search(); + if (!res.is_sat) { + do { + checkpoint(); - if (res.is_sat == l_undef) - { -#if _RESTART_INIT_ - m_tracker.randomize(); -#else - m_tracker.reset(m_assertions); -#endif - } - } while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ && - res.is_sat != l_true && m_stats.m_restarts++ < m_max_restarts); + IF_VERBOSE(1, verbose_stream() << "Satisfying... restarts left:" << (m_max_restarts - m_stats.m_restarts) << std::endl;); + res.is_sat = search(); + + if (res.is_sat == l_undef) + m_hard_tracker.randomize(m_assertions); + } while (m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ && + res.is_sat != l_true && m_stats.m_restarts++ < m_max_restarts); + } if (res.is_sat) - res.optimum = maximize(objective); + res.optimum = _maximize ? maximize(objective) : minimize(objective); + + TRACE("sls_opt", tout << "sat: " << res.is_sat << "; optimum: " << mk_ismt2_pp(res.optimum, m()) << std::endl;); return res; } expr_ref bvsls_opt_engine::maximize(expr_ref const & objective) { + SASSERT(m_hard_tracker.is_sat()); + + expr * obj_e = objective.get(); + unsigned obj_bv_sz = m_bv_util.get_bv_size(obj_e); + ptr_vector objs; + objs.push_back(obj_e); + m_obj_tracker.initialize(objs); + m_obj_evaluator.update_all(); + m_obj_tracker.set_model(m_hard_tracker.get_model()); + + TRACE("sls_opt", tout << "Initial opt model:" << std::endl; m_obj_tracker.show_model(tout);); + IF_VERBOSE(1, verbose_stream() << "Maximizing... restarts left:" << (m_max_restarts - m_stats.m_restarts) << std::endl;); + + mpz score, old_score, max_score, new_value; + unsigned new_const = (unsigned)-1, new_bit = 0; + ptr_vector consts = m_obj_tracker.get_constants(); + move_type move; + m_mpz_manager.set(score, m_obj_tracker.get_value(obj_e)); + m_mpz_manager.set(max_score, m_powers(obj_bv_sz)); m_mpz_manager.dec(max_score); + + save_model(score); + + while (check_restart((unsigned)m_stats.m_stopwatch.get_current_seconds()) && + m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ && + m_mpz_manager.lt(score, max_score)) { + checkpoint(); + m_stats.m_moves++; + m_mpz_manager.set(old_score, score); + new_const = (unsigned)-1; + + mpz score(0); + m_mpz_manager.set(score, + find_best_move(consts, score, new_const, new_value, new_bit, move, max_score, obj_e)); + + if (new_const == static_cast(-1)) { + m_mpz_manager.set(score, old_score); + if (m_mpz_manager.gt(score, m_best_model_score)) + save_model(score); + if (!randomize_wrt_hard()) { + // Can't improve and can't randomize; can't do anything other than bail out. + TRACE("sls_opt", tout << "Got stuck; bailing out." << std::endl;); + goto bailout; + } + m_mpz_manager.set(score, top_score()); + } + else { + TRACE("sls_opt", tout << "New best: " << m_mpz_manager.to_string(score) << std::endl;); + func_decl * fd = consts[new_const]; + incremental_score(fd, new_value); + m_mpz_manager.set(score, top_score()); + } + } + +bailout: + m_mpz_manager.del(new_value); + expr_ref res(m_manager); - res = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(objective)); - - // TODO. - + res = m_bv_util.mk_numeral(m_best_model_score, obj_bv_sz); return res; +} + +expr_ref bvsls_opt_engine::minimize(expr_ref const & objective) +{ + expr_ref n_obj(m_manager); + n_obj = m_bv_util.mk_bv_neg(objective); + return maximize(n_obj); +} + +void bvsls_opt_engine::save_model(mpz const & score) { + model_ref mdl = m_hard_tracker.get_model(); + model_ref obj_mdl = m_obj_tracker.get_model(); + + for (unsigned i = 0; i < obj_mdl->get_num_constants(); i++) { + func_decl * fd = obj_mdl->get_constant(i); + expr * val = obj_mdl->get_const_interp(fd); + if (mdl->has_interpretation(fd)) { + if (mdl->get_const_interp(fd) != val) + TRACE("sls_opt", tout << "model disagreement on " << fd->get_name() << ": " << + mk_ismt2_pp(val, m()) << " != " << mk_ismt2_pp(mdl->get_const_interp(fd), m()) << std::endl;); + SASSERT(mdl->get_const_interp(fd) == val); + } + else + mdl->register_decl(fd, val); + } + + m_best_model = mdl; + m_mpz_manager.set(m_best_model_score, score); +} + +// checks whether the score outcome of a given move is better than the previous score +bool bvsls_opt_engine::what_if( + func_decl * fd, + const unsigned & fd_inx, + const mpz & temp, + mpz & best_score, + unsigned & best_const, + mpz & best_value) +{ +#if _EARLY_PRUNE_ + double r = incremental_score_prune(fd, temp); +#else + double r = incremental_score(fd, temp); +#endif + + if (r >= 1.0 && m_tracker.is_sat()) { + m_obj_evaluator.update(fd, temp); + mpz cur_best(0); + m_mpz_manager.set(cur_best, top_score()); + + TRACE("sls_whatif", tout << "WHAT IF " << fd->get_name() << " WERE " << m_mpz_manager.to_string(temp) << + " --> " << r << "; score=" << m_mpz_manager.to_string(cur_best) << std::endl;); + + if (m_mpz_manager.gt(cur_best, best_score)) { + m_mpz_manager.set(best_score, cur_best); + best_const = fd_inx; + m_mpz_manager.set(best_value, temp); + return true; + } + } + + return false; +} + +mpz bvsls_opt_engine::find_best_move( + ptr_vector & to_evaluate, + mpz score, + unsigned & best_const, + mpz & best_value, + unsigned & new_bit, + move_type & move, + mpz const & max_score, + expr * objective) +{ + mpz old_value, temp; +#if _USE_MUL3_ || _USE_UNARY_MINUS_ + mpz temp2; +#endif + unsigned bv_sz; + mpz new_score = score; + + for (unsigned i = 0; i < to_evaluate.size() && m_mpz_manager.lt(new_score, max_score); i++) { + func_decl * fd = to_evaluate[i]; + sort * srt = fd->get_range(); + bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt); + m_mpz_manager.set(old_value, m_tracker.get_value(fd)); + + // first try to flip every bit + for (unsigned j = 0; j < bv_sz && m_mpz_manager.lt(new_score, max_score); j++) { + // What would happen if we flipped bit #i ? + mk_flip(srt, old_value, j, temp); + + if (what_if(fd, i, temp, new_score, best_const, best_value)) { + new_bit = j; + move = MV_FLIP; + } + } + + if (m_bv_util.is_bv_sort(srt) && bv_sz > 1) { +#if _USE_ADDSUB_ + if (!m_mpz_manager.is_even(old_value)) { + // for odd values, try +1 + mk_inc(bv_sz, old_value, temp); + if (what_if(fd, i, temp, new_score, best_const, best_value)) + move = MV_INC; + } + else { + // for even values, try -1 + mk_dec(bv_sz, old_value, temp); + if (what_if(fd, i, temp, new_score, best_const, best_value)) + move = MV_DEC; + } +#endif + // try inverting + mk_inv(bv_sz, old_value, temp); + if (what_if(fd, i, temp, new_score, best_const, best_value)) + move = MV_INV; + +#if _USE_UNARY_MINUS_ + mk_inc(bv_sz, temp, temp2); + if (what_if(fd, i, temp2, new_score, best_const, best_value)) + move = MV_UMIN; +#endif + +#if _USE_MUL2DIV2_ + // try multiplication by 2 + mk_mul2(bv_sz, old_value, temp); + if (what_if(fd, i, temp, new_score, best_const, best_value)) + move = MV_MUL2; + +#if _USE_MUL3_ + // try multiplication by 3 + mk_add(bv_sz, old_value, temp, temp2); + if (what_if(fd, i, temp2, new_score, best_const, best_value)) + move = MV_MUL3; +#endif + + // try division by 2 + mk_div2(bv_sz, old_value, temp); + if (what_if(fd, i, temp, new_score, best_const, best_value)) + move = MV_DIV2; +#endif + } + + // reset to what it was before + double check = incremental_score(fd, old_value); + } + + m_mpz_manager.del(old_value); + m_mpz_manager.del(temp); +#if _USE_MUL3_ + m_mpz_manager.del(temp2); +#endif + + return new_score; +} + +bool bvsls_opt_engine::randomize_wrt_hard() { + ptr_vector consts = m_obj_tracker.get_constants(); + unsigned csz = consts.size(); + unsigned retry_count = csz; + + while (retry_count-- > 0) + { + + unsigned ri = (m_tracker.get_random_uint((csz < 16) ? 4 : (csz < 256) ? 8 : (csz < 4096) ? 12 : (csz < 65536) ? 16 : 32)) % csz; + func_decl * random_fd = consts[ri]; // Random constant + + mpz random_val; // random value. + m_mpz_manager.set(random_val, m_tracker.get_random(random_fd->get_range())); + + mpz old_value; + m_mpz_manager.set(old_value, m_tracker.get_value(random_fd)); + + if (!m_mpz_manager.eq(random_val, old_value)) { + m_evaluator.update(random_fd, random_val); + + if (m_hard_tracker.is_sat()) { + TRACE("sls_opt", tout << "Randomizing " << random_fd->get_name() << " to " << + m_mpz_manager.to_string(random_val) << std::endl;); + m_obj_evaluator.update(random_fd, random_val); + return true; + } + else + m_evaluator.update(random_fd, old_value); + } + } + + return false; } \ No newline at end of file diff --git a/src/tactic/sls/bvsls_opt_engine.h b/src/tactic/sls/bvsls_opt_engine.h index 326e51df4..befd00353 100644 --- a/src/tactic/sls/bvsls_opt_engine.h +++ b/src/tactic/sls/bvsls_opt_engine.h @@ -22,6 +22,12 @@ Notes: #include "sls_engine.h" class bvsls_opt_engine : public sls_engine { + sls_tracker & m_hard_tracker; + sls_tracker m_obj_tracker; + sls_evaluator m_obj_evaluator; + model_ref m_best_model; + mpz m_best_model_score; + public: bvsls_opt_engine(ast_manager & m, params_ref const & p); ~bvsls_opt_engine(); @@ -33,10 +39,33 @@ public: optimization_result(ast_manager & m) : is_sat(l_undef), optimum(m) {} }; - optimization_result optimize(expr_ref const & objective); + optimization_result optimize(expr_ref const & objective, model_ref initial_model = model_ref(), bool maximize=true); + + void get_model(model_ref & result) { result = m_best_model; } protected: expr_ref maximize(expr_ref const & objective); + expr_ref minimize(expr_ref const & objective); + + bool what_if(func_decl * fd, const unsigned & fd_inx, const mpz & temp, + mpz & best_score, unsigned & best_const, mpz & best_value); + + mpz find_best_move(ptr_vector & to_evaluate, mpz score, + unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move, + mpz const & max_score, expr * objective); + + mpz top_score(void) { + mpz res(0); + obj_hashtable const & top_exprs = m_obj_tracker.get_top_exprs(); + for (obj_hashtable::iterator it = top_exprs.begin(); + it != top_exprs.end(); + it++) + m_mpz_manager.add(res, m_obj_tracker.get_value(*it), res); + return res; + } + + void save_model(mpz const & score); + bool randomize_wrt_hard(); }; #endif \ No newline at end of file diff --git a/src/tactic/sls/sls_evaluator.h b/src/tactic/sls/sls_evaluator.h index 0053763bb..5e8b10488 100644 --- a/src/tactic/sls/sls_evaluator.h +++ b/src/tactic/sls/sls_evaluator.h @@ -138,6 +138,14 @@ public: } break; } + case OP_ITE: { + SASSERT(n_args = 3); + if (m_mpz_manager.is_one(m_tracker.get_value(args[0]))) + m_mpz_manager.set(result, m_tracker.get_value(args[1])); + else + m_mpz_manager.set(result, m_tracker.get_value(args[2])); + break; + } default: NOT_IMPLEMENTED_YET(); } diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h index 50d0e4188..188df66b1 100644 --- a/src/tactic/sls/sls_tracker.h +++ b/src/tactic/sls/sls_tracker.h @@ -133,6 +133,19 @@ public: } #endif + inline obj_hashtable const & get_top_exprs() { + return m_top_expr; + } + + inline bool is_sat() { + for (obj_hashtable::iterator it = m_top_expr.begin(); + it != m_top_expr.end(); + it++) + if (!m_mpz_manager.is_one(get_value(*it))) + return false; + return true; + } + inline void set_value(expr * n, const mpz & r) { SASSERT(m_scores.contains(n)); m_mpz_manager.set(m_scores.find(n).value, r); @@ -522,6 +535,28 @@ public: } } + void set_model(model_ref const & mdl) { + for (unsigned i = 0; i < mdl->get_num_constants(); i++) { + func_decl * fd = mdl->get_constant(i); + expr * val = mdl->get_const_interp(fd); + if (m_entry_points.contains(fd)) { + if (m_manager.is_bool(val)) { + set_value(fd, m_manager.is_true(val) ? m_mpz_manager.mk_z(1) : m_mpz_manager.mk_z(0)); + } + else if (m_bv_util.is_numeral(val)) { + rational r_val; + unsigned bv_sz; + m_bv_util.is_numeral(val, r_val, bv_sz); + mpq q = r_val.to_mpq(); + SASSERT(m_mpz_manager.is_one(q.denominator())); + set_value(fd, q.numerator()); + } + else + NOT_IMPLEMENTED_YET(); + } + } + } + model_ref get_model() { model_ref res = alloc(model, m_manager); unsigned sz = get_num_constants(); @@ -674,6 +709,9 @@ public: m_scores.find(n).has_pos_occ = 1; } } + else if (m_bv_util.is_bv(n)) { + /* CMW: I need this for optimization. Safe to ignore? */ + } else NOT_IMPLEMENTED_YET(); } From 7d896e5a9a21039a66cba34b4c5c78e6cbe645c8 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 31 Mar 2014 17:58:19 +0100 Subject: [PATCH 2/2] bvsls_opt_engine bugfix Signed-off-by: Christoph M. Wintersteiger --- src/tactic/sls/bvsls_opt_engine.cpp | 30 ++++++++++++++++++----------- 1 file changed, 19 insertions(+), 11 deletions(-) diff --git a/src/tactic/sls/bvsls_opt_engine.cpp b/src/tactic/sls/bvsls_opt_engine.cpp index cad496fd0..37587428c 100644 --- a/src/tactic/sls/bvsls_opt_engine.cpp +++ b/src/tactic/sls/bvsls_opt_engine.cpp @@ -86,9 +86,9 @@ expr_ref bvsls_opt_engine::maximize(expr_ref const & objective) unsigned obj_bv_sz = m_bv_util.get_bv_size(obj_e); ptr_vector objs; objs.push_back(obj_e); - m_obj_tracker.initialize(objs); - m_obj_evaluator.update_all(); + m_obj_tracker.initialize(objs); m_obj_tracker.set_model(m_hard_tracker.get_model()); + m_obj_evaluator.update_all(); TRACE("sls_opt", tout << "Initial opt model:" << std::endl; m_obj_tracker.show_model(tout);); IF_VERBOSE(1, verbose_stream() << "Maximizing... restarts left:" << (m_max_restarts - m_stats.m_restarts) << std::endl;); @@ -97,10 +97,10 @@ expr_ref bvsls_opt_engine::maximize(expr_ref const & objective) unsigned new_const = (unsigned)-1, new_bit = 0; ptr_vector consts = m_obj_tracker.get_constants(); move_type move; - m_mpz_manager.set(score, m_obj_tracker.get_value(obj_e)); + m_mpz_manager.set(score, top_score()); m_mpz_manager.set(max_score, m_powers(obj_bv_sz)); m_mpz_manager.dec(max_score); - save_model(score); + save_model(score); while (check_restart((unsigned)m_stats.m_stopwatch.get_current_seconds()) && m_stats.m_stopwatch.get_current_seconds() < _TIMELIMIT_ && @@ -129,6 +129,7 @@ expr_ref bvsls_opt_engine::maximize(expr_ref const & objective) TRACE("sls_opt", tout << "New best: " << m_mpz_manager.to_string(score) << std::endl;); func_decl * fd = consts[new_const]; incremental_score(fd, new_value); + m_obj_evaluator.update(fd, new_value); m_mpz_manager.set(score, top_score()); } } @@ -184,7 +185,7 @@ bool bvsls_opt_engine::what_if( double r = incremental_score(fd, temp); #endif - if (r >= 1.0 && m_tracker.is_sat()) { + if (r >= 1.0 && m_hard_tracker.is_sat()) { m_obj_evaluator.update(fd, temp); mpz cur_best(0); m_mpz_manager.set(cur_best, top_score()); @@ -199,6 +200,11 @@ bool bvsls_opt_engine::what_if( return true; } } + else + { + TRACE("sls_whatif_failed", tout << "WHAT IF " << fd->get_name() << " WERE " << m_mpz_manager.to_string(temp) << + " --> unsatisfied hard constraints" << std::endl;); + } return false; } @@ -218,13 +224,14 @@ mpz bvsls_opt_engine::find_best_move( mpz temp2; #endif unsigned bv_sz; - mpz new_score = score; + mpz new_score; + m_mpz_manager.set(new_score, score); for (unsigned i = 0; i < to_evaluate.size() && m_mpz_manager.lt(new_score, max_score); i++) { func_decl * fd = to_evaluate[i]; sort * srt = fd->get_range(); bv_sz = (m_manager.is_bool(srt)) ? 1 : m_bv_util.get_bv_size(srt); - m_mpz_manager.set(old_value, m_tracker.get_value(fd)); + m_mpz_manager.set(old_value, m_obj_tracker.get_value(fd)); // first try to flip every bit for (unsigned j = 0; j < bv_sz && m_mpz_manager.lt(new_score, max_score); j++) { @@ -285,6 +292,7 @@ mpz bvsls_opt_engine::find_best_move( // reset to what it was before double check = incremental_score(fd, old_value); + m_obj_evaluator.update(fd, old_value); } m_mpz_manager.del(old_value); @@ -304,21 +312,21 @@ bool bvsls_opt_engine::randomize_wrt_hard() { while (retry_count-- > 0) { - unsigned ri = (m_tracker.get_random_uint((csz < 16) ? 4 : (csz < 256) ? 8 : (csz < 4096) ? 12 : (csz < 65536) ? 16 : 32)) % csz; + unsigned ri = (m_obj_tracker.get_random_uint((csz < 16) ? 4 : (csz < 256) ? 8 : (csz < 4096) ? 12 : (csz < 65536) ? 16 : 32)) % csz; func_decl * random_fd = consts[ri]; // Random constant mpz random_val; // random value. - m_mpz_manager.set(random_val, m_tracker.get_random(random_fd->get_range())); + m_mpz_manager.set(random_val, m_obj_tracker.get_random(random_fd->get_range())); mpz old_value; - m_mpz_manager.set(old_value, m_tracker.get_value(random_fd)); + m_mpz_manager.set(old_value, m_obj_tracker.get_value(random_fd)); if (!m_mpz_manager.eq(random_val, old_value)) { m_evaluator.update(random_fd, random_val); if (m_hard_tracker.is_sat()) { TRACE("sls_opt", tout << "Randomizing " << random_fd->get_name() << " to " << - m_mpz_manager.to_string(random_val) << std::endl;); + m_mpz_manager.to_string(random_val) << std::endl;); m_obj_evaluator.update(random_fd, random_val); return true; }