1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 dl_context.cpp 7 8 Abstract: 9 10 <abstract> 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2010-05-18. 15 16 Revision History: 17 18 --*/ 19 20 #include<sstream> 21 #include<limits> 22 #include "ast/arith_decl_plugin.h" 23 #include "ast/bv_decl_plugin.h" 24 #include "ast/for_each_expr.h" 25 #include "ast/ast_smt_pp.h" 26 #include "ast/ast_smt2_pp.h" 27 #include "ast/datatype_decl_plugin.h" 28 #include "ast/scoped_proof.h" 29 #include "ast/ast_pp_util.h" 30 #include "ast/ast_util.h" 31 #include "muz/base/dl_context.h" 32 #include "muz/base/fp_params.hpp" 33 34 namespace datalog { 35 36 // ----------------------------------- 37 // 38 // context::sort_domain 39 // 40 // ----------------------------------- 41 42 class context::sort_domain { 43 private: 44 sort_kind m_kind; 45 protected: 46 sort_ref m_sort; 47 bool m_limited_size; 48 uint64_t m_size; 49 sort_domain(sort_kind k,context & ctx,sort * s)50 sort_domain(sort_kind k, context & ctx, sort * s) 51 : m_kind(k), m_sort(s, ctx.get_manager()) { 52 m_limited_size = ctx.get_decl_util().try_get_size(s, m_size); 53 } 54 public: ~sort_domain()55 virtual ~sort_domain() {} 56 get_kind() const57 sort_kind get_kind() const { return m_kind; } 58 virtual unsigned get_constant_count() const = 0; 59 virtual void print_element(finite_element el_num, std::ostream & out) = 0; 60 }; 61 62 class context::symbol_sort_domain : public sort_domain { 63 typedef map<symbol, finite_element, symbol_hash_proc, symbol_eq_proc> sym2num; 64 typedef svector<symbol> num2sym; 65 66 sym2num m_el_numbers; 67 num2sym m_el_names; 68 public: symbol_sort_domain(context & ctx,sort * s)69 symbol_sort_domain(context & ctx, sort * s) : sort_domain(SK_SYMBOL, ctx, s) {} 70 get_number(symbol sym)71 finite_element get_number(symbol sym) { 72 //we number symbols starting from zero, so table->size() is equal to the 73 //index of the symbol to be added next 74 75 unsigned newIdx = m_el_numbers.size(); 76 77 unsigned idx = m_el_numbers.insert_if_not_there(sym, newIdx); 78 79 if (idx==newIdx) { 80 m_el_names.push_back(sym); 81 SASSERT(m_el_names.size()==m_el_numbers.size()); 82 } 83 84 if (m_limited_size && idx>=m_size) { 85 std::stringstream sstm; 86 sstm << "sort " << m_sort->get_name() << " contains more constants than its declared size " << m_size; 87 throw default_exception(sstm.str()); 88 } 89 return idx; 90 } 91 get_constant_count() const92 unsigned get_constant_count() const override { 93 return m_el_names.size(); 94 } print_element(finite_element el_num,std::ostream & out)95 void print_element(finite_element el_num, std::ostream & out) override { 96 if (el_num>=m_el_names.size()) { 97 out << el_num; 98 return; 99 } 100 out << m_el_names[el_num]; 101 } 102 }; 103 104 class context::uint64_sort_domain : public sort_domain { 105 typedef map<uint64_t, finite_element, uint64_hash, default_eq<uint64_t> > el2num; 106 typedef svector<uint64_t> num2el; 107 108 el2num m_el_numbers; 109 num2el m_el_names; 110 public: uint64_sort_domain(context & ctx,sort * s)111 uint64_sort_domain(context & ctx, sort * s) : sort_domain(SK_UINT64, ctx, s) {} 112 get_number(uint64_t el)113 finite_element get_number(uint64_t el) { 114 //we number symbols starting from zero, so table->size() is equal to the 115 //index of the symbol to be added next 116 117 unsigned newIdx = m_el_numbers.size(); 118 119 unsigned idx = m_el_numbers.insert_if_not_there(el, newIdx); 120 121 if (idx == newIdx) { 122 m_el_names.push_back(el); 123 SASSERT(m_el_names.size()==m_el_numbers.size()); 124 } 125 126 if (m_limited_size && idx>=m_size) { 127 std::stringstream sstm; 128 sstm << "sort " << m_sort->get_name() << " contains more constants than its declared size " << m_size; 129 throw default_exception(sstm.str()); 130 } 131 return idx; 132 } get_constant_count() const133 unsigned get_constant_count() const override { 134 return m_el_names.size(); 135 } print_element(finite_element el_num,std::ostream & out)136 void print_element(finite_element el_num, std::ostream & out) override { 137 if (el_num >= m_el_names.size()) { 138 out << "<unk " << m_sort->get_name() << ":" << el_num << '>'; 139 return; 140 } 141 out << m_el_names[el_num]; 142 } 143 }; 144 145 // ----------------------------------- 146 // 147 // trail stack for restoring rules 148 // 149 // ----------------------------------- 150 151 class context::restore_rules : public trail { 152 context& ctx; 153 rule_set* m_old_rules; reset()154 void reset() { 155 dealloc(m_old_rules); 156 m_old_rules = nullptr; 157 } 158 public: restore_rules(context & ctx,rule_set & r)159 restore_rules(context& ctx, rule_set& r): ctx(ctx), m_old_rules(alloc(rule_set, r)) {} 160 ~restore_rules()161 ~restore_rules() override {} 162 undo()163 void undo() override { 164 ctx.replace_rules(*m_old_rules); 165 reset(); 166 } 167 }; 168 169 template<typename Ctx, typename Vec> 170 class restore_vec_size_trail : public trail { 171 Vec& m_vector; 172 unsigned m_old_size; 173 public: restore_vec_size_trail(Vec & v)174 restore_vec_size_trail(Vec& v): m_vector(v), m_old_size(v.size()) {} ~restore_vec_size_trail()175 ~restore_vec_size_trail() override {} undo()176 void undo() override { m_vector.shrink(m_old_size); } 177 }; 178 push()179 void context::push() { 180 m_trail.push_scope(); 181 m_trail.push(restore_rules(*this, m_rule_set)); 182 m_trail.push(restore_vec_size_trail<context,expr_ref_vector>(m_rule_fmls)); 183 m_trail.push(restore_vec_size_trail<context,expr_ref_vector>(m_background)); 184 } 185 pop()186 void context::pop() { 187 if (m_trail.get_num_scopes() == 0) { 188 throw default_exception("there are no backtracking points to pop to"); 189 } 190 throw default_exception("pop operation is not supported"); 191 m_trail.pop_scope(1); 192 } 193 194 // ----------------------------------- 195 // 196 // context 197 // 198 // ----------------------------------- 199 context(ast_manager & m,register_engine_base & re,smt_params & fp,params_ref const & pa)200 context::context(ast_manager & m, register_engine_base& re, smt_params& fp, params_ref const& pa): 201 m(m), 202 m_register_engine(re), 203 m_fparams(fp), 204 m_params_ref(pa), 205 m_params(alloc(fp_params, m_params_ref)), 206 m_decl_util(m), 207 m_rewriter(m), 208 m_var_subst(m), 209 m_rule_manager(*this), 210 m_contains_p(*this), 211 m_rule_properties(m, m_rule_manager, *this, m_contains_p), 212 m_transf(*this), 213 m_trail(), 214 m_pinned(m), 215 m_bind_variables(m), 216 m_rule_set(*this), 217 m_transformed_rule_set(*this), 218 m_rule_fmls_head(0), 219 m_rule_fmls(m), 220 m_background(m), 221 m_mc(nullptr), 222 m_rel(nullptr), 223 m_engine(nullptr), 224 m_closed(false), 225 m_saturation_was_run(false), 226 m_enable_bind_variables(true), 227 m_last_status(OK), 228 m_last_answer(m), 229 m_last_ground_answer(m), 230 m_engine_type(LAST_ENGINE) { 231 re.set_context(this); 232 updt_params(pa); 233 } 234 ~context()235 context::~context() { 236 reset(); 237 dealloc(m_params); 238 } 239 reset()240 void context::reset() { 241 m_trail.reset(); 242 m_rule_set.reset(); 243 m_rule_fmls_head = 0; 244 m_rule_fmls.reset(); 245 m_rule_names.reset(); 246 m_rule_bounds.reset(); 247 m_argument_var_names.reset(); 248 m_preds.reset(); 249 m_preds_by_name.reset(); 250 reset_dealloc_values(m_sorts); 251 m_engine = nullptr; 252 m_rel = nullptr; 253 } 254 is_fact(app * head) const255 bool context::is_fact(app * head) const { 256 return m_rule_manager.is_fact(head); 257 } 258 has_sort_domain(relation_sort s) const259 bool context::has_sort_domain(relation_sort s) const { 260 return m_sorts.contains(s); 261 } 262 get_sort_domain(relation_sort s)263 context::sort_domain & context::get_sort_domain(relation_sort s) { 264 return *m_sorts.find(s); 265 } 266 get_sort_domain(relation_sort s) const267 const context::sort_domain & context::get_sort_domain(relation_sort s) const { 268 return *m_sorts.find(s); 269 } 270 271 generate_proof_trace() const272 bool context::generate_proof_trace() const { return m_generate_proof_trace; } output_profile() const273 bool context::output_profile() const { return m_params->datalog_output_profile(); } output_tuples() const274 bool context::output_tuples() const { return m_params->datalog_print_tuples(); } use_map_names() const275 bool context::use_map_names() const { return m_params->datalog_use_map_names(); } fix_unbound_vars() const276 bool context::fix_unbound_vars() const { return m_params->xform_fix_unbound_vars(); } default_table() const277 symbol context::default_table() const { return m_params->datalog_default_table(); } default_relation() const278 symbol context::default_relation() const { return m_default_relation; } set_default_relation(symbol const & s)279 void context::set_default_relation(symbol const& s) { m_default_relation = s; } print_aig() const280 symbol context::print_aig() const { return m_params->print_aig(); } check_relation() const281 symbol context::check_relation() const { return m_params->datalog_check_relation(); } default_table_checker() const282 symbol context::default_table_checker() const { return m_params->datalog_default_table_checker(); } default_table_checked() const283 bool context::default_table_checked() const { return m_params->datalog_default_table_checked(); } dbg_fpr_nonempty_relation_signature() const284 bool context::dbg_fpr_nonempty_relation_signature() const { return m_params->datalog_dbg_fpr_nonempty_relation_signature(); } dl_profile_milliseconds_threshold() const285 unsigned context::dl_profile_milliseconds_threshold() const { return m_params->datalog_profile_timeout_milliseconds(); } all_or_nothing_deltas() const286 bool context::all_or_nothing_deltas() const { return m_params->datalog_all_or_nothing_deltas(); } compile_with_widening() const287 bool context::compile_with_widening() const { return m_params->datalog_compile_with_widening(); } unbound_compressor() const288 bool context::unbound_compressor() const { return m_unbound_compressor; } set_unbound_compressor(bool f)289 void context::set_unbound_compressor(bool f) { m_unbound_compressor = f; } soft_timeout() const290 unsigned context::soft_timeout() const { return m_params->datalog_timeout(); } similarity_compressor() const291 bool context::similarity_compressor() const { return m_params->datalog_similarity_compressor(); } similarity_compressor_threshold() const292 unsigned context::similarity_compressor_threshold() const { return m_params->datalog_similarity_compressor_threshold(); } initial_restart_timeout() const293 unsigned context::initial_restart_timeout() const { return m_params->datalog_initial_restart_timeout(); } generate_explanations() const294 bool context::generate_explanations() const { return m_params->datalog_generate_explanations(); } explanations_on_relation_level() const295 bool context::explanations_on_relation_level() const { return m_params->datalog_explanations_on_relation_level(); } magic_sets_for_queries() const296 bool context::magic_sets_for_queries() const { return m_params->datalog_magic_sets_for_queries(); } tab_selection() const297 symbol context::tab_selection() const { return m_params->tab_selection(); } xform_coi() const298 bool context::xform_coi() const { return m_params->xform_coi(); } xform_slice() const299 bool context::xform_slice() const { return m_params->xform_slice(); } xform_bit_blast() const300 bool context::xform_bit_blast() const { return m_params->xform_bit_blast(); } karr() const301 bool context::karr() const { return false; } scale() const302 bool context::scale() const { return m_params->xform_scale(); } magic() const303 bool context::magic() const { return m_params->xform_magic(); } compress_unbound() const304 bool context::compress_unbound() const { return m_params->xform_compress_unbound(); } quantify_arrays() const305 bool context::quantify_arrays() const { return m_params->xform_quantify_arrays(); } instantiate_quantifiers() const306 bool context::instantiate_quantifiers() const { return m_params->xform_instantiate_quantifiers(); } array_blast() const307 bool context::array_blast() const { return m_params->xform_array_blast(); } array_blast_full() const308 bool context::array_blast_full() const { return m_params->xform_array_blast_full(); } elim_term_ite() const309 bool context::elim_term_ite() const {return m_params->xform_elim_term_ite();} blast_term_ite_inflation() const310 unsigned context::blast_term_ite_inflation() const { 311 return m_params->xform_elim_term_ite_inflation(); 312 } 313 314 register_finite_sort(sort * s,sort_kind k)315 void context::register_finite_sort(sort * s, sort_kind k) { 316 m_pinned.push_back(s); 317 SASSERT(!m_sorts.contains(s)); 318 sort_domain * dom; 319 switch (k) { 320 case SK_SYMBOL: 321 dom = alloc(symbol_sort_domain, *this, s); 322 break; 323 case SK_UINT64: 324 dom = alloc(uint64_sort_domain, *this, s); 325 break; 326 default: 327 UNREACHABLE(); 328 } 329 m_sorts.insert(s, dom); 330 } 331 register_variable(func_decl * var)332 void context::register_variable(func_decl* var) { 333 m_bind_variables.add_var(m.mk_const(var)); 334 } 335 bind_vars(expr * fml,bool is_forall)336 expr_ref context::bind_vars(expr* fml, bool is_forall) { 337 if (m_enable_bind_variables) { 338 return m_bind_variables(fml, is_forall); 339 } 340 else { 341 return expr_ref(fml, m); 342 } 343 } 344 register_predicate(func_decl * decl,bool named)345 void context::register_predicate(func_decl * decl, bool named) { 346 if (!is_predicate(decl)) { 347 m_pinned.push_back(decl); 348 m_preds.insert(decl); 349 TRACE("dl", tout << mk_pp(decl, m) << "\n";); 350 if (named) { 351 m_preds_by_name.insert(decl->get_name(), decl); 352 } 353 } 354 } 355 restrict_predicates(func_decl_set const & preds)356 void context::restrict_predicates(func_decl_set const& preds) { 357 m_preds.reset(); 358 for (func_decl* p : preds) { 359 TRACE("dl", tout << mk_pp(p, m) << "\n";); 360 m_preds.insert(p); 361 } 362 } 363 get_constant_number(relation_sort srt,symbol sym)364 context::finite_element context::get_constant_number(relation_sort srt, symbol sym) { 365 sort_domain & dom0 = get_sort_domain(srt); 366 SASSERT(dom0.get_kind() == SK_SYMBOL); 367 symbol_sort_domain & dom = static_cast<symbol_sort_domain &>(dom0); 368 return dom.get_number(sym); 369 } 370 get_constant_number(relation_sort srt,uint64_t el)371 context::finite_element context::get_constant_number(relation_sort srt, uint64_t el) { 372 373 sort_domain & dom0 = get_sort_domain(srt); 374 if (dom0.get_kind() == SK_SYMBOL) 375 return (finite_element)(el); 376 else { 377 uint64_sort_domain & dom = static_cast<uint64_sort_domain &>(dom0); 378 return dom.get_number(el); 379 } 380 } 381 print_constant_name(relation_sort srt,uint64_t num,std::ostream & out)382 void context::print_constant_name(relation_sort srt, uint64_t num, std::ostream & out) 383 { 384 if (has_sort_domain(srt)) { 385 SASSERT(num<=UINT_MAX); 386 get_sort_domain(srt).print_element(static_cast<unsigned>(num), out); 387 } 388 else { 389 out << num; 390 } 391 } 392 try_get_sort_constant_count(relation_sort srt,uint64_t & constant_count)393 bool context::try_get_sort_constant_count(relation_sort srt, uint64_t & constant_count) { 394 if (!has_sort_domain(srt)) { 395 return false; 396 } 397 constant_count = get_sort_domain(srt).get_constant_count(); 398 return true; 399 } 400 get_sort_size_estimate(relation_sort srt)401 uint64_t context::get_sort_size_estimate(relation_sort srt) { 402 if (get_decl_util().is_rule_sort(srt)) { 403 return 1; 404 } 405 uint64_t res; 406 if (!try_get_sort_constant_count(srt, res)) { 407 const sort_size & sz = srt->get_num_elements(); 408 if (sz.is_finite()) { 409 res = sz.size(); 410 } 411 else { 412 res = std::numeric_limits<uint64_t>::max(); 413 } 414 } 415 return res; 416 } 417 set_argument_names(const func_decl * pred,const svector<symbol> & var_names)418 void context::set_argument_names(const func_decl * pred, const svector<symbol> & var_names) 419 { 420 SASSERT(!m_argument_var_names.contains(pred)); 421 m_argument_var_names.insert(pred, var_names); 422 } 423 get_argument_name(const func_decl * pred,unsigned arg_index)424 symbol context::get_argument_name(const func_decl * pred, unsigned arg_index) 425 { 426 pred2syms::obj_map_entry * e = m_argument_var_names.find_core(pred); 427 if (!e) { 428 std::stringstream name_stm; 429 name_stm << '#' << arg_index; 430 return symbol(name_stm.str()); 431 } 432 SASSERT(arg_index < e->get_data().m_value.size()); 433 return e->get_data().m_value[arg_index]; 434 } 435 436 set_predicate_representation(func_decl * pred,unsigned relation_name_cnt,symbol const * relation_names)437 void context::set_predicate_representation(func_decl * pred, unsigned relation_name_cnt, 438 symbol const * relation_names) { 439 if (relation_name_cnt > 0) { 440 ensure_engine(); 441 } 442 if (relation_name_cnt > 0 && m_rel) { 443 m_rel->set_predicate_representation(pred, relation_name_cnt, relation_names); 444 } 445 } 446 mk_fresh_head_predicate(symbol const & prefix,symbol const & suffix,unsigned arity,sort * const * domain,func_decl * orig_pred)447 func_decl * context::mk_fresh_head_predicate(symbol const & prefix, symbol const & suffix, 448 unsigned arity, sort * const * domain, func_decl* orig_pred) { 449 func_decl* new_pred = 450 m.mk_fresh_func_decl(prefix, suffix, arity, domain, m.mk_bool_sort()); 451 452 register_predicate(new_pred, true); 453 454 if (m_rel) { 455 m_rel->inherit_predicate_kind(new_pred, orig_pred); 456 } 457 return new_pred; 458 } 459 add_rule(expr * rl,symbol const & name,unsigned bound)460 void context::add_rule(expr* rl, symbol const& name, unsigned bound) { 461 SASSERT(rl); 462 m_rule_fmls.push_back(rl); 463 m_rule_names.push_back(name); 464 m_rule_bounds.push_back(bound); 465 } 466 flush_add_rules()467 void context::flush_add_rules() { 468 datalog::rule_manager& rm = get_rule_manager(); 469 scoped_proof_mode _scp(m, generate_proof_trace()?PGM_ENABLED:PGM_DISABLED); 470 while (m_rule_fmls_head < m_rule_fmls.size()) { 471 expr* fml = m_rule_fmls[m_rule_fmls_head].get(); 472 proof* p = generate_proof_trace()?m.mk_asserted(fml):nullptr; 473 rm.mk_rule(fml, p, m_rule_set, m_rule_names[m_rule_fmls_head]); 474 ++m_rule_fmls_head; 475 } 476 check_rules(m_rule_set); 477 } 478 479 // 480 // Update a rule with a new. 481 // It requires basic subsumption. 482 // update_rule(expr * rl,symbol const & name)483 void context::update_rule(expr* rl, symbol const& name) { 484 datalog::rule_manager& rm = get_rule_manager(); 485 proof* p = nullptr; 486 if (generate_proof_trace()) { 487 p = m.mk_asserted(rl); 488 } 489 unsigned size_before = m_rule_set.get_num_rules(); 490 rm.mk_rule(rl, p, m_rule_set, name); 491 unsigned size_after = m_rule_set.get_num_rules(); 492 if (size_before + 1 != size_after) { 493 std::stringstream strm; 494 strm << "Rule " << name << " has a non-trivial body. It cannot be modified"; 495 throw default_exception(strm.str()); 496 } 497 // The new rule is inserted last: 498 rule_ref r(m_rule_set.get_rule(size_before), rm); 499 rule_ref_vector const& rls = m_rule_set.get_rules(); 500 rule* old_rule = nullptr; 501 for (unsigned i = 0; i < size_before; ++i) { 502 if (rls[i]->name() == name) { 503 if (old_rule) { 504 std::stringstream strm; 505 strm << "Rule " << name << " occurs twice. It cannot be modified"; 506 m_rule_set.del_rule(r); 507 throw default_exception(strm.str()); 508 } 509 old_rule = rls[i]; 510 } 511 } 512 if (old_rule) { 513 if (!check_subsumes(*old_rule, *r)) { 514 std::stringstream strm; 515 strm << "Old rule "; 516 old_rule->display(*this, strm); 517 strm << "does not subsume new rule "; 518 r->display(*this, strm); 519 m_rule_set.del_rule(r); 520 throw default_exception(strm.str()); 521 } 522 m_rule_set.del_rule(old_rule); 523 } 524 } 525 check_subsumes(rule const & stronger_rule,rule const & weaker_rule)526 bool context::check_subsumes(rule const& stronger_rule, rule const& weaker_rule) { 527 if (stronger_rule.get_head() != weaker_rule.get_head()) { 528 return false; 529 } 530 for (unsigned i = 0; i < stronger_rule.get_tail_size(); ++i) { 531 app* t = stronger_rule.get_tail(i); 532 bool found = false; 533 for (unsigned j = 0; j < weaker_rule.get_tail_size(); ++j) { 534 app* s = weaker_rule.get_tail(j); 535 if (s == t) { 536 found = true; 537 break; 538 } 539 } 540 if (!found) { 541 return false; 542 } 543 } 544 return true; 545 } 546 get_num_levels(func_decl * pred)547 unsigned context::get_num_levels(func_decl* pred) { 548 ensure_engine(); 549 return m_engine->get_num_levels(pred); 550 } 551 get_cover_delta(int level,func_decl * pred)552 expr_ref context::get_cover_delta(int level, func_decl* pred) { 553 ensure_engine(); 554 return m_engine->get_cover_delta(level, pred); 555 } 556 get_reachable(func_decl * pred)557 expr_ref context::get_reachable(func_decl *pred) { 558 ensure_engine(); 559 return m_engine->get_reachable(pred); 560 } add_cover(int level,func_decl * pred,expr * property)561 void context::add_cover(int level, func_decl* pred, expr* property) { 562 ensure_engine(); 563 m_engine->add_cover(level, pred, property); 564 } 565 add_invariant(func_decl * pred,expr * property)566 void context::add_invariant(func_decl* pred, expr *property) 567 { 568 ensure_engine(); 569 m_engine->add_invariant(pred, property); 570 } 571 check_rules(rule_set & r)572 void context::check_rules(rule_set& r) { 573 m_rule_properties.set_generate_proof(generate_proof_trace()); 574 TRACE("dl", m_rule_set.display(tout);); 575 switch(get_engine()) { 576 case DATALOG_ENGINE: 577 m_rule_properties.collect(r); 578 m_rule_properties.check_quantifier_free(); 579 m_rule_properties.check_uninterpreted_free(); 580 m_rule_properties.check_nested_free(); 581 m_rule_properties.check_infinite_sorts(); 582 break; 583 case SPACER_ENGINE: 584 m_rule_properties.collect(r); 585 m_rule_properties.check_existential_tail(); 586 m_rule_properties.check_for_negated_predicates(); 587 m_rule_properties.check_uninterpreted_free(); 588 m_rule_properties.check_quantifier_free(exists_k); 589 break; 590 case BMC_ENGINE: 591 m_rule_properties.collect(r); 592 m_rule_properties.check_for_negated_predicates(); 593 break; 594 case QBMC_ENGINE: 595 m_rule_properties.collect(r); 596 m_rule_properties.check_existential_tail(); 597 m_rule_properties.check_for_negated_predicates(); 598 break; 599 case TAB_ENGINE: 600 m_rule_properties.collect(r); 601 m_rule_properties.check_existential_tail(); 602 m_rule_properties.check_for_negated_predicates(); 603 break; 604 case CLP_ENGINE: 605 m_rule_properties.collect(r); 606 m_rule_properties.check_existential_tail(); 607 m_rule_properties.check_for_negated_predicates(); 608 break; 609 case DDNF_ENGINE: 610 break; 611 case LAST_ENGINE: 612 default: 613 UNREACHABLE(); 614 break; 615 } 616 } 617 add_rule(rule_ref & r)618 void context::add_rule(rule_ref& r) { 619 m_rule_set.add_rule(r); 620 } 621 add_fact(func_decl * pred,const relation_fact & fact)622 void context::add_fact(func_decl * pred, const relation_fact & fact) { 623 if (get_engine() == DATALOG_ENGINE) { 624 ensure_engine(); 625 m_rel->add_fact(pred, fact); 626 } 627 else { 628 expr_ref rule(m.mk_app(pred, fact.size(), (expr*const*)fact.data()), m); 629 add_rule(rule, symbol::null); 630 } 631 } 632 633 add_fact(app * head)634 void context::add_fact(app * head) { 635 SASSERT(is_fact(head)); 636 relation_fact fact(get_manager()); 637 unsigned n = head->get_num_args(); 638 for (unsigned i = 0; i < n; i++) { 639 fact.push_back(to_app(head->get_arg(i))); 640 } 641 add_fact(head->get_decl(), fact); 642 } 643 has_facts(func_decl * pred) const644 bool context::has_facts(func_decl * pred) const { 645 return m_rel && m_rel->has_facts(pred); 646 } 647 add_table_fact(func_decl * pred,const table_fact & fact)648 void context::add_table_fact(func_decl * pred, const table_fact & fact) { 649 if (get_engine() == DATALOG_ENGINE) { 650 ensure_engine(); 651 m_rel->add_fact(pred, fact); 652 } 653 else { 654 relation_fact rfact(m); 655 for (unsigned i = 0; i < fact.size(); ++i) { 656 rfact.push_back(m_decl_util.mk_numeral(fact[i], pred->get_domain()[i])); 657 } 658 add_fact(pred, rfact); 659 } 660 } 661 add_table_fact(func_decl * pred,unsigned num_args,unsigned args[])662 void context::add_table_fact(func_decl * pred, unsigned num_args, unsigned args[]) { 663 if (pred->get_arity() != num_args) { 664 std::ostringstream out; 665 out << "mismatched number of arguments passed to " << mk_ismt2_pp(pred, m) << " " << num_args << " passed"; 666 throw default_exception(out.str()); 667 } 668 table_fact fact; 669 for (unsigned i = 0; i < num_args; ++i) { 670 fact.push_back(args[i]); 671 } 672 add_table_fact(pred, fact); 673 } 674 close()675 void context::close() { 676 SASSERT(!m_closed); 677 if (!m_rule_set.close()) { 678 throw default_exception("Negation is not stratified!"); 679 } 680 m_closed = true; 681 } 682 ensure_closed()683 void context::ensure_closed() { 684 if (!m_closed) { 685 close(); 686 } 687 } ensure_opened()688 void context::ensure_opened() { 689 if (m_closed) { 690 reopen(); 691 } 692 } 693 reopen()694 void context::reopen() { 695 SASSERT(m_closed); 696 m_rule_set.reopen(); 697 m_closed = false; 698 } 699 transform_rules(rule_transformer::plugin * plugin)700 void context::transform_rules(rule_transformer::plugin* plugin) { 701 flet<bool> _enable_bv(m_enable_bind_variables, false); 702 rule_transformer transformer(*this); 703 transformer.register_plugin(plugin); 704 transform_rules(transformer); 705 } 706 transform_rules(rule_transformer & transf)707 void context::transform_rules(rule_transformer& transf) { 708 SASSERT(m_closed); //we must finish adding rules before we start transforming them 709 TRACE("dl", display_rules(tout);); 710 if (transf(m_rule_set)) { 711 //we have already ensured the negation is stratified and transformations 712 //should not break the stratification 713 m_rule_set.ensure_closed(); 714 TRACE("dl", display_rules(tout);); 715 TRACE("dl_verbose", display(tout);); 716 } 717 } 718 replace_rules(rule_set const & rs)719 void context::replace_rules(rule_set const & rs) { 720 SASSERT(!m_closed); 721 m_rule_set.replace_rules(rs); 722 if (m_rel) { 723 m_rel->restrict_predicates(get_predicates()); 724 } 725 } 726 record_transformed_rules()727 void context::record_transformed_rules() { 728 m_transformed_rule_set.replace_rules(m_rule_set); 729 } 730 apply_default_transformation()731 void context::apply_default_transformation() { 732 } 733 collect_params(param_descrs & p)734 void context::collect_params(param_descrs& p) { 735 fp_params::collect_param_descrs(p); 736 insert_timeout(p); 737 insert_ctrl_c(p); 738 } 739 updt_params(params_ref const & p)740 void context::updt_params(params_ref const& p) { 741 m_params_ref.copy(p); 742 if (m_engine.get()) m_engine->updt_params(); 743 m_generate_proof_trace = m_params->generate_proof_trace(); 744 m_unbound_compressor = m_params->datalog_unbound_compressor(); 745 m_default_relation = m_params->datalog_default_relation(); 746 } 747 get_background_assertion()748 expr_ref context::get_background_assertion() { 749 return mk_and(m_background); 750 } 751 assert_expr(expr * e)752 void context::assert_expr(expr* e) { 753 TRACE("dl", tout << mk_ismt2_pp(e, m) << "\n";); 754 m_background.push_back(e); 755 } 756 cleanup()757 void context::cleanup() { 758 m_last_status = OK; 759 if (m_engine) m_engine->cleanup(); 760 } 761 762 class context::engine_type_proc { 763 ast_manager& m; 764 arith_util a; 765 datatype_util dt; 766 bv_util bv; 767 array_util ar; 768 DL_ENGINE m_engine_type; 769 is_large_bv(sort * s)770 bool is_large_bv(sort* s) { 771 return false; 772 } 773 774 public: engine_type_proc(ast_manager & m)775 engine_type_proc(ast_manager& m): m(m), a(m), dt(m), bv(m), ar(m), m_engine_type(DATALOG_ENGINE) {} 776 get_engine() const777 DL_ENGINE get_engine() const { return m_engine_type; } 778 operator ()(expr * e)779 void operator()(expr* e) { 780 if (a.is_int_real(e)) { 781 m_engine_type = SPACER_ENGINE; 782 } 783 else if (is_var(e) && m.is_bool(e)) { 784 m_engine_type = SPACER_ENGINE; 785 } 786 else if (dt.is_datatype(e->get_sort())) { 787 m_engine_type = SPACER_ENGINE; 788 } 789 else if (is_large_bv(e->get_sort())) { 790 m_engine_type = SPACER_ENGINE; 791 } 792 else if (!e->get_sort()->get_num_elements().is_finite()) { 793 m_engine_type = SPACER_ENGINE; 794 } 795 else if (ar.is_array(e)) { 796 m_engine_type = SPACER_ENGINE; 797 } 798 } 799 }; 800 configure_engine(expr * q)801 void context::configure_engine(expr* q) { 802 TRACE("dl", tout << mk_pp(q, m) << " " << m_engine_type << "\n";); 803 if (m_engine_type != LAST_ENGINE) { 804 return; 805 } 806 symbol e = m_params->engine(); 807 808 if (e == symbol("datalog")) { 809 m_engine_type = DATALOG_ENGINE; 810 } 811 else if (e == symbol("spacer")) { 812 m_engine_type = SPACER_ENGINE; 813 } 814 else if (e == symbol("bmc")) { 815 m_engine_type = BMC_ENGINE; 816 } 817 else if (e == symbol("qbmc")) { 818 m_engine_type = QBMC_ENGINE; 819 } 820 else if (e == symbol("tab")) { 821 m_engine_type = TAB_ENGINE; 822 } 823 else if (e == symbol("clp")) { 824 m_engine_type = CLP_ENGINE; 825 } 826 else if (e == symbol("ddnf")) { 827 m_engine_type = DDNF_ENGINE; 828 } 829 else if (e == symbol("auto-config")) { 830 831 } 832 else { 833 throw default_exception("unsupported datalog engine type"); 834 } 835 836 if (m_engine_type == LAST_ENGINE) { 837 expr_fast_mark1 mark; 838 engine_type_proc proc(m); 839 m_engine_type = DATALOG_ENGINE; 840 if (q) { 841 quick_for_each_expr(proc, mark, q); 842 m_engine_type = proc.get_engine(); 843 } 844 845 for (unsigned i = 0; m_engine_type == DATALOG_ENGINE && i < m_rule_set.get_num_rules(); ++i) { 846 rule * r = m_rule_set.get_rule(i); 847 quick_for_each_expr(proc, mark, r->get_head()); 848 for (unsigned j = 0; j < r->get_tail_size(); ++j) { 849 quick_for_each_expr(proc, mark, r->get_tail(j)); 850 } 851 m_engine_type = proc.get_engine(); 852 } 853 for (unsigned i = m_rule_fmls_head; m_engine_type == DATALOG_ENGINE && i < m_rule_fmls.size(); ++i) { 854 expr* fml = m_rule_fmls[i].get(); 855 while (is_quantifier(fml)) { 856 fml = to_quantifier(fml)->get_expr(); 857 } 858 quick_for_each_expr(proc, mark, fml); 859 m_engine_type = proc.get_engine(); 860 } 861 } 862 } 863 query(expr * query)864 lbool context::query(expr* query) { 865 expr_ref _query(query, m); 866 m_mc = mk_skip_model_converter(); 867 m_last_status = OK; 868 m_last_answer = nullptr; 869 m_last_ground_answer = nullptr; 870 switch (get_engine(query)) { 871 case DATALOG_ENGINE: 872 case SPACER_ENGINE: 873 case BMC_ENGINE: 874 case QBMC_ENGINE: 875 case TAB_ENGINE: 876 case CLP_ENGINE: 877 case DDNF_ENGINE: 878 flush_add_rules(); 879 break; 880 default: 881 UNREACHABLE(); 882 } 883 ensure_engine(query); 884 lbool r = m_engine->query(query); 885 if (r != l_undef && get_params().print_certificate()) { 886 display_certificate(std::cout) << "\n"; 887 } 888 return r; 889 } 890 is_monotone()891 bool context::is_monotone() { 892 // assumes flush_add_rules was called 893 return m_rule_properties.is_monotone(); 894 } 895 896 query_from_lvl(expr * query,unsigned lvl)897 lbool context::query_from_lvl (expr* query, unsigned lvl) { 898 m_mc = mk_skip_model_converter(); 899 m_last_status = OK; 900 m_last_answer = nullptr; 901 m_last_ground_answer = nullptr; 902 switch (get_engine()) { 903 case DATALOG_ENGINE: 904 case SPACER_ENGINE: 905 case BMC_ENGINE: 906 case QBMC_ENGINE: 907 case TAB_ENGINE: 908 case CLP_ENGINE: 909 flush_add_rules(); 910 break; 911 default: 912 UNREACHABLE(); 913 } 914 ensure_engine(); 915 return m_engine->query_from_lvl (query, lvl); 916 } get_model()917 model_ref context::get_model() { 918 ensure_engine(); 919 return m_engine->get_model(); 920 } 921 get_proof()922 proof_ref context::get_proof() { 923 ensure_engine(); 924 return m_engine->get_proof(); 925 } 926 ensure_engine(expr * e)927 void context::ensure_engine(expr* e) { 928 if (!m_engine.get()) { 929 m_engine = m_register_engine.mk_engine(get_engine(e)); 930 m_engine->updt_params(); 931 932 // break abstraction. 933 if (get_engine() == DATALOG_ENGINE) { 934 m_rel = dynamic_cast<rel_context_base*>(m_engine.get()); 935 } 936 937 } 938 } 939 rel_query(unsigned num_rels,func_decl * const * rels)940 lbool context::rel_query(unsigned num_rels, func_decl * const* rels) { 941 m_last_answer = nullptr; 942 ensure_engine(); 943 return m_engine->query(num_rels, rels); 944 } 945 get_answer_as_formula()946 expr* context::get_answer_as_formula() { 947 if (m_last_answer) { 948 return m_last_answer.get(); 949 } 950 ensure_engine(); 951 m_last_answer = m_engine->get_answer(); 952 return m_last_answer.get(); 953 } 954 get_ground_sat_answer()955 expr* context::get_ground_sat_answer () { 956 if (m_last_ground_answer) { 957 return m_last_ground_answer; 958 } 959 ensure_engine (); 960 m_last_ground_answer = m_engine->get_ground_sat_answer (); 961 return m_last_ground_answer; 962 } 963 get_rules_along_trace(rule_ref_vector & rules)964 void context::get_rules_along_trace (rule_ref_vector& rules) { 965 ensure_engine (); 966 m_engine->get_rules_along_trace (rules); 967 } 968 get_rules_along_trace_as_formulas(expr_ref_vector & rules,svector<symbol> & names)969 void context::get_rules_along_trace_as_formulas (expr_ref_vector& rules, svector<symbol>& names) { 970 rule_manager& rm = get_rule_manager (); 971 rule_ref_vector rv (rm); 972 get_rules_along_trace (rv); 973 expr_ref fml (m); 974 for (auto* r : rv) { 975 m_rule_manager.to_formula (*r, fml); 976 rules.push_back (fml); 977 // The concatenated names are already stored last-first, so do not need to be reversed here 978 const symbol& rule_name = r->name(); 979 names.push_back (rule_name); 980 981 TRACE ("dl", 982 if (rule_name == symbol::null) { 983 tout << "Encountered unnamed rule: "; 984 r->display(*this, tout); 985 tout << "\n"; 986 }); 987 } 988 } 989 display_certificate(std::ostream & out)990 std::ostream& context::display_certificate(std::ostream& out) { 991 ensure_engine(); 992 m_engine->display_certificate(out); 993 return out; 994 } 995 display(std::ostream & out) const996 void context::display(std::ostream & out) const { 997 display_rules(out); 998 if (m_rel) m_rel->display_facts(out); 999 } 1000 display_profile(std::ostream & out) const1001 void context::display_profile(std::ostream& out) const { 1002 out << "\n---------------\n"; 1003 out << "Original rules\n"; 1004 display_rules(out); 1005 out << "\n---------------\n"; 1006 out << "Transformed rules\n"; 1007 m_transformed_rule_set.display(out); 1008 1009 if (m_rel) { 1010 m_rel->display_profile(out); 1011 } 1012 } 1013 reset_statistics()1014 void context::reset_statistics() { 1015 if (m_engine) { 1016 m_engine->reset_statistics(); 1017 } 1018 } 1019 collect_statistics(statistics & st) const1020 void context::collect_statistics(statistics& st) const { 1021 if (m_engine) { 1022 m_engine->collect_statistics(st); 1023 } 1024 get_memory_statistics(st); 1025 get_rlimit_statistics(m.limit(), st); 1026 } 1027 1028 get_status()1029 execution_result context::get_status() { return m_last_status; } 1030 result_contains_fact(relation_fact const & f)1031 bool context::result_contains_fact(relation_fact const& f) { 1032 return m_rel && m_rel->result_contains_fact(f); 1033 } 1034 1035 // NB: algebraic data-types declarations will not be printed. 1036 collect_free_funcs(unsigned sz,expr * const * exprs,ast_pp_util & v,mk_fresh_name & fresh_names)1037 static void collect_free_funcs(unsigned sz, expr* const* exprs, 1038 ast_pp_util& v, 1039 mk_fresh_name& fresh_names) { 1040 v.collect(sz, exprs); 1041 for (unsigned i = 0; i < sz; ++i) { 1042 expr* e = exprs[i]; 1043 while (is_quantifier(e)) { 1044 e = to_quantifier(e)->get_expr(); 1045 } 1046 fresh_names.add(e); 1047 } 1048 } 1049 get_raw_rule_formulas(expr_ref_vector & rules,svector<symbol> & names,unsigned_vector & bounds)1050 void context::get_raw_rule_formulas(expr_ref_vector& rules, svector<symbol>& names, unsigned_vector &bounds) { 1051 for (unsigned i = 0; i < m_rule_fmls.size(); ++i) { 1052 expr_ref r = bind_vars(m_rule_fmls[i].get(), true); 1053 rules.push_back(r.get()); 1054 names.push_back(m_rule_names[i]); 1055 bounds.push_back(m_rule_bounds[i]); 1056 } 1057 } 1058 get_rules_as_formulas(expr_ref_vector & rules,expr_ref_vector & queries,svector<symbol> & names)1059 void context::get_rules_as_formulas(expr_ref_vector& rules, expr_ref_vector& queries, svector<symbol>& names) { 1060 expr_ref fml(m); 1061 rule_manager& rm = get_rule_manager(); 1062 1063 // ensure that rules are all using bound variables. 1064 for (unsigned i = m_rule_fmls_head; i < m_rule_fmls.size(); ++i) { 1065 m_free_vars(m_rule_fmls[i].get()); 1066 if (!m_free_vars.empty()) { 1067 rm.mk_rule(m_rule_fmls[i].get(), nullptr, m_rule_set, m_rule_names[i]); 1068 m_rule_fmls[i] = m_rule_fmls.back(); 1069 m_rule_names[i] = m_rule_names.back(); 1070 m_rule_fmls.pop_back(); 1071 m_rule_names.pop_back(); 1072 m_rule_bounds.pop_back(); 1073 --i; 1074 } 1075 } 1076 for (rule* r : m_rule_set) { 1077 rm.to_formula(*r, fml); 1078 func_decl* h = r->get_decl(); 1079 if (m_rule_set.is_output_predicate(h)) { 1080 expr* body = fml; 1081 expr* e2; 1082 if (is_quantifier(body)) { 1083 quantifier* q = to_quantifier(body); 1084 expr* e = q->get_expr(); 1085 if (m.is_implies(e, body, e2)) { 1086 fml = m.mk_quantifier(exists_k, q->get_num_decls(), 1087 q->get_decl_sorts(), q->get_decl_names(), 1088 body); 1089 } 1090 else { 1091 fml = body; 1092 } 1093 } 1094 else { 1095 fml = body; 1096 if (m.is_implies(body, body, e2)) { 1097 fml = body; 1098 } 1099 } 1100 queries.push_back(fml); 1101 } 1102 else { 1103 rules.push_back(fml); 1104 names.push_back(r->name()); 1105 } 1106 } 1107 for (unsigned i = m_rule_fmls_head; i < m_rule_fmls.size(); ++i) { 1108 rules.push_back(m_rule_fmls[i].get()); 1109 names.push_back(m_rule_names[i]); 1110 } 1111 } 1112 display_symbol(std::ostream & out,symbol const & nm)1113 static std::ostream& display_symbol(std::ostream& out, symbol const& nm) { 1114 if (is_smt2_quoted_symbol(nm)) { 1115 out << mk_smt2_quoted_symbol(nm); 1116 } 1117 else { 1118 out << nm; 1119 } 1120 return out; 1121 } 1122 display_smt2(unsigned num_queries,expr * const * qs,std::ostream & out)1123 void context::display_smt2(unsigned num_queries, expr* const* qs, std::ostream& out) { 1124 ast_manager& m = get_manager(); 1125 ast_pp_util visitor(m); 1126 func_decl_set rels; 1127 unsigned num_axioms = m_background.size(); 1128 expr* const* axioms = m_background.data(); 1129 expr_ref fml(m); 1130 expr_ref_vector rules(m), queries(m); 1131 svector<symbol> names; 1132 bool use_fixedpoint_extensions = m_params->print_fixedpoint_extensions(); 1133 bool print_low_level = m_params->print_low_level_smt2(); 1134 bool do_declare_vars = m_params->print_with_variable_declarations(); 1135 1136 #define PP(_e_) if (print_low_level) out << mk_smt_pp(_e_, m); else ast_smt2_pp(out, _e_, env); 1137 1138 get_rules_as_formulas(rules, queries, names); 1139 queries.append(num_queries, qs); 1140 1141 smt2_pp_environment_dbg env(m); 1142 mk_fresh_name fresh_names; 1143 collect_free_funcs(num_axioms, axioms, visitor, fresh_names); 1144 collect_free_funcs(rules.size(), rules.data(), visitor, fresh_names); 1145 collect_free_funcs(queries.size(), queries.data(), visitor, fresh_names); 1146 func_decl_set funcs; 1147 unsigned sz = visitor.coll.get_num_decls(); 1148 for (unsigned i = 0; i < sz; ++i) { 1149 func_decl* f = visitor.coll.get_func_decls()[i]; 1150 if (f->get_family_id() != null_family_id) { 1151 // 1152 } 1153 else if (is_predicate(f) && use_fixedpoint_extensions) { 1154 rels.insert(f); 1155 } 1156 else { 1157 funcs.insert(f); 1158 } 1159 } 1160 1161 if (!use_fixedpoint_extensions) { 1162 out << "(set-logic HORN)\n"; 1163 } 1164 for (func_decl * f : rels) 1165 visitor.remove_decl(f); 1166 1167 visitor.display_decls(out); 1168 1169 for (func_decl * f : rels) 1170 display_rel_decl(out, f); 1171 1172 if (use_fixedpoint_extensions && do_declare_vars) { 1173 declare_vars(rules, fresh_names, out); 1174 } 1175 1176 if (num_axioms > 0 && !use_fixedpoint_extensions) { 1177 throw default_exception("Background axioms cannot be used with SMT-LIB2 HORN format"); 1178 } 1179 1180 for (unsigned i = 0; i < num_axioms; ++i) { 1181 out << "(assert "; 1182 PP(axioms[i]); 1183 out << ")\n"; 1184 } 1185 for (unsigned i = 0; i < rules.size(); ++i) { 1186 out << (use_fixedpoint_extensions?"(rule ":"(assert "); 1187 expr* r = rules[i].get(); 1188 symbol nm = names[i]; 1189 if (symbol::null != nm) { 1190 out << "(! "; 1191 } 1192 PP(r); 1193 if (symbol::null != nm) { 1194 out << " :named "; 1195 while (fresh_names.contains(nm)) { 1196 std::ostringstream s; 1197 s << nm << '!'; 1198 nm = symbol(s.str()); 1199 } 1200 fresh_names.add(nm); 1201 display_symbol(out, nm) << ')'; 1202 } 1203 out << ")\n"; 1204 } 1205 if (use_fixedpoint_extensions) { 1206 for (unsigned i = 0; i < queries.size(); ++i) { 1207 expr* q = queries[i].get(); 1208 func_decl_ref fn(m); 1209 if (is_query(q)) { 1210 fn = to_app(q)->get_decl(); 1211 } 1212 else { 1213 m_free_vars(q); 1214 m_free_vars.set_default_sort(m.mk_bool_sort()); 1215 sort* const* domain = m_free_vars.data(); 1216 expr_ref qfn(m); 1217 expr_ref_vector args(m); 1218 fn = m.mk_fresh_func_decl(symbol("q"), symbol(""), m_free_vars.size(), domain, m.mk_bool_sort()); 1219 display_rel_decl(out, fn); 1220 for (unsigned j = 0; j < m_free_vars.size(); ++j) { 1221 args.push_back(m.mk_var(j, m_free_vars[j])); 1222 } 1223 qfn = m.mk_implies(q, m.mk_app(fn, args.size(), args.data())); 1224 1225 out << "(assert "; 1226 PP(qfn); 1227 out << ")\n"; 1228 } 1229 out << "(query "; 1230 display_symbol(out, fn->get_name()) << ")\n"; 1231 } 1232 } 1233 else { 1234 for (unsigned i = 0; i < queries.size(); ++i) { 1235 if (queries.size() > 1) out << "(push 1)\n"; 1236 out << "(assert "; 1237 expr_ref q(m); 1238 q = m.mk_not(queries[i].get()); 1239 PP(q); 1240 out << ")\n"; 1241 out << "(check-sat)\n"; 1242 if (queries.size() > 1) out << "(pop 1)\n"; 1243 } 1244 } 1245 } 1246 display_rel_decl(std::ostream & out,func_decl * f)1247 void context::display_rel_decl(std::ostream& out, func_decl* f) { 1248 smt2_pp_environment_dbg env(m); 1249 out << "(declare-rel "; 1250 display_symbol(out, f->get_name()) << " ("; 1251 for (unsigned i = 0; i < f->get_arity(); ++i) { 1252 ast_smt2_pp(out, f->get_domain(i), env); 1253 if (i + 1 < f->get_arity()) { 1254 out << " "; 1255 } 1256 } 1257 out << "))\n"; 1258 } 1259 is_query(expr * q)1260 bool context::is_query(expr* q) { 1261 if (!is_app(q) || !is_predicate(to_app(q)->get_decl())) { 1262 return false; 1263 } 1264 app* a = to_app(q); 1265 for (unsigned i = 0; i < a->get_num_args(); ++i) { 1266 if (!is_var(a->get_arg(i))) { 1267 return false; 1268 } 1269 var* v = to_var(a->get_arg(i)); 1270 if (v->get_idx() != i) { 1271 return false; 1272 } 1273 } 1274 return true; 1275 } 1276 1277 declare_vars(expr_ref_vector & rules,mk_fresh_name & fresh_names,std::ostream & out)1278 void context::declare_vars(expr_ref_vector& rules, mk_fresh_name& fresh_names, std::ostream& out) { 1279 // 1280 // replace bound variables in rules by 'var declarations' 1281 // First remove quantifiers, then replace bound variables 1282 // by fresh constants. 1283 // 1284 smt2_pp_environment_dbg env(m); 1285 var_subst vsubst(m, false); 1286 1287 expr_ref_vector fresh_vars(m), subst(m); 1288 expr_ref res(m); 1289 obj_map<sort, unsigned_vector> var_idxs; 1290 obj_map<sort, unsigned> max_vars; 1291 for (unsigned i = 0; i < rules.size(); ++i) { 1292 expr* r = rules[i].get(); 1293 if (!is_forall(r)) { 1294 continue; 1295 } 1296 quantifier* q = to_quantifier(r); 1297 if (has_quantifiers(q->get_expr())) { 1298 continue; 1299 } 1300 max_vars.reset(); 1301 subst.reset(); 1302 unsigned max_var = 0; 1303 unsigned num_vars = q->get_num_decls(); 1304 for (unsigned j = 0; j < num_vars; ++j) { 1305 sort* s = q->get_decl_sort(num_vars-1-j); 1306 // maximal var for the given sort. 1307 if (!max_vars.find(s, max_var)) { 1308 max_var = 0; 1309 } 1310 else { 1311 ++max_var; 1312 } 1313 max_vars.insert(s, max_var); 1314 1315 // index into fresh variable array. 1316 // unsigned fresh_var_idx = 0; 1317 unsigned_vector& vars = var_idxs.insert_if_not_there(s, unsigned_vector()); 1318 if (max_var >= vars.size()) { 1319 SASSERT(vars.size() == max_var); 1320 vars.push_back(fresh_vars.size()); 1321 symbol name = fresh_names.next(); 1322 fresh_vars.push_back(m.mk_const(name, s)); 1323 out << "(declare-var " << name << " "; 1324 ast_smt2_pp(out, s, env); 1325 out << ")\n"; 1326 } 1327 subst.push_back(fresh_vars[vars[max_var]].get()); 1328 } 1329 1330 res = vsubst(q->get_expr(), subst.size(), subst.data()); 1331 rules[i] = res.get(); 1332 } 1333 } 1334 1335 1336 }; 1337