From 4c23527974aa50d37c49725f1581906400612ecf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 6 Jul 2017 08:53:08 -0700 Subject: [PATCH] Dev (#63) * introduce int_solver.h Signed-off-by: Lev Nachmanson * add int_solver class Signed-off-by: Lev Nachmanson * track which var is an integer Signed-off-by: Lev Nachmanson * add queries for integrality of vars Signed-off-by: Lev Nachmanson * resurrect lp_tst in its own director lp Signed-off-by: Lev Nachmanson * add file Signed-off-by: Lev Nachmanson * add_constraint has got a body Signed-off-by: Lev Nachmanson * fix add_constraint and substitute_terms_in_linear_expression Signed-off-by: Lev Nachmanson * after merge with Z3Prover Signed-off-by: Lev Nachmanson * adding stub check_int_feasibility() Signed-off-by: Lev Nachmanson * Dev (#50) * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner * small fix in lar_solver.cpp Signed-off-by: Lev Nachmanson * adding some content to the new check_int_feasibility() Signed-off-by: Lev Nachmanson * Dev (#51) * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner * adding more nlsat Signed-off-by: Nikolaj Bjorner * nlsat integration Signed-off-by: Nikolaj Bjorner * adding constraints Signed-off-by: Nikolaj Bjorner * adding nra solver Signed-off-by: Nikolaj Bjorner * add missing initialization Signed-off-by: Nikolaj Bjorner * adding nra solver Signed-off-by: Nikolaj Bjorner * test Signed-off-by: Lev Nachmanson * Dev (#53) * change in a comment Signed-off-by: Lev Nachmanson * Disabled debug output * removing FOCI2 interface from interp * remove foci reference from cmakelist.txt Signed-off-by: Nikolaj Bjorner * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner * adding more nlsat Signed-off-by: Nikolaj Bjorner * nlsat integration Signed-off-by: Nikolaj Bjorner * adding constraints Signed-off-by: Nikolaj Bjorner * adding nra solver Signed-off-by: Nikolaj Bjorner * add missing initialization Signed-off-by: Nikolaj Bjorner * adding nra solver Signed-off-by: Nikolaj Bjorner * adding nra Signed-off-by: Nikolaj Bjorner * debugging nra Signed-off-by: Nikolaj Bjorner * updates to nra_solver integration to call it directly from theory_lra instead of over lar_solver Signed-off-by: Nikolaj Bjorner * n/a Signed-off-by: Nikolaj Bjorner * integrate nlsat Signed-off-by: Nikolaj Bjorner * tidy Signed-off-by: Nikolaj Bjorner * preserve is_int flag Signed-off-by: Lev Nachmanson * remove a debug printout Signed-off-by: Lev Nachmanson * Dev (#54) * change in a comment Signed-off-by: Lev Nachmanson * Disabled debug output * removing FOCI2 interface from interp * remove foci reference from cmakelist.txt Signed-off-by: Nikolaj Bjorner * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner * adding more nlsat Signed-off-by: Nikolaj Bjorner * nlsat integration Signed-off-by: Nikolaj Bjorner * adding constraints Signed-off-by: Nikolaj Bjorner * adding nra solver Signed-off-by: Nikolaj Bjorner * add missing initialization Signed-off-by: Nikolaj Bjorner * adding nra solver Signed-off-by: Nikolaj Bjorner * adding nra Signed-off-by: Nikolaj Bjorner * debugging nra Signed-off-by: Nikolaj Bjorner * updates to nra_solver integration to call it directly from theory_lra instead of over lar_solver Signed-off-by: Nikolaj Bjorner * n/a Signed-off-by: Nikolaj Bjorner * integrate nlsat Signed-off-by: Nikolaj Bjorner * tidy Signed-off-by: Nikolaj Bjorner * use integer test from lra solver, updated it to work on term variables Signed-off-by: Nikolaj Bjorner * fix equality check in assume-eq Signed-off-by: Nikolaj Bjorner * fix model_is_int_feasible Signed-off-by: Lev Nachmanson * untested gcd_test() Signed-off-by: Lev Nachmanson * call fill_explanation_from_fixed_columns() Signed-off-by: Lev Nachmanson * add the call to pivot_fixed_vars_from_basis() to int_solver.cpp::check() Signed-off-by: Lev Nachmanson * port more of theory_arith_int.h Signed-off-by: Lev Nachmanson * use statistics of lar_solver by theory_lra.cpp Signed-off-by: Lev Nachmanson * port more code to int_solver.cpp Signed-off-by: Lev Nachmanson * add an assert Signed-off-by: Lev Nachmanson * more int porting Signed-off-by: Lev Nachmanson * fix a bug in pivot_fixed_vars_from_basis Signed-off-by: Lev Nachmanson * small change Signed-off-by: Lev Nachmanson * implement find_inf_int_base_column() Signed-off-by: Lev Nachmanson * catch unregistered vars in add_var_bound Signed-off-by: Lev Nachmanson * add a file Signed-off-by: Lev Nachmanson * compile for vs2012 Signed-off-by: Lev Nachmanson * fix asserts in add_var_bound Signed-off-by: Lev Nachmanson * fix the lp_solver init when workig on an mps file Signed-off-by: Lev Nachmanson * towards int_solver::check() Signed-off-by: Lev Nachmanson * change in int_solver::check() signature Signed-off-by: Lev Nachmanson * add handlers for lia moves Signed-off-by: Nikolaj Bjorner * spacing Signed-off-by: Nikolaj Bjorner * return branch from int_solver::check() Signed-off-by: Lev Nachmanson * add a stub for mk_gomory_cut Signed-off-by: Lev Nachmanson * Dev (#59) * add handlers for lia moves Signed-off-by: Nikolaj Bjorner * spacing Signed-off-by: Nikolaj Bjorner * loops Signed-off-by: Nikolaj Bjorner * Dev (#60) * add handlers for lia moves Signed-off-by: Nikolaj Bjorner * spacing Signed-off-by: Nikolaj Bjorner * loops Signed-off-by: Nikolaj Bjorner * loops Signed-off-by: Nikolaj Bjorner * Dev (#61) * add handlers for lia moves Signed-off-by: Nikolaj Bjorner * spacing Signed-off-by: Nikolaj Bjorner * loops Signed-off-by: Nikolaj Bjorner * loops Signed-off-by: Nikolaj Bjorner * more TRACE(arith_int) Signed-off-by: Lev Nachmanson * fix the build Signed-off-by: Lev Nachmanson * loops Signed-off-by: Nikolaj Bjorner * Dev (#62) * add handlers for lia moves Signed-off-by: Nikolaj Bjorner * spacing Signed-off-by: Nikolaj Bjorner * loops Signed-off-by: Nikolaj Bjorner * loops Signed-off-by: Nikolaj Bjorner * loops Signed-off-by: Nikolaj Bjorner * build fix Signed-off-by: Lev Nachmanson --- src/smt/theory_arith_int.h | 6 +- src/smt/theory_lra.cpp | 112 +++++++++++++------ src/util/lp/int_solver.cpp | 224 +++++++++++++++++++++++++++++++++---- src/util/lp/int_solver.h | 2 + src/util/lp/lar_term.h | 4 + 5 files changed, 291 insertions(+), 57 deletions(-) diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index e6e9e863c..ca3a485c6 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -201,10 +201,12 @@ namespace smt { SASSERT(is_int(v)); SASSERT(!get_value(v).is_int()); m_stats.m_branches++; - TRACE("arith_int", tout << "branching v" << v << " = " << get_value(v) << "\n"; - display_var(tout, v);); numeral k = ceil(get_value(v)); rational _k = k.to_rational(); + TRACE("arith_int", tout << "branching v" << v << " = " << get_value(v) << "\n"; + display_var(tout, v); + tout << "k = " << k << ", _k = "<< _k << std::endl; + ); expr_ref bound(get_manager()); expr* e = get_enode(v)->get_owner(); bound = m_util.mk_ge(e, m_util.mk_numeral(_k, m_util.is_int(e))); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index c35dbb94e..43d3820f3 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -54,13 +54,15 @@ namespace lp { class bound { smt::bool_var m_bv; smt::theory_var m_var; + bool m_is_int; rational m_value; bound_kind m_bound_kind; public: - bound(smt::bool_var bv, smt::theory_var v, rational const & val, bound_kind k): + bound(smt::bool_var bv, smt::theory_var v, bool is_int, rational const & val, bound_kind k): m_bv(bv), m_var(v), + m_is_int(is_int), m_value(val), m_bound_kind(k) { } @@ -68,11 +70,18 @@ namespace lp { smt::theory_var get_var() const { return m_var; } smt::bool_var get_bv() const { return m_bv; } bound_kind get_bound_kind() const { return m_bound_kind; } + bool is_int() const { return m_is_int; } rational const& get_value() const { return m_value; } inf_rational get_value(bool is_true) const { if (is_true) return inf_rational(m_value); // v >= value or v <= value - if (m_bound_kind == lower_t) return inf_rational(m_value, false); // v <= value - epsilon - return inf_rational(m_value, true); // v >= value + epsilon + if (m_is_int) { + if (m_bound_kind == lower_t) return inf_rational(m_value - rational::one()); // v <= value - 1 + return inf_rational(m_value + rational::one()); // v >= value + 1 + } + else { + if (m_bound_kind == lower_t) return inf_rational(m_value, false); // v <= value - epsilon + return inf_rational(m_value, true); // v >= value + epsilon + } } virtual std::ostream& display(std::ostream& out) const { return out << "v" << get_var() << " " << get_bound_kind() << " " << m_value; @@ -305,7 +314,6 @@ namespace smt { } } - void found_not_handled(expr* n) { m_not_handled = n; if (is_app(n) && is_underspecified(to_app(n))) { @@ -756,7 +764,7 @@ namespace smt { found_not_handled(atom); return true; } - lp::bound* b = alloc(lp::bound, bv, v, r, k); + lp::bound* b = alloc(lp::bound, bv, v, is_int(v), r, k); m_bounds[v].push_back(b); updt_unassigned_bounds(v, +1); m_bounds_trail.push_back(v); @@ -1211,33 +1219,49 @@ namespace smt { return FC_GIVEUP; } - // create a bound atom representing term >= k - lp::bound* mk_bound(lean::lar_term const& term, rational const& k) { - NOT_IMPLEMENTED_YET(); - lp::bound_kind bkind = lp::bound_kind::lower_t; - bool_var bv = null_bool_var; - theory_var v = null_theory_var; - lp::bound* result = alloc(lp::bound, bv, v, k, bkind); - return result; + // create a bound atom representing term <= k + app_ref mk_bound(lean::lar_term const& term, rational const& k) { + SASSERT(k.is_int()); + app_ref t = mk_term(term, true); + app_ref atom(a.mk_le(t, a.mk_numeral(k, true)), m); + TRACE("arith", tout << atom << "\n"; + m_solver->print_term(term, tout << "bound atom: "); tout << " <= " << k << "\n"; + display(tout); + ); + ctx().internalize(atom, true); + ctx().mark_as_relevant(atom.get()); + return atom; } lbool check_lia() { - std::cout << "called check_lia()\n"; + if (m.canceled()) return l_undef; lean::lar_term term; lean::mpq k; lean::explanation ex; // TBD, this should be streamlined accross different explanations switch(m_lia->check(term, k, ex)) { case lean::lia_move::ok: return l_true; - case lean::lia_move::branch: + case lean::lia_move::branch: { + (void)mk_bound(term, k); // branch on term <= k - NOT_IMPLEMENTED_YET(); + // at this point we have a new unassigned atom that the + // SAT core assigns a value to return l_false; - case lean::lia_move::cut: + } + case lean::lia_move::cut: { // m_explanation implies term <= k - m_explanation = ex.m_explanation; - NOT_IMPLEMENTED_YET(); + app_ref b = mk_bound(term, k); + m_eqs.reset(); + m_core.reset(); + m_params.reset(); + for (auto const& ev : ex.m_explanation) { + if (!ev.first.is_zero()) { + set_evidence(ev.second); + } + } + assign(literal(ctx().get_bool_var(b), false)); return l_false; + } case lean::lia_move::conflict: // ex contains unsat core m_explanation = ex.m_explanation; @@ -2030,12 +2054,13 @@ namespace smt { st.coeffs().push_back(rational::one()); init_left_side(st); lean::lconstraint_kind k = lean::EQ; + bool is_int = b.is_int(); switch (b.get_bound_kind()) { case lp::lower_t: - k = is_true ? lean::GE : lean::LT; + k = is_true ? lean::GE : (is_int ? lean::LE : lean::LT); break; case lp::upper_t: - k = is_true ? lean::LE : lean::GT; + k = is_true ? lean::LE : (is_int ? lean::GE : lean::GT); break; } if (k == lean::LT || k == lean::LE) { @@ -2045,7 +2070,15 @@ namespace smt { ++m_stats.m_assert_upper; } auto vi = get_var_index(b.get_var()); - auto ci = m_solver->add_var_bound(vi, k, b.get_value()); + rational bound = b.get_value(); + lean::constraint_index ci; + if (is_int && !is_true) { + rational bound = b.get_value(false).get_rational(); + ci = m_solver->add_var_bound(vi, k, bound); + } + else { + ci = m_solver->add_var_bound(vi, k, b.get_value()); + } TRACE("arith", tout << "v" << b.get_var() << "\n";); add_ineq_constraint(ci, literal(bv, !is_true)); @@ -2499,19 +2532,32 @@ namespace smt { return internalize_def(term); } + app_ref mk_term(lean::lar_term const& term, bool is_int) { + expr_ref_vector args(m); + for (auto & ti : term.m_coeffs) { + theory_var w = m_var_index2theory_var[ti.first]; + expr* o = get_enode(w)->get_owner(); + if (ti.second.is_one()) { + args.push_back(o); + } + else { + args.push_back(a.mk_mul(a.mk_numeral(ti.second, is_int), o)); + } + } + if (!term.m_v.is_zero()) { + args.push_back(a.mk_numeral(term.m_v, is_int)); + } + if (args.size() == 1) { + return app_ref(to_app(args[0].get()), m); + } + return app_ref(a.mk_add(args.size(), args.c_ptr()), m); + } + app_ref mk_obj(theory_var v) { lean::var_index vi = m_theory_var2var_index[v]; bool is_int = a.is_int(get_enode(v)->get_owner()); - if (m_solver->is_term(vi)) { - expr_ref_vector args(m); - const lean::lar_term& term = m_solver->get_term(vi); - for (auto & ti : term.m_coeffs) { - theory_var w = m_var_index2theory_var[ti.first]; - expr* o = get_enode(w)->get_owner(); - args.push_back(a.mk_mul(a.mk_numeral(ti.second, is_int), o)); - } - args.push_back(a.mk_numeral(term.m_v, is_int)); - return app_ref(a.mk_add(args.size(), args.c_ptr()), m); + if (m_solver->is_term(vi)) { + return mk_term(m_solver->get_term(vi), is_int); } else { theory_var w = m_var_index2theory_var[vi]; @@ -2537,7 +2583,7 @@ namespace smt { // ctx().set_enode_flag(bv, true); lp::bound_kind bkind = lp::bound_kind::lower_t; if (is_strict) bkind = lp::bound_kind::upper_t; - lp::bound* a = alloc(lp::bound, bv, v, r, bkind); + lp::bound* a = alloc(lp::bound, bv, v, is_int, r, bkind); mk_bound_axioms(*a); updt_unassigned_bounds(v, +1); m_bounds[v].push_back(a); diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp index e617a1e29..1a6d6ddae 100644 --- a/src/util/lp/int_solver.cpp +++ b/src/util/lp/int_solver.cpp @@ -101,6 +101,186 @@ int int_solver::find_inf_int_boxed_base_column_with_smallest_range() { } +bool int_solver::mk_gomory_cut(unsigned row_index, explanation & ex) { + lean_assert(false); + return true; + /* + const auto & row = m_lar_solver->A_r().m_rows[row_index]; + // The following assertion is wrong. It may be violated in mixed-integer problems. + // SASSERT(!all_coeff_int(r)); + theory_var x_i = r.get_base_var(); + + SASSERT(is_int(x_i)); + // The following assertion is wrong. It may be violated in mixed-real-interger problems. + // The check is_gomory_cut_target will discard rows where any variable contains infinitesimals. + // SASSERT(m_value[x_i].is_rational()); // infinitesimals are not used for integer variables + SASSERT(!m_value[x_i].is_int()); // the base variable is not assigned to an integer value. + + if (constrain_free_vars(r) || !is_gomory_cut_target(r)) { + TRACE("gomory_cut", tout << "failed to apply gomory cut:\n"; + tout << "constrain_free_vars(r): " << constrain_free_vars(r) << "\n";); + return false; + } + + TRACE("gomory_cut", tout << "applying cut at:\n"; display_row_info(tout, r);); + + antecedents ante(*this); + + m_stats.m_gomory_cuts++; + + // gomory will be pol >= k + numeral k(1); + buffer pol; + + numeral f_0 = Ext::fractional_part(m_value[x_i]); + numeral one_minus_f_0 = numeral(1) - f_0; + SASSERT(!f_0.is_zero()); + SASSERT(!one_minus_f_0.is_zero()); + + numeral lcm_den(1); + unsigned num_ints = 0; + + typename vector::const_iterator it = r.begin_entries(); + typename vector::const_iterator end = r.end_entries(); + for (; it != end; ++it) { + if (!it->is_dead() && it->m_var != x_i) { + theory_var x_j = it->m_var; + numeral a_ij = it->m_coeff; + a_ij.neg(); // make the used format compatible with the format used in: Integrating Simplex with DPLL(T) + if (is_real(x_j)) { + numeral new_a_ij; + if (at_lower(x_j)) { + if (a_ij.is_pos()) { + new_a_ij = a_ij / one_minus_f_0; + } + else { + new_a_ij = a_ij / f_0; + new_a_ij.neg(); + } + k.addmul(new_a_ij, lower_bound(x_j).get_rational()); + lower(x_j)->push_justification(ante, new_a_ij, coeffs_enabled()); + } + else { + SASSERT(at_upper(x_j)); + if (a_ij.is_pos()) { + new_a_ij = a_ij / f_0; + new_a_ij.neg(); // the upper terms are inverted. + } + else { + new_a_ij = a_ij / one_minus_f_0; + } + k.addmul(new_a_ij, upper_bound(x_j).get_rational()); + upper(x_j)->push_justification(ante, new_a_ij, coeffs_enabled()); + } + TRACE("gomory_cut_detail", tout << a_ij << "*v" << x_j << " k: " << k << "\n";); + pol.push_back(row_entry(new_a_ij, x_j)); + } + else { + ++num_ints; + SASSERT(is_int(x_j)); + numeral f_j = Ext::fractional_part(a_ij); + TRACE("gomory_cut_detail", + tout << a_ij << "*v" << x_j << "\n"; + tout << "fractional_part: " << Ext::fractional_part(a_ij) << "\n"; + tout << "f_j: " << f_j << "\n"; + tout << "f_0: " << f_0 << "\n"; + tout << "one_minus_f_0: " << one_minus_f_0 << "\n";); + if (!f_j.is_zero()) { + numeral new_a_ij; + if (at_lower(x_j)) { + if (f_j <= one_minus_f_0) { + new_a_ij = f_j / one_minus_f_0; + } + else { + new_a_ij = (numeral(1) - f_j) / f_0; + } + k.addmul(new_a_ij, lower_bound(x_j).get_rational()); + lower(x_j)->push_justification(ante, new_a_ij, coeffs_enabled()); + } + else { + SASSERT(at_upper(x_j)); + if (f_j <= f_0) { + new_a_ij = f_j / f_0; + } + else { + new_a_ij = (numeral(1) - f_j) / one_minus_f_0; + } + new_a_ij.neg(); // the upper terms are inverted + k.addmul(new_a_ij, upper_bound(x_j).get_rational()); + upper(x_j)->push_justification(ante, new_a_ij, coeffs_enabled()); + } + TRACE("gomory_cut_detail", tout << "new_a_ij: " << new_a_ij << " k: " << k << "\n";); + pol.push_back(row_entry(new_a_ij, x_j)); + lcm_den = lcm(lcm_den, denominator(new_a_ij)); + } + } + } + } + + CTRACE("empty_pol", pol.empty(), display_row_info(tout, r);); + + expr_ref bound(get_manager()); + if (pol.empty()) { + SASSERT(k.is_pos()); + // conflict 0 >= k where k is positive + set_conflict(ante, ante, "gomory-cut"); + return true; + } + else if (pol.size() == 1) { + theory_var v = pol[0].m_var; + k /= pol[0].m_coeff; + bool is_lower = pol[0].m_coeff.is_pos(); + if (is_int(v) && !k.is_int()) { + k = is_lower?ceil(k):floor(k); + } + rational _k = k.to_rational(); + if (is_lower) + bound = m_util.mk_ge(get_enode(v)->get_owner(), m_util.mk_numeral(_k, is_int(v))); + else + bound = m_util.mk_le(get_enode(v)->get_owner(), m_util.mk_numeral(_k, is_int(v))); + } + else { + if (num_ints > 0) { + lcm_den = lcm(lcm_den, denominator(k)); + TRACE("gomory_cut_detail", tout << "k: " << k << " lcm_den: " << lcm_den << "\n"; + for (unsigned i = 0; i < pol.size(); i++) { + tout << pol[i].m_coeff << " " << pol[i].m_var << "\n"; + } + tout << "k: " << k << "\n";); + SASSERT(lcm_den.is_pos()); + if (!lcm_den.is_one()) { + // normalize coefficients of integer parameters to be integers. + unsigned n = pol.size(); + for (unsigned i = 0; i < n; i++) { + pol[i].m_coeff *= lcm_den; + SASSERT(!is_int(pol[i].m_var) || pol[i].m_coeff.is_int()); + } + k *= lcm_den; + } + TRACE("gomory_cut_detail", tout << "after *lcm\n"; + for (unsigned i = 0; i < pol.size(); i++) { + tout << pol[i].m_coeff << " * v" << pol[i].m_var << "\n"; + } + tout << "k: " << k << "\n";); + } + mk_polynomial_ge(pol.size(), pol.c_ptr(), k.to_rational(), bound); + } + TRACE("gomory_cut", tout << "new cut:\n" << bound << "\n"; ante.display(tout);); + literal l = null_literal; + context & ctx = get_context(); + ctx.internalize(bound, true); + l = ctx.get_literal(bound); + ctx.mark_as_relevant(l); + dump_lemmas(l, ante); + ctx.assign(l, ctx.mk_justification( + gomory_cut_justification( + get_id(), ctx.get_region(), + ante.lits().size(), ante.lits().c_ptr(), + ante.eqs().size(), ante.eqs().c_ptr(), ante, l))); + return true; + */ + +} lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex) { lean_assert(is_feasible()); init_inf_int_set(); @@ -129,32 +309,35 @@ lia_move int_solver::check(lar_term& t, mpq& k, explanation& ex) { if ((++m_branch_cut_counter) % settings().m_int_branch_cut_threshold == 0) { move_non_base_vars_to_bounds(); - /* - if (!make_feasible()) { - TRACE("arith_int", tout << "failed to move variables to bounds.\n";); - failed(); - return FC_CONTINUE; + lp_status st = m_lar_solver->find_feasible_solution(); + if (st != lp_status::FEASIBLE && st != lp_status::OPTIMAL) { + return lia_move::give_up; } - int int_var = find_inf_int_base_var(); - if (int_var != null_int) { - TRACE("arith_int", tout << "v" << int_var << " does not have an integer assignment: " << get_value(int_var) << "\n";); - SASSERT(is_base(int_var)); - row const & r = m_rows[get_var_row(int_var)]; - if (!mk_gomory_cut(r)) { + int j = find_inf_int_base_column(); + if (j != -1) { + TRACE("arith_int", tout << "j = " << j << " does not have an integer assignment: " << get_value(j) << "\n";); + unsigned row_index = m_lar_solver->m_mpq_lar_core_solver.m_r_heading[j]; + if (!mk_gomory_cut(row_index, ex)) { + return lia_move::give_up; // silent failure } - return FC_CONTINUE; - }*/ + return lia_move::cut; + } } else { int j = find_inf_int_base_column(); - /* if (j != -1) { - TRACE("arith_int", tout << "v" << j << " does not have an integer assignment: " << get_value(j) << "\n";); - // apply branching - branch_infeasible_int_var(int_var); - return false; - }*/ + TRACE("arith_int", tout << "j" << j << " does not have an integer assignment: " << get_value(j) << "\n";); + + lean_assert(t.is_empty()); + t.add_to_map(j, mpq(1)); + k = floor(get_value(j)); + TRACE("arith_int", tout << "branching v" << j << " = " << get_value(j) << "\n"; + display_column(tout, j); + tout << "k = " << k << std::endl; + ); + return lia_move::branch; + } } // return true; return lia_move::give_up; @@ -259,7 +442,6 @@ mpq get_denominators_lcm(iterator_on_row &it) { bool int_solver::gcd_test_for_row(static_matrix> & A, unsigned i, explanation & ex) { iterator_on_row it(A.m_rows[i]); - std::cout << "gcd_test_for_row(" << i << ")\n"; mpq lcm_den = get_denominators_lcm(it); mpq consts(0); mpq gcds(0); @@ -350,8 +532,6 @@ bool int_solver::ext_gcd_test(iterator_on_row & it, mpq const & least_coeff, mpq const & lcm_den, mpq const & consts, explanation& ex) { - - std::cout << "calling ext_gcd_test" << std::endl; mpq gcds(0); mpq l(consts); mpq u(consts); diff --git a/src/util/lp/int_solver.h b/src/util/lp/int_solver.h index 981127bc8..edfba5e5b 100644 --- a/src/util/lp/int_solver.h +++ b/src/util/lp/int_solver.h @@ -96,5 +96,7 @@ private: int find_inf_int_boxed_base_column_with_smallest_range(); lp_settings& settings(); void move_non_base_vars_to_bounds(); + void branch_infeasible_int_var(unsigned); + bool mk_gomory_cut(unsigned row_index, explanation & ex); }; } diff --git a/src/util/lp/lar_term.h b/src/util/lp/lar_term.h index 0e715ad0b..dfdedb571 100644 --- a/src/util/lp/lar_term.h +++ b/src/util/lp/lar_term.h @@ -21,6 +21,10 @@ struct lar_term { } } + bool is_empty() const { + return m_coeffs.size() == 0 && is_zero(m_v); + } + unsigned size() const { return static_cast(m_coeffs.size()); } const std::unordered_map & coeffs() const {