mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

adding simplex

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-02-12 20:20:52 -08:00
parent a594597906
commit 51cb63b6c0
8 changed files with 42 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/math/simplex/simplex_def.h
View file

@ -161,6 +161,7 @@ namespace simplex {
template<typename Ext>
lbool simplex<Ext>::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;
}

26
src/math/simplex/sparse_matrix.h
View file

@ -106,8 +106,9 @@ namespace simplex {
svector<col_entry> 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;

2
src/math/simplex/sparse_matrix_def.h
View file

@ -200,7 +200,7 @@ namespace simplex {
*/
template<typename Ext>
inline void sparse_matrix<Ext>::column::compress_if_needed(vector<_row> & rows) {
if (size() * 2 < num_entries()) {
if (size() * 2 < num_entries() && m_refs == 0) {
compress(rows);
}
}

1
src/opt/maxsmt.cpp
View file

@ -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;

13
src/opt/opt_context.cpp
View file

@ -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));
}

4
src/opt/optsmt.cpp
View file

@ -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;

5
src/smt/theory_pb.cpp
View file

@ -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) {

2
src/smt/theory_pb.h
View file

@ -173,6 +173,8 @@ namespace smt {
u_map<row_info> 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