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

fix row pivot/del

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-05-10 19:53:34 -07:00
parent 0b6c7cd7b4
commit be7b964206
2 changed files with 27 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -217,11 +217,11 @@ namespace polysat {
template<typename Ext>
void fixplex<Ext>::del_row(row const& r) {
var_t var = m_row2base[r.id()];
var_t var = m_rows[r.id()].m_base;
m_vars[var].m_is_base = false;
m_vars[var].lo = 0;
m_vars[var].hi = 0;
m_row2base[r.id()] = null_var;
m_rows[r.id()].m_base = null_var;
M.del(r);
SASSERT(M.col_begin(var) == M.col_end(var));
SASSERT(well_formed());
@ -240,7 +240,7 @@ namespace polysat {
for (auto c : M.col_entries(var)) {
unsigned tzc = m.trailing_zeros(c.get_row_entry().coeff());
if (tzc < tz) {
r = c.get_row_entry();
r = c.get_row();
tz = tzc;
coeff = c.get_row_entry().coeff();
if (tz == 0)
@ -249,7 +249,7 @@ namespace polysat {
}
if (tz == UINT_MAX)
return;
var_t old_base = m_row2base[r.id()];
var_t old_base = m_rows[r.id()].m_base;
numeral new_value;
var_info& vi = m_vars[old_base];
if (!vi.contains(value(old_base)))
@ -626,10 +626,10 @@ namespace polysat {
unsigned tz2 = m.trailing_zeros(c);
SASSERT(tz1 <= tz2);
numeral b1 = b >> tz1;
numeral c1 = m.inv(c >> (tz2 - tz1));
numeral c1 = 0 - (c >> (tz2 - tz1));
M.mul(r_z, b1);
M.add(r_z, c1, r_x);
row_z.m_value = (b1 * (row_z.m_value - old_value_y)) + c1 * row_x.m_value;
row_z.m_value = (b1 * (row_z.m_value - c * old_value_y)) + c1 * row_x.m_value;
row_z.m_base_coeff *= b1;
set_base_value(z);
SASSERT(well_formed_row(r_z));
@ -951,7 +951,7 @@ namespace polysat {
for (unsigned i = 0; i < m_vars.size(); ++i) {
var_info const& vi = m_vars[i];
out << "v" << i << " " << pp(value(i)) << " " << vi << " ";
if (vi.m_is_base) out << "b:" << vi.m_base2row << " ";
if (vi.m_is_base) out << "b:" << vi.m_base2row << " " << pp(m_rows[vi.m_base2row].m_value) << " ";
out << "\n";
}
return out;
@ -965,7 +965,7 @@ namespace polysat {
out << pp(e.coeff()) << " * ";
out << "v" << v << " ";
if (values)
out << pp(value(v)) << " " << m_vars[v];
out << pp(value(v)) << " " << m_vars[v] << " ";
}
return out << "\n";
}

19
src/test/fixplex.cpp
View file

@ -81,6 +81,23 @@ namespace polysat {
fp.reset();
}
static void test5() {
std::cout << "test5\n";
scoped_fp fp;
var_t x = 0, y = 1, z = 2, u = 3;
var_t ys[3] = { x, y, z };
numeral coeffs[3] = { 1, 1, 1 };
fp.add_row(x, 3, ys, coeffs);
fp.set_bounds(x, 3, 4);
fp.set_bounds(y, 3, 6);
var_t ys2[3] = { u, y, z };
fp.add_row(u, 3, ys2, coeffs);
fp.run();
fp.del_row(x);
std::cout << fp << "\n";
}
static void test_interval() {
interval<uint64_t> i1(1, 2);
interval<uint64_t> i2(3, 6);
@ -112,6 +129,8 @@ void tst_fixplex() {
polysat::test2();
polysat::test3();
polysat::test4();
polysat::test5();
polysat::test_interval();
polysat::test_gcd();
}