mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 17:45:32 +00:00
working on pivot
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
80751bdd12
commit
36cd80748f
6 changed files with 74 additions and 55 deletions
|
|
@ -18,6 +18,7 @@ Author:
|
|||
|
||||
#pragma once
|
||||
|
||||
#include <limits>
|
||||
#include "math/simplex/sparse_matrix.h"
|
||||
#include "util/heap.h"
|
||||
#include "util/lbool.h"
|
||||
|
|
@ -141,7 +142,7 @@ namespace polysat {
|
|||
void update_and_pivot(var_t x_i, var_t x_j, numeral const& a_ij, numeral const& new_value) {}
|
||||
void update_value(var_t v, numeral const& delta) {}
|
||||
void update_value_core(var_t v, numeral const& delta) {}
|
||||
void pivot(var_t x_i, var_t x_j, numeral const& a_ij) {}
|
||||
void pivot(var_t x_i, var_t x_j, numeral a_ij);
|
||||
void move_to_bound(var_t x, bool to_lower) {}
|
||||
var_t select_pivot(var_t x_i, bool is_below, scoped_numeral& out_a_ij) { throw nullptr; }
|
||||
var_t select_pivot_blands(var_t x_i, bool is_below, scoped_numeral& out_a_ij) { throw nullptr; }
|
||||
|
|
@ -169,16 +170,24 @@ namespace polysat {
|
|||
|
||||
struct uint64_ext {
|
||||
typedef uint64_t numeral;
|
||||
static const uint64_t max_numeral = 0; // std::limits<uint64_t>::max();
|
||||
struct manager {
|
||||
typedef uint64_t numeral;
|
||||
void reset() {}
|
||||
void reset(numeral& n) {}
|
||||
void reset(numeral& n) { n = 0; }
|
||||
void del(numeral const& n) {}
|
||||
bool is_zero(numeral const& n) const { return n == 0; }
|
||||
bool is_one(numeral const& n) const { return n == 1; }
|
||||
bool is_minus_one(numeral const& n) const { return max_numeral == n; }
|
||||
void add(numeral const& a, numeral const& b, numeral& r) { r = a + b; }
|
||||
void sub(numeral const& a, numeral const& b, numeral& r) { r = a - b; }
|
||||
void mul(numeral const& a, numeral const& b, numeral& r) { r = a * b; }
|
||||
void set(numeral& r, numeral const& a) { r = a; }
|
||||
void neg(numeral& a) { a = 0 - a; }
|
||||
numeral inv(numeral const& a) { return 0 - a; }
|
||||
void swap(numeral& a, numeral& b) { std::swap(a, b); }
|
||||
};
|
||||
struct scoped_numeral {
|
||||
scoped_numeral(manager& m) { n = 0; }
|
||||
numeral n;
|
||||
numeral& operator()() { return n; }
|
||||
};
|
||||
typedef _scoped_numeral<manager> scoped_numeral;
|
||||
};
|
||||
|
||||
};
|
||||
|
|
|
|||
|
|
@ -46,6 +46,8 @@ namespace polysat {
|
|||
m_row2base.reset();
|
||||
m_left_basis.reset();
|
||||
m_base_vars.reset();
|
||||
|
||||
pivot(0,1, 2);
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
|
|
@ -129,32 +131,14 @@ namespace polysat {
|
|||
}
|
||||
|
||||
/**
|
||||
* make v a basic variable.
|
||||
* If v is already a basic variable in preferred_row, skip
|
||||
* If v
|
||||
* If v is non-basic but basic in a different row, then
|
||||
* eliminate v from one of the rows.
|
||||
* If v if non-basic
|
||||
*/
|
||||
|
||||
template<typename Ext>
|
||||
void fixplex<Ext>::make_basic(var_t v, row const& preferred_row) {
|
||||
numeral c1 = 0;
|
||||
for (auto const& e : M.row_entries(preferred_row)) {
|
||||
if (e.m_var == v) {
|
||||
c1 = e.m_coeff;
|
||||
break;
|
||||
}
|
||||
}
|
||||
auto c2 = m_vars[v].m_base_coeff;
|
||||
auto r2 = m_vars[v].m_base2row;
|
||||
unsigned exp1 = trailing_zeros(c1); // exponent of two for v in r
|
||||
unsigned exp2 = trailing_zeros(c2); // exponent of two for v in r2
|
||||
if (exp1 >= exp2) {
|
||||
// eliminate v from r
|
||||
}
|
||||
else {
|
||||
// eliminate v from r2,
|
||||
// make v the new base for r
|
||||
// perform gauss-jordan for both r and r2 (add to queue)
|
||||
}
|
||||
|
||||
NOT_IMPLEMENTED_YET();
|
||||
|
||||
|
|
@ -189,43 +173,64 @@ namespace polysat {
|
|||
SASSERT(new_value == x_iI.m_value);
|
||||
pivot(x_i, x_j, a_ij);
|
||||
}
|
||||
#endif
|
||||
|
||||
template<typename Ext>
|
||||
void fixplex<Ext>::pivot(var_t x_i, var_t x_j, numeral const& a_ij) {
|
||||
void fixplex<Ext>::pivot(var_t x_i, var_t x_j, numeral a_ij) {
|
||||
++m_stats.m_num_pivots;
|
||||
var_info& x_iI = m_vars[x_i];
|
||||
var_info& x_jI = m_vars[x_j];
|
||||
unsigned r_i = x_iI.m_base2row;
|
||||
m_row2base[r_i] = x_j;
|
||||
x_jI.m_base2row = r_i;
|
||||
x_jI.m_base_coeff = a_ij;
|
||||
unsigned ri = x_iI.m_base2row;
|
||||
m_row2base[ri] = x_j;
|
||||
x_jI.m_base2row = ri;
|
||||
x_jI.m_is_base = true;
|
||||
x_iI.m_is_base = false;
|
||||
row r_i(ri);
|
||||
add_patch(x_j);
|
||||
SASSERT(well_formed_row(row(r_i)));
|
||||
SASSERT(well_formed_row(r_i));
|
||||
|
||||
col_iterator it = M.col_begin(x_j), end = M.col_end(x_j);
|
||||
scoped_numeral a_kj(m), g(m);
|
||||
for (; it != end; ++it) {
|
||||
row r_k = it.get_row();
|
||||
if (r_k.id() != r_i) {
|
||||
a_kj = it.get_row_entry().m_coeff;
|
||||
a_kj.neg();
|
||||
M.mul(r_k, a_ij);
|
||||
M.add(r_k, a_kj, row(r_i));
|
||||
var_t s = m_row2base[r_k.id()];
|
||||
numeral& coeff = m_vars[s].m_base_coeff;
|
||||
m.mul(coeff, a_ij, coeff);
|
||||
M.gcd_normalize(r_k, g);
|
||||
if (!m.is_one(g)) {
|
||||
m.div(coeff, g, coeff);
|
||||
}
|
||||
SASSERT(well_formed_row(row(r_k)));
|
||||
unsigned tz1 = trailing_zeros(a_ij);
|
||||
|
||||
for (auto c : M.col_entries(x_j)) {
|
||||
row r_k = c.get_row();
|
||||
unsigned rk = r_k.id();
|
||||
if (rk == ri)
|
||||
continue;
|
||||
|
||||
numeral a_kj = c.get_row_entry().m_coeff;
|
||||
unsigned tz2 = trailing_zeros(a_kj);
|
||||
if (tz2 >= tz1) {
|
||||
// eliminate x_j from row r_k
|
||||
numeral a = a_ij >> tz1;
|
||||
numeral b = m.inv(a_kj >> (tz2 - tz1));
|
||||
M.mul(r_k, a);
|
||||
M.add(r_k, b, r_i);
|
||||
}
|
||||
else {
|
||||
// eliminate x_j from row r_i
|
||||
// The new base variable for r_i is base of r_k
|
||||
// The new base variable for r_k is x_j.
|
||||
|
||||
numeral a = a_kj >> tz2;
|
||||
numeral b = m.inv(a_ij >> (tz1 - tz2));
|
||||
M.mul(r_i, a);
|
||||
M.add(r_i, b, r_k);
|
||||
unsigned x_k = m_row2base[rk];
|
||||
std::swap(m_row2base[ri], m_row2base[rk]);
|
||||
m_vars[x_j].m_base2row = rk;
|
||||
m_vars[x_k].m_base2row = ri;
|
||||
tz1 = tz2;
|
||||
r_i = r_k;
|
||||
ri = rk;
|
||||
a_ij = a_kj;
|
||||
}
|
||||
SASSERT(well_formed_row(r_k));
|
||||
}
|
||||
SASSERT(well_formed());
|
||||
}
|
||||
|
||||
#if 0
|
||||
|
||||
template<typename Ext>
|
||||
void fixplex<Ext>::update_value(var_t v, eps_numeral const& delta) {
|
||||
if (em.is_zero(delta)) {
|
||||
|
|
|
|||
|
|
@ -250,7 +250,8 @@ namespace simplex {
|
|||
col_iterator & operator++() { ++m_curr; move_to_used(); return *this; }
|
||||
col_iterator operator++(int) { col_iterator tmp = *this; ++*this; return tmp; }
|
||||
bool operator==(col_iterator const & it) const { return m_curr == it.m_curr; }
|
||||
bool operator!=(col_iterator const & it) const { return m_curr != it.m_curr; }
|
||||
bool operator!=(col_iterator const & it) const { return m_curr != it.m_curr; }
|
||||
col_iterator& operator*() { return *this; }
|
||||
};
|
||||
|
||||
col_iterator col_begin(int v) const { return col_iterator(m_columns[v], m_rows, true); }
|
||||
|
|
|
|||
|
|
@ -98,7 +98,7 @@ namespace simplex {
|
|||
if (!t1.is_dead()) {
|
||||
if (i != j) {
|
||||
_row_entry & t2 = m_entries[j];
|
||||
t2.m_coeff.swap(t1.m_coeff);
|
||||
m.swap(t2.m_coeff, t1.m_coeff);
|
||||
t2.m_var = t1.m_var;
|
||||
t2.m_col_idx = t1.m_col_idx;
|
||||
SASSERT(!t2.is_dead());
|
||||
|
|
|
|||
|
|
@ -88,6 +88,8 @@ public:
|
|||
|
||||
void neg(mpf & o);
|
||||
void neg(mpf const & x, mpf & o);
|
||||
|
||||
void swap(mpf& a, mpf& b) { a.swap(b); }
|
||||
|
||||
bool is_zero(mpf const & x);
|
||||
bool is_neg(mpf const & x);
|
||||
|
|
|
|||
|
|
@ -61,11 +61,13 @@ public:
|
|||
}
|
||||
|
||||
void swap(_scoped_numeral & n) {
|
||||
m_num.swap(n.m_num);
|
||||
m().swap(m_num, n.m_num);
|
||||
// m_num.swap(n.m_num);
|
||||
}
|
||||
|
||||
void swap(numeral & n) {
|
||||
m_num.swap(n);
|
||||
m().swap(m_num, n);
|
||||
// m_num.swap(n);
|
||||
}
|
||||
|
||||
_scoped_numeral & operator+=(numeral const & a) {
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue