diff --git a/src/math/simplex/simplex_def.h b/src/math/simplex/simplex_def.h index 3f1d7cdb0..285cb24ac 100644 --- a/src/math/simplex/simplex_def.h +++ b/src/math/simplex/simplex_def.h @@ -161,6 +161,7 @@ namespace simplex { template lbool simplex::make_feasible() { + TRACE("simplex", tout << "\n";); m_left_basis.reset(); m_infeasible_var = null_var; unsigned num_iterations = 0; @@ -168,6 +169,7 @@ namespace simplex { var_t v = null_var; SASSERT(well_formed()); while ((v = select_var_to_fix()) != null_var) { + TRACE("simplex", tout << "v" << v << "\n";); if (m_cancel || num_iterations > m_max_iterations) { return l_undef; } diff --git a/src/math/simplex/sparse_matrix.h b/src/math/simplex/sparse_matrix.h index d16d1d1cf..9705ea56c 100644 --- a/src/math/simplex/sparse_matrix.h +++ b/src/math/simplex/sparse_matrix.h @@ -106,8 +106,9 @@ namespace simplex { svector m_entries; unsigned m_size; int m_first_free_idx; + mutable unsigned m_refs; - column():m_size(0), m_first_free_idx(-1) {} + column():m_size(0), m_first_free_idx(-1), m_refs(0) {} unsigned size() const { return m_size; } unsigned num_entries() const { return m_entries.size(); } void reset(); @@ -160,9 +161,9 @@ namespace simplex { class row_iterator { friend sparse_matrix; unsigned m_curr; - _row & m_row; + _row & m_row; void move_to_used() { - while (m_curr < m_row.m_entries.size() && + while (m_curr < m_row.num_entries() && m_row.m_entries[m_curr].is_dead()) { ++m_curr; } @@ -173,7 +174,7 @@ namespace simplex { move_to_used(); } else { - m_curr = m_row.m_entries.size(); + m_curr = m_row.num_entries(); } } public: @@ -192,25 +193,32 @@ namespace simplex { class col_iterator { friend sparse_matrix; - unsigned m_curr; - column const& m_col; + unsigned m_curr; + column const& m_col; vector<_row> const& m_rows; void move_to_used() { - while (m_curr < m_col.m_entries.size() && m_col.m_entries[m_curr].is_dead()) { + while (m_curr < m_col.num_entries() && m_col.m_entries[m_curr].is_dead()) { ++m_curr; } } col_iterator(column const& c, vector<_row> const& r, bool begin): m_curr(0), m_col(c), m_rows(r) { + ++m_col.m_refs; if (begin) { move_to_used(); } else { - m_curr = m_col.m_entries.size(); + m_curr = m_col.num_entries(); } } public: - row get_row() { return row(m_col.m_entries[m_curr].m_row_id); } + ~col_iterator() { + --m_col.m_refs; + } + + row get_row() { + return row(m_col.m_entries[m_curr].m_row_id); + } row_entry const& get_row_entry() { col_entry const& c = m_col.m_entries[m_curr]; int row_id = c.m_row_id; diff --git a/src/math/simplex/sparse_matrix_def.h b/src/math/simplex/sparse_matrix_def.h index a170ee47f..d44f0c796 100644 --- a/src/math/simplex/sparse_matrix_def.h +++ b/src/math/simplex/sparse_matrix_def.h @@ -200,7 +200,7 @@ namespace simplex { */ template inline void sparse_matrix::column::compress_if_needed(vector<_row> & rows) { - if (size() * 2 < num_entries()) { + if (size() * 2 < num_entries() && m_refs == 0) { compress(rows); } } diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index e72223118..74fe48650 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -30,6 +30,7 @@ namespace opt { lbool is_sat; m_msolver = 0; m_s = &s; + IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";); if (m_soft_constraints.empty()) { TRACE("opt", tout << "no constraints\n";); m_msolver = 0; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index b17f1ba29..3399854a5 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -29,6 +29,9 @@ Notes: #include "elim01_tactic.h" #include "solve_eqs_tactic.h" #include "simplify_tactic.h" +#include "propagate_values_tactic.h" +#include "solve_eqs_tactic.h" +#include "elim_uncnstr_tactic.h" #include "tactical.h" #include "model_smt2_pp.h" @@ -93,11 +96,13 @@ namespace opt { s.assert_expr(m_hard_constraints[i].get()); } + IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n";); lbool is_sat = s.check_sat_core(0,0); if (is_sat != l_true) { m_model = 0; return is_sat; } + IF_VERBOSE(1, verbose_stream() << "(optimize:sat)\n";); s.get_model(m_model); m_optsmt.setup(s); update_lower(); @@ -299,7 +304,12 @@ namespace opt { for (unsigned i = 0; i < fmls.size(); ++i) { g->assert_expr(fmls[i].get()); } - tactic_ref tac0 = mk_simplify_tactic(m); + tactic_ref tac0 = + and_then(mk_simplify_tactic(m), + mk_propagate_values_tactic(m), + mk_solve_eqs_tactic(m), + mk_elim_uncnstr_tactic(m), + mk_simplify_tactic(m)); tactic_ref tac2 = mk_elim01_tactic(m); tactic_ref tac3 = mk_lia2card_tactic(m); tactic_ref tac; @@ -317,6 +327,7 @@ namespace opt { SASSERT(result.size() == 1); goal* r = result[0]; fmls.reset(); + expr_ref tmp(m); for (unsigned i = 0; i < r->size(); ++i) { fmls.push_back(r->form(i)); } diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 3a895446d..c1fc60de2 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -118,7 +118,7 @@ namespace opt { void optsmt::update_lower(unsigned idx, rational const& r) { inf_eps v(r); if (m_lower[idx] < v) { - m_lower[idx] = v; + m_lower[idx] = v; if (m_s) m_s->get_model(m_model); } } @@ -229,6 +229,7 @@ namespace opt { } lbool optsmt::lex(unsigned obj_index) { + IF_VERBOSE(1, verbose_stream() << "(optsmt:lex)\n";); solver::scoped_push _push(*m_s); SASSERT(obj_index < m_vars.size()); return basic_lex(obj_index); @@ -238,6 +239,7 @@ namespace opt { lbool is_sat = l_true; expr_ref block(m); + while (is_sat == l_true && !m_cancel) { is_sat = m_s->check_sat(0, 0); if (is_sat != l_true) break; diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index f21ec9dc6..67b9d9472 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -595,7 +595,9 @@ namespace smt { } ctx.push_trail(undo_bound(*this, v, is_true)); lbool is_sat = m_simplex.make_feasible(); - std::cout << is_sat << "\n"; + if (is_sat == l_false) { + std::cout << "unsat\n"; + } } for (unsigned i = 0; i < ineqs->size(); ++i) { @@ -632,6 +634,7 @@ namespace smt { 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) { diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index 238ed5558..f1bba5405 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -173,6 +173,8 @@ 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 unsigned_vector m_ineqs_trail; unsigned_vector m_ineqs_lim; literal_vector m_literals; // temporary vector