1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 api_datalog.cpp 7 8 Abstract: 9 Datalog API 10 11 Author: 12 13 Leonardo de Moura (leonardo) 2012-02-29. 14 15 Revision History: 16 17 --*/ 18 #include "api/api_datalog.h" 19 #include "api/api_context.h" 20 #include "api/api_util.h" 21 #include "ast/ast_pp.h" 22 #include "api/api_ast_vector.h" 23 #include "api/api_log_macros.h" 24 #include "api/api_stats.h" 25 #include "muz/fp/datalog_parser.h" 26 #include "util/cancel_eh.h" 27 #include "util/scoped_ctrl_c.h" 28 #include "util/scoped_timer.h" 29 #include "muz/fp/dl_cmds.h" 30 #include "cmd_context/cmd_context.h" 31 #include "parsers/smt2/smt2parser.h" 32 #include "muz/base/dl_context.h" 33 #include "muz/fp/dl_register_engine.h" 34 #include "muz/rel/dl_external_relation.h" 35 #include "ast/dl_decl_plugin.h" 36 #include "muz/rel/rel_context.h" 37 38 namespace api { 39 40 class fixedpoint_context : public datalog::external_relation_context { 41 void * m_state; 42 reduce_app_callback_fptr m_reduce_app; 43 reduce_assign_callback_fptr m_reduce_assign; 44 datalog::register_engine m_register_engine; 45 datalog::context m_context; 46 ast_ref_vector m_trail; 47 public: fixedpoint_context(ast_manager & m,smt_params & p)48 fixedpoint_context(ast_manager& m, smt_params& p): 49 m_state(nullptr), 50 m_reduce_app(nullptr), 51 m_reduce_assign(nullptr), 52 m_context(m, m_register_engine, p), 53 m_trail(m) {} 54 ~fixedpoint_context()55 ~fixedpoint_context() override {} get_family_id() const56 family_id get_family_id() const override { return const_cast<datalog::context&>(m_context).get_decl_util().get_family_id(); } set_state(void * state)57 void set_state(void* state) { 58 SASSERT(!m_state); 59 m_state = state; 60 symbol name("datalog_relation"); 61 ast_manager& m = m_context.get_manager(); 62 if (!m.has_plugin(name)) { 63 m.register_plugin(name, alloc(datalog::dl_decl_plugin)); 64 } 65 datalog::rel_context_base* rel = m_context.get_rel_context(); 66 if (rel) { 67 datalog::relation_manager& r = rel->get_rmanager(); 68 r.register_plugin(alloc(datalog::external_relation_plugin, *this, r)); 69 } 70 } set_reduce_app(reduce_app_callback_fptr f)71 void set_reduce_app(reduce_app_callback_fptr f) { 72 m_reduce_app = f; 73 } set_reduce_assign(reduce_assign_callback_fptr f)74 void set_reduce_assign(reduce_assign_callback_fptr f) { 75 m_reduce_assign = f; 76 } reduce(func_decl * f,unsigned num_args,expr * const * args,expr_ref & result)77 void reduce(func_decl* f, unsigned num_args, expr * const* args, expr_ref& result) override { 78 expr* r = nullptr; 79 if (m_reduce_app) { 80 m_reduce_app(m_state, f, num_args, args, &r); 81 result = r; 82 m_trail.push_back(f); 83 for (unsigned i = 0; i < num_args; ++i) { 84 m_trail.push_back(args[i]); 85 } 86 m_trail.push_back(r); 87 } 88 // allow fallthrough. 89 if (r == nullptr) { 90 ast_manager& m = m_context.get_manager(); 91 result = m.mk_app(f, num_args, args); 92 } 93 } reduce_assign(func_decl * f,unsigned num_args,expr * const * args,unsigned num_out,expr * const * outs)94 void reduce_assign(func_decl* f, unsigned num_args, expr * const* args, unsigned num_out, expr* const* outs) override { 95 if (m_reduce_assign) { 96 m_trail.push_back(f); 97 for (unsigned i = 0; i < num_args; ++i) { 98 m_trail.push_back(args[i]); 99 } 100 m_reduce_assign(m_state, f, num_args, args, num_out, outs); 101 } 102 } ctx()103 datalog::context& ctx() { return m_context; } add_rule(expr * rule,symbol const & name)104 void add_rule(expr* rule, symbol const& name) { 105 m_context.add_rule(rule, name); 106 } update_rule(expr * rule,symbol const & name)107 void update_rule(expr* rule, symbol const& name) { 108 m_context.update_rule(rule, name); 109 } add_table_fact(func_decl * r,unsigned num_args,unsigned args[])110 void add_table_fact(func_decl* r, unsigned num_args, unsigned args[]) { 111 m_context.add_table_fact(r, num_args, args); 112 } get_last_status()113 std::string get_last_status() { 114 datalog::execution_result status = m_context.get_status(); 115 switch(status) { 116 case datalog::INPUT_ERROR: 117 return "input error"; 118 case datalog::OK: 119 return "ok"; 120 case datalog::TIMEOUT: 121 return "timeout"; 122 case datalog::APPROX: 123 return "approximated"; 124 default: 125 UNREACHABLE(); 126 return "unknown"; 127 } 128 } to_string(unsigned num_queries,expr * const * queries)129 std::string to_string(unsigned num_queries, expr* const* queries) { 130 std::stringstream str; 131 m_context.display_smt2(num_queries, queries, str); 132 return str.str(); 133 } get_num_levels(func_decl * pred)134 unsigned get_num_levels(func_decl* pred) { 135 return m_context.get_num_levels(pred); 136 } get_cover_delta(int level,func_decl * pred)137 expr_ref get_cover_delta(int level, func_decl* pred) { 138 return m_context.get_cover_delta(level, pred); 139 } add_cover(int level,func_decl * pred,expr * predicate)140 void add_cover(int level, func_decl* pred, expr* predicate) { 141 m_context.add_cover(level, pred, predicate); 142 } collect_param_descrs(param_descrs & p)143 void collect_param_descrs(param_descrs & p) { m_context.collect_params(p); } updt_params(params_ref const & p)144 void updt_params(params_ref const& p) { m_context.updt_params(p); } 145 }; 146 }; 147 148 extern "C" { 149 150 //////////////////////////////////// 151 // Datalog utilities 152 // 153 154 Z3_get_relation_arity(Z3_context c,Z3_sort s)155 unsigned Z3_API Z3_get_relation_arity(Z3_context c, Z3_sort s) { 156 Z3_TRY; 157 LOG_Z3_get_relation_arity(c, s); 158 RESET_ERROR_CODE(); 159 sort * r = to_sort(s); 160 if (Z3_get_sort_kind(c, s) != Z3_RELATION_SORT) { 161 SET_ERROR_CODE(Z3_INVALID_ARG, "sort should be a relation"); 162 return 0; 163 } 164 return r->get_num_parameters(); 165 Z3_CATCH_RETURN(0); 166 } 167 Z3_get_relation_column(Z3_context c,Z3_sort s,unsigned col)168 Z3_sort Z3_API Z3_get_relation_column(Z3_context c, Z3_sort s, unsigned col) { 169 Z3_TRY; 170 LOG_Z3_get_relation_column(c, s, col); 171 RESET_ERROR_CODE(); 172 sort * r = to_sort(s); 173 if (Z3_get_sort_kind(c, s) != Z3_RELATION_SORT) { 174 SET_ERROR_CODE(Z3_INVALID_ARG, "sort should be a relation"); 175 RETURN_Z3(nullptr); 176 } 177 if (col >= r->get_num_parameters()) { 178 SET_ERROR_CODE(Z3_IOB, nullptr); 179 RETURN_Z3(nullptr); 180 } 181 parameter const& p = r->get_parameter(col); 182 if (!p.is_ast() || !is_sort(p.get_ast())) { 183 UNREACHABLE(); 184 warning_msg("Sort parameter expected at %d", col); 185 SET_ERROR_CODE(Z3_INTERNAL_FATAL, "sort parameter expected"); 186 RETURN_Z3(nullptr); 187 } 188 Z3_sort res = of_sort(to_sort(p.get_ast())); 189 RETURN_Z3(res); 190 Z3_CATCH_RETURN(nullptr); 191 } 192 Z3_mk_finite_domain_sort(Z3_context c,Z3_symbol name,uint64_t size)193 Z3_sort Z3_API Z3_mk_finite_domain_sort(Z3_context c, Z3_symbol name, uint64_t size) { 194 Z3_TRY; 195 LOG_Z3_mk_finite_domain_sort(c, name, size); 196 RESET_ERROR_CODE(); 197 sort* s = mk_c(c)->datalog_util().mk_sort(to_symbol(name), size); 198 mk_c(c)->save_ast_trail(s); 199 RETURN_Z3(of_sort(s)); 200 Z3_CATCH_RETURN(nullptr); 201 } 202 Z3_get_finite_domain_sort_size(Z3_context c,Z3_sort s,uint64_t * out)203 bool Z3_API Z3_get_finite_domain_sort_size(Z3_context c, Z3_sort s, uint64_t * out) { 204 Z3_TRY; 205 if (out) { 206 *out = 0; 207 } 208 if (Z3_get_sort_kind(c, s) != Z3_FINITE_DOMAIN_SORT) { 209 return false; 210 } 211 if (!out) { 212 return false; 213 } 214 // must start logging here, since function uses Z3_get_sort_kind above 215 LOG_Z3_get_finite_domain_sort_size(c, s, out); 216 RESET_ERROR_CODE(); 217 VERIFY(mk_c(c)->datalog_util().try_get_size(to_sort(s), *out)); 218 return true; 219 Z3_CATCH_RETURN(false); 220 } 221 Z3_mk_fixedpoint(Z3_context c)222 Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c) { 223 Z3_TRY; 224 LOG_Z3_mk_fixedpoint(c); 225 RESET_ERROR_CODE(); 226 Z3_fixedpoint_ref * d = alloc(Z3_fixedpoint_ref, *mk_c(c)); 227 d->m_datalog = alloc(api::fixedpoint_context, mk_c(c)->m(), mk_c(c)->fparams()); 228 mk_c(c)->save_object(d); 229 Z3_fixedpoint r = of_datalog(d); 230 RETURN_Z3(r); 231 Z3_CATCH_RETURN(nullptr); 232 } 233 Z3_fixedpoint_inc_ref(Z3_context c,Z3_fixedpoint s)234 void Z3_API Z3_fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint s) { 235 Z3_TRY; 236 LOG_Z3_fixedpoint_inc_ref(c, s); 237 RESET_ERROR_CODE(); 238 to_fixedpoint(s)->inc_ref(); 239 Z3_CATCH; 240 } 241 Z3_fixedpoint_dec_ref(Z3_context c,Z3_fixedpoint s)242 void Z3_API Z3_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint s) { 243 Z3_TRY; 244 LOG_Z3_fixedpoint_dec_ref(c, s); 245 RESET_ERROR_CODE(); 246 to_fixedpoint(s)->dec_ref(); 247 Z3_CATCH; 248 } 249 Z3_fixedpoint_assert(Z3_context c,Z3_fixedpoint d,Z3_ast a)250 void Z3_API Z3_fixedpoint_assert(Z3_context c, Z3_fixedpoint d, Z3_ast a) { 251 Z3_TRY; 252 LOG_Z3_fixedpoint_assert(c, d, a); 253 RESET_ERROR_CODE(); 254 CHECK_FORMULA(a,); 255 to_fixedpoint_ref(d)->ctx().assert_expr(to_expr(a)); 256 Z3_CATCH; 257 } 258 Z3_fixedpoint_add_rule(Z3_context c,Z3_fixedpoint d,Z3_ast a,Z3_symbol name)259 void Z3_API Z3_fixedpoint_add_rule(Z3_context c, Z3_fixedpoint d, Z3_ast a, Z3_symbol name) { 260 Z3_TRY; 261 LOG_Z3_fixedpoint_add_rule(c, d, a, name); 262 RESET_ERROR_CODE(); 263 CHECK_FORMULA(a,); 264 to_fixedpoint_ref(d)->add_rule(to_expr(a), to_symbol(name)); 265 Z3_CATCH; 266 } 267 Z3_fixedpoint_add_fact(Z3_context c,Z3_fixedpoint d,Z3_func_decl r,unsigned num_args,unsigned args[])268 void Z3_API Z3_fixedpoint_add_fact(Z3_context c, Z3_fixedpoint d, 269 Z3_func_decl r, unsigned num_args, unsigned args[]) { 270 Z3_TRY; 271 LOG_Z3_fixedpoint_add_fact(c, d, r, num_args, args); 272 RESET_ERROR_CODE(); 273 to_fixedpoint_ref(d)->add_table_fact(to_func_decl(r), num_args, args); 274 Z3_CATCH; 275 } 276 Z3_fixedpoint_query(Z3_context c,Z3_fixedpoint d,Z3_ast q)277 Z3_lbool Z3_API Z3_fixedpoint_query(Z3_context c,Z3_fixedpoint d, Z3_ast q) { 278 Z3_TRY; 279 LOG_Z3_fixedpoint_query(c, d, q); 280 RESET_ERROR_CODE(); 281 lbool r = l_undef; 282 unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout()); 283 unsigned rlimit = to_fixedpoint(d)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit()); 284 bool use_ctrl_c = to_fixedpoint(d)->m_params.get_bool("ctrl_c", true); 285 { 286 scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit); 287 cancel_eh<reslimit> eh(mk_c(c)->m().limit()); 288 api::context::set_interruptable si(*(mk_c(c)), eh); 289 scoped_timer timer(timeout, &eh); 290 scoped_ctrl_c ctrlc(eh, false, use_ctrl_c); 291 try { 292 r = to_fixedpoint_ref(d)->ctx().query(to_expr(q)); 293 } 294 catch (z3_exception& ex) { 295 r = l_undef; 296 mk_c(c)->handle_exception(ex); 297 } 298 to_fixedpoint_ref(d)->ctx().cleanup(); 299 } 300 return of_lbool(r); 301 Z3_CATCH_RETURN(Z3_L_UNDEF); 302 } 303 Z3_fixedpoint_query_relations(Z3_context c,Z3_fixedpoint d,unsigned num_relations,Z3_func_decl const relations[])304 Z3_lbool Z3_API Z3_fixedpoint_query_relations( 305 Z3_context c,Z3_fixedpoint d, 306 unsigned num_relations, Z3_func_decl const relations[]) { 307 Z3_TRY; 308 LOG_Z3_fixedpoint_query_relations(c, d, num_relations, relations); 309 RESET_ERROR_CODE(); 310 lbool r = l_undef; 311 unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout()); 312 cancel_eh<reslimit> eh(mk_c(c)->m().limit()); 313 api::context::set_interruptable si(*(mk_c(c)), eh); 314 { 315 scoped_timer timer(timeout, &eh); 316 try { 317 r = to_fixedpoint_ref(d)->ctx().rel_query(num_relations, to_func_decls(relations)); 318 } 319 catch (z3_exception& ex) { 320 mk_c(c)->handle_exception(ex); 321 r = l_undef; 322 } 323 to_fixedpoint_ref(d)->ctx().cleanup(); 324 } 325 return of_lbool(r); 326 Z3_CATCH_RETURN(Z3_L_UNDEF); 327 } 328 Z3_fixedpoint_get_answer(Z3_context c,Z3_fixedpoint d)329 Z3_ast Z3_API Z3_fixedpoint_get_answer(Z3_context c, Z3_fixedpoint d) { 330 Z3_TRY; 331 LOG_Z3_fixedpoint_get_answer(c, d); 332 RESET_ERROR_CODE(); 333 expr* e = to_fixedpoint_ref(d)->ctx().get_answer_as_formula(); 334 mk_c(c)->save_ast_trail(e); 335 RETURN_Z3(of_expr(e)); 336 Z3_CATCH_RETURN(nullptr); 337 } 338 Z3_fixedpoint_get_reason_unknown(Z3_context c,Z3_fixedpoint d)339 Z3_string Z3_API Z3_fixedpoint_get_reason_unknown(Z3_context c,Z3_fixedpoint d) { 340 Z3_TRY; 341 LOG_Z3_fixedpoint_get_reason_unknown(c, d); 342 RESET_ERROR_CODE(); 343 return mk_c(c)->mk_external_string(to_fixedpoint_ref(d)->get_last_status()); 344 Z3_CATCH_RETURN(""); 345 } 346 Z3_fixedpoint_to_string(Z3_context c,Z3_fixedpoint d,unsigned num_queries,Z3_ast _queries[])347 Z3_string Z3_API Z3_fixedpoint_to_string( 348 Z3_context c, 349 Z3_fixedpoint d, 350 unsigned num_queries, 351 Z3_ast _queries[]) { 352 Z3_TRY; 353 expr*const* queries = to_exprs(num_queries, _queries); 354 LOG_Z3_fixedpoint_to_string(c, d, num_queries, _queries); 355 RESET_ERROR_CODE(); 356 return mk_c(c)->mk_external_string(to_fixedpoint_ref(d)->to_string(num_queries, queries)); 357 Z3_CATCH_RETURN(""); 358 } 359 Z3_fixedpoint_from_stream(Z3_context c,Z3_fixedpoint d,std::istream & s)360 Z3_ast_vector Z3_fixedpoint_from_stream( 361 Z3_context c, 362 Z3_fixedpoint d, 363 std::istream& s) { 364 ast_manager& m = mk_c(c)->m(); 365 dl_collected_cmds coll(m); 366 cmd_context ctx(false, &m); 367 install_dl_collect_cmds(coll, ctx); 368 ctx.set_ignore_check(true); 369 if (!parse_smt2_commands(ctx, s)) { 370 SET_ERROR_CODE(Z3_PARSER_ERROR, nullptr); 371 return nullptr; 372 } 373 374 Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, *mk_c(c), m); 375 mk_c(c)->save_object(v); 376 for (expr * q : coll.m_queries) { 377 v->m_ast_vector.push_back(q); 378 } 379 for (func_decl * f : coll.m_rels) { 380 to_fixedpoint_ref(d)->ctx().register_predicate(f, true); 381 } 382 for (unsigned i = 0; i < coll.m_rules.size(); ++i) { 383 to_fixedpoint_ref(d)->add_rule(coll.m_rules[i].get(), coll.m_names[i]); 384 } 385 for (expr * e : ctx.assertions()) { 386 to_fixedpoint_ref(d)->ctx().assert_expr(e); 387 } 388 389 return of_ast_vector(v); 390 } 391 Z3_fixedpoint_from_string(Z3_context c,Z3_fixedpoint d,Z3_string s)392 Z3_ast_vector Z3_API Z3_fixedpoint_from_string( 393 Z3_context c, 394 Z3_fixedpoint d, 395 Z3_string s) { 396 Z3_TRY; 397 LOG_Z3_fixedpoint_from_string(c, d, s); 398 std::string str(s); 399 std::istringstream is(str); 400 RETURN_Z3(Z3_fixedpoint_from_stream(c, d, is)); 401 Z3_CATCH_RETURN(nullptr); 402 } 403 Z3_fixedpoint_from_file(Z3_context c,Z3_fixedpoint d,Z3_string s)404 Z3_ast_vector Z3_API Z3_fixedpoint_from_file( 405 Z3_context c, 406 Z3_fixedpoint d, 407 Z3_string s) { 408 Z3_TRY; 409 LOG_Z3_fixedpoint_from_file(c, d, s); 410 std::ifstream is(s); 411 if (!is) { 412 SET_ERROR_CODE(Z3_PARSER_ERROR, nullptr); 413 RETURN_Z3(nullptr); 414 } 415 RETURN_Z3(Z3_fixedpoint_from_stream(c, d, is)); 416 Z3_CATCH_RETURN(nullptr); 417 } 418 419 Z3_fixedpoint_get_statistics(Z3_context c,Z3_fixedpoint d)420 Z3_stats Z3_API Z3_fixedpoint_get_statistics(Z3_context c,Z3_fixedpoint d) { 421 Z3_TRY; 422 LOG_Z3_fixedpoint_get_statistics(c, d); 423 RESET_ERROR_CODE(); 424 Z3_stats_ref * st = alloc(Z3_stats_ref, (*mk_c(c))); 425 to_fixedpoint_ref(d)->ctx().collect_statistics(st->m_stats); 426 mk_c(c)->save_object(st); 427 Z3_stats r = of_stats(st); 428 RETURN_Z3(r); 429 Z3_CATCH_RETURN(nullptr); 430 } 431 Z3_fixedpoint_register_relation(Z3_context c,Z3_fixedpoint d,Z3_func_decl f)432 void Z3_API Z3_fixedpoint_register_relation(Z3_context c,Z3_fixedpoint d, Z3_func_decl f) { 433 Z3_TRY; 434 LOG_Z3_fixedpoint_register_relation(c, d, f); 435 to_fixedpoint_ref(d)->ctx().register_predicate(to_func_decl(f), true); 436 Z3_CATCH; 437 } 438 Z3_fixedpoint_set_predicate_representation(Z3_context c,Z3_fixedpoint d,Z3_func_decl f,unsigned num_relations,Z3_symbol const relation_kinds[])439 void Z3_API Z3_fixedpoint_set_predicate_representation( 440 Z3_context c, 441 Z3_fixedpoint d, 442 Z3_func_decl f, 443 unsigned num_relations, 444 Z3_symbol const relation_kinds[]) { 445 Z3_TRY; 446 LOG_Z3_fixedpoint_set_predicate_representation(c, d, f, num_relations, relation_kinds); 447 svector<symbol> kinds; 448 for (unsigned i = 0; i < num_relations; ++i) { 449 kinds.push_back(to_symbol(relation_kinds[i])); 450 } 451 to_fixedpoint_ref(d)->ctx().set_predicate_representation(to_func_decl(f), num_relations, kinds.c_ptr()); 452 Z3_CATCH; 453 } 454 455 Z3_fixedpoint_get_rules(Z3_context c,Z3_fixedpoint d)456 Z3_ast_vector Z3_API Z3_fixedpoint_get_rules( 457 Z3_context c, 458 Z3_fixedpoint d) 459 { 460 Z3_TRY; 461 LOG_Z3_fixedpoint_get_rules(c, d); 462 ast_manager& m = mk_c(c)->m(); 463 Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, *mk_c(c), m); 464 mk_c(c)->save_object(v); 465 expr_ref_vector rules(m), queries(m); 466 svector<symbol> names; 467 468 to_fixedpoint_ref(d)->ctx().get_rules_as_formulas(rules, queries, names); 469 for (expr* r : rules) { 470 v->m_ast_vector.push_back(r); 471 } 472 for (expr* q : queries) { 473 v->m_ast_vector.push_back(m.mk_not(q)); 474 } 475 RETURN_Z3(of_ast_vector(v)); 476 Z3_CATCH_RETURN(nullptr); 477 } 478 Z3_fixedpoint_get_assertions(Z3_context c,Z3_fixedpoint d)479 Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions( 480 Z3_context c, 481 Z3_fixedpoint d) 482 { 483 Z3_TRY; 484 LOG_Z3_fixedpoint_get_assertions(c, d); 485 ast_manager& m = mk_c(c)->m(); 486 Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, *mk_c(c), m); 487 mk_c(c)->save_object(v); 488 unsigned num_asserts = to_fixedpoint_ref(d)->ctx().get_num_assertions(); 489 for (unsigned i = 0; i < num_asserts; ++i) { 490 v->m_ast_vector.push_back(to_fixedpoint_ref(d)->ctx().get_assertion(i)); 491 } 492 RETURN_Z3(of_ast_vector(v)); 493 Z3_CATCH_RETURN(nullptr); 494 } 495 Z3_fixedpoint_set_reduce_assign_callback(Z3_context c,Z3_fixedpoint d,Z3_fixedpoint_reduce_assign_callback_fptr f)496 void Z3_API Z3_fixedpoint_set_reduce_assign_callback( 497 Z3_context c, Z3_fixedpoint d, Z3_fixedpoint_reduce_assign_callback_fptr f) { 498 Z3_TRY; 499 // no logging 500 to_fixedpoint_ref(d)->set_reduce_assign((reduce_assign_callback_fptr)f); 501 Z3_CATCH; 502 } 503 Z3_fixedpoint_set_reduce_app_callback(Z3_context c,Z3_fixedpoint d,Z3_fixedpoint_reduce_app_callback_fptr f)504 void Z3_API Z3_fixedpoint_set_reduce_app_callback( 505 Z3_context c, Z3_fixedpoint d, Z3_fixedpoint_reduce_app_callback_fptr f) { 506 Z3_TRY; 507 // no logging 508 to_fixedpoint_ref(d)->set_reduce_app((reduce_app_callback_fptr)f); 509 Z3_CATCH; 510 } 511 Z3_fixedpoint_init(Z3_context c,Z3_fixedpoint d,void * state)512 void Z3_API Z3_fixedpoint_init(Z3_context c,Z3_fixedpoint d, void* state) { 513 Z3_TRY; 514 // not logged 515 to_fixedpoint_ref(d)->set_state(state); 516 Z3_CATCH; 517 } 518 519 Z3_fixedpoint_update_rule(Z3_context c,Z3_fixedpoint d,Z3_ast a,Z3_symbol name)520 void Z3_API Z3_fixedpoint_update_rule(Z3_context c, Z3_fixedpoint d, Z3_ast a, Z3_symbol name) { 521 Z3_TRY; 522 LOG_Z3_fixedpoint_update_rule(c, d, a, name); 523 RESET_ERROR_CODE(); 524 CHECK_FORMULA(a,); 525 to_fixedpoint_ref(d)->update_rule(to_expr(a), to_symbol(name)); 526 Z3_CATCH; 527 } 528 Z3_fixedpoint_get_num_levels(Z3_context c,Z3_fixedpoint d,Z3_func_decl pred)529 unsigned Z3_API Z3_fixedpoint_get_num_levels(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred) { 530 Z3_TRY; 531 LOG_Z3_fixedpoint_get_num_levels(c, d, pred); 532 RESET_ERROR_CODE(); 533 return to_fixedpoint_ref(d)->get_num_levels(to_func_decl(pred)); 534 Z3_CATCH_RETURN(0) 535 } 536 Z3_fixedpoint_get_cover_delta(Z3_context c,Z3_fixedpoint d,int level,Z3_func_decl pred)537 Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred) { 538 Z3_TRY; 539 LOG_Z3_fixedpoint_get_cover_delta(c, d, level, pred); 540 RESET_ERROR_CODE(); 541 expr_ref r = to_fixedpoint_ref(d)->get_cover_delta(level, to_func_decl(pred)); 542 mk_c(c)->save_ast_trail(r); 543 RETURN_Z3(of_expr(r.get())); 544 Z3_CATCH_RETURN(nullptr); 545 } 546 Z3_fixedpoint_add_cover(Z3_context c,Z3_fixedpoint d,int level,Z3_func_decl pred,Z3_ast property)547 void Z3_API Z3_fixedpoint_add_cover(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred, Z3_ast property) { 548 Z3_TRY; 549 LOG_Z3_fixedpoint_add_cover(c, d, level, pred, property); 550 RESET_ERROR_CODE(); 551 to_fixedpoint_ref(d)->add_cover(level, to_func_decl(pred), to_expr(property)); 552 Z3_CATCH; 553 } 554 Z3_fixedpoint_get_help(Z3_context c,Z3_fixedpoint d)555 Z3_string Z3_API Z3_fixedpoint_get_help(Z3_context c, Z3_fixedpoint d) { 556 Z3_TRY; 557 LOG_Z3_fixedpoint_get_help(c, d); 558 RESET_ERROR_CODE(); 559 std::ostringstream buffer; 560 param_descrs descrs; 561 to_fixedpoint_ref(d)->collect_param_descrs(descrs); 562 descrs.display(buffer); 563 return mk_c(c)->mk_external_string(buffer.str()); 564 Z3_CATCH_RETURN(""); 565 } 566 Z3_fixedpoint_get_param_descrs(Z3_context c,Z3_fixedpoint f)567 Z3_param_descrs Z3_API Z3_fixedpoint_get_param_descrs(Z3_context c, Z3_fixedpoint f) { 568 Z3_TRY; 569 LOG_Z3_fixedpoint_get_param_descrs(c, f); 570 RESET_ERROR_CODE(); 571 Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref, *mk_c(c)); 572 mk_c(c)->save_object(d); 573 to_fixedpoint_ref(f)->collect_param_descrs(d->m_descrs); 574 Z3_param_descrs r = of_param_descrs(d); 575 RETURN_Z3(r); 576 Z3_CATCH_RETURN(nullptr); 577 } 578 Z3_fixedpoint_set_params(Z3_context c,Z3_fixedpoint d,Z3_params p)579 void Z3_API Z3_fixedpoint_set_params(Z3_context c, Z3_fixedpoint d, Z3_params p) { 580 Z3_TRY; 581 LOG_Z3_fixedpoint_set_params(c, d, p); 582 RESET_ERROR_CODE(); 583 param_descrs descrs; 584 to_fixedpoint_ref(d)->collect_param_descrs(descrs); 585 to_params(p)->m_params.validate(descrs); 586 to_fixedpoint_ref(d)->updt_params(to_param_ref(p)); 587 to_fixedpoint(d)->m_params = to_param_ref(p); 588 Z3_CATCH; 589 } 590 Z3_fixedpoint_add_callback(Z3_context c,Z3_fixedpoint d,void * state,Z3_fixedpoint_new_lemma_eh new_lemma_eh,Z3_fixedpoint_predecessor_eh predecessor_eh,Z3_fixedpoint_unfold_eh unfold_eh)591 void Z3_API Z3_fixedpoint_add_callback(Z3_context c, Z3_fixedpoint d, 592 void *state, 593 Z3_fixedpoint_new_lemma_eh new_lemma_eh, 594 Z3_fixedpoint_predecessor_eh predecessor_eh, 595 Z3_fixedpoint_unfold_eh unfold_eh){ 596 Z3_TRY; 597 // not logged 598 to_fixedpoint_ref(d)->ctx().add_callback(state, 599 reinterpret_cast<datalog::t_new_lemma_eh>(new_lemma_eh), 600 reinterpret_cast<datalog::t_predecessor_eh>(predecessor_eh), 601 reinterpret_cast<datalog::t_unfold_eh>(unfold_eh)); 602 603 Z3_CATCH; 604 } 605 Z3_fixedpoint_add_constraint(Z3_context c,Z3_fixedpoint d,Z3_ast e,unsigned lvl)606 void Z3_API Z3_fixedpoint_add_constraint (Z3_context c, Z3_fixedpoint d, Z3_ast e, unsigned lvl){ 607 to_fixedpoint_ref(d)->ctx().add_constraint(to_expr(e), lvl); 608 } 609 Z3_fixedpoint_query_from_lvl(Z3_context c,Z3_fixedpoint d,Z3_ast q,unsigned lvl)610 Z3_lbool Z3_API Z3_fixedpoint_query_from_lvl (Z3_context c, Z3_fixedpoint d, Z3_ast q, unsigned lvl) { 611 Z3_TRY; 612 LOG_Z3_fixedpoint_query_from_lvl (c, d, q, lvl); 613 RESET_ERROR_CODE(); 614 lbool r = l_undef; 615 unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout()); 616 unsigned rlimit = to_fixedpoint(d)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit()); 617 { 618 scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit); 619 cancel_eh<reslimit> eh(mk_c(c)->m().limit()); 620 api::context::set_interruptable si(*(mk_c(c)), eh); 621 scoped_timer timer(timeout, &eh); 622 try { 623 r = to_fixedpoint_ref(d)->ctx().query_from_lvl (to_expr(q), lvl); 624 } 625 catch (z3_exception& ex) { 626 mk_c(c)->handle_exception(ex); 627 r = l_undef; 628 } 629 to_fixedpoint_ref(d)->ctx().cleanup(); 630 } 631 return of_lbool(r); 632 Z3_CATCH_RETURN(Z3_L_UNDEF); 633 } 634 Z3_fixedpoint_get_ground_sat_answer(Z3_context c,Z3_fixedpoint d)635 Z3_ast Z3_API Z3_fixedpoint_get_ground_sat_answer(Z3_context c, Z3_fixedpoint d) { 636 Z3_TRY; 637 LOG_Z3_fixedpoint_get_ground_sat_answer(c, d); 638 RESET_ERROR_CODE(); 639 expr* e = to_fixedpoint_ref(d)->ctx().get_ground_sat_answer(); 640 mk_c(c)->save_ast_trail(e); 641 RETURN_Z3(of_expr(e)); 642 Z3_CATCH_RETURN(nullptr); 643 } 644 Z3_fixedpoint_get_rules_along_trace(Z3_context c,Z3_fixedpoint d)645 Z3_ast_vector Z3_API Z3_fixedpoint_get_rules_along_trace( 646 Z3_context c, 647 Z3_fixedpoint d) 648 { 649 Z3_TRY; 650 LOG_Z3_fixedpoint_get_rules_along_trace(c, d); 651 ast_manager& m = mk_c(c)->m(); 652 Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, *mk_c(c), m); 653 mk_c(c)->save_object(v); 654 expr_ref_vector rules(m); 655 svector<symbol> names; 656 657 to_fixedpoint_ref(d)->ctx().get_rules_along_trace_as_formulas(rules, names); 658 for (unsigned i = 0; i < rules.size(); ++i) { 659 v->m_ast_vector.push_back(rules[i].get()); 660 } 661 RETURN_Z3(of_ast_vector(v)); 662 Z3_CATCH_RETURN(nullptr); 663 } 664 Z3_fixedpoint_get_rule_names_along_trace(Z3_context c,Z3_fixedpoint d)665 Z3_symbol Z3_API Z3_fixedpoint_get_rule_names_along_trace( 666 Z3_context c, 667 Z3_fixedpoint d) 668 { 669 Z3_TRY; 670 LOG_Z3_fixedpoint_get_rule_names_along_trace(c, d); 671 ast_manager& m = mk_c(c)->m(); 672 Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, *mk_c(c), m); 673 mk_c(c)->save_object(v); 674 expr_ref_vector rules(m); 675 svector<symbol> names; 676 std::stringstream ss; 677 678 to_fixedpoint_ref(d)->ctx().get_rules_along_trace_as_formulas(rules, names); 679 for (unsigned i = 0; i < names.size(); ++i) { 680 if (i != 0) 681 ss << ';'; 682 ss << names[i].str(); 683 } 684 return of_symbol(symbol(ss.str())); 685 Z3_CATCH_RETURN(of_symbol(symbol::null)); 686 } 687 Z3_fixedpoint_add_invariant(Z3_context c,Z3_fixedpoint d,Z3_func_decl pred,Z3_ast property)688 void Z3_API Z3_fixedpoint_add_invariant(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred, Z3_ast property) { 689 Z3_TRY; 690 LOG_Z3_fixedpoint_add_invariant(c, d, pred, property); 691 RESET_ERROR_CODE(); 692 to_fixedpoint_ref(d)->ctx ().add_invariant(to_func_decl(pred), to_expr(property)); 693 Z3_CATCH; 694 } 695 Z3_fixedpoint_get_reachable(Z3_context c,Z3_fixedpoint d,Z3_func_decl pred)696 Z3_ast Z3_API Z3_fixedpoint_get_reachable(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred) { 697 Z3_TRY; 698 LOG_Z3_fixedpoint_get_reachable(c, d, pred); 699 RESET_ERROR_CODE(); 700 expr_ref r = to_fixedpoint_ref(d)->ctx().get_reachable(to_func_decl(pred)); 701 mk_c(c)->save_ast_trail(r); 702 RETURN_Z3(of_expr(r.get())); 703 Z3_CATCH_RETURN(nullptr); 704 } 705 706 }; 707