1 /*++ 2 Copyright (c) 2013 Microsoft Corporation 3 4 Module Name: 5 6 api_opt.cpp 7 8 Abstract: 9 API for optimization 10 11 Author: 12 13 Nikolaj Bjorner (nbjorner) 2013-12-3. 14 15 Revision History: 16 17 --*/ 18 #include<iostream> 19 #include "util/cancel_eh.h" 20 #include "util/scoped_timer.h" 21 #include "util/scoped_ctrl_c.h" 22 #include "util/file_path.h" 23 #include "parsers/smt2/smt2parser.h" 24 #include "model/model_params.hpp" 25 #include "opt/opt_context.h" 26 #include "opt/opt_cmds.h" 27 #include "opt/opt_parse.h" 28 #include "api/z3.h" 29 #include "api/api_log_macros.h" 30 #include "api/api_stats.h" 31 #include "api/api_context.h" 32 #include "api/api_util.h" 33 #include "api/api_model.h" 34 #include "api/api_ast_vector.h" 35 36 37 extern "C" { 38 39 struct Z3_optimize_ref : public api::object { 40 opt::context* m_opt; 41 Z3_optimize_ref(api::context& c): api::object(c), m_opt(nullptr) {} 42 ~Z3_optimize_ref() override { dealloc(m_opt); } 43 }; 44 inline Z3_optimize_ref * to_optimize(Z3_optimize o) { return reinterpret_cast<Z3_optimize_ref *>(o); } 45 inline Z3_optimize of_optimize(Z3_optimize_ref * o) { return reinterpret_cast<Z3_optimize>(o); } 46 inline opt::context* to_optimize_ptr(Z3_optimize o) { return to_optimize(o)->m_opt; } 47 48 Z3_optimize Z3_API Z3_mk_optimize(Z3_context c) { 49 Z3_TRY; 50 LOG_Z3_mk_optimize(c); 51 RESET_ERROR_CODE(); 52 Z3_optimize_ref * o = alloc(Z3_optimize_ref, *mk_c(c)); 53 o->m_opt = alloc(opt::context,mk_c(c)->m()); 54 mk_c(c)->save_object(o); 55 RETURN_Z3(of_optimize(o)); 56 Z3_CATCH_RETURN(nullptr); 57 } 58 59 void Z3_API Z3_optimize_inc_ref(Z3_context c, Z3_optimize o) { 60 Z3_TRY; 61 LOG_Z3_optimize_inc_ref(c, o); 62 RESET_ERROR_CODE(); 63 to_optimize(o)->inc_ref(); 64 Z3_CATCH; 65 } 66 67 void Z3_API Z3_optimize_dec_ref(Z3_context c, Z3_optimize o) { 68 Z3_TRY; 69 LOG_Z3_optimize_dec_ref(c, o); 70 RESET_ERROR_CODE(); 71 to_optimize(o)->dec_ref(); 72 Z3_CATCH; 73 } 74 75 void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a) { 76 Z3_TRY; 77 LOG_Z3_optimize_assert(c, o, a); 78 RESET_ERROR_CODE(); 79 CHECK_FORMULA(a,); 80 to_optimize_ptr(o)->add_hard_constraint(to_expr(a)); 81 Z3_CATCH; 82 } 83 84 void Z3_API Z3_optimize_assert_and_track(Z3_context c, Z3_optimize o, Z3_ast a, Z3_ast t) { 85 Z3_TRY; 86 LOG_Z3_optimize_assert_and_track(c, o, a, t); 87 RESET_ERROR_CODE(); 88 CHECK_FORMULA(a,); 89 CHECK_FORMULA(t,); 90 to_optimize_ptr(o)->add_hard_constraint(to_expr(a), to_expr(t)); 91 Z3_CATCH; 92 } 93 94 unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id) { 95 Z3_TRY; 96 LOG_Z3_optimize_assert_soft(c, o, a, weight, id); 97 RESET_ERROR_CODE(); 98 CHECK_FORMULA(a,0); 99 rational w(weight); 100 return to_optimize_ptr(o)->add_soft_constraint(to_expr(a), w, to_symbol(id)); 101 Z3_CATCH_RETURN(0); 102 } 103 104 unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t) { 105 Z3_TRY; 106 LOG_Z3_optimize_maximize(c, o, t); 107 RESET_ERROR_CODE(); 108 CHECK_VALID_AST(t,0); 109 return to_optimize_ptr(o)->add_objective(to_app(t), true); 110 Z3_CATCH_RETURN(0); 111 } 112 113 unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t) { 114 Z3_TRY; 115 LOG_Z3_optimize_minimize(c, o, t); 116 RESET_ERROR_CODE(); 117 CHECK_VALID_AST(t,0); 118 return to_optimize_ptr(o)->add_objective(to_app(t), false); 119 Z3_CATCH_RETURN(0); 120 } 121 122 void Z3_API Z3_optimize_push(Z3_context c,Z3_optimize d) { 123 Z3_TRY; 124 LOG_Z3_optimize_push(c, d); 125 RESET_ERROR_CODE(); 126 to_optimize_ptr(d)->push(); 127 Z3_CATCH; 128 } 129 130 void Z3_API Z3_optimize_pop(Z3_context c,Z3_optimize d) { 131 Z3_TRY; 132 LOG_Z3_optimize_pop(c, d); 133 RESET_ERROR_CODE(); 134 to_optimize_ptr(d)->pop(1); 135 Z3_CATCH; 136 } 137 138 139 Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o, unsigned num_assumptions, Z3_ast const assumptions[]) { 140 Z3_TRY; 141 LOG_Z3_optimize_check(c, o, num_assumptions, assumptions); 142 RESET_ERROR_CODE(); 143 for (unsigned i = 0; i < num_assumptions; i++) { 144 if (!is_expr(to_ast(assumptions[i]))) { 145 SET_ERROR_CODE(Z3_INVALID_ARG, "assumption is not an expression"); 146 return Z3_L_UNDEF; 147 } 148 } 149 lbool r = l_undef; 150 cancel_eh<reslimit> eh(mk_c(c)->m().limit()); 151 unsigned timeout = to_optimize_ptr(o)->get_params().get_uint("timeout", mk_c(c)->get_timeout()); 152 unsigned rlimit = to_optimize_ptr(o)->get_params().get_uint("rlimit", mk_c(c)->get_rlimit()); 153 bool use_ctrl_c = to_optimize_ptr(o)->get_params().get_bool("ctrl_c", true); 154 api::context::set_interruptable si(*(mk_c(c)), eh); 155 { 156 scoped_ctrl_c ctrlc(eh, false, use_ctrl_c); 157 scoped_timer timer(timeout, &eh); 158 scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit); 159 try { 160 expr_ref_vector asms(mk_c(c)->m()); 161 asms.append(num_assumptions, to_exprs(num_assumptions, assumptions)); 162 r = to_optimize_ptr(o)->optimize(asms); 163 } 164 catch (z3_exception& ex) { 165 if (mk_c(c)->m().inc()) { 166 mk_c(c)->handle_exception(ex); 167 } 168 r = l_undef; 169 if (!mk_c(c)->m().inc()) { 170 to_optimize_ptr(o)->set_reason_unknown(ex.msg()); 171 } 172 else { 173 mk_c(c)->handle_exception(ex); 174 } 175 } 176 // to_optimize_ref(d).cleanup(); 177 } 178 return of_lbool(r); 179 Z3_CATCH_RETURN(Z3_L_UNDEF); 180 } 181 182 Z3_ast_vector Z3_API Z3_optimize_get_unsat_core(Z3_context c, Z3_optimize o) { 183 Z3_TRY; 184 LOG_Z3_optimize_get_unsat_core(c, o); 185 RESET_ERROR_CODE(); 186 expr_ref_vector core(mk_c(c)->m()); 187 to_optimize_ptr(o)->get_unsat_core(core); 188 Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); 189 mk_c(c)->save_object(v); 190 for (expr* e : core) { 191 v->m_ast_vector.push_back(e); 192 } 193 RETURN_Z3(of_ast_vector(v)); 194 Z3_CATCH_RETURN(nullptr); 195 } 196 197 198 Z3_string Z3_API Z3_optimize_get_reason_unknown(Z3_context c, Z3_optimize o) { 199 Z3_TRY; 200 LOG_Z3_optimize_to_string(c, o); 201 RESET_ERROR_CODE(); 202 return mk_c(c)->mk_external_string(to_optimize_ptr(o)->reason_unknown()); 203 Z3_CATCH_RETURN(""); 204 } 205 206 Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o) { 207 Z3_TRY; 208 LOG_Z3_optimize_get_model(c, o); 209 RESET_ERROR_CODE(); 210 model_ref _m; 211 to_optimize_ptr(o)->get_model(_m); 212 Z3_model_ref * m_ref = alloc(Z3_model_ref, *mk_c(c)); 213 if (_m) { 214 model_params mp(to_optimize_ptr(o)->get_params()); 215 if (mp.compact()) _m->compress(); 216 m_ref->m_model = _m; 217 } 218 else { 219 m_ref->m_model = alloc(model, mk_c(c)->m()); 220 } 221 mk_c(c)->save_object(m_ref); 222 RETURN_Z3(of_model(m_ref)); 223 Z3_CATCH_RETURN(nullptr); 224 } 225 226 void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p) { 227 Z3_TRY; 228 LOG_Z3_optimize_set_params(c, o, p); 229 RESET_ERROR_CODE(); 230 param_descrs descrs; 231 to_optimize_ptr(o)->collect_param_descrs(descrs); 232 to_params(p)->m_params.validate(descrs); 233 to_optimize_ptr(o)->updt_params(to_param_ref(p)); 234 Z3_CATCH; 235 } 236 237 Z3_param_descrs Z3_API Z3_optimize_get_param_descrs(Z3_context c, Z3_optimize o) { 238 Z3_TRY; 239 LOG_Z3_optimize_get_param_descrs(c, o); 240 RESET_ERROR_CODE(); 241 Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref, *mk_c(c)); 242 mk_c(c)->save_object(d); 243 to_optimize_ptr(o)->collect_param_descrs(d->m_descrs); 244 Z3_param_descrs r = of_param_descrs(d); 245 RETURN_Z3(r); 246 Z3_CATCH_RETURN(nullptr); 247 } 248 249 // get lower value or current approximation 250 Z3_ast Z3_API Z3_optimize_get_lower(Z3_context c, Z3_optimize o, unsigned idx) { 251 Z3_TRY; 252 LOG_Z3_optimize_get_lower(c, o, idx); 253 RESET_ERROR_CODE(); 254 expr_ref e = to_optimize_ptr(o)->get_lower(idx); 255 mk_c(c)->save_ast_trail(e); 256 RETURN_Z3(of_expr(e)); 257 Z3_CATCH_RETURN(nullptr); 258 } 259 260 // get upper or current approximation 261 Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx) { 262 Z3_TRY; 263 LOG_Z3_optimize_get_upper(c, o, idx); 264 RESET_ERROR_CODE(); 265 expr_ref e = to_optimize_ptr(o)->get_upper(idx); 266 mk_c(c)->save_ast_trail(e); 267 RETURN_Z3(of_expr(e)); 268 Z3_CATCH_RETURN(nullptr); 269 } 270 271 // get lower value or current approximation 272 Z3_ast_vector Z3_API Z3_optimize_get_lower_as_vector(Z3_context c, Z3_optimize o, unsigned idx) { 273 Z3_TRY; 274 LOG_Z3_optimize_get_lower_as_vector(c, o, idx); 275 RESET_ERROR_CODE(); 276 expr_ref_vector es(mk_c(c)->m()); 277 to_optimize_ptr(o)->get_lower(idx, es); 278 Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); 279 mk_c(c)->save_object(v); 280 v->m_ast_vector.append(es.size(), (ast*const*)es.c_ptr()); 281 RETURN_Z3(of_ast_vector(v)); 282 Z3_CATCH_RETURN(nullptr); 283 } 284 285 // get upper or current approximation 286 Z3_ast_vector Z3_API Z3_optimize_get_upper_as_vector(Z3_context c, Z3_optimize o, unsigned idx) { 287 Z3_TRY; 288 LOG_Z3_optimize_get_upper_as_vector(c, o, idx); 289 RESET_ERROR_CODE(); 290 expr_ref_vector es(mk_c(c)->m()); 291 to_optimize_ptr(o)->get_upper(idx, es); 292 Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); 293 mk_c(c)->save_object(v); 294 v->m_ast_vector.append(es.size(), (ast*const*)es.c_ptr()); 295 RETURN_Z3(of_ast_vector(v)); 296 Z3_CATCH_RETURN(nullptr); 297 } 298 299 Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o) { 300 Z3_TRY; 301 LOG_Z3_optimize_to_string(c, o); 302 RESET_ERROR_CODE(); 303 return mk_c(c)->mk_external_string(to_optimize_ptr(o)->to_string()); 304 Z3_CATCH_RETURN(""); 305 } 306 307 Z3_string Z3_API Z3_optimize_get_help(Z3_context c, Z3_optimize d) { 308 Z3_TRY; 309 LOG_Z3_optimize_get_help(c, d); 310 RESET_ERROR_CODE(); 311 std::ostringstream buffer; 312 param_descrs descrs; 313 to_optimize_ptr(d)->collect_param_descrs(descrs); 314 descrs.display(buffer); 315 return mk_c(c)->mk_external_string(buffer.str()); 316 Z3_CATCH_RETURN(""); 317 } 318 319 Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c,Z3_optimize d) { 320 Z3_TRY; 321 LOG_Z3_optimize_get_statistics(c, d); 322 RESET_ERROR_CODE(); 323 Z3_stats_ref * st = alloc(Z3_stats_ref, *mk_c(c)); 324 to_optimize_ptr(d)->collect_statistics(st->m_stats); 325 mk_c(c)->save_object(st); 326 Z3_stats r = of_stats(st); 327 RETURN_Z3(r); 328 Z3_CATCH_RETURN(nullptr); 329 } 330 331 static void Z3_optimize_from_stream( 332 Z3_context c, 333 Z3_optimize opt, 334 std::istream& s, 335 char const* ext) { 336 ast_manager& m = mk_c(c)->m(); 337 if (ext && std::string("opb") == ext) { 338 unsigned_vector h; 339 parse_opb(*to_optimize_ptr(opt), s, h); 340 return; 341 } 342 if (ext && std::string("wcnf") == ext) { 343 unsigned_vector h; 344 parse_wcnf(*to_optimize_ptr(opt), s, h); 345 return; 346 } 347 if (ext && std::string("lp") == ext) { 348 unsigned_vector h; 349 parse_lp(*to_optimize_ptr(opt), s, h); 350 return; 351 } 352 scoped_ptr<cmd_context> ctx = alloc(cmd_context, false, &m); 353 install_opt_cmds(*ctx.get(), to_optimize_ptr(opt)); 354 std::stringstream errstrm; 355 ctx->set_regular_stream(errstrm); 356 ctx->set_ignore_check(true); 357 try { 358 if (!parse_smt2_commands(*ctx.get(), s)) { 359 ctx = nullptr; 360 SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str()); 361 return; 362 } 363 } 364 catch (z3_exception& e) { 365 errstrm << e.msg(); 366 ctx = nullptr; 367 SET_ERROR_CODE(Z3_PARSER_ERROR, errstrm.str()); 368 return; 369 } 370 371 for (expr * e : ctx->assertions()) { 372 to_optimize_ptr(opt)->add_hard_constraint(e); 373 } 374 } 375 376 377 378 void Z3_API Z3_optimize_from_string( 379 Z3_context c, 380 Z3_optimize d, 381 Z3_string s) { 382 Z3_TRY; 383 //LOG_Z3_optimize_from_string(c, d, s); 384 std::string str(s); 385 std::istringstream is(str); 386 Z3_optimize_from_stream(c, d, is, nullptr); 387 Z3_CATCH; 388 } 389 390 void Z3_API Z3_optimize_from_file( 391 Z3_context c, 392 Z3_optimize d, 393 Z3_string s) { 394 Z3_TRY; 395 //LOG_Z3_optimize_from_file(c, d, s); 396 std::ifstream is(s); 397 if (!is) { 398 std::ostringstream strm; 399 strm << "Could not open file " << s; 400 throw default_exception(strm.str()); 401 } 402 Z3_optimize_from_stream(c, d, is, get_extension(s)); 403 Z3_CATCH; 404 } 405 406 407 Z3_ast_vector Z3_API Z3_optimize_get_assertions(Z3_context c, Z3_optimize o) { 408 Z3_TRY; 409 LOG_Z3_optimize_get_assertions(c, o); 410 RESET_ERROR_CODE(); 411 Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); 412 mk_c(c)->save_object(v); 413 expr_ref_vector hard(mk_c(c)->m()); 414 to_optimize_ptr(o)->get_hard_constraints(hard); 415 for (expr* h : hard) { 416 v->m_ast_vector.push_back(h); 417 } 418 RETURN_Z3(of_ast_vector(v)); 419 Z3_CATCH_RETURN(nullptr); 420 } 421 422 Z3_ast_vector Z3_API Z3_optimize_get_objectives(Z3_context c, Z3_optimize o) { 423 Z3_TRY; 424 LOG_Z3_optimize_get_objectives(c, o); 425 RESET_ERROR_CODE(); 426 unsigned n = to_optimize_ptr(o)->num_objectives(); 427 Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); 428 mk_c(c)->save_object(v); 429 for (unsigned i = 0; i < n; i++) { 430 v->m_ast_vector.push_back(to_optimize_ptr(o)->get_objective(i)); 431 } 432 RETURN_Z3(of_ast_vector(v)); 433 Z3_CATCH_RETURN(nullptr); 434 } 435 436 437 438 }; 439