From e2db1418f9fb187c8048f4a2a0616b0d5b6ecc4b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 21 Feb 2014 14:39:54 -0800 Subject: [PATCH] debugging simplex/pb Signed-off-by: Nikolaj Bjorner --- examples/dotnet/Program.cs | 4 +- src/math/simplex/simplex.h | 13 +- src/math/simplex/simplex_def.h | 46 +++++- src/math/simplex/sparse_matrix.h | 1 + src/math/simplex/sparse_matrix_def.h | 17 ++- src/smt/theory_pb.cpp | 209 ++++++++++++++++++++------- src/smt/theory_pb.h | 18 ++- 7 files changed, 235 insertions(+), 73 deletions(-) diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs index 4361cab96..d3fb65200 100644 --- a/examples/dotnet/Program.cs +++ b/examples/dotnet/Program.cs @@ -759,8 +759,10 @@ namespace test_mapi foreach (BoolExpr a in g.Formulas) solver.Assert(a); - if (solver.Check() != Status.SATISFIABLE) + if (solver.Check() != Status.SATISFIABLE) { + Console.WriteLine("{0}",solver); throw new TestFailedException(); +} ApplyResult ar = ApplyTactic(ctx, ctx.MkTactic("simplify"), g); if (ar.NumSubgoals == 1 && (ar.Subgoals[0].IsDecidedSat || ar.Subgoals[0].IsDecidedUnsat)) diff --git a/src/math/simplex/simplex.h b/src/math/simplex/simplex.h index 5a45bbf0a..985d6c608 100644 --- a/src/math/simplex/simplex.h +++ b/src/math/simplex/simplex.h @@ -115,9 +115,19 @@ namespace simplex { void ensure_var(var_t v); row add_row(var_t base, unsigned num_vars, var_t const* vars, numeral const* coeffs); row get_infeasible_row(); + var_t get_base_var(row const& r) const { return m_row2base[r.id()]; } + numeral const& get_base_coeff(row const& r) const { return m_vars[m_row2base[r.id()]].m_base_coeff; } void del_row(row const& r); void set_lower(var_t var, eps_numeral const& b); void set_upper(var_t var, eps_numeral const& b); + void get_lower(var_t var, scoped_eps_numeral& b) const { b = m_vars[var].m_lower; } + void get_upper(var_t var, scoped_eps_numeral& b) const { b = m_vars[var].m_upper; } + bool above_lower(var_t var, eps_numeral const& b) const; + bool below_upper(var_t var, eps_numeral const& b) const; + bool below_lower(var_t v) const; + bool above_upper(var_t v) const; + bool lower_valid(var_t var) const { return m_vars[var].m_lower_valid; } + bool upper_valid(var_t var) const { return m_vars[var].m_upper_valid; } void unset_lower(var_t var); void unset_upper(var_t var); void set_value(var_t var, eps_numeral const& b); @@ -127,6 +137,7 @@ namespace simplex { lbool minimize(var_t var); eps_numeral const& get_value(var_t v); void display(std::ostream& out) const; + void display_row(std::ostream& out, row const& r, bool values = true); unsigned get_num_vars() const { return m_vars.size(); } @@ -159,8 +170,6 @@ namespace simplex { bool at_lower(var_t v) const; bool at_upper(var_t v) const; - bool below_lower(var_t v) const; - bool above_upper(var_t v) const; bool above_lower(var_t v) const; bool below_upper(var_t v) const; bool outside_bounds(var_t v) const { return below_lower(v) || above_upper(v); } diff --git a/src/math/simplex/simplex_def.h b/src/math/simplex/simplex_def.h index a56110287..51405aef5 100644 --- a/src/math/simplex/simplex_def.h +++ b/src/math/simplex/simplex_def.h @@ -47,10 +47,12 @@ namespace simplex { m.set(b, m_vars[v].m_base_coeff); m.lcm(a, b, c); TRACE("simplex", - m.display(tout << "a: ", a); - m.display(tout << "b v" << v << " : ", b); - m.display(tout << "c: ", c); + m.display(tout << " a: ", a); + m.display(tout << " b v" << v << " : ", b); + m.display(tout << " c: ", c); tout << "\n"; + M.display_row(tout, r); + M.display_row(tout, row(m_vars[v].m_base2row)); if (m.is_zero(b)) { display(tout); }); @@ -58,11 +60,11 @@ namespace simplex { m.abs(c); m.div(c, a, b); m.div(c, m_vars[v].m_base_coeff, a); - m.set(mul, a); - m.abs(mul); + m.mul(mul, b, mul); M.mul(r, b); m.neg(a); M.add(r, a, row(m_vars[v].m_base2row)); + TRACE("simplex", M.display_row(tout, r);); } scoped_numeral base_coeff(m); @@ -136,6 +138,18 @@ namespace simplex { M.del(r); } + template + bool simplex::above_lower(var_t var, eps_numeral const& b) const { + var_info const& vi = m_vars[var]; + return !vi.m_lower_valid || em.gt(b, vi.m_lower); + } + + template + bool simplex::below_upper(var_t var, eps_numeral const& b) const { + var_info const& vi = m_vars[var]; + return !vi.m_upper_valid || em.lt(b, vi.m_upper); + } + template void simplex::set_lower(var_t var, eps_numeral const& b) { var_info& vi = m_vars[var]; @@ -206,6 +220,26 @@ namespace simplex { } } + template + void simplex::display_row(std::ostream& out, row const& r, bool values) { + row_iterator it = M.row_begin(r), end = M.row_end(r); + for (; it != end; ++it) { + m.display(out, it->m_coeff); + out << "*v" << it->m_var << " "; + if (values) { + var_info const& vi = m_vars[it->m_var]; + out << em.to_string(vi.m_value); + out << " ["; + if (vi.m_lower_valid) out << em.to_string(vi.m_lower); else out << "-oo"; + out << ":"; + if (vi.m_upper_valid) out << em.to_string(vi.m_upper); else out << "oo"; + out << "] "; + } + } + out << "\n"; + } + + template void simplex::ensure_var(var_t v) { while (v >= m_vars.size()) { @@ -344,6 +378,8 @@ namespace simplex { return vi.m_lower_valid && em.lt(vi.m_value, vi.m_lower); } + + template bool simplex::above_upper(var_t v) const { var_info const& vi = m_vars[v]; diff --git a/src/math/simplex/sparse_matrix.h b/src/math/simplex/sparse_matrix.h index 9705ea56c..e3c00e511 100644 --- a/src/math/simplex/sparse_matrix.h +++ b/src/math/simplex/sparse_matrix.h @@ -235,6 +235,7 @@ namespace simplex { col_iterator col_end(int v) const { return col_iterator(m_columns[v], m_rows, false); } void display(std::ostream& out); + void display_row(std::ostream& out, row const& r); bool well_formed() const; diff --git a/src/math/simplex/sparse_matrix_def.h b/src/math/simplex/sparse_matrix_def.h index d44f0c796..e62fc6c41 100644 --- a/src/math/simplex/sparse_matrix_def.h +++ b/src/math/simplex/sparse_matrix_def.h @@ -554,15 +554,20 @@ namespace simplex { void sparse_matrix::display(std::ostream& out) { for (unsigned i = 0; i < m_rows.size(); ++i) { if (m_rows[i].size() == 0) continue; - row_iterator it = row_begin(row(i)), end = row_end(row(i)); - for (; it != end; ++it) { - m.display(out, it->m_coeff); - out << "*v" << it->m_var << " "; - } - out << "\n"; + display_row(out, row(i)); } } + template + void sparse_matrix::display_row(std::ostream& out, row const& r) { + row_iterator it = row_begin(r), end = row_end(r); + for (; it != end; ++it) { + m.display(out, it->m_coeff); + out << "*v" << it->m_var << " "; + } + out << "\n"; + } + }; diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 08468b792..49944b3c4 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -202,44 +202,140 @@ namespace smt { } }; - class theory_pb::reset_bound : public trail { - theory_pb& pb; - unsigned v; - bool is_lower; - public: - reset_bound(theory_pb& pb, unsigned v, bool is_lower): - pb(pb), v(v), is_lower(is_lower) {} - - virtual void undo(context& ctx) { - if (is_lower) { - pb.m_simplex.unset_lower(v); - } - else { - pb.m_simplex.unset_upper(v); - } - } - }; - class theory_pb::undo_bound : public trail { - theory_pb& pb; - unsigned v; - bool is_lower; + theory_pb& pb; + unsigned m_v; + bool m_is_lower; + scoped_eps_numeral m_last_bound; + bool m_last_bound_valid; + literal m_last_explain; + public: - undo_bound(theory_pb& pb, unsigned v, bool is_lower): - pb(pb), v(v), is_lower(is_lower) {} + undo_bound(theory_pb& pb, unsigned v, + bool is_lower, + scoped_eps_numeral& last_bound, + bool last_bound_valid, + literal last_explain): + pb(pb), + m_v(v), + m_is_lower(is_lower), + m_last_bound(last_bound), + m_last_bound_valid(last_bound_valid), + m_last_explain(last_explain) {} virtual void undo(context& ctx) { - if (is_lower) { - mpq_inf zero(mpq(0),mpq(0)); - pb.m_simplex.set_lower(v, zero); + //std::cout << "undo bound: " << m_v << " " << m_last_explain; + //std::cout << (m_is_lower?" lower ":" upper ") << pb.m_mpq_inf_mgr.to_string(m_last_bound) << "\n"; + if (m_is_lower) { + if (m_last_bound_valid) { + pb.m_simplex.set_lower(m_v, m_last_bound); + } + else { + pb.m_simplex.unset_lower(m_v); + } + pb.set_explain(pb.m_explain_lower, m_v, m_last_explain); } else { - mpq_inf one(mpq(1),mpq(0)); - pb.m_simplex.set_upper(v, one); + if (m_last_bound_valid) { + pb.m_simplex.set_upper(m_v, m_last_bound); + } + else { + pb.m_simplex.unset_upper(m_v); + } + pb.set_explain(pb.m_explain_upper, m_v, m_last_explain); + } + m_last_bound.reset(); + } + }; + + literal theory_pb::set_explain(literal_vector& explains, unsigned var, literal expl) { + if (var >= explains.size()) { + explains.resize(var+1, null_literal); + } + literal last_explain = explains[var]; + explains[var] = expl; + return last_explain; + } + + void theory_pb::update_bound(bool_var v, literal explain, bool is_lower, mpq_inf const& bound) { + // std::cout << v << " " << explain << (is_lower?" lower ":" upper ") << m_mpq_inf_mgr.to_string(bound) << "\n"; + if (is_lower) { + if (m_simplex.above_lower(v, bound)) { + scoped_eps_numeral last_bound(m_mpq_inf_mgr); + bool last_bound_valid = m_simplex.lower_valid(v); + if (last_bound_valid) { + m_simplex.get_lower(v, last_bound); + } + m_simplex.set_lower(v, bound); + literal last_explain = set_explain(m_explain_lower, v, explain); + get_context().push_trail(undo_bound(*this, v, true, last_bound, last_bound_valid, last_explain)); + } + } + else { + if (m_simplex.below_upper(v, bound)) { + scoped_eps_numeral last_bound(m_mpq_inf_mgr); + bool last_bound_valid = m_simplex.upper_valid(v); + if (last_bound_valid) { + m_simplex.get_upper(v, last_bound); + } + m_simplex.set_upper(v, bound); + literal last_explain = set_explain(m_explain_upper, v, explain); + get_context().push_trail(undo_bound(*this, v, false, last_bound, last_bound_valid, last_explain)); } } }; + bool theory_pb::check_feasible() { + lbool is_sat = m_simplex.make_feasible(); + if (l_false != is_sat) { + return true; + } + + row r = m_simplex.get_infeasible_row(); + // m_simplex.display_row(std::cout, r, true); + mpz const& coeff = m_simplex.get_base_coeff(r); + bool_var base_var = m_simplex.get_base_var(r); + SASSERT(m_simplex.below_lower(base_var) || m_simplex.above_upper(base_var)); + bool cant_increase = m_simplex.below_lower(base_var)?m_mpz_mgr.is_pos(coeff):m_mpz_mgr.is_neg(coeff); + + literal_vector explains; + row_iterator it = m_simplex.row_begin(r), end = m_simplex.row_end(r); + for (; it != end; ++it) { + bool_var v = it->m_var; + if (v == base_var) { + if (m_simplex.below_lower(base_var)) { + explains.push_back(m_explain_lower.get(v, null_literal)); + } + else { + explains.push_back(m_explain_upper.get(v, null_literal)); + } + } + else if (cant_increase == m_mpz_mgr.is_pos(it->m_coeff)) { + explains.push_back(m_explain_lower.get(v, null_literal)); + } + else { + explains.push_back(m_explain_upper.get(v, null_literal)); + } + } + + // m_simplex.display(std::cout); + literal_vector lits; + for (unsigned i = 0; i < explains.size(); ++i) { + literal lit(explains[i]); + if (lit != null_literal) { + //std::cout << lit << " "; + lits.push_back(~lit); + } + } + //std::cout << "\n"; + + m_stats.m_num_conflicts++; + justification* js = 0; + get_context().mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0); + + return false; + } + bool theory_pb::internalize_atom(app * atom, bool gate_ctx) { SASSERT(m_util.is_at_most_k(atom) || m_util.is_le(atom) || m_util.is_ge(atom) || m_util.is_at_least_k(atom) || @@ -372,16 +468,29 @@ namespace smt { else { m_ineq_rep.insert(rep, abv); svector vars; - unsynch_mpz_manager mgr; - scoped_mpz_vector coeffs(mgr); + scoped_mpz_vector coeffs(m_mpz_mgr); for (unsigned i = 0; i < rep.size(); ++i) { unsigned v = rep.lit(i).var(); m_simplex.ensure_var(v); vars.push_back(v); if (!m_vars.contains(v)) { mpq_inf zero(mpq(0),mpq(0)), one(mpq(1),mpq(0)); - m_simplex.set_lower(v, zero); - m_simplex.set_upper(v, one); + switch(ctx.get_assignment(rep.lit(i))) { + case l_true: + std::cout << "true\n"; + update_bound(v, literal(v), true, one); + m_simplex.set_upper(v, one); + break; + case l_false: + std::cout << "false\n"; + update_bound(v, literal(v), false, zero); + m_simplex.set_upper(v, zero); + break; + default: + m_simplex.set_lower(v, zero); + m_simplex.set_upper(v, one); + break; + } m_vars.insert(v); ctx.push_trail(remove_var(*this, v)); } @@ -588,16 +697,15 @@ namespace smt { if (m_enable_simplex) { if (is_true) { mpq_inf one(mpq(1),mpq(0)); - m_simplex.set_lower(v, one); + update_bound(v, ~nlit, true, one); } else { mpq_inf zero(mpq(0),mpq(0)); - m_simplex.set_upper(v, zero); + update_bound(v, ~nlit, false, zero); } - ctx.push_trail(undo_bound(*this, v, is_true)); - lbool is_sat = m_simplex.make_feasible(); - if (is_sat == l_false) { - std::cout << "unsat\n"; + + if (!check_feasible()) { + return; } } @@ -620,28 +728,19 @@ namespace smt { if (m_ineqs.find(v, c)) { if (m_enable_simplex) { row_info const& info = m_ineq_row_info.find(v); - unsynch_mpq_inf_manager mgr; - _scoped_numeral coeff(mgr); + scoped_eps_numeral coeff(m_mpq_inf_mgr); coeff = std::make_pair(info.m_bound.to_mpq(), mpq(0)); unsigned slack = info.m_slack; if (is_true) { - m_simplex.set_lower(slack, coeff); + update_bound(slack, literal(v), true, coeff); } else { - mgr.sub(coeff, std::make_pair(mpq(1),mpq(0)), coeff); - m_simplex.set_upper(slack, coeff); + m_mpq_inf_mgr.sub(coeff, std::make_pair(mpq(1),mpq(0)), coeff); + update_bound(slack, ~literal(v), false, coeff); } - ctx.push_trail(reset_bound(*this, slack, is_true)); - lbool is_sat = m_simplex.make_feasible(); - if (l_false == is_sat) { - std::cout << "unsat inequality\n"; - row r = m_simplex.get_infeasible_row(); - row_iterator it = m_simplex.row_begin(r), end = m_simplex.row_end(r); - for (; it != end; ++it) { - it->m_var; - it->m_coeff; - } + if (!check_feasible()) { + return; } } if (c->is_ge()) { @@ -1335,9 +1434,11 @@ namespace smt { c.m_watch_sum = numeral::zero(); c.m_watch_sz = 0; c.m_max_watch = numeral::zero(); - for (unsigned i = 0; c.watch_sum() < c.k() + c.max_watch() && i < c.size(); ++i) { + bool watch_more = c.watch_sum() < c.k() + c.max_watch(); + for (unsigned i = 0; watch_more && i < c.size(); ++i) { if (ctx.get_assignment(c.lit(i)) != l_false) { add_watch(c, i); + watch_more = c.watch_sum() < c.k() + c.max_watch(); } } ctx.push_trail(unwatch_ge(*this, c)); diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index f1bba5405..702fffc90 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -37,13 +37,14 @@ namespace smt { class rewatch_vars; class negate_ineq; class remove_var; - class reset_bound; class undo_bound; typedef rational numeral; typedef vector > arg_t; typedef simplex::simplex simplex; typedef simplex::row row; typedef simplex::row_iterator row_iterator; + typedef unsynch_mpq_inf_manager eps_manager; + typedef _scoped_numeral scoped_eps_numeral; struct stats { unsigned m_num_conflicts; @@ -96,8 +97,8 @@ namespace smt { unsigned watch_size() const { return m_watch_sz; } // variable watch infrastructure - numeral min_sum() const { return m_min_sum; } - numeral max_sum() const { return m_max_sum; } + numeral const& min_sum() const { return m_min_sum; } + numeral const& max_sum() const { return m_max_sum; } unsigned nfixed() const { return m_nfixed; } bool vwatch_initialized() const { return !max_sum().is_zero(); } void vwatch_reset() { m_min_sum.reset(); m_max_sum.reset(); m_nfixed = 0; } @@ -173,8 +174,10 @@ namespace smt { u_map m_ineq_row_info; // Simplex: row information per variable uint_set m_vars; // Simplex: 0-1 variables. simplex m_simplex; // Simplex: tableau - unsigned_vector m_explain_lower; // Simplex: explanations for lower bounds - unsigned_vector m_explain_upper; // Simplex: explanations for upper bounds + literal_vector m_explain_lower; // Simplex: explanations for lower bounds + literal_vector m_explain_upper; // Simplex: explanations for upper bounds + unsynch_mpq_inf_manager m_mpq_inf_mgr; // Simplex: manage inf_mpq numerals + unsynch_mpz_manager m_mpz_mgr; // Simplex: manager mpz numerals unsigned_vector m_ineqs_trail; unsigned_vector m_ineqs_lim; literal_vector m_literals; // temporary vector @@ -204,6 +207,11 @@ namespace smt { void assign_ineq(ineq& c, bool is_true); void assign_eq(ineq& c, bool is_true); + // simplex: + literal set_explain(literal_vector& explains, unsigned var, literal expl); + void update_bound(bool_var v, literal explain, bool is_lower, mpq_inf const& bound); + bool check_feasible(); + std::ostream& display(std::ostream& out, ineq const& c, bool values = false) const; virtual void display(std::ostream& out) const; void display_resolved_lemma(std::ostream& out) const;