1 /*++ 2 Copyright (c) 2017 Arie Gurfinkel 3 4 Module Name: 5 6 spacer_unsat_core_plugin.cpp 7 8 Abstract: 9 plugin for itp cores 10 11 Author: 12 Bernhard Gleiss 13 14 Revision History: 15 16 17 --*/ 18 #include <set> 19 #include <limits> 20 21 #include "ast/rewriter/bool_rewriter.h" 22 #include "ast/arith_decl_plugin.h" 23 #include "ast/proofs/proof_utils.h" 24 25 #include "solver/solver.h" 26 27 #include "smt/smt_farkas_util.h" 28 #include "smt/smt_solver.h" 29 30 #include "muz/spacer/spacer_matrix.h" 31 #include "muz/spacer/spacer_unsat_core_plugin.h" 32 #include "muz/spacer/spacer_unsat_core_learner.h" 33 #include "muz/spacer/spacer_iuc_proof.h" 34 35 namespace spacer { 36 unsat_core_plugin(unsat_core_learner & ctx)37 unsat_core_plugin::unsat_core_plugin(unsat_core_learner& ctx): 38 m(ctx.get_manager()), m_ctx(ctx) {}; 39 compute_partial_core(proof * step)40 void unsat_core_plugin_lemma::compute_partial_core(proof* step) { 41 SASSERT(m_ctx.is_a(step)); 42 SASSERT(m_ctx.is_b(step)); 43 44 for (auto* p : m.get_parents(step)) { 45 if (m_ctx.is_b_open (p)) { 46 // by IH, premises that are AB marked are already closed 47 SASSERT(!m_ctx.is_a(p)); 48 add_lowest_split_to_core(p); 49 } 50 } 51 m_ctx.set_closed(step, true); 52 } 53 add_lowest_split_to_core(proof * step) const54 void unsat_core_plugin_lemma::add_lowest_split_to_core(proof* step) const { 55 SASSERT(m_ctx.is_b_open(step)); 56 57 ptr_buffer<proof> todo; 58 todo.push_back(step); 59 60 while (!todo.empty()) { 61 proof* pf = todo.back(); 62 todo.pop_back(); 63 64 // if current step hasn't been processed, 65 if (!m_ctx.is_closed(pf)) { 66 m_ctx.set_closed(pf, true); 67 // the step is b-marked and not closed. 68 // by I.H. the step must be already visited 69 // so if it is also a-marked, it must be closed 70 SASSERT(m_ctx.is_b(pf)); 71 SASSERT(!m_ctx.is_a(pf)); 72 73 // the current step needs to be interpolated: 74 expr* fact = m.get_fact(pf); 75 // if we trust the current step and we are able to use it 76 if (m_ctx.is_b_pure (pf) && (m.is_asserted(pf) || spacer::is_literal(m, fact))) { 77 // just add it to the core 78 m_ctx.add_lemma_to_core(fact); 79 } 80 // otherwise recurse on premises 81 else { 82 for (proof* premise : m.get_parents(pf)) 83 if (m_ctx.is_b_open(premise)) 84 todo.push_back(premise); 85 } 86 } 87 } 88 } 89 90 91 /*** 92 * FARKAS 93 */ compute_partial_core(proof * step)94 void unsat_core_plugin_farkas_lemma::compute_partial_core(proof* step) { 95 SASSERT(m_ctx.is_a(step)); 96 SASSERT(m_ctx.is_b(step)); 97 // XXX this assertion should be true so there is no need to check for it 98 SASSERT (!m_ctx.is_closed (step)); 99 func_decl* d = step->get_decl(); 100 symbol sym; 101 TRACE("spacer.farkas", 102 tout << "looking at: " << mk_pp(step, m) << "\n";); 103 if (!m_ctx.is_closed(step) && is_farkas_lemma(m, step)) { 104 // weaker check : d->get_num_parameters() >= m.get_num_parents(step) + 2 105 106 SASSERT(d->get_num_parameters() == m.get_num_parents(step) + 2); 107 SASSERT(m.has_fact(step)); 108 109 coeff_lits_t coeff_lits; 110 expr_ref_vector pinned(m); 111 112 /* The farkas lemma represents a subproof starting from premise(-set)s A, BNP and BP(ure) and 113 * ending in a disjunction D. We need to compute the contribution of BP, i.e. a formula, which 114 * is entailed by BP and together with A and BNP entails D. 115 * 116 * Let Fark(F) be the farkas coefficient for F. We can use the fact that 117 * (A*Fark(A) + BNP*Fark(BNP) + BP*Fark(BP) + (neg D)*Fark(D)) => false. (E1) 118 * We further have that A+B => C implies (A \land B) => C. (E2) 119 * 120 * Alternative 1: 121 * From (E1) immediately get that BP*Fark(BP) is a solution. 122 * 123 * Alternative 2: 124 * We can rewrite (E2) to rewrite (E1) to 125 * (BP*Fark(BP)) => (neg(A*Fark(A) + BNP*Fark(BNP) + (neg D)*Fark(D))) (E3) 126 * and since we can derive (A*Fark(A) + BNP*Fark(BNP) + (neg D)*Fark(D)) from 127 * A, BNP and D, we also know that it is inconsistent. Therefore 128 * neg(A*Fark(A) + BNP*Fark(BNP) + (neg D)*Fark(D)) is a solution. 129 * 130 * Finally we also need the following workaround: 131 * 1) Although we know from theory, that the Farkas coefficients are always nonnegative, 132 * the Farkas coefficients provided by arith_core are sometimes negative (must be a bug) 133 * as workaround we take the absolute value of the provided coefficients. 134 */ 135 parameter const* params = d->get_parameters() + 2; // point to the first Farkas coefficient 136 137 TRACE("spacer.farkas", 138 tout << "Farkas input: "<< "\n"; 139 for (unsigned i = 0; i < m.get_num_parents(step); ++i) { 140 proof * prem = m.get_parent(step, i); 141 rational coef = params[i].get_rational(); 142 bool b_pure = m_ctx.is_b_pure (prem); 143 tout << (b_pure?"B":"A") << " " << coef << " " << mk_pp(m.get_fact(prem), m) << "\n"; 144 } 145 ); 146 147 bool done = true; 148 149 for (unsigned i = 0; i < m.get_num_parents(step); ++i) { 150 proof * premise = m.get_parent(step, i); 151 152 if (m_ctx.is_b_open (premise)) { 153 SASSERT(!m_ctx.is_a(premise)); 154 155 if (m_ctx.is_b_pure (premise)) { 156 if (!m_use_constant_from_a) { 157 rational coefficient = params[i].get_rational(); 158 coeff_lits.push_back(std::make_pair(abs(coefficient), (app*)m.get_fact(premise))); 159 } 160 } 161 else { 162 // -- mixed premise, won't be able to close this proof step 163 done = false; 164 165 if (m_use_constant_from_a) { 166 rational coefficient = params[i].get_rational(); 167 coeff_lits.push_back(std::make_pair(abs(coefficient), (app*)m.get_fact(premise))); 168 } 169 } 170 } 171 else { 172 if (m_use_constant_from_a) { 173 rational coefficient = params[i].get_rational(); 174 coeff_lits.push_back(std::make_pair(abs(coefficient), (app*)m.get_fact(premise))); 175 } 176 } 177 } 178 179 // TBD: factor into another method 180 if (m_use_constant_from_a) { 181 params += m.get_num_parents(step); // point to the first Farkas coefficient, which corresponds to a formula in the conclusion 182 183 // the conclusion can either be a single formula or a disjunction of several formulas, we have to deal with both situations 184 if (m.get_num_parents(step) + 2 < d->get_num_parameters()) { 185 unsigned num_args = 1; 186 expr* conclusion = m.get_fact(step); 187 expr* const* args = &conclusion; 188 if (m.is_or(conclusion)) { 189 app* _or = to_app(conclusion); 190 num_args = _or->get_num_args(); 191 args = _or->get_args(); 192 } 193 SASSERT(m.get_num_parents(step) + 2 + num_args == d->get_num_parameters()); 194 195 bool_rewriter brw(m); 196 for (unsigned i = 0; i < num_args; ++i) { 197 expr* premise = args[i]; 198 199 expr_ref negatedPremise(m); 200 brw.mk_not(premise, negatedPremise); 201 pinned.push_back(negatedPremise); 202 rational coefficient = params[i].get_rational(); 203 coeff_lits.push_back(std::make_pair(abs(coefficient), to_app(negatedPremise))); 204 } 205 } 206 } 207 208 // only if all b-premises can be used directly, add the farkas core and close the step 209 // AG: this decision needs to be re-evaluated. If the proof cannot be closed, literals above 210 // AG: it will go into the core. However, it does not mean that this literal should/could not be added. 211 m_ctx.set_closed(step, done); 212 expr_ref res = compute_linear_combination(coeff_lits); 213 TRACE("spacer.farkas", tout << "Farkas core: " << res << "\n";); 214 m_ctx.add_lemma_to_core(res); 215 } 216 } 217 compute_linear_combination(const coeff_lits_t & coeff_lits)218 expr_ref unsat_core_plugin_farkas_lemma::compute_linear_combination(const coeff_lits_t& coeff_lits) 219 { 220 221 smt::farkas_util util(m); 222 if (m_use_constant_from_a) { 223 util.set_split_literals (m_split_literals); // small optimization: if flag m_split_literals is set, then preserve diff constraints 224 } 225 for (auto& p : coeff_lits) { 226 util.add(p.first, p.second); 227 } 228 if (m_use_constant_from_a) { 229 return util.get(); 230 } 231 else { 232 return expr_ref(mk_not(m, util.get()), m); 233 } 234 } 235 compute_partial_core(proof * step)236 void unsat_core_plugin_farkas_lemma_optimized::compute_partial_core(proof* step) 237 { 238 SASSERT(m_ctx.is_a(step)); 239 SASSERT(m_ctx.is_b(step)); 240 241 func_decl* d = step->get_decl(); 242 symbol sym; 243 if (!m_ctx.is_closed(step) && // if step is not already interpolated 244 is_farkas_lemma(m, step)) { 245 SASSERT(d->get_num_parameters() == m.get_num_parents(step) + 2); 246 SASSERT(m.has_fact(step)); 247 248 coeff_lits_t linear_combination; // collects all summands of the linear combination 249 250 parameter const* params = d->get_parameters() + 2; // point to the first Farkas coefficient 251 252 TRACE("spacer.farkas", 253 tout << "Farkas input: "<< "\n"; 254 for (unsigned i = 0; i < m.get_num_parents(step); ++i) { 255 proof * prem = m.get_parent(step, i); 256 rational coef = params[i].get_rational(); 257 bool b_pure = m_ctx.is_b_pure (prem); 258 tout << (b_pure?"B":"A") << " " << coef << " " << mk_pp(m.get_fact(prem), m) << "\n"; 259 } 260 ); 261 262 bool can_be_closed = true; 263 for (unsigned i = 0; i < m.get_num_parents(step); ++i) { 264 proof * premise = m.get_parent(step, i); 265 266 if (m_ctx.is_b(premise) && !m_ctx.is_closed(premise)) 267 { 268 SASSERT(!m_ctx.is_a(premise)); 269 270 if (m_ctx.is_b_pure(premise)) 271 { 272 rational coefficient = params[i].get_rational(); 273 linear_combination.push_back 274 (std::make_pair(abs(coefficient), to_app(m.get_fact(premise)))); 275 } 276 else 277 { 278 can_be_closed = false; 279 } 280 } 281 } 282 283 // only if all b-premises can be used directly, close the step and add linear combinations for later processing 284 if (can_be_closed) 285 { 286 m_ctx.set_closed(step, true); 287 if (!linear_combination.empty()) 288 { 289 m_linear_combinations.push_back(linear_combination); 290 } 291 } 292 } 293 } 294 295 struct farkas_optimized_less_than_pairs 296 { operator ()spacer::farkas_optimized_less_than_pairs297 inline bool operator() (const std::pair<rational, app*>& pair1, const std::pair<rational, app*>& pair2) const 298 { 299 return (pair1.second->get_id() < pair2.second->get_id()); 300 } 301 }; 302 finalize()303 void unsat_core_plugin_farkas_lemma_optimized::finalize() 304 { 305 if (m_linear_combinations.empty()) 306 { 307 return; 308 } 309 DEBUG_CODE( 310 for (auto& linear_combination : m_linear_combinations) { 311 SASSERT(!linear_combination.empty()); 312 }); 313 314 // 1. construct ordered basis 315 ptr_vector<app> ordered_basis; 316 obj_map<app, unsigned> map; 317 unsigned counter = 0; 318 for (const auto& linear_combination : m_linear_combinations) { 319 for (const auto& pair : linear_combination) { 320 if (!map.contains(pair.second)) { 321 ordered_basis.push_back(pair.second); 322 map.insert(pair.second, counter++); 323 } 324 } 325 } 326 327 // 2. populate matrix 328 spacer_matrix matrix(m_linear_combinations.size(), ordered_basis.size()); 329 330 for (unsigned i = 0; i < m_linear_combinations.size(); ++i) { 331 auto linear_combination = m_linear_combinations[i]; 332 for (const auto& pair : linear_combination) { 333 matrix.set(i, map[pair.second], pair.first); 334 } 335 } 336 337 // 3. perform gaussian elimination 338 unsigned i = matrix.perform_gaussian_elimination(); 339 340 // 4. extract linear combinations from matrix and add result to core 341 for (unsigned k = 0; k < i; ++k)// i points to the row after the last row which is non-zero 342 { 343 coeff_lits_t coeff_lits; 344 for (unsigned l = 0; l < matrix.num_cols(); ++l) { 345 if (!matrix.get(k,l).is_zero()) { 346 coeff_lits.push_back(std::make_pair(matrix.get(k, l), ordered_basis[l])); 347 } 348 } 349 SASSERT(!coeff_lits.empty()); 350 expr_ref linear_combination = compute_linear_combination(coeff_lits); 351 352 m_ctx.add_lemma_to_core(linear_combination); 353 } 354 355 } 356 compute_linear_combination(const coeff_lits_t & coeff_lits)357 expr_ref unsat_core_plugin_farkas_lemma_optimized::compute_linear_combination(const coeff_lits_t& coeff_lits) { 358 smt::farkas_util util(m); 359 for (auto const & p : coeff_lits) { 360 util.add(p.first, p.second); 361 } 362 expr_ref negated_linear_combination = util.get(); 363 SASSERT(m.is_not(negated_linear_combination)); 364 return expr_ref(mk_not(m, negated_linear_combination), m); 365 //TODO: rewrite the get-method to return nonnegated stuff? 366 } 367 finalize()368 void unsat_core_plugin_farkas_lemma_bounded::finalize() { 369 if (m_linear_combinations.empty()) { 370 return; 371 } 372 DEBUG_CODE( 373 for (auto& linear_combination : m_linear_combinations) { 374 SASSERT(!linear_combination.empty()); 375 }); 376 377 // 1. construct ordered basis 378 ptr_vector<app> ordered_basis; 379 obj_map<app, unsigned> map; 380 unsigned counter = 0; 381 for (const auto& linear_combination : m_linear_combinations) { 382 for (const auto& pair : linear_combination) { 383 if (!map.contains(pair.second)) { 384 ordered_basis.push_back(pair.second); 385 map.insert(pair.second, counter++); 386 } 387 } 388 } 389 390 // 2. populate matrix 391 spacer_matrix matrix(m_linear_combinations.size(), ordered_basis.size()); 392 393 for (unsigned i=0; i < m_linear_combinations.size(); ++i) { 394 auto linear_combination = m_linear_combinations[i]; 395 for (const auto& pair : linear_combination) { 396 matrix.set(i, map[pair.second], pair.first); 397 } 398 } 399 matrix.print_matrix(); 400 401 // 3. normalize matrix to integer values 402 matrix.normalize(); 403 404 405 arith_util util(m); 406 407 vector<expr_ref_vector> coeffs; 408 for (unsigned i = 0; i < matrix.num_rows(); ++i) { 409 coeffs.push_back(expr_ref_vector(m)); 410 } 411 412 vector<expr_ref_vector> bounded_vectors; 413 for (unsigned j = 0; j < matrix.num_cols(); ++j) { 414 bounded_vectors.push_back(expr_ref_vector(m)); 415 } 416 417 // 4. find smallest n using guess and check algorithm 418 for (unsigned n = 1; true; ++n) 419 { 420 params_ref p; 421 p.set_bool("model", true); 422 solver_ref s = mk_smt_solver(m, p, symbol::null); // TODO: incremental version? 423 424 // add new variables w_in, 425 for (unsigned i = 0; i < matrix.num_rows(); ++i) { 426 std::string name = "w_" + std::to_string(i) + std::to_string(n); 427 coeffs[i].push_back(m.mk_const(name, util.mk_int())); 428 } 429 430 // we need s_jn 431 for (unsigned j = 0; j < matrix.num_cols(); ++j) { 432 std::string name = "s_" + std::to_string(j) + std::to_string(n); 433 bounded_vectors[j].push_back(m.mk_const(name, util.mk_int())); 434 } 435 436 // assert bounds for all s_jn 437 for (unsigned l = 0; l < n; ++l) { 438 for (unsigned j = 0; j < matrix.num_cols(); ++j) { 439 expr* s_jn = bounded_vectors[j][l].get(); 440 expr_ref lb(util.mk_le(util.mk_int(0), s_jn), m); 441 expr_ref ub(util.mk_le(s_jn, util.mk_int(1)), m); 442 s->assert_expr(lb); 443 s->assert_expr(ub); 444 } 445 } 446 447 // assert: forall i,j: a_ij = sum_k w_ik * s_jk 448 for (unsigned i = 0; i < matrix.num_rows(); ++i) { 449 for (unsigned j = 0; j < matrix.num_cols(); ++j) { 450 SASSERT(matrix.get(i, j).is_int()); 451 app_ref a_ij(util.mk_numeral(matrix.get(i,j), true), m); 452 453 app_ref sum(util.mk_int(0), m); 454 for (unsigned k = 0; k < n; ++k) { 455 sum = util.mk_add(sum, util.mk_mul(coeffs[i][k].get(), bounded_vectors[j][k].get())); 456 } 457 expr_ref eq(m.mk_eq(a_ij, sum), m); 458 s->assert_expr(eq); 459 } 460 } 461 462 // check result 463 lbool res = s->check_sat(0, nullptr); 464 465 // if sat extract model and add corresponding linear combinations to core 466 if (res == lbool::l_true) { 467 model_ref model; 468 s->get_model(model); 469 470 for (unsigned k = 0; k < n; ++k) { 471 coeff_lits_t coeff_lits; 472 for (unsigned j = 0; j < matrix.num_cols(); ++j) { 473 expr_ref evaluation(m); 474 475 evaluation = (*model)(bounded_vectors[j][k].get()); 476 if (!util.is_zero(evaluation)) { 477 coeff_lits.push_back(std::make_pair(rational(1), ordered_basis[j])); 478 } 479 } 480 SASSERT(!coeff_lits.empty()); // since then previous outer loop would have found solution already 481 expr_ref linear_combination = compute_linear_combination(coeff_lits); 482 483 m_ctx.add_lemma_to_core(linear_combination); 484 } 485 return; 486 } 487 } 488 } 489 unsat_core_plugin_min_cut(unsat_core_learner & learner,ast_manager & m)490 unsat_core_plugin_min_cut::unsat_core_plugin_min_cut(unsat_core_learner& learner, ast_manager& m) : unsat_core_plugin(learner) {} 491 492 /* 493 * traverses proof rooted in step and constructs graph, which corresponds to the proof-DAG, with the following differences: 494 * 495 * 1) we want to skip vertices, which have a conclusion, which we don't like (call those steps bad and the other ones good). In other words, we start at a good step r and compute the smallest subproof with root r, which has only good leaves. Then we add an edge from the root to each of the leaves and remember that we already dealt with s. Then we recurse on all leaves. 496 * 2) we want to introduce two vertices for all (unskipped) edges in order to run the min-cut algorithm 497 * 3) we want to introduce a single super-source vertex, which is connected to all source-vertices of the proof-DAG and a 498 * single super-sink vertex, to which all sink-vertices of the proof-DAG are connected 499 * 500 * 1) is dealt with using advance_to_lowest_partial_cut 501 * 2) and 3) are dealt with using add_edge 502 */ compute_partial_core(proof * step)503 void unsat_core_plugin_min_cut::compute_partial_core(proof* step) 504 { 505 ptr_vector<proof> todo; 506 507 SASSERT(m_ctx.is_a(step)); 508 SASSERT(m_ctx.is_b(step)); 509 SASSERT(m.get_num_parents(step) > 0); 510 SASSERT(!m_ctx.is_closed(step)); 511 todo.push_back(step); 512 513 while (!todo.empty()) 514 { 515 proof* current = todo.back(); 516 todo.pop_back(); 517 518 // if we need to deal with the node and if we haven't added the corresponding edges so far 519 if (!m_ctx.is_closed(current) && !m_visited.is_marked(current)) 520 { 521 // compute smallest subproof rooted in current, which has only good edges 522 // add an edge from current to each leaf of that subproof 523 // add the leaves to todo 524 advance_to_lowest_partial_cut(current, todo); 525 526 m_visited.mark(current, true); 527 528 } 529 } 530 m_ctx.set_closed(step, true); 531 } 532 533 advance_to_lowest_partial_cut(proof * step,ptr_vector<proof> & todo)534 void unsat_core_plugin_min_cut::advance_to_lowest_partial_cut(proof* step, ptr_vector<proof>& todo) 535 { 536 bool is_sink = true; 537 538 ptr_buffer<proof> todo_subproof; 539 540 for (proof* premise : m.get_parents(step)) { 541 if (m_ctx.is_b(premise)) { 542 todo_subproof.push_back(premise); 543 } 544 } 545 while (!todo_subproof.empty()) 546 { 547 proof* current = todo_subproof.back(); 548 todo_subproof.pop_back(); 549 550 // if we need to deal with the node 551 if (!m_ctx.is_closed(current)) 552 { 553 SASSERT(!m_ctx.is_a(current)); // by I.H. the step must be already visited 554 555 // and the current step needs to be interpolated: 556 if (m_ctx.is_b(current)) 557 { 558 // if we trust the current step and we are able to use it 559 if (m_ctx.is_b_pure (current) && 560 (m.is_asserted(current) || 561 spacer::is_literal(m, m.get_fact(current)))) 562 { 563 // we found a leaf of the subproof, so 564 // 1) we add corresponding edges 565 if (m_ctx.is_a(step)) 566 { 567 add_edge(nullptr, current); // current is sink 568 } 569 else 570 { 571 add_edge(step, current); // standard edge 572 } 573 // 2) add the leaf to todo 574 todo.push_back(current); 575 is_sink = false; 576 } 577 // otherwise continue search for leaves of subproof 578 else 579 { 580 for (proof* premise : m.get_parents(current)) { 581 todo_subproof.push_back(premise); 582 } 583 } 584 } 585 } 586 } 587 588 if (is_sink) 589 { 590 add_edge(step, nullptr); 591 } 592 } 593 594 /* 595 * adds an edge from the out-vertex of i to the in-vertex of j to the graph 596 * if i or j isn't already present, it adds the corresponding in- and out-vertices to the graph 597 * if i is a nullptr, it is treated as source vertex 598 * if j is a nullptr, it is treated as sink vertex 599 */ add_edge(proof * i,proof * j)600 void unsat_core_plugin_min_cut::add_edge(proof* i, proof* j) 601 { 602 SASSERT(i != nullptr || j != nullptr); 603 604 unsigned node_i; 605 unsigned node_j; 606 if (i == nullptr) 607 { 608 node_i = 0; 609 } 610 else 611 { 612 unsigned tmp; 613 if (m_proof_to_node_plus.find(i, tmp)) 614 { 615 node_i = tmp; 616 } 617 else 618 { 619 unsigned node_other = m_min_cut.new_node(); 620 node_i = m_min_cut.new_node(); 621 622 m_proof_to_node_minus.insert(i, node_other); 623 m_proof_to_node_plus.insert(i, node_i); 624 625 if (node_i >= m_node_to_formula.size()) 626 { 627 m_node_to_formula.resize(node_i + 1); 628 } 629 m_node_to_formula[node_other] = m.get_fact(i); 630 m_node_to_formula[node_i] = m.get_fact(i); 631 632 m_min_cut.add_edge(node_other, node_i, 1); 633 } 634 } 635 636 if (j == nullptr) 637 { 638 node_j = 1; 639 } 640 else 641 { 642 unsigned tmp; 643 if (m_proof_to_node_minus.find(j, tmp)) 644 { 645 node_j = tmp; 646 } 647 else 648 { 649 node_j = m_min_cut.new_node(); 650 unsigned node_other = m_min_cut.new_node(); 651 652 m_proof_to_node_minus.insert(j, node_j); 653 m_proof_to_node_plus.insert(j, node_other); 654 655 if (node_other >= m_node_to_formula.size()) 656 { 657 m_node_to_formula.resize(node_other + 1); 658 } 659 m_node_to_formula[node_j] = m.get_fact(j); 660 m_node_to_formula[node_other] = m.get_fact(j); 661 662 m_min_cut.add_edge(node_j, node_other, 1); 663 } 664 } 665 666 // finally connect nodes (if there is not already a connection i -> j (only relevant if i is the supersource)) 667 if (!(i == nullptr && m_connected_to_s.is_marked(j))) 668 { 669 m_min_cut.add_edge(node_i, node_j, 1); 670 } 671 672 if (i == nullptr) 673 { 674 m_connected_to_s.mark(j, true); 675 } 676 } 677 678 /* 679 * computes min-cut on the graph constructed by compute_partial_core-method 680 * and adds the corresponding lemmas to the core 681 */ finalize()682 void unsat_core_plugin_min_cut::finalize() { 683 unsigned_vector cut_nodes; 684 m_min_cut.compute_min_cut(cut_nodes); 685 686 for (unsigned cut_node : cut_nodes) { 687 m_ctx.add_lemma_to_core(m_node_to_formula[cut_node]); 688 } 689 } 690 } 691