mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-16 02:46:16 +00:00
Code Activity

working on simplex

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-02-02 14:11:35 +01:00
parent 9ba4b532f6
commit 480ec049c0
3 changed files with 29 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -97,6 +97,7 @@ namespace simplex {
unsigned m_blands_rule_threshold; unsigned m_blands_rule_threshold;
random_gen m_random; random_gen m_random;
uint_set m_left_basis; uint_set m_left_basis;
unsigned m_infeasible_var;
public: public:
simplex(): simplex():
@ -112,6 +113,7 @@ namespace simplex {
void ensure_var(var_t v); void ensure_var(var_t v);
row add_row(var_t base, unsigned num_vars, var_t const* vars, numeral const* coeffs); row add_row(var_t base, unsigned num_vars, var_t const* vars, numeral const* coeffs);
row get_infeasible_row();
void del_row(row const& r); void del_row(row const& r);
void set_lower(var_t var, eps_numeral const& b); void set_lower(var_t var, eps_numeral const& b);
void set_upper(var_t var, eps_numeral const& b); void set_upper(var_t var, eps_numeral const& b);

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

@ -24,11 +24,6 @@ namespace simplex {
template<typename Ext> template<typename Ext>
typename simplex<Ext>::row typename simplex<Ext>::row
simplex<Ext>::add_row(var_t base, unsigned num_vars, var_t const* vars, numeral const* coeffs) { simplex<Ext>::add_row(var_t base, unsigned num_vars, var_t const* vars, numeral const* coeffs) {
DEBUG_CODE(
bool found = false;
for (unsigned i = 0; !found && i < num_vars; ++i) found = vars[i] == base;
SASSERT(found);
);
scoped_numeral base_coeff(m); scoped_numeral base_coeff(m);
scoped_eps_numeral value(em), tmp(em); scoped_eps_numeral value(em), tmp(em);
row r = M.mk_row(); row r = M.mk_row();
@ -49,7 +44,7 @@ namespace simplex {
em.neg(value); em.neg(value);
em.div(value, base_coeff, value); em.div(value, base_coeff, value);
SASSERT(!m.is_zero(base_coeff)); SASSERT(!m.is_zero(base_coeff));
SASSERT(!m_vars[base].m_is_base); SASSERT(!is_base(base));
while (m_row2base.size() <= r.id()) { while (m_row2base.size() <= r.id()) {
m_row2base.push_back(null_var); m_row2base.push_back(null_var);
} }
@ -63,6 +58,14 @@ namespace simplex {
return r; return r;
} }
template<typename Ext>
typename simplex<Ext>::row
simplex<Ext>::get_infeasible_row() {
SASSERT(is_base(m_infeasible_var));
unsigned row_id = m_vars[m_infeasible_var].m_base2row;
return row(row_id);
}
template<typename Ext> template<typename Ext>
void simplex<Ext>::add_patch(var_t v) { void simplex<Ext>::add_patch(var_t v) {
SASSERT(is_base(v)); SASSERT(is_base(v));
@ -140,10 +143,10 @@ namespace simplex {
if (vi.m_upper_valid) out << em.to_string(vi.m_upper); else out << "oo"; if (vi.m_upper_valid) out << em.to_string(vi.m_upper); else out << "oo";
out << "] "; out << "] ";
if (vi.m_is_base) out << "b:" << vi.m_base2row << " "; if (vi.m_is_base) out << "b:" << vi.m_base2row << " ";
col_iterator it = M.col_begin(i), end = M.col_end(i); //col_iterator it = M.col_begin(i), end = M.col_end(i);
for (; it != end; ++it) { //for (; it != end; ++it) {
out << "r" << it.get_row().id() << " "; // out << "r" << it.get_row().id() << " ";
} //}
out << "\n"; out << "\n";
} }
} }
@ -159,6 +162,7 @@ namespace simplex {
template<typename Ext> template<typename Ext>
lbool simplex<Ext>::make_feasible() { lbool simplex<Ext>::make_feasible() {
m_left_basis.reset(); m_left_basis.reset();
m_infeasible_var = null_var;
unsigned num_iterations = 0; unsigned num_iterations = 0;
unsigned num_repeated = 0; unsigned num_repeated = 0;
var_t v = null_var; var_t v = null_var;
@ -169,6 +173,7 @@ namespace simplex {
} }
check_blands_rule(v, num_repeated); check_blands_rule(v, num_repeated);
if (!make_var_feasible(v)) { if (!make_var_feasible(v)) {
m_infeasible_var = v;
return l_false; return l_false;
} }
++num_iterations; ++num_iterations;
@ -529,6 +534,7 @@ namespace simplex {
pivot(x_i, x_j, a_ij); pivot(x_i, x_j, a_ij);
move_to_bound(x_i, inc == m.is_pos(a_ij)); move_to_bound(x_i, inc == m.is_pos(a_ij));
SASSERT(well_formed_row(row(m_vars[x_j].m_base2row)));
} }
return l_true; return l_true;
} }

14
src/test/simplex.cpp
View file

@ -78,9 +78,6 @@ void add_row(Simplex& S, vector<R> const& _v, R const& _b, bool is_eq = false) {
mpq_inf one(mpq(1),mpq(0)); mpq_inf one(mpq(1),mpq(0));
mpq_inf zero(mpq(0),mpq(0)); mpq_inf zero(mpq(0),mpq(0));
SASSERT(vars.size() == coeffs.size()); SASSERT(vars.size() == coeffs.size());
std::cout << coeffs.size() << " " << nv << "\n";
for (unsigned i = 0; i < vars.size(); ++i) std::cout << vars[i] << " ";
std::cout << "\n";
S.set_lower(nv, zero); S.set_lower(nv, zero);
if (is_eq) S.set_upper(nv, zero); if (is_eq) S.set_upper(nv, zero);
S.set_lower(nv+1, one); S.set_lower(nv+1, one);
@ -119,6 +116,16 @@ static void test3() {
feas(S); feas(S);
} }
static void test4() {
Simplex S;
add_row(S, vec(1, 0), R(1));
add_row(S, vec(0, -1), R(-1));
add_row(S, vec(1, 1), R(1), true);
feas(S);
}
void tst_simplex() { void tst_simplex() {
Simplex S; Simplex S;
@ -153,4 +160,5 @@ void tst_simplex() {
test1(); test1();
test2(); test2();
test3(); test3();
test4();
} }