3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00

working on stand-alone simplex

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-01-26 20:25:36 -08:00
parent c14c65465a
commit 363af825c0
4 changed files with 32 additions and 6 deletions

View file

@ -29,9 +29,13 @@ namespace simplex {
for (unsigned i = 0; !found && i < num_vars; ++i) found = vars[i] == base;
SASSERT(found);
);
scoped_numeral base_coeff(m);
row r = M.mk_row();
for (unsigned i = 0; i < num_vars; ++i) {
M.add(r, coeffs[i], vars[i]);
if (vars[i] == base) {
m.set(base_coeff, coeffs[i]);
}
}
while (m_row2base.size() <= r.id()) {
m_row2base.push_back(null_var);
@ -39,6 +43,7 @@ namespace simplex {
m_row2base[r.id()] = base;
m_vars[base].m_base2row = r.id();
m_vars[base].m_is_base = true;
m.set(m_vars[base].m_base_coeff, base_coeff);
return r;
}
@ -54,7 +59,8 @@ namespace simplex {
var_info& vi = m_vars[var];
em.set(vi.m_lower, b);
vi.m_lower_valid = true;
if (em.lt(vi.m_value, b)) {
SASSERT(!vi.m_upper_valid || em.le(b, vi.m_upper));
if (!vi.m_is_base && em.lt(vi.m_value, b)) {
scoped_eps_numeral delta(em);
em.sub(b, vi.m_value, delta);
update_value(var, delta);
@ -66,7 +72,8 @@ namespace simplex {
var_info& vi = m_vars[var];
em.set(vi.m_upper, b);
vi.m_upper_valid = true;
if (em.gt(vi.m_value, b)) {
SASSERT(!vi.m_lower_valid || em.le(vi.m_lower, b));
if (!vi.m_is_base && em.gt(vi.m_value, b)) {
scoped_eps_numeral delta(em);
em.sub(b, vi.m_value, delta);
update_value(var, delta);
@ -102,13 +109,13 @@ namespace simplex {
for (unsigned i = 0; i < m_vars.size(); ++i) {
var_info const& vi = m_vars[i];
out << "v" << i << " ";
if (vi.m_is_base) out << "b:" << vi.m_base2row << " ";
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 << "]";
if (vi.m_is_base) out << " b:" << vi.m_base2row;
out << "\n";
}
}
@ -176,8 +183,9 @@ namespace simplex {
var_info& x_iI = m_vars[x_i];
var_info& x_jI = m_vars[x_j];
unsigned r_i = x_iI.m_base2row;
x_jI.m_base2row = r_i;
m_row2base[r_i] = x_j;
x_jI.m_base2row = r_i;
m.set(x_jI.m_base_coeff, a_ij);
x_jI.m_is_base = true;
x_iI.m_is_base = false;
if (outside_bounds(x_j)) {

View file

@ -1359,7 +1359,8 @@ namespace smt {
SASSERT(valid_row_assignment());
SASSERT(satisfy_bounds());
result = skipped_row?BEST_EFFORT:OPTIMIZED;
break; }
break;
}
if (x_i == null_theory_var) {
// can increase/decrease x_j as much as we want.

View file

@ -218,6 +218,7 @@ int main(int argc, char ** argv) {
TST(expr_substitution);
TST(sorting_network);
TST(theory_pb);
TST(simplex);
}
void initialize_mam() {}

View file

@ -2,6 +2,7 @@
#include "sparse_matrix_def.h"
#include "simplex.h"
#include "simplex_def.h"
#include "mpq_inf.h"
typedef simplex::simplex<simplex::mpz_ext> Simplex;
@ -9,9 +10,13 @@ void tst_simplex() {
simplex::sparse_matrix<simplex::mpz_ext> M;
Simplex S;
S.make_feasible();
std::cout << "simplex\n";
lbool is_sat = S.make_feasible();
std::cout << "feasible: " << is_sat << "\n";
unsynch_mpz_manager m;
unsynch_mpq_inf_manager em;
scoped_mpz_vector coeffs(m);
svector<unsigned> vars;
for (unsigned i = 0; i < 5; ++i) {
@ -21,4 +26,15 @@ void tst_simplex() {
}
Simplex::row r = S.add_row(1, coeffs.size(), vars.c_ptr(), coeffs.c_ptr());
is_sat = S.make_feasible();
std::cout << "feasible: " << is_sat << "\n";
S.display(std::cout);
_scoped_numeral<unsynch_mpq_inf_manager> num(em);
num = std::make_pair(mpq(1), mpq(0));
S.set_lower(0, num);
S.set_upper(0, num);
is_sat = S.make_feasible();
std::cout << "feasible: " << is_sat << "\n";
S.display(std::cout);
}