1 /*++ 2 Copyright (c) 2013 Microsoft Corporation 3 4 Module Name: 5 6 tab_context.cpp 7 8 Abstract: 9 10 Tabulation/subsumption/cyclic proof context. 11 12 Author: 13 14 Nikolaj Bjorner (nbjorner) 2013-01-15 15 16 Revision History: 17 18 --*/ 19 20 #include "muz/tab/tab_context.h" 21 #include "util/trail.h" 22 #include "muz/base/dl_rule_set.h" 23 #include "muz/base/dl_context.h" 24 #include "muz/transforms/dl_mk_rule_inliner.h" 25 #include "smt/smt_kernel.h" 26 #include "qe/qe_lite.h" 27 #include "ast/rewriter/bool_rewriter.h" 28 #include "ast/rewriter/th_rewriter.h" 29 #include "ast/datatype_decl_plugin.h" 30 #include "ast/for_each_expr.h" 31 #include "ast/substitution/matcher.h" 32 #include "ast/scoped_proof.h" 33 #include "muz/base/fp_params.hpp" 34 #include "ast/ast_util.h" 35 36 namespace tb { 37 38 // semantic matcher. 39 class matcher { 40 typedef std::pair<expr *, expr *> expr_pair; 41 ast_manager& m; 42 svector<expr_pair> m_todo; 43 datatype_util m_dt; 44 is_eq(expr * _s,expr * _t)45 lbool is_eq(expr* _s, expr* _t) { 46 if (_s == _t) { 47 return l_true; 48 } 49 if (!is_app(_s) || !is_app(_t)) { 50 return l_undef; 51 } 52 app* s = to_app(_s); 53 app* t = to_app(_t); 54 55 if (m.is_value(s) && m.is_value(t)) { 56 IF_VERBOSE(2, verbose_stream() << "different:" << mk_pp(s, m) << " " << mk_pp(t, m) << "\n";); 57 return l_false; 58 } 59 60 if (m_dt.is_constructor(s) && m_dt.is_constructor(t)) { 61 if (s->get_decl() == t->get_decl()) { 62 lbool state = l_true; 63 for (unsigned i = 0; i < s->get_num_args(); ++i) { 64 // move is_eq: decompose arguments to constraints. 65 switch (is_eq(s->get_arg(i), t->get_arg(i))) { 66 case l_undef: 67 state = l_undef; 68 break; 69 case l_false: 70 return l_false; 71 default: 72 break; 73 } 74 } 75 return state; 76 } 77 else { 78 IF_VERBOSE(2, verbose_stream() << "different constructors:" << mk_pp(s, m) << " " << mk_pp(t, m) << "\n";); 79 return l_false; 80 } 81 } 82 return l_undef; 83 } 84 match_var(var * v,app * t,substitution & s,expr_ref_vector & conds)85 bool match_var(var* v, app* t, substitution& s, expr_ref_vector& conds) { 86 expr_offset r; 87 if (s.find(v, 0, r)) { 88 app* p = to_app(r.get_expr()); 89 switch (is_eq(p, t)) { 90 case l_true: 91 break; 92 case l_false: 93 return false; 94 default: 95 conds.push_back(m.mk_eq(p, t)); 96 break; 97 } 98 } 99 else { 100 s.insert(v, 0, expr_offset(t, 1)); 101 } 102 return true; 103 } 104 match_app(app * p,app * t,substitution & s,expr_ref_vector & conds)105 bool match_app(app* p, app* t, substitution& s, expr_ref_vector& conds) { 106 switch(is_eq(p, t)) { 107 case l_true: 108 return true; 109 case l_false: 110 return false; 111 default: 112 conds.push_back(m.mk_eq(p, t)); 113 return true; 114 } 115 } 116 117 118 public: matcher(ast_manager & m)119 matcher(ast_manager& m): m(m), m_dt(m) {} 120 operator ()(app * pat,app * term,substitution & s,expr_ref_vector & conds)121 bool operator()(app* pat, app* term, substitution& s, expr_ref_vector& conds) { 122 // top-most term to match is a predicate. The predicates should be the same. 123 if (pat->get_decl() != term->get_decl() || 124 pat->get_num_args() != term->get_num_args()) { 125 return false; 126 } 127 m_todo.reset(); 128 for (unsigned i = 0; i < pat->get_num_args(); ++i) { 129 m_todo.push_back(expr_pair(pat->get_arg(i), term->get_arg(i))); 130 } 131 while (!m_todo.empty()) { 132 expr_pair const& pr = m_todo.back(); 133 expr* p = pr.first; 134 expr* t = pr.second; 135 m_todo.pop_back(); 136 if (!is_app(t)) { 137 IF_VERBOSE(2, verbose_stream() << "term is not app\n";); 138 return false; 139 } 140 else if (is_var(p) && match_var(to_var(p), to_app(t), s, conds)) { 141 continue; 142 } 143 else if (!is_app(p)) { 144 IF_VERBOSE(2, verbose_stream() << "pattern is not app\n";); 145 return false; 146 } 147 else if (!match_app(to_app(p), to_app(t), s, conds)) { 148 return false; 149 } 150 } 151 return true; 152 } 153 }; 154 155 class clause { 156 app_ref m_head; // head predicate 157 app_ref_vector m_predicates; // predicates used in goal 158 expr_ref m_constraint; // side constraint 159 unsigned m_seqno; // sequence number of goal 160 unsigned m_index; // index of goal into set of goals 161 unsigned m_num_vars; // maximal free variable index+1 162 unsigned m_predicate_index; // selected predicate 163 unsigned m_parent_rule; // rule used to produce goal 164 unsigned m_parent_index; // index of parent goal 165 unsigned m_next_rule; // next rule to expand goal on 166 unsigned m_ref; // reference count 167 168 public: 169 clause(ast_manager & m)170 clause(ast_manager& m): 171 m_head(m), 172 m_predicates(m), 173 m_constraint(m), 174 m_seqno(0), 175 m_index(0), 176 m_num_vars(0), 177 m_predicate_index(0), 178 m_parent_rule(0), 179 m_parent_index(0), 180 m_next_rule(static_cast<unsigned>(-1)), 181 m_ref(0) { 182 } 183 set_seqno(unsigned seqno)184 void set_seqno(unsigned seqno) { m_seqno = seqno; } get_seqno() const185 unsigned get_seqno() const { return m_seqno; } get_next_rule() const186 unsigned get_next_rule() const { return m_next_rule; } inc_next_rule()187 void inc_next_rule() { m_next_rule++; } get_predicate_index() const188 unsigned get_predicate_index() const { return m_predicate_index; } set_predicate_index(unsigned i)189 void set_predicate_index(unsigned i) { m_predicate_index = i; } get_num_predicates() const190 unsigned get_num_predicates() const { return m_predicates.size(); } get_predicate(unsigned i) const191 app* get_predicate(unsigned i) const { return m_predicates[i]; } get_constraint() const192 expr* get_constraint() const { return m_constraint; } get_num_vars() const193 unsigned get_num_vars() const { return m_num_vars; } get_index() const194 unsigned get_index() const { return m_index; } set_index(unsigned index)195 void set_index(unsigned index) { m_index = index; } get_head() const196 app* get_head() const { return m_head; } get_decl() const197 func_decl* get_decl() const { return m_head->get_decl(); } set_head(app * h)198 void set_head(app* h) { m_head = h; } get_parent_index() const199 unsigned get_parent_index() const { return m_parent_index; } get_parent_rule() const200 unsigned get_parent_rule() const { return m_parent_rule; } set_parent(ref<tb::clause> & parent)201 void set_parent(ref<tb::clause>& parent) { 202 m_parent_index = parent->get_index(); 203 m_parent_rule = parent->get_next_rule(); 204 } 205 get_body() const206 expr_ref get_body() const { 207 ast_manager& m = get_manager(); 208 expr_ref_vector fmls(m); 209 expr_ref fml(m); 210 for (unsigned i = 0; i < m_predicates.size(); ++i) { 211 fmls.push_back(m_predicates[i]); 212 } 213 fmls.push_back(m_constraint); 214 flatten_and(fmls); 215 bool_rewriter(m).mk_and(fmls.size(), fmls.c_ptr(), fml); 216 return fml; 217 } 218 get_free_vars(ptr_vector<sort> & vars) const219 void get_free_vars(ptr_vector<sort>& vars) const { 220 expr_free_vars fv; 221 fv(m_head); 222 for (unsigned i = 0; i < m_predicates.size(); ++i) { 223 fv.accumulate(m_predicates[i]); 224 } 225 fv.accumulate(m_constraint); 226 vars.append(fv.size(), fv.c_ptr()); 227 } 228 to_formula() const229 expr_ref to_formula() const { 230 ast_manager& m = get_manager(); 231 expr_ref body = get_body(); 232 if (m.is_true(body)) { 233 body = m_head; 234 } 235 else { 236 body = m.mk_implies(body, m_head); 237 } 238 ptr_vector<sort> vars; 239 svector<symbol> names; 240 get_free_vars(vars); 241 mk_fresh_name fresh; 242 fresh.add(body); 243 vars.reverse(); 244 for (unsigned i = 0; i < vars.size(); ++i) { 245 names.push_back(fresh.next()); 246 if (!vars[i]) vars[i] = m.mk_bool_sort(); 247 } 248 if (!vars.empty()) { 249 body = m.mk_forall(vars.size(), vars.c_ptr(), names.c_ptr(), body); 250 } 251 return body; 252 } 253 init(app * head,app_ref_vector const & predicates,expr * constraint)254 void init(app* head, app_ref_vector const& predicates, expr* constraint) { 255 m_index = 0; 256 m_predicate_index = 0; 257 m_next_rule = static_cast<unsigned>(-1); 258 m_head = head; 259 m_predicates.reset(); 260 m_predicates.append(predicates); 261 m_constraint = constraint; 262 ptr_vector<sort> sorts; 263 get_free_vars(sorts); 264 m_num_vars = sorts.size(); 265 reduce_equalities(); 266 } 267 init(datalog::rule_ref & g)268 void init(datalog::rule_ref& g) { 269 m_index = 0; 270 m_predicate_index = 0; 271 m_next_rule = static_cast<unsigned>(-1); 272 init_from_rule(g); 273 reduce_equalities(); 274 // IF_VERBOSE(1, display(verbose_stream());); 275 } 276 inc_ref()277 void inc_ref() { 278 m_ref++; 279 } 280 dec_ref()281 void dec_ref() { 282 --m_ref; 283 if (m_ref == 0) { 284 dealloc(this); 285 } 286 } 287 display(std::ostream & out) const288 void display(std::ostream& out) const { 289 ast_manager& m = m_head.get_manager(); 290 expr_ref_vector fmls(m); 291 expr_ref fml(m); 292 for (unsigned i = 0; i < m_predicates.size(); ++i) { 293 fmls.push_back(m_predicates[i]); 294 } 295 fmls.push_back(m_constraint); 296 bool_rewriter(m).mk_and(fmls.size(), fmls.c_ptr(), fml); 297 if (!m.is_false(m_head)) { 298 if (m.is_true(fml)) { 299 fml = m_head; 300 } 301 else { 302 fml = m.mk_implies(fml, m_head); 303 } 304 } 305 out << mk_pp(fml, m) << "\n"; 306 } 307 308 private: 309 get_manager() const310 ast_manager& get_manager() const { return m_head.get_manager(); } 311 312 // Given a rule, initialize fields: 313 // - m_num_vars - number of free variables in rule 314 // - m_head - head predicate 315 // - m_predicates - auxiliary predicates in body. 316 // - m_constraint - side constraint 317 // init_from_rule(datalog::rule_ref const & r)318 void init_from_rule(datalog::rule_ref const& r) { 319 ast_manager& m = get_manager(); 320 expr_ref_vector fmls(m); 321 unsigned utsz = r->get_uninterpreted_tail_size(); 322 unsigned tsz = r->get_tail_size(); 323 for (unsigned i = utsz; i < tsz; ++i) { 324 fmls.push_back(r->get_tail(i)); 325 } 326 m_num_vars = 1 + r.get_manager().get_counter().get_max_rule_var(*r); 327 m_head = r->get_head(); 328 m_predicates.reset(); 329 for (unsigned i = 0; i < utsz; ++i) { 330 m_predicates.push_back(r->get_tail(i)); 331 } 332 bool_rewriter(m).mk_and(fmls.size(), fmls.c_ptr(), m_constraint); 333 } 334 335 // Simplify a clause by applying equalities as substitutions on predicates. 336 // x = t[y], if x does not occur in t[y], then add t[y] to subst. reduce_equalities()337 void reduce_equalities() { 338 ast_manager& m = get_manager(); 339 th_rewriter rw(m); 340 unsigned delta[1] = { 0 }; 341 expr_ref_vector fmls(m); 342 expr_ref tmp(m); 343 substitution subst(m); 344 subst.reserve(1, get_num_vars()); 345 flatten_and(m_constraint, fmls); 346 unsigned num_fmls = fmls.size(); 347 for (unsigned i = 0; i < num_fmls; ++i) { 348 if (get_subst(rw, subst, i, fmls)) { 349 fmls[i] = m.mk_true(); 350 } 351 } 352 subst.apply(1, delta, expr_offset(m_head, 0), tmp); 353 m_head = to_app(tmp); 354 for (unsigned i = 0; i < m_predicates.size(); ++i) { 355 subst.apply(1, delta, expr_offset(m_predicates[i].get(), 0), tmp); 356 m_predicates[i] = to_app(tmp); 357 } 358 bool_rewriter(m).mk_and(fmls.size(), fmls.c_ptr(), m_constraint); 359 subst.apply(1, delta, expr_offset(m_constraint, 0), m_constraint); 360 rw(m_constraint); 361 } 362 get_subst(th_rewriter & rw,substitution & S,unsigned i,expr_ref_vector & fmls)363 bool get_subst(th_rewriter& rw, substitution& S, unsigned i, expr_ref_vector& fmls) { 364 ast_manager& m = get_manager(); 365 unsigned delta[1] = { 0 }; 366 expr* f = fmls[i].get(); 367 expr_ref e(m), tr(m); 368 expr* t, *v; 369 S.apply(1, delta, expr_offset(f, 0), e); 370 rw(e); 371 fmls[i] = e; 372 if (!m.is_eq(e, v, t)) { 373 return false; 374 } 375 if (!is_var(v)) { 376 std::swap(v, t); 377 } 378 if (!is_var(v)) { 379 return false; 380 } 381 if (!can_be_substituted(m, t)) { 382 return false; 383 } 384 SASSERT(!S.contains(to_var(v), 0)); 385 S.push_scope(); 386 S.insert(to_var(v)->get_idx(), 0, expr_offset(t, 0)); 387 if (!S.acyclic()) { 388 S.pop_scope(); 389 return false; 390 } 391 fmls[i] = m.mk_true(); 392 return true; 393 } 394 395 struct non_constructor {}; 396 397 struct constructor_test { 398 ast_manager& m; 399 datatype_util dt; constructor_testtb::clause::constructor_test400 constructor_test(ast_manager& m): m(m), dt(m) {} operator ()tb::clause::constructor_test401 void operator()(app* e) { 402 if (!m.is_value(e) && 403 !dt.is_constructor(e->get_decl())) { 404 throw non_constructor(); 405 } 406 } operator ()tb::clause::constructor_test407 void operator()(var* v) { } operator ()tb::clause::constructor_test408 void operator()(quantifier* ) { 409 throw non_constructor(); 410 } 411 }; 412 can_be_substituted(ast_manager & m,expr * t)413 bool can_be_substituted(ast_manager& m, expr* t) { 414 constructor_test p(m); 415 try { 416 quick_for_each_expr(p, t); 417 } 418 catch (const non_constructor &) { 419 return false; 420 } 421 return true; 422 } 423 424 }; 425 426 // rules 427 class rules { 428 typedef obj_map<func_decl, unsigned_vector> map; 429 vector<ref<clause> > m_rules; 430 map m_index; 431 public: 432 433 typedef vector<ref<clause> >::const_iterator iterator; 434 begin() const435 iterator begin() const { return m_rules.begin(); } end() const436 iterator end() const { return m_rules.end(); } 437 init(datalog::rule_set const & rules)438 void init(datalog::rule_set const& rules) { 439 reset(); 440 datalog::rule_manager& rm = rules.get_rule_manager(); 441 datalog::rule_ref r(rm); 442 datalog::rule_set::iterator it = rules.begin(); 443 datalog::rule_set::iterator end = rules.end(); 444 for (unsigned i = 0; it != end; ++it) { 445 r = *it; 446 ref<clause> g = alloc(clause, rm.get_manager()); 447 g->init(r); 448 g->set_index(i++); 449 insert(g); 450 } 451 } 452 insert(ref<clause> & g)453 void insert(ref<clause>& g) { 454 unsigned idx = m_rules.size(); 455 m_rules.push_back(g); 456 func_decl* f = g->get_decl(); 457 m_index.insert_if_not_there(f, unsigned_vector()).push_back(idx); 458 } 459 get_num_rules(func_decl * p) const460 unsigned get_num_rules(func_decl* p) const { 461 map::obj_map_entry* e = m_index.find_core(p); 462 if (e) { 463 return e->get_data().get_value().size(); 464 } 465 else { 466 return 0; 467 } 468 } 469 get_decls(ptr_vector<func_decl> & decls) const470 void get_decls(ptr_vector<func_decl>& decls) const { 471 map::iterator it = m_index.begin(); 472 map::iterator end = m_index.end(); 473 for (; it != end; ++it) { 474 decls.push_back(it->m_key); 475 } 476 } 477 get_rule(func_decl * p,unsigned idx) const478 ref<clause> get_rule(func_decl* p, unsigned idx) const { 479 map::obj_map_entry* e = m_index.find_core(p); 480 SASSERT(p); 481 unsigned rule_id = e->get_data().get_value()[idx]; 482 return m_rules[rule_id]; 483 } 484 private: reset()485 void reset() { 486 m_rules.reset(); 487 m_index.reset(); 488 } 489 }; 490 491 492 // subsumption index structure. 493 class index { 494 ast_manager& m; 495 app_ref_vector m_preds; 496 app_ref m_head; 497 expr_ref m_precond; 498 expr_ref_vector m_sideconds; 499 ref<clause> m_clause; 500 vector<ref<clause> > m_index; 501 matcher m_matcher; 502 expr_ref_vector m_refs; 503 obj_hashtable<expr> m_sat_lits; 504 substitution m_subst; 505 qe_lite m_qe; 506 uint_set m_empty_set; 507 bool_rewriter m_rw; 508 smt_params m_fparams; 509 smt::kernel m_solver; 510 511 public: index(ast_manager & m)512 index(ast_manager& m): 513 m(m), 514 m_preds(m), 515 m_head(m), 516 m_precond(m), 517 m_sideconds(m), 518 m_matcher(m), 519 m_refs(m), 520 m_subst(m), 521 m_qe(m, params_ref()), 522 m_rw(m), 523 m_solver(m, m_fparams) {} 524 insert(ref<clause> & g)525 void insert(ref<clause>& g) { 526 m_index.push_back(g); 527 } 528 is_subsumed(ref<tb::clause> & g,unsigned & subsumer)529 bool is_subsumed(ref<tb::clause>& g, unsigned& subsumer) { 530 setup(*g); 531 m_clause = g; 532 m_solver.push(); 533 m_solver.assert_expr(m_precond); 534 bool found = find_match(subsumer); 535 m_solver.pop(1); 536 return found; 537 } 538 539 reset()540 void reset() { 541 m_index.reset(); 542 } 543 544 private: 545 setup(clause const & g)546 void setup(clause const& g) { 547 m_preds.reset(); 548 m_refs.reset(); 549 m_sat_lits.reset(); 550 expr_ref_vector fmls(m); 551 expr_ref_vector vars(m); 552 expr_ref fml(m); 553 ptr_vector<sort> sorts; 554 g.get_free_vars(sorts); 555 var_subst vs(m, false); 556 for (unsigned i = 0; i < sorts.size(); ++i) { 557 if (!sorts[i]) { 558 sorts[i] = m.mk_bool_sort(); 559 } 560 vars.push_back(m.mk_const(symbol(i), sorts[i])); 561 } 562 fml = vs(g.get_head(), vars.size(), vars.c_ptr()); 563 m_head = to_app(fml); 564 for (unsigned i = 0; i < g.get_num_predicates(); ++i) { 565 fml = vs(g.get_predicate(i), vars.size(), vars.c_ptr()); 566 m_preds.push_back(to_app(fml)); 567 } 568 fml = vs(g.get_constraint(), vars.size(), vars.c_ptr()); 569 fmls.push_back(fml); 570 m_precond = m.mk_and(fmls.size(), fmls.c_ptr()); 571 IF_VERBOSE(2, 572 verbose_stream() << "setup-match: "; 573 for (unsigned i = 0; i < m_preds.size(); ++i) { 574 verbose_stream() << mk_pp(m_preds[i].get(), m) << " "; 575 } 576 verbose_stream() << mk_pp(m_precond, m) << "\n";); 577 } 578 579 580 // extract pre_cond => post_cond validation obligation from match. find_match(unsigned & subsumer)581 bool find_match(unsigned& subsumer) { 582 for (unsigned i = 0; m.inc() && i < m_index.size(); ++i) { 583 if (match_rule(i)) { 584 subsumer = m_index[i]->get_seqno(); 585 return true; 586 } 587 } 588 return false; 589 } 590 // 591 // check that each predicate in r is matched by some predicate in premise. 592 // for now: skip multiple matches within the same rule (incomplete). 593 // match_rule(unsigned rule_index)594 bool match_rule(unsigned rule_index) { 595 clause const& g = *m_index[rule_index]; 596 m_sideconds.reset(); 597 m_subst.reset(); 598 m_subst.reserve(2, g.get_num_vars()); 599 600 IF_VERBOSE(2, g.display(verbose_stream() << "try-match\n");); 601 602 return match_head(g); 603 } 604 match_head(clause const & g)605 bool match_head(clause const& g) { 606 return 607 m_head->get_decl() == g.get_decl() && 608 m_matcher(m_head, g.get_head(), m_subst, m_sideconds) && 609 match_predicates(0, g); 610 } 611 match_predicates(unsigned predicate_index,clause const & g)612 bool match_predicates(unsigned predicate_index, clause const& g) { 613 if (predicate_index == g.get_num_predicates()) { 614 return check_substitution(g); 615 } 616 617 app* q = g.get_predicate(predicate_index); 618 619 for (unsigned i = 0; m.inc() && i < m_preds.size(); ++i) { 620 app* p = m_preds[i].get(); 621 m_subst.push_scope(); 622 unsigned limit = m_sideconds.size(); 623 IF_VERBOSE(2, 624 for (unsigned j = 0; j < predicate_index; ++j) { 625 verbose_stream() << " "; 626 } 627 verbose_stream() << mk_pp(q, m) << " = " << mk_pp(p, m) << "\n"; 628 ); 629 630 631 if (q->get_decl() == p->get_decl() && 632 m_matcher(q, p, m_subst, m_sideconds) && 633 match_predicates(predicate_index + 1, g)) { 634 return true; 635 } 636 m_subst.pop_scope(1); 637 m_sideconds.resize(limit); 638 } 639 return false; 640 } 641 check_substitution(clause const & g)642 bool check_substitution(clause const& g) { 643 unsigned deltas[2] = {0, 0}; 644 expr_ref q(m), postcond(m); 645 expr_ref_vector fmls(m_sideconds); 646 m_subst.reset_cache(); 647 648 for (unsigned i = 0; m.inc() && i < fmls.size(); ++i) { 649 m_subst.apply(2, deltas, expr_offset(fmls[i].get(), 0), q); 650 fmls[i] = q; 651 } 652 m_subst.apply(2, deltas, expr_offset(g.get_constraint(), 0), q); 653 fmls.push_back(q); 654 655 656 m_qe(m_empty_set, false, fmls); 657 flatten_and(fmls); 658 for (unsigned i = 0; i < fmls.size(); ++i) { 659 expr_ref n = normalize(fmls[i].get()); 660 if (m_sat_lits.contains(n)) { 661 return false; 662 } 663 } 664 m_rw.mk_and(fmls.size(), fmls.c_ptr(), postcond); 665 if (!m.inc()) { 666 return false; 667 } 668 if (m.is_false(postcond)) { 669 return false; 670 } 671 if (m.is_true(postcond)) { 672 return true; 673 } 674 IF_VERBOSE(2, 675 for (unsigned i = 0; i < g.get_num_predicates(); ++i) { 676 verbose_stream() << " "; 677 } 678 verbose_stream() << "check: " << mk_pp(postcond, m, 7 + g.get_num_predicates()) << "\n";); 679 680 if (!is_ground(postcond)) { 681 IF_VERBOSE(1, verbose_stream() << "TBD: non-ground\n" 682 << mk_pp(postcond, m) << "\n"; 683 m_clause->display(verbose_stream()); 684 verbose_stream() << "\n=>\n"; 685 g.display(verbose_stream()); 686 verbose_stream() << "\n";); 687 return false; 688 } 689 postcond = m.mk_not(postcond); 690 m_solver.push(); 691 m_solver.assert_expr(postcond); 692 lbool is_sat = m_solver.check(); 693 if (is_sat == l_true) { 694 expr* n; 695 model_ref mdl; 696 m_solver.get_model(mdl); 697 for (unsigned i = 0; i < fmls.size(); ++i) { 698 n = fmls[i].get(); 699 if (mdl->is_false(n)) { 700 m_refs.push_back(normalize(n)); 701 m_sat_lits.insert(m_refs.back()); 702 } 703 } 704 } 705 m_solver.pop(1); 706 return is_sat == l_false; 707 } 708 normalize(expr * e)709 expr_ref normalize(expr* e) { 710 expr* x, *y; 711 if (m.is_eq(e, x, y) && x->get_id() > y->get_id()) { 712 return expr_ref(m.mk_eq(y, x), m); 713 } 714 else { 715 return expr_ref(e, m); 716 } 717 } 718 }; 719 720 721 // predicate selection strategy. 722 class selection { 723 enum strategy { 724 WEIGHT_SELECT, 725 BASIC_WEIGHT_SELECT, 726 FIRST_SELECT, 727 VAR_USE_SELECT 728 }; 729 typedef svector<double> double_vector; 730 typedef obj_map<func_decl, double_vector> score_map; 731 typedef obj_map<app, double> pred_map; 732 ast_manager& m; 733 datatype_util dt; 734 score_map m_score_map; 735 double_vector m_scores; 736 double_vector m_var_scores; 737 strategy m_strategy; 738 pred_map m_pred_map; 739 expr_ref_vector m_refs; 740 double m_weight_multiply; 741 unsigned m_update_frequency; 742 unsigned m_next_update; 743 744 745 public: selection(datalog::context & ctx)746 selection(datalog::context& ctx): 747 m(ctx.get_manager()), 748 dt(m), 749 m_refs(m), 750 m_weight_multiply(1.0), 751 m_update_frequency(20), 752 m_next_update(20) { 753 set_strategy(ctx.tab_selection()); 754 } 755 init(rules const & rs)756 void init(rules const& rs) { 757 reset(); 758 double_vector& scores = m_scores; 759 rules::iterator it = rs.begin(), end = rs.end(); 760 for (; it != end; ++it) { 761 ref<clause> g = *it; 762 app* p = g->get_head(); 763 scores.reset(); 764 basic_score_predicate(p, scores); 765 insert_score(p->get_decl(), scores); 766 } 767 normalize_scores(rs); 768 } 769 select(clause const & g)770 unsigned select(clause const& g) { 771 switch(m_strategy) { 772 case WEIGHT_SELECT: 773 return weight_select(g); 774 case BASIC_WEIGHT_SELECT: 775 return basic_weight_select(g); 776 case FIRST_SELECT: 777 return trivial_select(g); 778 case VAR_USE_SELECT: 779 return andrei_select(g); 780 default: 781 return weight_select(g); 782 783 } 784 } 785 reset()786 void reset() { 787 m_score_map.reset(); 788 m_scores.reset(); 789 m_var_scores.reset(); 790 } 791 792 private: 793 794 // determine if constructors in p are matches by rules. is_reductive(app * p,double_vector const & p_scores)795 bool is_reductive(app* p, double_vector const& p_scores) { 796 func_decl* f = p->get_decl(); 797 score_map::obj_map_entry* e = m_score_map.find_core(f); 798 if (!e) { 799 return false; 800 } 801 double_vector const& scores = e->get_data().m_value; 802 SASSERT(scores.size() == p->get_num_args()); 803 bool has_reductive = false; 804 bool is_red = true; 805 for (unsigned i = 0; is_red && i < scores.size(); ++i) { 806 if (scores[i] >= 1) { 807 has_reductive = true; 808 is_red &= p_scores[i] >= 1; 809 } 810 } 811 return has_reductive && is_red; 812 } 813 set_strategy(symbol const & str)814 void set_strategy(symbol const& str) { 815 if (str == symbol("weight")) { 816 m_strategy = WEIGHT_SELECT; 817 } 818 if (str == symbol("basic-weight")) { 819 m_strategy = BASIC_WEIGHT_SELECT; 820 } 821 else if (str == symbol("first")) { 822 m_strategy = FIRST_SELECT; 823 } 824 else if (str == symbol("var-use")) { 825 m_strategy = VAR_USE_SELECT; 826 } 827 else { 828 m_strategy = WEIGHT_SELECT; 829 } 830 } 831 trivial_select(clause const & g)832 unsigned trivial_select(clause const& g) { 833 return 0; 834 } 835 andrei_select(clause const & g)836 unsigned andrei_select(clause const& g) { 837 score_variables(g); 838 double_vector& scores = m_scores; 839 double max_score = 0; 840 unsigned result = 0; 841 for (unsigned i = 0; i < g.get_num_predicates(); ++i) { 842 scores.reset(); 843 double_vector p_scores; 844 double score = 0; 845 app* p = g.get_predicate(i); 846 basic_score_predicate(p, scores); 847 m_score_map.find(p->get_decl(), p_scores); 848 SASSERT(p_scores.empty() || p->get_num_args() == p_scores.size()); 849 p_scores.resize(p->get_num_args()); 850 for (unsigned j = 0; j < p->get_num_args(); ++j) { 851 if (is_var(p->get_arg(j))) { 852 unsigned idx = to_var(p->get_arg(j))->get_idx(); 853 score += m_var_scores[idx]; 854 } 855 else { 856 IF_VERBOSE(2, verbose_stream() << p_scores[j] << " " << scores[j] << "\n";); 857 score += p_scores[j]*scores[j]; 858 } 859 } 860 IF_VERBOSE(2, verbose_stream() << "score: " << mk_pp(p, m) << " " << score << "\n";); 861 if (score > max_score) { 862 max_score = score; 863 result = i; 864 } 865 } 866 IF_VERBOSE(1, verbose_stream() << "select:" << result << "\n";); 867 868 return result; 869 } 870 basic_weight_select(clause const & g)871 unsigned basic_weight_select(clause const& g) { 872 double max_score = 0; 873 unsigned result = 0; 874 for (unsigned i = 0; i < g.get_num_predicates(); ++i) { 875 app* p = g.get_predicate(i); 876 double score = basic_score_predicate(p); 877 IF_VERBOSE(2, verbose_stream() << "score: " << mk_pp(p, m) << " " << score << "\n";); 878 if (score > max_score) { 879 max_score = score; 880 result = i; 881 } 882 } 883 IF_VERBOSE(2, verbose_stream() << "select " << result << "\n";); 884 return result; 885 } 886 weight_select(clause const & g)887 unsigned weight_select(clause const& g) { 888 prepare_weight_select(); 889 double max_score = 0; 890 unsigned result = 0; 891 for (unsigned i = 0; i < g.get_num_predicates(); ++i) { 892 app* p = g.get_predicate(i); 893 double score = score_predicate(p); 894 IF_VERBOSE(2, verbose_stream() << "score: " << mk_pp(p, m) << " " << score << "\n";); 895 if (score > max_score) { 896 max_score = score; 897 result = i; 898 } 899 } 900 IF_VERBOSE(2, verbose_stream() << "select " << result << "\n";); 901 return result; 902 } 903 904 score_variables(clause const & g)905 void score_variables(clause const& g) { 906 m_var_scores.reset(); 907 for (unsigned i = 0; i < g.get_num_predicates(); ++i) { 908 app* p = g.get_predicate(i); 909 score_variables(p); 910 } 911 } 912 score_variables(app * p)913 void score_variables(app* p) { 914 score_map::obj_map_entry* e = m_score_map.find_core(p->get_decl()); 915 if (!e) { 916 return; 917 } 918 double_vector& scores = e->get_data().m_value; 919 for (unsigned i = 0; i < p->get_num_args(); ++i) { 920 if (is_var(p->get_arg(i))) { 921 unsigned idx = to_var(p->get_arg(i))->get_idx(); 922 if (m_var_scores.size() <= idx) { 923 m_var_scores.resize(idx+1); 924 } 925 m_var_scores[idx] += scores[i]; 926 } 927 } 928 } 929 normalize_scores(rules const & rs)930 void normalize_scores(rules const& rs) { 931 ptr_vector<func_decl> decls; 932 rs.get_decls(decls); 933 for (unsigned i = 0; i < decls.size(); ++i) { 934 unsigned nr = rs.get_num_rules(decls[i]); 935 score_map::obj_map_entry& e = *m_score_map.find_core(decls[i]); 936 double_vector& scores = e.get_data().m_value; 937 for (unsigned j = 0; j < scores.size(); ++j) { 938 scores[j] = scores[j]/nr; 939 } 940 } 941 } 942 basic_score_predicate(app * p)943 double basic_score_predicate(app* p) { 944 double score = 1; 945 for (unsigned i = 0; i < p->get_num_args(); ++i) { 946 score += score_argument(p->get_arg(i)); 947 } 948 return score; 949 } 950 basic_score_predicate(app * p,double_vector & scores)951 void basic_score_predicate(app* p, double_vector& scores) { 952 for (unsigned i = 0; i < p->get_num_args(); ++i) { 953 scores.push_back(score_argument(p->get_arg(i))); 954 } 955 } 956 957 score_predicate(app * p)958 double score_predicate(app* p) { 959 double score = 1; 960 if (find_score(p, score)) { 961 return score; 962 } 963 for (unsigned i = 0; i < p->get_num_args(); ++i) { 964 score += score_argument(p->get_arg(i)); 965 } 966 score = adjust_score(score); 967 insert_score(p, score); 968 return score; 969 } 970 score_argument(expr * arg)971 unsigned score_argument(expr* arg) { 972 unsigned score = 0; 973 score_argument(arg, score, 20); 974 return score; 975 } 976 score_argument(expr * arg,unsigned & score,unsigned max_score)977 void score_argument(expr* arg, unsigned& score, unsigned max_score) { 978 if (score < max_score && is_app(arg)) { 979 app* a = to_app(arg); 980 if (dt.is_constructor(a->get_decl())) { 981 score += 1; 982 for (unsigned i = 0; i < a->get_num_args(); ++i) { 983 score_argument(a->get_arg(i), score, max_score); 984 } 985 } 986 else if (m.is_value(a)) { 987 ++score; 988 } 989 } 990 } 991 prepare_weight_select()992 void prepare_weight_select() { 993 SASSERT(m_next_update > 0); 994 --m_next_update; 995 if (m_next_update == 0) { 996 if (m_update_frequency >= (1 << 16)) { 997 m_update_frequency = 20; 998 m_weight_multiply = 1.0; 999 } 1000 m_update_frequency *= 11; 1001 m_update_frequency /= 10; 1002 m_next_update = m_update_frequency; 1003 m_weight_multiply *= 1.1; 1004 } 1005 } 1006 find_score(app * p,double & score)1007 bool find_score(app* p, double& score) { 1008 return m_pred_map.find(p, score); 1009 } 1010 adjust_score(double score)1011 double adjust_score(double score) { 1012 return score/m_weight_multiply; 1013 } 1014 insert_score(app * p,double score)1015 void insert_score(app* p, double score) { 1016 m_pred_map.insert(p, score); 1017 m_refs.push_back(p); 1018 } 1019 insert_score(func_decl * f,double_vector const & scores)1020 void insert_score(func_decl* f, double_vector const& scores) { 1021 score_map::obj_map_entry* e = m_score_map.find_core(f); 1022 if (e) { 1023 double_vector & old_scores = e->get_data().m_value; 1024 SASSERT(scores.size() == old_scores.size()); 1025 for (unsigned i = 0; i < scores.size(); ++i) { 1026 old_scores[i] += scores[i]; 1027 } 1028 } 1029 else { 1030 m_score_map.insert(f, scores); 1031 } 1032 } 1033 }; 1034 1035 class unifier { 1036 ast_manager& m; 1037 ::unifier m_unifier; 1038 substitution m_S1; 1039 var_subst m_S2; 1040 expr_ref_vector m_rename; 1041 expr_ref_vector m_sub1; 1042 expr_ref_vector m_sub2; 1043 public: unifier(ast_manager & m)1044 unifier(ast_manager& m): 1045 m(m), 1046 m_unifier(m), 1047 m_S1(m), 1048 m_S2(m, false), 1049 m_rename(m), 1050 m_sub1(m), 1051 m_sub2(m) {} 1052 operator ()(ref<clause> & tgt,unsigned idx,ref<clause> & src,bool compute_subst,ref<clause> & result)1053 bool operator()(ref<clause>& tgt, unsigned idx, ref<clause>& src, bool compute_subst, ref<clause>& result) { 1054 return unify(*tgt, idx, *src, compute_subst, result); 1055 } 1056 get_rule_subst(bool is_tgt)1057 expr_ref_vector get_rule_subst(bool is_tgt) { 1058 if (is_tgt) { 1059 return m_sub1; 1060 } 1061 else { 1062 return m_sub2; 1063 } 1064 } 1065 unify(clause const & tgt,unsigned idx,clause const & src,bool compute_subst,ref<clause> & result)1066 bool unify(clause const& tgt, unsigned idx, clause const& src, bool compute_subst, ref<clause>& result) { 1067 qe_lite qe(m, params_ref()); 1068 reset(); 1069 SASSERT(tgt.get_predicate(idx)->get_decl() == src.get_decl()); 1070 unsigned var_cnt = std::max(tgt.get_num_vars(), src.get_num_vars()); 1071 m_S1.reserve(2, var_cnt); 1072 if (!m_unifier(tgt.get_predicate(idx), src.get_head(), m_S1)) { 1073 return false; 1074 } 1075 app_ref_vector predicates(m); 1076 expr_ref tmp(m), tmp2(m), constraint(m); 1077 app_ref head(m); 1078 result = alloc(clause, m); 1079 unsigned delta[2] = { 0, var_cnt }; 1080 m_S1.apply(2, delta, expr_offset(tgt.get_head(), 0), tmp); 1081 head = to_app(tmp); 1082 for (unsigned i = 0; i < tgt.get_num_predicates(); ++i) { 1083 if (i != idx) { 1084 m_S1.apply(2, delta, expr_offset(tgt.get_predicate(i), 0), tmp); 1085 predicates.push_back(to_app(tmp)); 1086 } 1087 else { 1088 for (unsigned j = 0; j < src.get_num_predicates(); ++j) { 1089 m_S1.apply(2, delta, expr_offset(src.get_predicate(j), 1), tmp); 1090 predicates.push_back(to_app(tmp)); 1091 } 1092 } 1093 } 1094 m_S1.apply(2, delta, expr_offset(tgt.get_constraint(), 0), tmp); 1095 m_S1.apply(2, delta, expr_offset(src.get_constraint(), 1), tmp2); 1096 constraint = m.mk_and(tmp, tmp2); 1097 1098 // perform trivial quantifier-elimination: 1099 uint_set index_set; 1100 expr_free_vars fv; 1101 fv(head); 1102 for (unsigned i = 0; i < predicates.size(); ++i) { 1103 fv.accumulate(predicates[i].get()); 1104 } 1105 for (unsigned i = 0; i < fv.size(); ++i) { 1106 if (fv[i]) { 1107 index_set.insert(i); 1108 } 1109 } 1110 qe(index_set, false, constraint); 1111 if (m.is_false(constraint)) { 1112 return false; 1113 } 1114 1115 // initialize rule. 1116 result->init(head, predicates, constraint); 1117 ptr_vector<sort> vars; 1118 result->get_free_vars(vars); 1119 bool change = false; 1120 var_ref w(m); 1121 for (unsigned i = 0, j = 0; i < vars.size(); ++i) { 1122 if (vars[i]) { 1123 w = m.mk_var(j, vars[i]); 1124 m_rename.push_back(w); 1125 ++j; 1126 } 1127 else { 1128 change = true; 1129 m_rename.push_back(nullptr); 1130 } 1131 } 1132 if (change) { 1133 constraint = m_S2(result->get_constraint(), m_rename.size(), m_rename.c_ptr()); 1134 for (unsigned i = 0; i < result->get_num_predicates(); ++i) { 1135 tmp = m_S2(result->get_predicate(i), m_rename.size(), m_rename.c_ptr()); 1136 predicates[i] = to_app(tmp); 1137 } 1138 tmp = m_S2(result->get_head(), m_rename.size(), m_rename.c_ptr()); 1139 head = to_app(tmp); 1140 result->init(head, predicates, constraint); 1141 } 1142 if (compute_subst) { 1143 extract_subst(delta, tgt, 0); 1144 extract_subst(delta, src, 1); 1145 } 1146 // init result using head, predicates, constraint 1147 return true; 1148 } 1149 1150 1151 private: reset()1152 void reset() { 1153 m_S1.reset(); 1154 m_S2.reset(); 1155 m_rename.reset(); 1156 m_sub1.reset(); 1157 m_sub2.reset(); 1158 } 1159 extract_subst(unsigned const * delta,clause const & g,unsigned offset)1160 void extract_subst(unsigned const* delta, clause const& g, unsigned offset) { 1161 ptr_vector<sort> vars; 1162 var_ref v(m); 1163 expr_ref tmp(m); 1164 g.get_free_vars(vars); 1165 for (unsigned i = 0; i < vars.size(); ++i) { 1166 if (vars[i]) { 1167 v = m.mk_var(i, vars[i]); 1168 m_S1.apply(2, delta, expr_offset(v, offset), tmp); 1169 tmp = m_S2(tmp, m_rename.size(), m_rename.c_ptr()); 1170 insert_subst(offset, tmp); 1171 } 1172 else { 1173 insert_subst(offset, m.mk_true()); 1174 } 1175 } 1176 } 1177 insert_subst(unsigned offset,expr * e)1178 void insert_subst(unsigned offset, expr* e) { 1179 if (offset == 0) { 1180 m_sub1.push_back(e); 1181 } 1182 else { 1183 m_sub2.push_back(e); 1184 } 1185 } 1186 }; 1187 1188 1189 1190 class extract_delta { 1191 ast_manager& m; 1192 unifier m_unifier; 1193 public: extract_delta(ast_manager & m)1194 extract_delta(ast_manager& m): 1195 m(m), 1196 m_unifier(m) 1197 {} 1198 1199 1200 // 1201 // Given a clause 1202 // P(s) :- P(t), Phi(x). 1203 // Compute the clauses: 1204 // acc: P(s) :- Delta(z,t), P(z), Phi(x). 1205 // delta1: Delta(z,z). 1206 // delta2: Delta(z,s) :- Delta(z,t), Phi(x). 1207 // 1208 mk_delta_clauses(clause const & g,ref<clause> & acc,ref<clause> & delta1,ref<clause> & delta2)1209 void mk_delta_clauses(clause const& g, ref<clause>& acc, ref<clause>& delta1, ref<clause>& delta2) { 1210 SASSERT(g.get_num_predicates() > 0); 1211 app* p = g.get_head(); 1212 app* q = g.get_predicate(0); 1213 SASSERT(p->get_decl() == q->get_decl()); 1214 expr_ref_vector zs = mk_fresh_vars(g); 1215 expr_ref_vector zszs(m); 1216 func_decl_ref delta(m); 1217 sort_ref_vector dom(m); 1218 for (unsigned j = 0; j < 1; ++j) { 1219 for (unsigned i = 0; i < zs.size(); ++i) { 1220 dom.push_back(m.get_sort(zs[i].get())); 1221 zszs.push_back(zs[i].get()); 1222 } 1223 } 1224 app_ref_vector preds(m); 1225 delta = m.mk_fresh_func_decl("Delta", dom.size(), dom.c_ptr(), m.mk_bool_sort()); 1226 acc = alloc(clause, m); 1227 delta1 = alloc(clause, m); 1228 delta2 = alloc(clause, m); 1229 delta1->init(m.mk_app(delta, zszs.size(), zszs.c_ptr()), preds, m.mk_true()); 1230 for (unsigned i = 0; i < zs.size(); ++i) { 1231 zszs[i+zs.size()] = p->get_arg(i); 1232 } 1233 app_ref head(m), pred(m); 1234 head = m.mk_app(delta, zszs.size(), zszs.c_ptr()); 1235 for (unsigned i = 0; i < zs.size(); ++i) { 1236 zszs[i+zs.size()] = q->get_arg(i); 1237 } 1238 pred = m.mk_app(delta, zszs.size(), zszs.c_ptr()); 1239 preds.push_back(pred); 1240 for (unsigned i = 1; i < g.get_num_predicates(); ++i) { 1241 preds.push_back(g.get_predicate(i)); 1242 } 1243 delta2->init(head, preds, g.get_constraint()); 1244 preds.push_back(m.mk_app(q->get_decl(), zs.size(), zs.c_ptr())); 1245 acc->init(p, preds, g.get_constraint()); 1246 1247 IF_VERBOSE(1, 1248 delta1->display(verbose_stream() << "delta1:\n"); 1249 delta2->display(verbose_stream() << "delta2:\n"); 1250 acc->display(verbose_stream() << "acc:\n");); 1251 } 1252 1253 // 1254 // Given a sequence of clauses and inference rules 1255 // compute a super-predicate and auxiliary clauses. 1256 // 1257 // P1(x) :- P2(y), R(z) 1258 // P2(y) :- P3(z), T(u) 1259 // P3(z) :- P1(x), U(v) 1260 // => 1261 // P1(x) :- P1(x), R(z), T(u), U(v) 1262 // 1263 resolve_rules(unsigned num_clauses,clause * const * clauses,unsigned const * positions)1264 ref<clause> resolve_rules(unsigned num_clauses, clause*const* clauses, unsigned const* positions) { 1265 ref<clause> result = clauses[0]; 1266 ref<clause> tmp; 1267 unsigned offset = 0; 1268 for (unsigned i = 0; i + 1 < num_clauses; ++i) { 1269 clause const& cl = *clauses[i+1]; 1270 offset += positions[i]; 1271 VERIFY (m_unifier.unify(*result, offset, cl, false, tmp)); 1272 result = tmp; 1273 } 1274 return result; 1275 } 1276 1277 1278 private: 1279 mk_fresh_vars(clause const & g)1280 expr_ref_vector mk_fresh_vars(clause const& g) { 1281 expr_ref_vector result(m); 1282 app* p = g.get_head(); 1283 unsigned num_vars = g.get_num_vars(); 1284 for (unsigned i = 0; i < p->get_num_args(); ++i) { 1285 result.push_back(m.mk_var(num_vars+i, m.get_sort(p->get_arg(i)))); 1286 } 1287 return result; 1288 } 1289 }; 1290 1291 enum instruction { 1292 SELECT_RULE, 1293 SELECT_PREDICATE, 1294 BACKTRACK, 1295 SATISFIABLE, 1296 UNSATISFIABLE, 1297 CANCEL 1298 }; 1299 operator <<(std::ostream & out,instruction i)1300 std::ostream& operator<<(std::ostream& out, instruction i) { 1301 switch(i) { 1302 case SELECT_RULE: return out << "select-rule"; 1303 case SELECT_PREDICATE: return out << "select-predicate"; 1304 case BACKTRACK: return out << "backtrack"; 1305 case SATISFIABLE: return out << "sat"; 1306 case UNSATISFIABLE: return out << "unsat"; 1307 case CANCEL: return out << "cancel"; 1308 } 1309 return out << "unmatched instruction"; 1310 } 1311 }; 1312 1313 namespace datalog { 1314 1315 class tab::imp { 1316 struct stats { statsdatalog::tab::imp::stats1317 stats() { reset(); } resetdatalog::tab::imp::stats1318 void reset() { memset(this, 0, sizeof(*this)); } 1319 unsigned m_num_unfold; 1320 unsigned m_num_no_unfold; 1321 unsigned m_num_subsumed; 1322 }; 1323 1324 context& m_ctx; 1325 ast_manager& m; 1326 rule_manager& rm; 1327 tb::index m_index; 1328 tb::selection m_selection; 1329 smt_params m_fparams; 1330 smt::kernel m_solver; 1331 mutable tb::unifier m_unifier; 1332 tb::rules m_rules; 1333 vector<ref<tb::clause> > m_clauses; 1334 unsigned m_seqno; 1335 tb::instruction m_instruction; 1336 lbool m_status; 1337 stats m_stats; 1338 uint_set m_displayed_rules; 1339 public: imp(context & ctx)1340 imp(context& ctx): 1341 m_ctx(ctx), 1342 m(ctx.get_manager()), 1343 rm(ctx.get_rule_manager()), 1344 m_index(m), 1345 m_selection(ctx), 1346 m_solver(m, m_fparams), 1347 m_unifier(m), 1348 m_rules(), 1349 m_seqno(0), 1350 m_instruction(tb::SELECT_PREDICATE), 1351 m_status(l_undef) 1352 { 1353 // m_fparams.m_relevancy_lvl = 0; 1354 m_fparams.m_mbqi = false; 1355 } 1356 ~imp()1357 ~imp() {} 1358 query(expr * query)1359 lbool query(expr* query) { 1360 m_ctx.ensure_opened(); 1361 m_index.reset(); 1362 m_selection.reset(); 1363 m_displayed_rules.reset(); 1364 m_rules.init(m_ctx.get_rules()); 1365 m_selection.init(m_rules); 1366 rule_set query_rules(m_ctx); 1367 rule_ref clause(rm); 1368 rm.mk_query(query, query_rules); 1369 clause = query_rules.last(); 1370 ref<tb::clause> g = alloc(tb::clause, m); 1371 g->init(clause); 1372 g->set_head(m.mk_false()); 1373 init_clause(g); 1374 IF_VERBOSE(1, display_clause(*get_clause(), verbose_stream() << "g" << get_clause()->get_seqno() << " ");); 1375 return run(); 1376 } 1377 cleanup()1378 void cleanup() { 1379 m_clauses.reset(); 1380 } 1381 reset_statistics()1382 void reset_statistics() { 1383 m_stats.reset(); 1384 } 1385 collect_statistics(statistics & st) const1386 void collect_statistics(statistics& st) const { 1387 st.update("tab.num_unfold", m_stats.m_num_unfold); 1388 st.update("tab.num_unfold_fail", m_stats.m_num_no_unfold); 1389 st.update("tab.num_subsumed", m_stats.m_num_subsumed); 1390 } 1391 display_certificate(std::ostream & out) const1392 void display_certificate(std::ostream& out) const { 1393 expr_ref ans = get_answer(); 1394 out << mk_pp(ans, m) << "\n"; 1395 } 1396 get_answer() const1397 expr_ref get_answer() const { 1398 switch(m_status) { 1399 case l_undef: 1400 UNREACHABLE(); 1401 return expr_ref(m.mk_false(), m); 1402 case l_true: { 1403 proof_ref pr = get_proof(); 1404 return expr_ref(pr.get(), m); 1405 } 1406 case l_false: 1407 // NOT_IMPLEMENTED_YET(); 1408 return expr_ref(m.mk_true(), m); 1409 } 1410 UNREACHABLE(); 1411 return expr_ref(m.mk_true(), m); 1412 } 1413 private: 1414 select_predicate()1415 void select_predicate() { 1416 tb::clause & g = *get_clause(); 1417 unsigned num_predicates = g.get_num_predicates(); 1418 if (num_predicates == 0) { 1419 m_instruction = tb::UNSATISFIABLE; 1420 IF_VERBOSE(2, g.display(verbose_stream()); ); 1421 } 1422 else { 1423 m_instruction = tb::SELECT_RULE; 1424 unsigned pi = m_selection.select(g); 1425 g.set_predicate_index(pi); 1426 IF_VERBOSE(2, verbose_stream() << mk_pp(g.get_predicate(pi), m) << "\n";); 1427 } 1428 } 1429 apply_rule(ref<tb::clause> & r)1430 void apply_rule(ref<tb::clause>& r) { 1431 ref<tb::clause> clause = get_clause(); 1432 ref<tb::clause> next_clause; 1433 if (m_unifier(clause, clause->get_predicate_index(), r, false, next_clause) && 1434 !query_is_tautology(*next_clause)) { 1435 init_clause(next_clause); 1436 unsigned subsumer = 0; 1437 IF_VERBOSE(1, 1438 display_rule(*clause, verbose_stream()); 1439 display_premise(*clause, 1440 verbose_stream() << "g" << next_clause->get_seqno() << " "); 1441 display_clause(*next_clause, verbose_stream()); 1442 ); 1443 if (m_index.is_subsumed(next_clause, subsumer)) { 1444 IF_VERBOSE(1, verbose_stream() << "subsumed by g" << subsumer << "\n";); 1445 m_stats.m_num_subsumed++; 1446 m_clauses.pop_back(); 1447 m_instruction = tb::SELECT_RULE; 1448 } 1449 else { 1450 m_stats.m_num_unfold++; 1451 next_clause->set_parent(clause); 1452 m_index.insert(next_clause); 1453 m_instruction = tb::SELECT_PREDICATE; 1454 } 1455 } 1456 else { 1457 m_stats.m_num_no_unfold++; 1458 m_instruction = tb::SELECT_RULE; 1459 } 1460 } 1461 select_rule()1462 void select_rule() { 1463 tb::clause& g = *get_clause(); 1464 g.inc_next_rule(); 1465 unsigned pi = g.get_predicate_index(); 1466 func_decl* p = g.get_predicate(pi)->get_decl(); 1467 unsigned num_rules = m_rules.get_num_rules(p); 1468 unsigned index = g.get_next_rule(); 1469 if (num_rules <= index) { 1470 m_instruction = tb::BACKTRACK; 1471 } 1472 else { 1473 ref<tb::clause> rl = m_rules.get_rule(p, index); 1474 apply_rule(rl); 1475 } 1476 } 1477 backtrack()1478 void backtrack() { 1479 SASSERT(!m_clauses.empty()); 1480 m_clauses.pop_back(); 1481 if (m_clauses.empty()) { 1482 m_instruction = tb::SATISFIABLE; 1483 } 1484 else { 1485 m_instruction = tb::SELECT_RULE; 1486 } 1487 } 1488 run()1489 lbool run() { 1490 m_instruction = tb::SELECT_PREDICATE; 1491 m_status = l_undef; 1492 while (true) { 1493 IF_VERBOSE(2, verbose_stream() << m_instruction << "\n";); 1494 if (!m.inc()) { 1495 cleanup(); 1496 return l_undef; 1497 } 1498 switch(m_instruction) { 1499 case tb::SELECT_PREDICATE: 1500 select_predicate(); 1501 break; 1502 case tb::SELECT_RULE: 1503 select_rule(); 1504 break; 1505 case tb::BACKTRACK: 1506 backtrack(); 1507 break; 1508 case tb::SATISFIABLE: 1509 m_status = l_false; 1510 return l_false; 1511 case tb::UNSATISFIABLE: 1512 m_status = l_true; 1513 IF_VERBOSE(1, display_certificate(verbose_stream());); 1514 return l_true; 1515 case tb::CANCEL: 1516 cleanup(); 1517 m_status = l_undef; 1518 return l_undef; 1519 } 1520 } 1521 } 1522 query_is_tautology(tb::clause const & g)1523 bool query_is_tautology(tb::clause const& g) { 1524 expr_ref fml = g.to_formula(); 1525 fml = m.mk_not(fml); 1526 m_solver.push(); 1527 m_solver.assert_expr(fml); 1528 lbool is_sat = m_solver.check(); 1529 m_solver.pop(1); 1530 1531 TRACE("dl", tout << is_sat << ":\n" << mk_pp(fml, m) << "\n";); 1532 1533 return l_false == is_sat; 1534 1535 } 1536 1537 init_clause(ref<tb::clause> & clause)1538 void init_clause(ref<tb::clause>& clause) { 1539 clause->set_index(m_clauses.size()); 1540 clause->set_seqno(m_seqno++); 1541 m_clauses.push_back(clause); 1542 } 1543 get_clause() const1544 ref<tb::clause> get_clause() const { return m_clauses.back(); } 1545 1546 display_rule(tb::clause const & p,std::ostream & out)1547 void display_rule(tb::clause const& p, std::ostream& out) { 1548 func_decl* f = p.get_predicate(p.get_predicate_index())->get_decl(); 1549 ref<tb::clause> rl = m_rules.get_rule(f, p.get_next_rule()); 1550 unsigned idx = rl->get_index(); 1551 if (!m_displayed_rules.contains(idx)) { 1552 m_displayed_rules.insert(idx); 1553 rl->display(out << "r" << p.get_next_rule() << ": "); 1554 } 1555 } 1556 display_premise(tb::clause & p,std::ostream & out)1557 void display_premise(tb::clause& p, std::ostream& out) { 1558 func_decl* f = p.get_predicate(p.get_predicate_index())->get_decl(); 1559 out << "{g" << p.get_seqno() << " " << f->get_name() << " pos: " 1560 << p.get_predicate_index() << " rule: " << p.get_next_rule() << "}\n"; 1561 } 1562 display_clause(tb::clause & g,std::ostream & out)1563 void display_clause(tb::clause& g, std::ostream& out) { 1564 g.display(out); 1565 } 1566 get_proof() const1567 proof_ref get_proof() const { 1568 scoped_proof sp(m); 1569 proof_ref pr(m); 1570 proof_ref_vector prs(m); 1571 ref<tb::clause> clause = get_clause(); 1572 ref<tb::clause> replayed_clause; 1573 replace_proof_converter pc(m); 1574 1575 // clause is a empty clause. 1576 // Pretend it is asserted. 1577 // It gets replaced by premises. 1578 SASSERT(clause->get_num_predicates() == 0); 1579 expr_ref root = clause->to_formula(); 1580 1581 vector<expr_ref_vector> substs; 1582 while (0 != clause->get_index()) { 1583 SASSERT(clause->get_parent_index() < clause->get_index()); 1584 unsigned p_index = clause->get_parent_index(); 1585 unsigned p_rule = clause->get_parent_rule(); 1586 ref<tb::clause> parent = m_clauses[p_index]; 1587 unsigned pi = parent->get_predicate_index(); 1588 func_decl* pred = parent->get_predicate(pi)->get_decl(); 1589 ref<tb::clause> rl = m_rules.get_rule(pred, p_rule); 1590 VERIFY(m_unifier(parent, parent->get_predicate_index(), rl, true, replayed_clause)); 1591 expr_ref_vector s1(m_unifier.get_rule_subst(true)); 1592 expr_ref_vector s2(m_unifier.get_rule_subst(false)); 1593 resolve_rule(pc, *parent, *rl, s1, s2, *clause); 1594 clause = parent; 1595 substs.push_back(s1); 1596 } 1597 IF_VERBOSE(1, display_body_insts(substs, *clause, verbose_stream());); 1598 1599 pc.invert(); 1600 prs.push_back(m.mk_asserted(root)); 1601 pr = pc(m, 1, prs.c_ptr()); 1602 return pr; 1603 } 1604 display_body_insts(vector<expr_ref_vector> const & substs,tb::clause const & clause,std::ostream & out) const1605 void display_body_insts(vector<expr_ref_vector> const& substs, tb::clause const& clause, std::ostream& out) const { 1606 expr_ref_vector subst(m); 1607 for (unsigned i = substs.size(); i > 0; ) { 1608 --i; 1609 apply_subst(subst, substs[i]); 1610 } 1611 expr_ref body = clause.get_body(); 1612 var_subst vs(m, false); 1613 body = vs(body, subst.size(), subst.c_ptr()); 1614 out << body << "\n"; 1615 } 1616 resolve_rule(replace_proof_converter & pc,tb::clause const & r1,tb::clause const & r2,expr_ref_vector const & s1,expr_ref_vector const & s2,tb::clause const & res) const1617 void resolve_rule(replace_proof_converter& pc, tb::clause const& r1, tb::clause const& r2, 1618 expr_ref_vector const& s1, expr_ref_vector const& s2, tb::clause const& res) const { 1619 unsigned idx = r1.get_predicate_index(); 1620 expr_ref fml = res.to_formula(); 1621 vector<expr_ref_vector> substs; 1622 svector<std::pair<unsigned, unsigned> > positions; 1623 substs.push_back(s1); 1624 substs.push_back(s2); 1625 scoped_proof _sc(m); 1626 proof_ref pr(m); 1627 proof_ref_vector premises(m); 1628 premises.push_back(m.mk_asserted(r1.to_formula())); 1629 premises.push_back(m.mk_asserted(r2.to_formula())); 1630 positions.push_back(std::make_pair(idx+1, 0)); 1631 pr = m.mk_hyper_resolve(2, premises.c_ptr(), fml, positions, substs); 1632 pc.insert(pr); 1633 } 1634 }; 1635 tab(context & ctx)1636 tab::tab(context& ctx): 1637 datalog::engine_base(ctx.get_manager(),"tabulation"), 1638 m_imp(alloc(imp, ctx)) { 1639 } ~tab()1640 tab::~tab() { 1641 dealloc(m_imp); 1642 } query(expr * query)1643 lbool tab::query(expr* query) { 1644 return m_imp->query(query); 1645 } cleanup()1646 void tab::cleanup() { 1647 m_imp->cleanup(); 1648 } reset_statistics()1649 void tab::reset_statistics() { 1650 m_imp->reset_statistics(); 1651 } collect_statistics(statistics & st) const1652 void tab::collect_statistics(statistics& st) const { 1653 m_imp->collect_statistics(st); 1654 } display_certificate(std::ostream & out) const1655 void tab::display_certificate(std::ostream& out) const { 1656 m_imp->display_certificate(out); 1657 } get_answer()1658 expr_ref tab::get_answer() { 1659 return m_imp->get_answer(); 1660 } 1661 1662 }; 1663