mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-04-27 22:52:59 -07:00
parent 9e505d60f0
commit efbb382646
4 changed files with 64 additions and 49 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/math/polysat/eq_constraint.cpp
View file

@ -48,6 +48,7 @@ namespace polysat {
if (is_negative())
return diseq_resolve(s, v);
UNREACHABLE();
return nullptr;
}
void eq_constraint::narrow(solver& s) {
@ -63,6 +64,7 @@ namespace polysat {
if (is_negative())
return p().is_zero();
UNREACHABLE();
return false;
}
bool eq_constraint::is_currently_false(solver& s) {
@ -72,6 +74,7 @@ namespace polysat {
if (is_negative())
return r.is_zero();
UNREACHABLE();
return false;
}
bool eq_constraint::is_currently_true(solver& s) {
@ -81,6 +84,7 @@ namespace polysat {
if (is_negative())
return r.is_never_zero();
UNREACHABLE();
return false;
}
/**
@ -148,6 +152,7 @@ namespace polysat {
constraint* eq_constraint::diseq_resolve(solver& s, pvar v) {
NOT_IMPLEMENTED_YET();
return nullptr;
}
void eq_constraint::diseq_narrow(solver& s) {

15
src/math/polysat/fixplex.h
View file

@ -68,6 +68,12 @@ namespace polysat {
{}
};
struct row_info {
var_t m_base;
numeral m_value;
numeral m_base_coeff;
};
static const var_t null_var = 0;
reslimit& m_limit;
mutable manager m;
@ -75,7 +81,7 @@ namespace polysat {
unsigned m_max_iterations;
var_heap m_to_patch;
vector<var_info> m_vars;
svector<var_t> m_row2base;
vector<row_info> m_rows;
bool m_bland;
unsigned m_blands_rule_threshold;
random_gen m_random;
@ -99,7 +105,7 @@ namespace polysat {
typedef typename matrix::row_iterator row_iterator;
typedef typename matrix::col_iterator col_iterator;
var_t get_base_var(row const& r) const { return m_row2base[r.id()]; }
var_t get_base_var(row const& r) const { return m_rows[r.id()].m_base; }
numeral const& get_lo(var_t var) const { return m_vars[var].m_lo; }
numeral const& get_hi(var_t var) const { return m_vars[var].m_hi; }
void set_max_iterations(unsigned n) { m_max_iterations = n; }
@ -130,6 +136,8 @@ namespace polysat {
void gauss_jordan();
void make_basic(var_t v, row const& r);
void update_value_core(var_t v, numeral const& delta);
// TBD:
void del_row(row const& r) {}
@ -140,8 +148,7 @@ namespace polysat {
void check_blands_rule(var_t v, unsigned& num_repeated) {}
bool make_var_feasible(var_t x_i) { return false; }
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 update_value(var_t v, numeral const& delta);
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; }

91
src/math/polysat/fixplex_def.h
View file

@ -43,7 +43,7 @@ namespace polysat {
M.reset();
m_to_patch.reset();
m_vars.reset();
m_row2base.reset();
m_rows.reset();
m_left_basis.reset();
m_base_vars.reset();
@ -101,13 +101,14 @@ namespace polysat {
}
SASSERT(base_coeff != 0);
SASSERT(!is_base(base_var));
while (m_row2base.size() <= r.id())
m_row2base.push_back(null_var);
m_row2base[r.id()] = base_var;
while (m_rows.size() <= r.id())
m_rows.push_back(row_info());
m_rows[r.id()].m_base = base_var;
m_rows[r.id()].m_base_coeff = base_coeff;
m_rows[r.id()].m_value = value;
m_vars[base_var].m_base2row = r.id();
m_vars[base_var].m_is_base = true;
m_vars[base_var].m_base_coeff = base_coeff;
m_vars[base_var].m_value = value / base_coeff;
m_vars[base_var].m_value = 0 - (value / base_coeff);
// TBD: record when base_coeff does not divide value
add_patch(base_var);
if (!m_base_vars.empty()) {
@ -118,6 +119,38 @@ namespace polysat {
return r;
}
/**
* increment v by delta
*/
template<typename Ext>
void fixplex<Ext>::update_value(var_t v, numeral const& delta) {
if (delta == 0)
return;
m_vars[v].m_value += delta;
if (is_base(v)) {
add_patch(v);
return;
}
//
// v <- v + delta
// s*s_coeff + R = 0, where R contains v*v_coeff
// ->
// R.value += delta*v_coeff
// s.value = - R.value / s_coeff
//
for (auto c : M.col_entries(v)) {
row r = c.get_row();
row_info& ri = m_rows[r.id()];
var_t s = ri.m_base;
var_info& si = m_vars[s];
ri.m_value += delta * c.get_row_entry().m_coeff;
si.m_value = 0 - (ri.m_value / ri.m_base_coeff);
add_patch(s);
}
}
template<typename Ext>
void fixplex<Ext>::gauss_jordan() {
while (!m_base_vars.empty()) {
@ -181,7 +214,9 @@ namespace polysat {
var_info& x_iI = m_vars[x_i];
var_info& x_jI = m_vars[x_j];
unsigned ri = x_iI.m_base2row;
m_row2base[ri] = x_j;
m_rows[ri].m_base = x_j;
m_rows[ri].m_value = 0; // TBD
m_rows[ri].m_base_coeff = a_ij;
x_jI.m_base2row = ri;
x_jI.m_is_base = true;
x_iI.m_is_base = false;
@ -215,8 +250,10 @@ namespace polysat {
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]);
unsigned x_k = m_row[rk].m_base;
// TBD: redo according to slides
// TBD: std::swap(m_row2base[ri], m_row2base[rk]);
m_vars[x_j].m_base2row = rk;
m_vars[x_k].m_base2row = ri;
tz1 = tz2;
@ -230,42 +267,6 @@ namespace polysat {
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)) {
return;
}
update_value_core(v, delta);
col_iterator it = M.col_begin(v), end = M.col_end(v);
// v <- v + delta
// s*s_coeff + v*v_coeff + R = 0
// ->
// (v + delta)*v_coeff + (s - delta*v_coeff/s_coeff)*v + R = 0
for (; it != end; ++it) {
row r = it.get_row();
var_t s = m_row2base[r.id()];
var_info& si = m_vars[s];
scoped_eps_numeral delta2(em);
numeral const& coeff = it.get_row_entry().m_coeff;
em.mul(delta, coeff, delta2);
em.div(delta2, si.m_base_coeff, delta2);
delta2.neg();
update_value_core(s, delta2);
}
}
template<typename Ext>
void fixplex<Ext>::update_value_core(var_t v, eps_numeral const& delta) {
eps_numeral& val = m_vars[v].m_value;
em.add(val, delta, val);
if (is_base(v)) {
add_patch(v);
}
}
#endif
}

2
src/math/polysat/ule_constraint.cpp
View file

@ -114,6 +114,7 @@ namespace polysat {
if (is_negative())
return lhs.is_val() && rhs.is_val() && !(lhs.val() > rhs.val());
UNREACHABLE();
return false;
}
bool ule_constraint::is_always_false() {
@ -134,6 +135,7 @@ namespace polysat {
if (is_negative())
return p.is_val() && q.is_val() && p.val() > q.val();
UNREACHABLE();
return false;
}
}