1 /*++ 2 Copyright (c) 2013 Microsoft Corporation 3 4 Module Name: 5 6 opt_solver.cpp 7 8 Abstract: 9 10 Wraps smt::kernel as a solver for optimization 11 12 Author: 13 14 Anh-Dung Phan (t-anphan) 2013-10-16 15 16 Notes: 17 18 Based directly on smt_solver. 19 20 --*/ 21 #include <typeinfo> 22 #include "ast/reg_decl_plugins.h" 23 #include "opt/opt_solver.h" 24 #include "smt/smt_context.h" 25 #include "smt/theory_arith.h" 26 #include "smt/theory_diff_logic.h" 27 #include "smt/theory_dense_diff_logic.h" 28 #include "smt/theory_pb.h" 29 #include "smt/theory_lra.h" 30 #include "ast/ast_pp.h" 31 #include "ast/ast_smt_pp.h" 32 #include "ast/pp_params.hpp" 33 #include "opt/opt_params.hpp" 34 #include "model/model_smt2_pp.h" 35 #include "util/stopwatch.h" 36 37 namespace opt { 38 opt_solver(ast_manager & mgr,params_ref const & p,generic_model_converter & fm)39 opt_solver::opt_solver(ast_manager & mgr, params_ref const & p, 40 generic_model_converter& fm): 41 solver_na2as(mgr), 42 m_params(p), 43 m_context(mgr, m_params), 44 m(mgr), 45 m_fm(fm), 46 m_objective_terms(m), 47 m_dump_benchmarks(false), 48 m_first(true), 49 m_was_unknown(false) { 50 solver::updt_params(p); 51 m_params.updt_params(p); 52 if (m_params.m_case_split_strategy == CS_ACTIVITY_DELAY_NEW) { 53 m_params.m_relevancy_lvl = 0; 54 } 55 m_params.m_arith_auto_config_simplex = false; 56 m_params.m_threads = 1; // need to interact with the solver that created model so can't have threads 57 // m_params.m_auto_config = false; 58 } 59 60 unsigned opt_solver::m_dump_count = 0; 61 ~opt_solver()62 opt_solver::~opt_solver() { 63 } 64 updt_params(params_ref const & _p)65 void opt_solver::updt_params(params_ref const & _p) { 66 opt_params p(_p); 67 m_dump_benchmarks = p.dump_benchmarks(); 68 m_params.updt_params(_p); 69 m_context.updt_params(_p); 70 m_params.m_arith_auto_config_simplex = false; 71 } 72 translate(ast_manager & m,params_ref const & p)73 solver* opt_solver::translate(ast_manager& m, params_ref const& p) { 74 UNREACHABLE(); 75 return nullptr; 76 } 77 collect_param_descrs(param_descrs & r)78 void opt_solver::collect_param_descrs(param_descrs & r) { 79 m_context.collect_param_descrs(r); 80 } 81 collect_statistics(statistics & st) const82 void opt_solver::collect_statistics(statistics & st) const { 83 m_context.collect_statistics(st); 84 } 85 assert_expr_core(expr * t)86 void opt_solver::assert_expr_core(expr * t) { 87 m_last_model = nullptr; 88 if (has_quantifiers(t)) { 89 m_params.m_relevancy_lvl = 2; 90 } 91 m_context.assert_expr(t); 92 } 93 push_core()94 void opt_solver::push_core() { 95 m_context.push(); 96 } 97 pop_core(unsigned n)98 void opt_solver::pop_core(unsigned n) { 99 m_context.pop(n); 100 } 101 set_logic(symbol const & logic)102 void opt_solver::set_logic(symbol const& logic) { 103 m_logic = logic; 104 m_context.set_logic(logic); 105 } 106 ensure_pb()107 void opt_solver::ensure_pb() { 108 smt::theory_id th_id = m.get_family_id("pb"); 109 smt::theory* th = get_context().get_theory(th_id); 110 if (!th) { 111 get_context().register_plugin(alloc(smt::theory_pb, get_context())); 112 } 113 } 114 get_optimizer()115 smt::theory_opt& opt_solver::get_optimizer() { 116 smt::context& ctx = m_context.get_context(); 117 smt::theory_id arith_id = m_context.m().get_family_id("arith"); 118 smt::theory* arith_theory = ctx.get_theory(arith_id); 119 120 if (!arith_theory) { 121 ctx.register_plugin(alloc(smt::theory_mi_arith, ctx)); 122 arith_theory = ctx.get_theory(arith_id); 123 SASSERT(arith_theory); 124 } 125 if (typeid(smt::theory_mi_arith) == typeid(*arith_theory)) { 126 return dynamic_cast<smt::theory_mi_arith&>(*arith_theory); 127 } 128 else if (typeid(smt::theory_i_arith) == typeid(*arith_theory)) { 129 return dynamic_cast<smt::theory_i_arith&>(*arith_theory); 130 } 131 else if (typeid(smt::theory_inf_arith) == typeid(*arith_theory)) { 132 return dynamic_cast<smt::theory_inf_arith&>(*arith_theory); 133 } 134 else if (typeid(smt::theory_rdl&) == typeid(*arith_theory)) { 135 return dynamic_cast<smt::theory_rdl&>(*arith_theory); 136 } 137 else if (typeid(smt::theory_idl&) == typeid(*arith_theory)) { 138 return dynamic_cast<smt::theory_idl&>(*arith_theory); 139 } 140 else if (typeid(smt::theory_dense_mi&) == typeid(*arith_theory)) { 141 return dynamic_cast<smt::theory_dense_mi&>(*arith_theory); 142 } 143 else if (typeid(smt::theory_dense_i&) == typeid(*arith_theory)) { 144 return dynamic_cast<smt::theory_dense_i&>(*arith_theory); 145 } 146 else if (typeid(smt::theory_dense_smi&) == typeid(*arith_theory)) { 147 return dynamic_cast<smt::theory_dense_smi&>(*arith_theory); 148 } 149 else if (typeid(smt::theory_dense_si&) == typeid(*arith_theory)) { 150 return dynamic_cast<smt::theory_dense_si&>(*arith_theory); 151 } 152 else if (typeid(smt::theory_lra&) == typeid(*arith_theory)) { 153 return dynamic_cast<smt::theory_lra&>(*arith_theory); 154 } 155 else { 156 UNREACHABLE(); 157 return dynamic_cast<smt::theory_mi_arith&>(*arith_theory); 158 } 159 } 160 dump_benchmarks()161 bool opt_solver::dump_benchmarks() { 162 return m_dump_benchmarks; 163 } 164 check_sat_core2(unsigned num_assumptions,expr * const * assumptions)165 lbool opt_solver::check_sat_core2(unsigned num_assumptions, expr * const * assumptions) { 166 TRACE("opt_verbose", { 167 tout << "context size: " << m_context.size() << "\n"; 168 for (unsigned i = 0; i < m_context.size(); ++i) { 169 tout << mk_pp(m_context.get_formula(i), m_context.m()) << "\n"; 170 } 171 }); 172 stopwatch w; 173 if (dump_benchmarks()) { 174 w.start(); 175 std::stringstream file_name; 176 file_name << "opt_solver" << ++m_dump_count << ".smt2"; 177 std::ofstream buffer(file_name.str()); 178 to_smt2_benchmark(buffer, num_assumptions, assumptions, "opt_solver"); 179 buffer.close(); 180 IF_VERBOSE(1, verbose_stream() << "(created benchmark: " << file_name.str() << "..."; 181 verbose_stream().flush();); 182 } 183 lbool r; 184 m_last_model = nullptr; 185 if (m_first && num_assumptions == 0 && m_context.get_scope_level() == 0) { 186 r = m_context.setup_and_check(); 187 } 188 else { 189 r = m_context.check(num_assumptions, assumptions); 190 } 191 r = adjust_result(r); 192 if (r == l_true) { 193 m_context.get_model(m_last_model); 194 if (m_models.size() == 1) 195 m_models.set(0, m_last_model.get()); 196 } 197 m_first = false; 198 if (dump_benchmarks()) { 199 w.stop(); 200 IF_VERBOSE(1, verbose_stream() << ".. " << r << " " << std::fixed << w.get_seconds() << ")\n";); 201 } 202 return r; 203 } 204 maximize_objectives1(expr_ref_vector & blockers)205 bool opt_solver::maximize_objectives1(expr_ref_vector& blockers) { 206 expr_ref blocker(m); 207 for (unsigned i = 0; i < m_objective_vars.size(); ++i) { 208 if (!maximize_objective(i, blocker)) 209 return false; 210 blockers.push_back(blocker); 211 } 212 return true; 213 } 214 find_mutexes(expr_ref_vector const & vars,vector<expr_ref_vector> & mutexes)215 lbool opt_solver::find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) { 216 return m_context.find_mutexes(vars, mutexes); 217 } 218 preferred_sat(expr_ref_vector const & asms,vector<expr_ref_vector> & cores)219 lbool opt_solver::preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) { 220 return m_context.preferred_sat(asms, cores); 221 } 222 get_levels(ptr_vector<expr> const & vars,unsigned_vector & depth)223 void opt_solver::get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) { 224 return m_context.get_levels(vars, depth); 225 } 226 227 228 /** 229 \brief maximize the value of objective i in the current state. 230 Return a predicate that blocks the current maximal value. 231 232 The result of 'maximize' is post-processed. 233 When maximization involves shared symbols the model produced 234 by local optimization does not necessarily satisfy combination 235 constraints (it may not be a real model). 236 In this case, the model is post-processed (update_model 237 causes an additional call to final_check to propagate theory equalities 238 when 'has_shared' is true). 239 240 Precondition: the state of the solver is satisfiable and such that a current model can be extracted. 241 242 */ maximize_objective(unsigned i,expr_ref & blocker)243 bool opt_solver::maximize_objective(unsigned i, expr_ref& blocker) { 244 smt::theory_var v = m_objective_vars[i]; 245 bool has_shared = false; 246 m_last_model = nullptr; 247 // 248 // compute an optimization hint. 249 // The hint is valid if there are no shared symbols (a pure LP). 250 // Generally, the hint is not necessarily valid and has to be checked 251 // relative to other theories. 252 // 253 inf_eps val = get_optimizer().maximize(v, blocker, has_shared); 254 m_context.get_model(m_last_model); 255 inf_eps val2; 256 has_shared = true; 257 TRACE("opt", tout << (has_shared?"has shared":"non-shared") << " " << val << " " << blocker << "\n"; 258 if (m_last_model) tout << *m_last_model << "\n";); 259 if (!m_models[i]) 260 m_models.set(i, m_last_model.get()); 261 262 // 263 // retrieve value of objective from current model and update 264 // current optimal. 265 // 266 auto update_objective = [&]() { 267 rational r; 268 expr_ref value = (*m_last_model)(m_objective_terms.get(i)); 269 if (arith_util(m).is_numeral(value, r) && r > m_objective_values[i]) 270 m_objective_values[i] = inf_eps(r); 271 }; 272 273 update_objective(); 274 275 276 // 277 // check that "val" obtained from optimization hint is a valid bound. 278 // 279 auto check_bound = [&]() { 280 SASSERT(has_shared); 281 bool ok = bound_value(i, val); 282 if (l_true != m_context.check(0, nullptr)) 283 return false; 284 m_context.get_model(m_last_model); 285 update_objective(); 286 return ok; 287 }; 288 289 if (!val.is_finite()) { 290 // skip model updates 291 } 292 else if (m_context.get_context().update_model(has_shared)) { 293 TRACE("opt", tout << "updated\n";); 294 m_last_model = nullptr; 295 m_context.get_model(m_last_model); 296 if (!has_shared || val == current_objective_value(i)) 297 m_models.set(i, m_last_model.get()); 298 else if (!check_bound()) 299 return false; 300 } 301 else if (!check_bound()) 302 return false; 303 m_objective_values[i] = val; 304 TRACE("opt", { 305 tout << "objective: " << mk_pp(m_objective_terms.get(i), m) << "\n"; 306 tout << "maximal value: " << val << "\n"; 307 tout << "new condition: " << blocker << "\n"; 308 if (m_models[i]) model_smt2_pp(tout << "update model:\n", m, *m_models[i], 0); 309 if (m_last_model) model_smt2_pp(tout << "last model:\n", m, *m_last_model, 0); 310 }); 311 return true; 312 } 313 bound_value(unsigned i,inf_eps & val)314 bool opt_solver::bound_value(unsigned i, inf_eps& val) { 315 push_core(); 316 expr_ref ge = mk_ge(i, val); 317 assert_expr(ge); 318 lbool is_sat = m_context.check(0, nullptr); 319 is_sat = adjust_result(is_sat); 320 if (is_sat == l_true) { 321 m_context.get_model(m_last_model); 322 m_models.set(i, m_last_model.get()); 323 } 324 pop_core(1); 325 return is_sat == l_true; 326 } 327 adjust_result(lbool r)328 lbool opt_solver::adjust_result(lbool r) { 329 if (r == l_undef && m_context.last_failure() == smt::QUANTIFIERS) { 330 r = l_true; 331 m_was_unknown = true; 332 } 333 return r; 334 } 335 get_unsat_core(expr_ref_vector & r)336 void opt_solver::get_unsat_core(expr_ref_vector & r) { 337 r.reset(); 338 unsigned sz = m_context.get_unsat_core_size(); 339 for (unsigned i = 0; i < sz; i++) { 340 r.push_back(m_context.get_unsat_core_expr(i)); 341 } 342 } 343 get_model_core(model_ref & m)344 void opt_solver::get_model_core(model_ref & m) { 345 for (unsigned i = m_models.size(); i-- > 0; ) { 346 auto* mdl = m_models[i]; 347 if (mdl) { 348 TRACE("opt", tout << "get " << i << "\n" << *mdl << "\n";); 349 m = mdl; 350 return; 351 } 352 } 353 TRACE("opt", tout << "get last\n";); 354 m = m_last_model.get(); 355 } 356 get_proof()357 proof * opt_solver::get_proof() { 358 return m_context.get_proof(); 359 } 360 reason_unknown() const361 std::string opt_solver::reason_unknown() const { 362 return m_context.last_failure_as_string(); 363 } 364 set_reason_unknown(char const * msg)365 void opt_solver::set_reason_unknown(char const* msg) { 366 m_context.set_reason_unknown(msg); 367 } 368 get_labels(svector<symbol> & r)369 void opt_solver::get_labels(svector<symbol> & r) { 370 r.reset(); 371 buffer<symbol> tmp; 372 m_context.get_relevant_labels(nullptr, tmp); 373 r.append(tmp.size(), tmp.data()); 374 } 375 set_progress_callback(progress_callback * callback)376 void opt_solver::set_progress_callback(progress_callback * callback) { 377 m_callback = callback; 378 m_context.set_progress_callback(callback); 379 } 380 get_num_assertions() const381 unsigned opt_solver::get_num_assertions() const { 382 return m_context.size(); 383 } 384 get_assertion(unsigned idx) const385 expr * opt_solver::get_assertion(unsigned idx) const { 386 SASSERT(idx < get_num_assertions()); 387 return m_context.get_formula(idx); 388 } 389 add_objective(app * term)390 smt::theory_var opt_solver::add_objective(app* term) { 391 smt::theory_var v = get_optimizer().add_objective(term); 392 TRACE("opt", tout << v << " " << mk_pp(term, m) << "\n";); 393 m_objective_vars.push_back(v); 394 m_objective_values.push_back(inf_eps(rational::minus_one(), inf_rational())); 395 m_objective_terms.push_back(term); 396 m_models.push_back(nullptr); 397 return v; 398 } 399 get_objective_values()400 vector<inf_eps> const& opt_solver::get_objective_values() { 401 return m_objective_values; 402 } 403 saved_objective_value(unsigned i)404 inf_eps const& opt_solver::saved_objective_value(unsigned i) { 405 return m_objective_values[i]; 406 } 407 current_objective_value(unsigned i)408 inf_eps opt_solver::current_objective_value(unsigned i) { 409 smt::theory_var v = m_objective_vars[i]; 410 return get_optimizer().value(v); 411 } 412 mk_ge(unsigned var,inf_eps const & _val)413 expr_ref opt_solver::mk_ge(unsigned var, inf_eps const& _val) { 414 if (!_val.is_finite()) { 415 return expr_ref(_val.is_pos() ? m.mk_false() : m.mk_true(), m); 416 } 417 inf_eps val = _val; 418 if (val.get_infinitesimal().is_neg()) { 419 val = inf_eps(val.get_rational()); 420 } 421 smt::theory_opt& opt = get_optimizer(); 422 smt::theory_var v = m_objective_vars[var]; 423 TRACE("opt", tout << "v" << var << " " << val << "\n";); 424 425 if (typeid(smt::theory_inf_arith) == typeid(opt)) { 426 smt::theory_inf_arith& th = dynamic_cast<smt::theory_inf_arith&>(opt); 427 return th.mk_ge(m_fm, v, val); 428 } 429 430 if (typeid(smt::theory_mi_arith) == typeid(opt)) { 431 smt::theory_mi_arith& th = dynamic_cast<smt::theory_mi_arith&>(opt); 432 SASSERT(val.is_finite()); 433 return th.mk_ge(m_fm, v, val.get_numeral()); 434 } 435 436 if (typeid(smt::theory_i_arith) == typeid(opt)) { 437 SASSERT(val.is_finite()); 438 SASSERT(val.get_infinitesimal().is_zero()); 439 smt::theory_i_arith& th = dynamic_cast<smt::theory_i_arith&>(opt); 440 return th.mk_ge(m_fm, v, val.get_rational()); 441 } 442 443 if (typeid(smt::theory_idl) == typeid(opt)) { 444 smt::theory_idl& th = dynamic_cast<smt::theory_idl&>(opt); 445 return th.mk_ge(m_fm, v, val); 446 } 447 448 if (typeid(smt::theory_rdl) == typeid(opt)) { 449 smt::theory_rdl& th = dynamic_cast<smt::theory_rdl&>(opt); 450 return th.mk_ge(m_fm, v, val); 451 } 452 453 if (typeid(smt::theory_dense_i) == typeid(opt) && 454 val.get_infinitesimal().is_zero()) { 455 smt::theory_dense_i& th = dynamic_cast<smt::theory_dense_i&>(opt); 456 return th.mk_ge(m_fm, v, val); 457 } 458 459 if (typeid(smt::theory_dense_mi) == typeid(opt) && 460 val.get_infinitesimal().is_zero()) { 461 smt::theory_dense_mi& th = dynamic_cast<smt::theory_dense_mi&>(opt); 462 return th.mk_ge(m_fm, v, val); 463 } 464 465 if (typeid(smt::theory_lra) == typeid(opt)) { 466 smt::theory_lra& th = dynamic_cast<smt::theory_lra&>(opt); 467 SASSERT(val.is_finite()); 468 return th.mk_ge(m_fm, v, val.get_numeral()); 469 } 470 471 // difference logic? 472 if (typeid(smt::theory_dense_si) == typeid(opt) && 473 val.get_infinitesimal().is_zero()) { 474 smt::theory_dense_si& th = dynamic_cast<smt::theory_dense_si&>(opt); 475 return th.mk_ge(m_fm, v, val); 476 } 477 478 if (typeid(smt::theory_dense_smi) == typeid(opt) && 479 val.get_infinitesimal().is_zero()) { 480 smt::theory_dense_smi& th = dynamic_cast<smt::theory_dense_smi&>(opt); 481 return th.mk_ge(m_fm, v, val); 482 } 483 484 if (typeid(smt::theory_dense_mi) == typeid(opt)) { 485 smt::theory_dense_mi& th = dynamic_cast<smt::theory_dense_mi&>(opt); 486 return th.mk_ge(m_fm, v, val); 487 } 488 489 IF_VERBOSE(0, verbose_stream() << "WARNING: unhandled theory " << typeid(opt).name() << "\n";); 490 return expr_ref(m.mk_true(), m); 491 } 492 reset_objectives()493 void opt_solver::reset_objectives() { 494 m_objective_vars.reset(); 495 m_objective_values.reset(); 496 m_objective_terms.reset(); 497 } 498 to_opt(solver & s)499 opt_solver& opt_solver::to_opt(solver& s) { 500 if (typeid(opt_solver) != typeid(s)) { 501 throw default_exception("BUG: optimization context has not been initialized correctly"); 502 } 503 return dynamic_cast<opt_solver&>(s); 504 } 505 506 to_smt2_benchmark(std::ofstream & buffer,unsigned num_assumptions,expr * const * assumptions,char const * name,symbol const & logic,char const * status,char const * attributes)507 void opt_solver::to_smt2_benchmark( 508 std::ofstream & buffer, 509 unsigned num_assumptions, 510 expr * const * assumptions, 511 char const * name, 512 symbol const& logic, 513 char const * status, 514 char const * attributes) { 515 ast_smt_pp pp(m); 516 pp.set_benchmark_name(name); 517 pp.set_logic(logic); 518 pp.set_status(status); 519 pp.add_attributes(attributes); 520 pp_params params; 521 pp.set_simplify_implies(params.simplify_implies()); 522 523 for (unsigned i = 0; i < num_assumptions; ++i) { 524 pp.add_assumption(assumptions[i]); 525 } 526 for (unsigned i = 0; i < get_num_assertions(); ++i) { 527 pp.add_assumption(get_assertion(i)); 528 } 529 pp.display_smt2(buffer, m.mk_true()); 530 } 531 532 533 } 534