mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-15 15:25:26 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-08-11 21:40:23 -07:00
parent 524ebed44f
commit f1f5b9e311
3 changed files with 64 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -530,27 +530,34 @@ namespace polysat {
void fixplex<Ext>::set_bounds(var_t v, numeral const& l, numeral const& h, unsigned dep) {
ensure_var(v);
update_bounds(v, l, h, mk_leaf(dep));
}
template<typename Ext>
void fixplex<Ext>::update_bounds(var_t v, numeral const& l, numeral const& h, u_dependency* dep) {
if (inconsistent())
return;
auto lo0 = m_vars[v].lo;
auto hi0 = m_vars[v].hi;
m_stashed_bounds.push_back(stashed_bound(v, m_vars[v]));
m_trail.push_back(trail_i::set_bound_i);
std::cout << "new bound " << v << " " << m_vars[v] << " " << mod_interval<numeral>(l, h) << " -> ";
m_vars[v] &= mod_interval(l, h);
if (lo0 != m_vars[v].lo)
m_vars[v].m_lo_dep = dep;
if (hi0 != m_vars[v].hi)
m_vars[v].m_hi_dep = dep;
std::cout << m_vars[v] << "\n";
if (m_vars[v].is_empty()) {
conflict(m_vars[v].m_lo_dep, m_vars[v].m_hi_dep);
return;
}
if (in_bounds(v))
return;
if (is_base(v))
add_patch(v);
else
update_value(v, value2delta(v, value(v)));
}
template<typename Ext>
void fixplex<Ext>::update_bounds(var_t v, numeral const& l, numeral const& h, u_dependency* dep) {
auto lo0 = m_vars[v].lo;
auto hi0 = m_vars[v].hi;
m_stashed_bounds.push_back(stashed_bound(v, m_vars[v]));
m_trail.push_back(trail_i::set_bound_i);
// std::cout << "new bound " << x << " " << m_vars[x] << " " << mod_interval<numeral>(l, h) << " -> ";
m_vars[v] &= mod_interval(l, h);
if (lo0 != m_vars[v].lo)
m_vars[v].m_lo_dep = dep;
if (hi0 != m_vars[v].hi)
m_vars[v].m_hi_dep = dep;
// std::cout << m_vars[x] << "\n";
SASSERT(in_bounds(v));
}
template<typename Ext>
@ -1155,6 +1162,8 @@ namespace polysat {
template<typename Ext>
lbool fixplex<Ext>::propagate_ineqs(ineq const& i0) {
numeral old_lo = m_vars[i0.w].lo;
SASSERT(!m_inconsistent);
std::cout << "propagate " << i0 << "\n";
if (!propagate_ineq(i0))
return l_false;
if (old_lo == m_vars[i0.w].lo)
@ -1172,6 +1181,9 @@ namespace polysat {
auto& i_out = m_ineqs[ineqs[ineq_out]];
if (i.w != i_out.v)
continue;
for (unsigned j = 0; j < stack.size(); ++j)
std::cout << " ";
std::cout << " -> " << i_out << "\n";
old_lo = m_vars[i_out.w].lo;
if (!propagate_ineq(i_out))
return l_false;
@ -1501,10 +1513,11 @@ namespace polysat {
template<typename Ext>
bool fixplex<Ext>::new_bound(ineq const& i, var_t x, numeral const& l, numeral const& h, u_dependency* a, u_dependency* b, u_dependency* c, u_dependency* d) {
bool was_fixed = lo(x) + 1 == hi(x);
SASSERT(!inconsistent());
u_dependency* dep = m_deps.mk_join(mk_leaf(i.dep), m_deps.mk_join(a, m_deps.mk_join(b, m_deps.mk_join(c, d))));
update_bounds(x, l, h, dep);
if (m_vars[x].is_empty())
return conflict(m_vars[x].m_lo_dep, m_vars[x].m_hi_dep), false;
if (inconsistent())
return false;
else if (!was_fixed && lo(x) + 1 == hi(x)) {
// TBD: track based on inequality not row
// fixed_var_eh(r, x);
@ -1516,11 +1529,12 @@ namespace polysat {
bool fixplex<Ext>::new_bound(row const& r, var_t x, mod_interval<numeral> const& range) {
if (range.is_free())
return l_true;
SASSERT(!inconsistent());
bool was_fixed = lo(x) + 1 == hi(x);
update_bounds(x, range.lo, range.hi, row2dep(r));
IF_VERBOSE(0, verbose_stream() << "new-bound v" << x << " " << m_vars[x] << "\n");
if (m_vars[x].is_empty())
return conflict(m_vars[x].m_lo_dep, m_vars[x].m_hi_dep), false;
if (inconsistent())
return false;
else if (!was_fixed && lo(x) + 1 == hi(x))
fixed_var_eh(r, x);
return true;

4
src/math/polysat/log.cpp
View file

@ -68,7 +68,9 @@ std::pair<std::ostream&, bool> polysat_log(LogLevel msg_level, std::string fn, s
std::ostream& os = std::cerr;
size_t width = 20;
size_t padding = width - std::min(width, fn.size());
size_t padding = 0;
if (width > fn.size())
padding = width - fn.size();
char const* color = nullptr;
color = level_color(msg_level);
#ifdef _MSC_VER

42
src/test/fixplex.cpp
View file

@ -420,11 +420,9 @@ namespace polysat {
solver.assert_expr(bv.mk_ule(variables.get(i.v), variables.get(i.w)));
}
}
unsigned v = 0;
for (auto const& b : bounds) {
for (unsigned v = 0; v < bounds.size(); ++v) {
auto const& b = bounds[v];
++index;
if (b.is_free())
continue;
fp.set_bounds(v, rational(b.lo, rational::ui64()), rational(b.hi, rational::ui64()), index);
@ -439,31 +437,31 @@ namespace polysat {
solver.assert_expr(m.mk_or(A, B));
}
solver.display(std::cout);
std::cout << fp << "\n";
lbool r1 = solver.check();
lbool r2 = fp.make_feasible();
std::cout << r1 << " " << r2 << "\n" << fp << "\n";
std::cout << r1 << " " << r2 << "\n";
#define VALIDATE(_test_) if (!(_test_)) { std::cout << "failed " << #_test_ << "\n"; solver.display(std::cout << fp << "\n"); SASSERT(false);}
if (r2 == l_true) {
for (auto const& row : rows) {
uint64_t sum = 0;
for (auto col : row)
sum += col.second * fp.value(col.first);
SASSERT(sum == 0);
VALIDATE(sum == 0);
}
for (unsigned i = 0; i < bounds.size(); ++i) {
uint64_t val = fp.value(i);
uint64_t lo = bounds[i].lo;
uint64_t hi = bounds[i].hi;
SASSERT(!(lo < hi || hi == 0) || lo <= val && val < hi);
SASSERT(!(hi > lo) || val < hi || lo <= val);
VALIDATE(!(lo < hi) || (lo <= val && val < hi));
VALIDATE(!(0 < lo && hi == 0) || lo <= val);
VALIDATE(!(hi > lo) || val < hi || lo <= val);
}
for (auto const& i : ineqs) {
SASSERT(fp.value(i.v) <= fp.value(i.w));
SASSERT(!i.strict || fp.value(i.v) < fp.value(i.w));
VALIDATE(fp.value(i.v) <= fp.value(i.w));
VALIDATE(!i.strict || fp.value(i.v) < fp.value(i.w));
}
}
if (r1 == r2) {
@ -480,7 +478,17 @@ namespace polysat {
std::cout << fp << "\n";
}
else {
std::cout << r2 << " missed with verdict " << r1 << "\n";
std::cout << fp << "\n";
if (r1 == l_false && false && rows.empty()) {
std::cout << "BUG should not miss unsat verdict when there are no rows\n";
solver.display(std::cout);
std::cout << "\n";
std::cout << fp << "\n";
SASSERT(false);
}
}
}
@ -503,8 +511,14 @@ namespace polysat {
svector<std::pair<unsigned, uint64_t>> row;
uint64_t coeff = (r() % 2 == 0) ? r() % 100 : (0 - r() % 10);
row.push_back(std::make_pair(i, coeff));
uint_set seen;
for (unsigned j = 0; j + 1 < num_vars_per_row; ++j) {
var_t v = (r() % (num_vars - num_vars_per_row)) + num_vars_per_row;
var_t v;
do {
v = (r() % (num_vars - num_vars_per_row)) + num_vars_per_row;
}
while (seen.contains(v));
seen.insert(v);
coeff = (r() % 2 == 0) ? r() % 100 : (0 - r() % 10);
row.push_back(std::make_pair(v, coeff));
}