1 /*++ 2 Copyright (c) 2017 Microsoft Corporation 3 4 Module Name: 5 6 sat_drat.cpp 7 8 Abstract: 9 10 Produce DRAT proofs. 11 12 Check them using a very simple forward checker 13 that interacts with external plugins. 14 15 Author: 16 17 Nikolaj Bjorner (nbjorner) 2017-2-3 18 19 Notes: 20 21 --*/ 22 #include "sat_solver.h" 23 #include "sat_drat.h" 24 25 26 namespace sat { drat(solver & s)27 drat::drat(solver& s) : 28 s(s), 29 m_out(nullptr), 30 m_bout(nullptr), 31 m_inconsistent(false), 32 m_check_unsat(false), 33 m_check_sat(false), 34 m_check(false), 35 m_activity(false) 36 { 37 if (s.get_config().m_drat && s.get_config().m_drat_file.is_non_empty_string()) { 38 auto mode = s.get_config().m_drat_binary ? (std::ios_base::binary | std::ios_base::out | std::ios_base::trunc) : std::ios_base::out; 39 m_out = alloc(std::ofstream, s.get_config().m_drat_file.str(), mode); 40 if (s.get_config().m_drat_binary) 41 std::swap(m_out, m_bout); 42 } 43 } 44 ~drat()45 drat::~drat() { 46 if (m_out) m_out->flush(); 47 if (m_bout) m_bout->flush(); 48 dealloc(m_out); 49 dealloc(m_bout); 50 for (unsigned i = 0; i < m_proof.size(); ++i) { 51 clause* c = m_proof[i]; 52 if (c) 53 m_alloc.del_clause(c); 54 } 55 m_proof.reset(); 56 m_out = nullptr; 57 m_bout = nullptr; 58 } 59 updt_config()60 void drat::updt_config() { 61 m_check_unsat = s.get_config().m_drat_check_unsat; 62 m_check_sat = s.get_config().m_drat_check_sat; 63 m_check = m_check_unsat || m_check_sat; 64 m_activity = s.get_config().m_drat_activity; 65 } 66 pp(std::ostream & out,status st) const67 std::ostream& drat::pp(std::ostream& out, status st) const { 68 if (st.is_redundant()) 69 out << "l"; 70 else if (st.is_deleted()) 71 out << "d"; 72 else if (st.is_asserted()) 73 out << "a"; 74 else if (st.is_input()) 75 out << "i"; 76 77 if (!st.is_sat()) 78 out << " " << m_theory[st.get_th()]; 79 return out; 80 } 81 dump(unsigned n,literal const * c,status st)82 void drat::dump(unsigned n, literal const* c, status st) { 83 if (st.is_asserted() && !s.m_ext) 84 return; 85 if (m_activity && ((m_stats.m_num_add % 1000) == 0)) 86 dump_activity(); 87 88 char buffer[10000]; 89 char digits[20]; // enough for storing unsigned 90 char* lastd = digits + sizeof(digits); 91 92 unsigned len = 0; 93 94 if (st.is_deleted()) { 95 buffer[len++] = 'd'; 96 buffer[len++] = ' '; 97 } 98 else if (st.is_input()) { 99 buffer[len++] = 'i'; 100 buffer[len++] = ' '; 101 } 102 else if (!st.is_sat()) { 103 if (st.is_redundant()) { 104 buffer[len++] = 'r'; 105 buffer[len++] = ' '; 106 } 107 else if (st.is_asserted()) { 108 buffer[len++] = 'a'; 109 buffer[len++] = ' '; 110 } 111 } 112 113 if (!st.is_sat()) { 114 for (char ch : m_theory[st.get_th()]) 115 buffer[len++] = ch; 116 buffer[len++] = ' '; 117 } 118 for (unsigned i = 0; i < n; ++i) { 119 literal lit = c[i]; 120 unsigned v = lit.var(); 121 if (lit.sign()) buffer[len++] = '-'; 122 char* d = lastd; 123 SASSERT(v > 0); 124 while (v > 0) { 125 d--; 126 *d = (v % 10) + '0'; 127 v /= 10; 128 SASSERT(d > digits); 129 } 130 SASSERT(len + lastd < sizeof(buffer) + d); 131 memcpy(buffer + len, d, lastd - d); 132 len += static_cast<unsigned>(lastd - d); 133 buffer[len++] = ' '; 134 if (static_cast<size_t>(len) + 50 > sizeof(buffer)) { 135 m_out->write(buffer, len); 136 len = 0; 137 } 138 } 139 buffer[len++] = '0'; 140 buffer[len++] = '\n'; 141 m_out->write(buffer, len); 142 143 } 144 dump_activity()145 void drat::dump_activity() { 146 (*m_out) << "c activity "; 147 for (unsigned v = 0; v < s.num_vars(); ++v) { 148 (*m_out) << s.m_activity[v] << " "; 149 } 150 (*m_out) << "\n"; 151 } 152 bdump(unsigned n,literal const * c,status st)153 void drat::bdump(unsigned n, literal const* c, status st) { 154 unsigned char ch = 0; 155 if (st.is_redundant()) 156 ch = 'a'; 157 else if (st.is_deleted()) 158 ch = 'd'; 159 else return; 160 char buffer[10000]; 161 int len = 0; 162 buffer[len++] = ch; 163 164 for (unsigned i = 0; i < n; ++i) { 165 literal lit = c[i]; 166 unsigned v = 2 * lit.var() + (lit.sign() ? 1 : 0); 167 do { 168 ch = static_cast<unsigned char>(v & 255); 169 v >>= 7; 170 if (v) ch |= 128; 171 buffer[len++] = ch; 172 if (len == sizeof(buffer)) { 173 m_bout->write(buffer, len); 174 len = 0; 175 } 176 } while (v); 177 } 178 buffer[len++] = 0; 179 m_bout->write(buffer, len); 180 } 181 is_cleaned(clause & c) const182 bool drat::is_cleaned(clause& c) const { 183 literal last = null_literal; 184 unsigned n = c.size(); 185 for (unsigned i = 0; i < n; ++i) { 186 if (c[i] == last) return true; 187 last = c[i]; 188 } 189 return false; 190 } 191 trace(std::ostream & out,unsigned n,literal const * c,status st)192 void drat::trace(std::ostream& out, unsigned n, literal const* c, status st) { 193 pp(out, st) << " "; 194 literal last = null_literal; 195 for (unsigned i = 0; i < n; ++i) { 196 if (c[i] != last) { 197 out << c[i] << " "; 198 last = c[i]; 199 } 200 } 201 out << "\n"; 202 } 203 append(literal l,status st)204 void drat::append(literal l, status st) { 205 TRACE("sat_drat", pp(tout, st) << " " << l << "\n";); 206 207 declare(l); 208 IF_VERBOSE(20, trace(verbose_stream(), 1, &l, st);); 209 if (st.is_redundant() && st.is_sat()) 210 verify(1, &l); 211 212 if (st.is_deleted()) 213 return; 214 215 if (m_check_unsat) 216 assign_propagate(l); 217 218 m_units.push_back(l); 219 } 220 append(literal l1,literal l2,status st)221 void drat::append(literal l1, literal l2, status st) { 222 TRACE("sat_drat", pp(tout, st) << " " << l1 << " " << l2 << "\n";); 223 declare(l1); 224 declare(l2); 225 literal lits[2] = { l1, l2 }; 226 227 IF_VERBOSE(20, trace(verbose_stream(), 2, lits, st);); 228 if (st.is_deleted()) { 229 // noop 230 // don't record binary as deleted. 231 } 232 else { 233 if (st.is_redundant() && st.is_sat()) 234 verify(2, lits); 235 236 clause* c = m_alloc.mk_clause(2, lits, st.is_redundant()); 237 m_proof.push_back(c); 238 m_status.push_back(st); 239 if (!m_check_unsat) return; 240 unsigned idx = m_watched_clauses.size(); 241 m_watched_clauses.push_back(watched_clause(c, l1, l2)); 242 m_watches[(~l1).index()].push_back(idx); 243 m_watches[(~l2).index()].push_back(idx); 244 245 if (value(l1) == l_false && value(l2) == l_false) 246 m_inconsistent = true; 247 else if (value(l1) == l_false) 248 assign_propagate(l2); 249 else if (value(l2) == l_false) 250 assign_propagate(l1); 251 } 252 } 253 bool_def(bool_var v,unsigned n)254 void drat::bool_def(bool_var v, unsigned n) { 255 if (m_out) 256 (*m_out) << "b " << v << " " << n << " 0\n"; 257 } 258 def_begin(char id,unsigned n,std::string const & name)259 void drat::def_begin(char id, unsigned n, std::string const& name) { 260 if (m_out) 261 (*m_out) << id << " " << n << " " << name; 262 } 263 def_add_arg(unsigned arg)264 void drat::def_add_arg(unsigned arg) { 265 if (m_out) 266 (*m_out) << " " << arg; 267 } 268 def_end()269 void drat::def_end() { 270 if (m_out) 271 (*m_out) << " 0\n"; 272 } 273 log_adhoc(std::function<void (std::ostream &)> & fn)274 void drat::log_adhoc(std::function<void(std::ostream&)>& fn) { 275 if (m_out) 276 fn(*m_out); 277 } 278 279 280 #if 0 281 // debugging code 282 bool drat::is_clause(clause& c, literal l1, literal l2, literal l3, drat::status st1, drat::status st2) { 283 //if (st1 != st2) return false; 284 if (c.size() != 3) return false; 285 if (l1 == c[0]) { 286 if (l2 == c[1] && l3 == c[2]) return true; 287 if (l2 == c[2] && l3 == c[1]) return true; 288 } 289 if (l2 == c[0]) { 290 if (l1 == c[1] && l3 == c[2]) return true; 291 if (l1 == c[2] && l3 == c[1]) return true; 292 } 293 if (l3 == c[0]) { 294 if (l1 == c[1] && l2 == c[2]) return true; 295 if (l1 == c[2] && l2 == c[1]) return true; 296 } 297 return false; 298 } 299 #endif 300 append(clause & c,status st)301 void drat::append(clause& c, status st) { 302 TRACE("sat_drat", pp(tout, st) << " " << c << "\n";); 303 for (literal lit : c) declare(lit); 304 unsigned n = c.size(); 305 IF_VERBOSE(20, trace(verbose_stream(), n, c.begin(), st);); 306 307 if (st.is_redundant() && st.is_sat()) { 308 verify(c); 309 } 310 311 m_status.push_back(st); 312 m_proof.push_back(&c); 313 if (st.is_deleted()) { 314 if (n > 0) del_watch(c, c[0]); 315 if (n > 1) del_watch(c, c[1]); 316 return; 317 } 318 unsigned num_watch = 0; 319 literal l1, l2; 320 for (unsigned i = 0; i < n; ++i) { 321 if (value(c[i]) != l_false) { 322 if (num_watch == 0) { 323 l1 = c[i]; 324 ++num_watch; 325 } 326 else { 327 l2 = c[i]; 328 ++num_watch; 329 break; 330 } 331 } 332 } 333 switch (num_watch) { 334 case 0: 335 m_inconsistent = true; 336 break; 337 case 1: 338 assign_propagate(l1); 339 break; 340 default: { 341 SASSERT(num_watch == 2); 342 unsigned idx = m_watched_clauses.size(); 343 m_watched_clauses.push_back(watched_clause(&c, l1, l2)); 344 m_watches[(~l1).index()].push_back(idx); 345 m_watches[(~l2).index()].push_back(idx); 346 break; 347 } 348 } 349 } 350 del_watch(clause & c,literal l)351 void drat::del_watch(clause& c, literal l) { 352 watch& w = m_watches[(~l).index()]; 353 for (unsigned i = 0; i < w.size(); ++i) { 354 if (m_watched_clauses[w[i]].m_clause == &c) { 355 w[i] = w.back(); 356 w.pop_back(); 357 break; 358 } 359 } 360 } 361 declare(literal l)362 void drat::declare(literal l) { 363 if (!m_check) return; 364 unsigned n = static_cast<unsigned>(l.var()); 365 while (m_assignment.size() <= n) { 366 m_assignment.push_back(l_undef); 367 m_watches.push_back(watch()); 368 m_watches.push_back(watch()); 369 } 370 } 371 is_drup(unsigned n,literal const * c,literal_vector & units)372 bool drat::is_drup(unsigned n, literal const* c, literal_vector& units) { 373 if (m_inconsistent) 374 return true; 375 if (n == 0) 376 return false; 377 378 unsigned num_units = m_units.size(); 379 for (unsigned i = 0; !m_inconsistent && i < n; ++i) { 380 declare(c[i]); 381 assign_propagate(~c[i]); 382 } 383 384 for (unsigned i = num_units; i < m_units.size(); ++i) { 385 m_assignment[m_units[i].var()] = l_undef; 386 } 387 units.append(m_units.size() - num_units, m_units.data() + num_units); 388 m_units.shrink(num_units); 389 bool ok = m_inconsistent; 390 m_inconsistent = false; 391 return ok; 392 } 393 is_drup(unsigned n,literal const * c)394 bool drat::is_drup(unsigned n, literal const* c) { 395 if (m_inconsistent) 396 return true; 397 if (n == 0) 398 return false; 399 unsigned num_units = m_units.size(); 400 for (unsigned i = 0; !m_inconsistent && i < n; ++i) 401 assign_propagate(~c[i]); 402 403 DEBUG_CODE(if (!m_inconsistent) validate_propagation();); 404 DEBUG_CODE( 405 for (literal u : m_units) 406 SASSERT(m_assignment[u.var()] != l_undef); 407 ); 408 409 #if 0 410 if (!m_inconsistent) { 411 literal_vector lits(n, c); 412 IF_VERBOSE(0, verbose_stream() << "not drup " << lits << "\n"); 413 for (unsigned v = 0; v < m_assignment.size(); ++v) { 414 lbool val = m_assignment[v]; 415 if (val != l_undef) { 416 IF_VERBOSE(0, verbose_stream() << literal(v, false) << " |-> " << val << "\n"); 417 } 418 } 419 for (clause* cp : s.m_clauses) { 420 clause& cl = *cp; 421 bool found = false; 422 for (literal l : cl) { 423 if (m_assignment[l.var()] != (l.sign() ? l_true : l_false)) { 424 found = true; 425 break; 426 } 427 } 428 if (!found) { 429 IF_VERBOSE(0, verbose_stream() << "Clause is false under assignment: " << cl << "\n"); 430 } 431 } 432 for (clause* cp : s.m_learned) { 433 clause& cl = *cp; 434 bool found = false; 435 for (literal l : cl) { 436 if (m_assignment[l.var()] != (l.sign() ? l_true : l_false)) { 437 found = true; 438 break; 439 } 440 } 441 if (!found) { 442 IF_VERBOSE(0, verbose_stream() << "Clause is false under assignment: " << cl << "\n"); 443 } 444 } 445 svector<sat::solver::bin_clause> bin; 446 s.collect_bin_clauses(bin, true); 447 for (auto& b : bin) { 448 bool found = false; 449 if (m_assignment[b.first.var()] != (b.first.sign() ? l_true : l_false)) found = true; 450 if (m_assignment[b.second.var()] != (b.second.sign() ? l_true : l_false)) found = true; 451 if (!found) { 452 IF_VERBOSE(0, verbose_stream() << "Bin clause is false under assignment: " << b.first << " " << b.second << "\n"); 453 } 454 } 455 IF_VERBOSE(0, s.display(verbose_stream())); 456 exit(0); 457 } 458 #endif 459 460 for (unsigned i = num_units; i < m_units.size(); ++i) 461 m_assignment[m_units[i].var()] = l_undef; 462 463 m_units.shrink(num_units); 464 bool ok = m_inconsistent; 465 m_inconsistent = false; 466 return ok; 467 } 468 is_drat(unsigned n,literal const * c)469 bool drat::is_drat(unsigned n, literal const* c) { 470 return false; 471 if (m_inconsistent || n == 0) 472 return true; 473 for (unsigned i = 0; i < n; ++i) 474 if (is_drat(n, c, i)) 475 return true; 476 return false; 477 } 478 validate_propagation() const479 void drat::validate_propagation() const { 480 for (unsigned i = 0; i < m_proof.size(); ++i) { 481 status st = m_status[i]; 482 if (m_proof[i] && m_proof[i]->size() > 1 && !st.is_deleted()) { 483 clause& c = *m_proof[i]; 484 unsigned num_undef = 0, num_true = 0; 485 for (unsigned j = 0; j < c.size(); ++j) { 486 switch (value(c[j])) { 487 case l_false: break; 488 case l_true: num_true++; break; 489 case l_undef: num_undef++; break; 490 } 491 } 492 CTRACE("sat_drat", num_true == 0 && num_undef == 1, display(tout);); 493 SASSERT(num_true != 0 || num_undef != 1); 494 } 495 } 496 } 497 is_drat(unsigned n,literal const * c,unsigned pos)498 bool drat::is_drat(unsigned n, literal const* c, unsigned pos) { 499 SASSERT(pos < n); 500 literal l = c[pos]; 501 literal_vector lits(n, c); 502 SASSERT(lits.size() == n); 503 for (unsigned i = 0; i < m_proof.size(); ++i) { 504 status st = m_status[i]; 505 if (m_proof[i] && m_proof[i]->size() > 1 && st.is_asserted()) { 506 clause& c = *m_proof[i]; 507 unsigned j = 0; 508 for (; j < c.size() && c[j] != ~l; ++j) {} 509 if (j != c.size()) { 510 lits.append(j, c.begin()); 511 lits.append(c.size() - j - 1, c.begin() + j + 1); 512 if (!is_drup(lits.size(), lits.data())) 513 return false; 514 lits.resize(n); 515 } 516 } 517 } 518 return true; 519 520 } 521 verify(unsigned n,literal const * c)522 void drat::verify(unsigned n, literal const* c) { 523 if (!m_check_unsat) { 524 return; 525 } 526 for (unsigned i = 0; i < n; ++i) { 527 declare(c[i]); 528 } 529 if (is_drup(n, c)) { 530 ++m_stats.m_num_drup; 531 return; 532 } 533 if (is_drat(n, c)) { 534 ++m_stats.m_num_drat; 535 return; 536 } 537 538 literal_vector lits(n, c); 539 IF_VERBOSE(0, verbose_stream() << "Verification of " << lits << " failed\n"); 540 // s.display(std::cout); 541 std::string line; 542 std::getline(std::cin, line); 543 exit(0); 544 #if 0 545 SASSERT(false); 546 INVOKE_DEBUGGER(); 547 exit(0); 548 UNREACHABLE(); 549 //display(std::cout); 550 TRACE("sat_drat", 551 tout << literal_vector(n, c) << "\n"; 552 display(tout); 553 s.display(tout);); 554 UNREACHABLE(); 555 #endif 556 } 557 contains(literal c,justification const & j)558 bool drat::contains(literal c, justification const& j) { 559 if (!m_check_sat) { 560 return true; 561 } 562 switch (j.get_kind()) { 563 case justification::NONE: 564 return m_units.contains(c); 565 case justification::BINARY: 566 return contains(c, j.get_literal()); 567 case justification::TERNARY: 568 return contains(c, j.get_literal1(), j.get_literal2()); 569 case justification::CLAUSE: 570 return contains(s.get_clause(j)); 571 default: 572 return true; 573 } 574 } 575 contains(unsigned n,literal const * lits)576 bool drat::contains(unsigned n, literal const* lits) { 577 if (!m_check) return true; 578 unsigned num_add = 0; 579 unsigned num_del = 0; 580 for (unsigned i = m_proof.size(); i-- > 0; ) { 581 clause& c = *m_proof[i]; 582 status st = m_status[i]; 583 if (match(n, lits, c)) { 584 if (st.is_deleted()) { 585 num_del++; 586 } 587 else { 588 num_add++; 589 } 590 } 591 } 592 return num_add > num_del; 593 } 594 match(unsigned n,literal const * lits,clause const & c) const595 bool drat::match(unsigned n, literal const* lits, clause const& c) const { 596 if (n == c.size()) { 597 for (unsigned i = 0; i < n; ++i) { 598 literal lit1 = lits[i]; 599 bool found = false; 600 for (literal lit2 : c) { 601 if (lit1 == lit2) { 602 found = true; 603 break; 604 } 605 } 606 if (!found) { 607 return false; 608 } 609 } 610 return true; 611 } 612 return false; 613 } 614 display(std::ostream & out) const615 void drat::display(std::ostream& out) const { 616 out << "units: " << m_units << "\n"; 617 for (unsigned i = 0; i < m_assignment.size(); ++i) { 618 lbool v = value(literal(i, false)); 619 if (v != l_undef) out << i << ": " << v << "\n"; 620 } 621 for (unsigned i = 0; i < m_proof.size(); ++i) { 622 clause* c = m_proof[i]; 623 if (!m_status[i].is_deleted() && c) { 624 unsigned num_true = 0; 625 unsigned num_undef = 0; 626 for (unsigned j = 0; j < c->size(); ++j) { 627 switch (value((*c)[j])) { 628 case l_true: num_true++; break; 629 case l_undef: num_undef++; break; 630 default: break; 631 } 632 } 633 if (num_true == 0 && num_undef == 0) { 634 out << "False "; 635 } 636 if (num_true == 0 && num_undef == 1) { 637 out << "Unit "; 638 } 639 pp(out, m_status[i]) << " " << i << ": " << *c << "\n"; 640 } 641 } 642 for (unsigned i = 0; i < m_assignment.size(); ++i) { 643 watch const& w1 = m_watches[2 * i]; 644 watch const& w2 = m_watches[2 * i + 1]; 645 if (!w1.empty()) { 646 out << i << " |-> "; 647 for (unsigned i = 0; i < w1.size(); ++i) out << *(m_watched_clauses[w1[i]].m_clause) << " "; 648 out << "\n"; 649 } 650 if (!w2.empty()) { 651 out << "-" << i << " |-> "; 652 for (unsigned i = 0; i < w2.size(); ++i) out << *(m_watched_clauses[w2[i]].m_clause) << " "; 653 out << "\n"; 654 } 655 } 656 } 657 value(literal l) const658 lbool drat::value(literal l) const { 659 lbool val = m_assignment.get(l.var(), l_undef); 660 return val == l_undef || !l.sign() ? val : ~val; 661 } 662 assign(literal l)663 void drat::assign(literal l) { 664 lbool new_value = l.sign() ? l_false : l_true; 665 lbool old_value = value(l); 666 // TRACE("sat_drat", tout << "assign " << l << " := " << new_value << " from " << old_value << "\n";); 667 switch (old_value) { 668 case l_false: 669 m_inconsistent = true; 670 break; 671 case l_true: 672 break; 673 case l_undef: 674 m_assignment.setx(l.var(), new_value, l_undef); 675 m_units.push_back(l); 676 break; 677 } 678 } 679 assign_propagate(literal l)680 void drat::assign_propagate(literal l) { 681 unsigned num_units = m_units.size(); 682 assign(l); 683 for (unsigned i = num_units; !m_inconsistent && i < m_units.size(); ++i) { 684 propagate(m_units[i]); 685 } 686 } 687 propagate(literal l)688 void drat::propagate(literal l) { 689 watch& clauses = m_watches[l.index()]; 690 watch::iterator it = clauses.begin(); 691 watch::iterator it2 = it; 692 watch::iterator end = clauses.end(); 693 for (; it != end; ++it) { 694 unsigned idx = *it; 695 watched_clause& wc = m_watched_clauses[idx]; 696 clause& c = *wc.m_clause; 697 698 //TRACE("sat_drat", tout << "Propagate " << l << " " << c << " watch: " << wc.m_l1 << " " << wc.m_l2 << "\n";); 699 if (wc.m_l1 == ~l) { 700 std::swap(wc.m_l1, wc.m_l2); 701 } 702 703 SASSERT(wc.m_l2 == ~l); 704 if (value(wc.m_l1) == l_true) { 705 *it2 = *it; 706 it2++; 707 } 708 else { 709 bool done = false; 710 for (unsigned i = 0; !done && i < c.size(); ++i) { 711 literal lit = c[i]; 712 if (lit != wc.m_l1 && lit != wc.m_l2 && value(lit) != l_false) { 713 wc.m_l2 = lit; 714 m_watches[(~lit).index()].push_back(idx); 715 done = true; 716 } 717 } 718 if (done) { 719 continue; 720 } 721 else if (value(wc.m_l1) == l_false) { 722 m_inconsistent = true; 723 goto end_process_watch; 724 } 725 else { 726 *it2 = *it; 727 it2++; 728 assign(wc.m_l1); 729 } 730 } 731 } 732 end_process_watch: 733 for (; it != end; ++it, ++it2) 734 *it2 = *it; 735 clauses.set_end(it2); 736 } 737 get_status(bool learned) const738 status drat::get_status(bool learned) const { 739 if (learned || s.m_searching) 740 return status::redundant(); 741 return status::asserted(); 742 } 743 add()744 void drat::add() { 745 ++m_stats.m_num_add; 746 if (m_out) (*m_out) << "0\n"; 747 if (m_bout) bdump(0, nullptr, status::redundant()); 748 if (m_check_unsat) { 749 verify(0, nullptr); 750 SASSERT(m_inconsistent); 751 } 752 } add(literal l,bool learned)753 void drat::add(literal l, bool learned) { 754 ++m_stats.m_num_add; 755 status st = get_status(learned); 756 if (m_out) dump(1, &l, st); 757 if (m_bout) bdump(1, &l, st); 758 if (m_check) append(l, st); 759 } add(literal l1,literal l2,status st)760 void drat::add(literal l1, literal l2, status st) { 761 if (st.is_deleted()) 762 ++m_stats.m_num_del; 763 else 764 ++m_stats.m_num_add; 765 literal ls[2] = { l1, l2 }; 766 if (m_out) dump(2, ls, st); 767 if (m_bout) bdump(2, ls, st); 768 if (m_check) append(l1, l2, st); 769 } add(clause & c,status st)770 void drat::add(clause& c, status st) { 771 if (st.is_deleted()) 772 ++m_stats.m_num_del; 773 else 774 ++m_stats.m_num_add; 775 if (m_out) dump(c.size(), c.begin(), st); 776 if (m_bout) bdump(c.size(), c.begin(), st); 777 if (m_check) { 778 clause* cl = m_alloc.mk_clause(c.size(), c.begin(), st.is_redundant()); 779 append(*cl, st); 780 } 781 } add(literal_vector const & lits,status st)782 void drat::add(literal_vector const& lits, status st) { 783 add(lits.size(), lits.data(), st); 784 } 785 add(unsigned sz,literal const * lits,status st)786 void drat::add(unsigned sz, literal const* lits, status st) { 787 if (st.is_deleted()) 788 ++m_stats.m_num_del; 789 else 790 ++m_stats.m_num_add; 791 if (m_check) { 792 switch (sz) { 793 case 0: add(); break; 794 case 1: append(lits[0], st); break; 795 default: { 796 clause* c = m_alloc.mk_clause(sz, lits, st.is_redundant()); 797 append(*c, st); 798 break; 799 } 800 } 801 } 802 if (m_out) 803 dump(sz, lits, st); 804 } 805 add(literal_vector const & c)806 void drat::add(literal_vector const& c) { 807 ++m_stats.m_num_add; 808 if (m_out) dump(c.size(), c.begin(), status::redundant()); 809 if (m_bout) bdump(c.size(), c.begin(), status::redundant()); 810 if (m_check) { 811 for (literal lit : c) declare(lit); 812 switch (c.size()) { 813 case 0: add(); break; 814 case 1: append(c[0], status::redundant()); break; 815 default: { 816 verify(c.size(), c.begin()); 817 clause* cl = m_alloc.mk_clause(c.size(), c.data(), true); 818 append(*cl, status::redundant()); 819 break; 820 } 821 } 822 } 823 } 824 del(literal l)825 void drat::del(literal l) { 826 ++m_stats.m_num_del; 827 if (m_out) dump(1, &l, status::deleted()); 828 if (m_bout) bdump(1, &l, status::deleted()); 829 if (m_check_unsat) append(l, status::deleted()); 830 } 831 del(literal l1,literal l2)832 void drat::del(literal l1, literal l2) { 833 ++m_stats.m_num_del; 834 literal ls[2] = { l1, l2 }; 835 if (m_out) dump(2, ls, status::deleted()); 836 if (m_bout) bdump(2, ls, status::deleted()); 837 if (m_check) append(l1, l2, status::deleted()); 838 } 839 del(clause & c)840 void drat::del(clause& c) { 841 842 #if 0 843 // check_duplicates: 844 for (literal lit : c) { 845 VERIFY(!m_seen[lit.index()]); 846 m_seen[lit.index()] = true; 847 } 848 for (literal lit : c) { 849 m_seen[lit.index()] = false; 850 } 851 #endif 852 ++m_stats.m_num_del; 853 if (m_out) dump(c.size(), c.begin(), status::deleted()); 854 if (m_bout) bdump(c.size(), c.begin(), status::deleted()); 855 if (m_check) { 856 clause* c1 = m_alloc.mk_clause(c.size(), c.begin(), c.is_learned()); 857 append(*c1, status::deleted()); 858 } 859 } 860 del(literal_vector const & c)861 void drat::del(literal_vector const& c) { 862 ++m_stats.m_num_del; 863 if (m_out) dump(c.size(), c.begin(), status::deleted()); 864 if (m_bout) bdump(c.size(), c.begin(), status::deleted()); 865 if (m_check) { 866 clause* c1 = m_alloc.mk_clause(c.size(), c.begin(), true); 867 append(*c1, status::deleted()); 868 } 869 } 870 check_model(model const & m)871 void drat::check_model(model const& m) { 872 } 873 collect_statistics(statistics & st) const874 void drat::collect_statistics(statistics& st) const { 875 st.update("num-drup", m_stats.m_num_drup); 876 st.update("num-drat", m_stats.m_num_drat); 877 st.update("num-add", m_stats.m_num_add); 878 st.update("num-del", m_stats.m_num_del); 879 } 880 881 operator <<(std::ostream & out,sat::status const & st)882 std::ostream& operator<<(std::ostream& out, sat::status const& st) { 883 std::function<symbol(int)> th = [&](int id) { return symbol(id); }; 884 return out << sat::status_pp(st, th); 885 } 886 operator <<(std::ostream & out,sat::status_pp const & p)887 std::ostream& operator<<(std::ostream& out, sat::status_pp const& p) { 888 auto st = p.st; 889 if (st.is_deleted()) 890 out << "d"; 891 else if (st.is_input()) 892 out << "i"; 893 else if (st.is_asserted()) 894 out << "a"; 895 else if (st.is_redundant() && !st.is_sat()) 896 out << "r"; 897 if (!st.is_sat()) 898 out << " " << p.th(st.get_th()); 899 return out; 900 } 901 902 } 903