mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 03:15:50 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-08-12 08:38:54 -07:00
parent f1f5b9e311
commit 39e98b3835
2 changed files with 35 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -63,8 +63,9 @@ namespace polysat {
var_t w = UINT_MAX; var_t w = UINT_MAX;
bool strict = false; bool strict = false;
bool is_active = true; bool is_active = true;
unsigned dep = UINT_MAX; bool is_touched = false;
ineq(var_t v, var_t w, unsigned dep, bool s) : u_dependency* dep = nullptr;
ineq(var_t v, var_t w, u_dependency* dep, bool s) :
v(v), w(w), strict(s), dep(dep) {} v(v), w(w), strict(s), dep(dep) {}
std::ostream& display(std::ostream& out) const { std::ostream& display(std::ostream& out) const {

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

@ -494,14 +494,13 @@ namespace polysat {
/** /**
* Compute delta to add to the value, such that value + delta is either lo(v), or hi(v) - 1 * Compute delta to add to the value, such that value + delta is either lo(v), or hi(v) - 1
* A pre-condition is that value is not in the interval [lo(v),hi(v)[, * A pre-condition, when used during pivoting, is that value is not in the interval [lo(v),hi(v)[,
* and therefore as a consequence lo(v) != hi(v). * and therefore as a consequence lo(v) != hi(v).
*/ */
template<typename Ext> template<typename Ext>
typename fixplex<Ext>::numeral typename fixplex<Ext>::numeral
fixplex<Ext>::value2delta(var_t v, numeral const& value) const { fixplex<Ext>::value2delta(var_t v, numeral const& value) const {
SASSERT(!in_bounds(v));
SASSERT(lo(v) != hi(v));
if (lo(v) - value < value - hi(v)) if (lo(v) - value < value - hi(v))
return lo(v) - value; return lo(v) - value;
else else
@ -540,19 +539,21 @@ namespace polysat {
auto hi0 = m_vars[v].hi; auto hi0 = m_vars[v].hi;
m_stashed_bounds.push_back(stashed_bound(v, m_vars[v])); m_stashed_bounds.push_back(stashed_bound(v, m_vars[v]));
m_trail.push_back(trail_i::set_bound_i); m_trail.push_back(trail_i::set_bound_i);
std::cout << "new bound " << v << " " << m_vars[v] << " " << mod_interval<numeral>(l, h) << " -> "; // std::cout << "new bound " << v << " " << m_vars[v] << " " << mod_interval<numeral>(l, h) << " -> ";
m_vars[v] &= mod_interval(l, h); m_vars[v] &= mod_interval(l, h);
if (lo0 != m_vars[v].lo) if (lo0 != m_vars[v].lo)
m_vars[v].m_lo_dep = dep; m_vars[v].m_lo_dep = dep;
if (hi0 != m_vars[v].hi) if (hi0 != m_vars[v].hi)
m_vars[v].m_hi_dep = dep; m_vars[v].m_hi_dep = dep;
std::cout << m_vars[v] << "\n"; // std::cout << m_vars[v] << "\n";
if (m_vars[v].is_empty()) { if (m_vars[v].is_empty()) {
conflict(m_vars[v].m_lo_dep, m_vars[v].m_hi_dep); conflict(m_vars[v].m_lo_dep, m_vars[v].m_hi_dep);
return; return;
} }
if (in_bounds(v)) if (in_bounds(v))
return; return;
SASSERT(lo(v) != hi(v));
if (is_base(v)) if (is_base(v))
add_patch(v); add_patch(v);
else else
@ -598,7 +599,7 @@ namespace polysat {
m_var2ineqs[w].push_back(idx); m_var2ineqs[w].push_back(idx);
m_ineqs_to_check.push_back(idx); m_ineqs_to_check.push_back(idx);
m_trail.push_back(trail_i::add_ineq_i); m_trail.push_back(trail_i::add_ineq_i);
m_ineqs.push_back(ineq(v, w, dep, strict)); m_ineqs.push_back(ineq(v, w, mk_leaf(dep), strict));
} }
template<typename Ext> template<typename Ext>
@ -1163,10 +1164,10 @@ namespace polysat {
lbool fixplex<Ext>::propagate_ineqs(ineq const& i0) { lbool fixplex<Ext>::propagate_ineqs(ineq const& i0) {
numeral old_lo = m_vars[i0.w].lo; numeral old_lo = m_vars[i0.w].lo;
SASSERT(!m_inconsistent); SASSERT(!m_inconsistent);
std::cout << "propagate " << i0 << "\n"; // std::cout << "propagate " << i0 << "\n";
if (!propagate_ineq(i0)) if (!propagate_ineq(i0))
return l_false; return l_false;
if (old_lo == m_vars[i0.w].lo) if (old_lo == m_vars[i0.w].lo && i0.is_touched)
return l_true; return l_true;
on_stack.reset(); on_stack.reset();
stack.reset(); stack.reset();
@ -1181,14 +1182,16 @@ namespace polysat {
auto& i_out = m_ineqs[ineqs[ineq_out]]; auto& i_out = m_ineqs[ineqs[ineq_out]];
if (i.w != i_out.v) if (i.w != i_out.v)
continue; continue;
for (unsigned j = 0; j < stack.size(); ++j) // for (unsigned j = 0; j < stack.size(); ++j)
std::cout << " "; // std::cout << " ";
std::cout << " -> " << i_out << "\n"; // std::cout << " -> " << i_out << "\n";
old_lo = m_vars[i_out.w].lo; old_lo = m_vars[i_out.w].lo;
if (!propagate_ineq(i_out)) if (!propagate_ineq(i_out))
return l_false; return l_false;
bool is_onstack = on_stack.contains(i_out.w); bool is_onstack = on_stack.contains(i_out.w);
if (old_lo != m_vars[i_out.w].lo && !is_onstack) { if ((old_lo != m_vars[i_out.w].lo || !i_out.is_touched) && !is_onstack) {
i_out.is_touched = true;
on_stack.insert(i_out.w); on_stack.insert(i_out.w);
stack.back().first = ineq_out + 1; stack.back().first = ineq_out + 1;
stack.push_back(std::make_pair(0, i_out)); stack.push_back(std::make_pair(0, i_out));
@ -1200,18 +1203,22 @@ namespace polysat {
continue; continue;
} }
bool strict = i_out.strict, found = false; bool strict = i_out.strict, found = false, empty = false;
auto bound = m_vars[i_out.w];
unsigned j = stack.size(); unsigned j = stack.size();
for (; !found && j-- > 0; ) { for (; !found && j-- > 0; ) {
ineq i2 = stack[j].second; ineq i2 = stack[j].second;
strict |= i2.strict; strict |= i2.strict;
bound &= m_vars[i2.w];
if (i2.v == i_out.w) if (i2.v == i_out.w)
found = true; found = true;
if (bound.is_empty())
empty = true;
} }
if (strict && found) { if ((empty || strict) && found) {
auto* d = mk_leaf(i_out.dep); auto* d = i_out.dep;
for (; j < stack.size(); ++j) for (; j < stack.size(); ++j)
d = m_deps.mk_join(d, mk_leaf(stack[j].second.dep)); d = m_deps.mk_join(d, stack[j].second.dep);
conflict(d); conflict(d);
return l_false; return l_false;
} }
@ -1381,6 +1388,10 @@ namespace polysat {
return false; return false;
if (is_fixed(w) && lo(w) <= lo(v) && !new_bound(i, v, lo(v) + 1, hi(w) - 1, wlo, whi, vlo)) if (is_fixed(w) && lo(w) <= lo(v) && !new_bound(i, v, lo(v) + 1, hi(w) - 1, wlo, whi, vlo))
return false; return false;
if (value(v) >= value(w) && value(v) + 1 != 0 && m_vars[w].contains(value(v) + 1))
update_value(w, value(v) - value(w) + 1);
return true; return true;
} }
@ -1473,6 +1484,9 @@ namespace polysat {
return false; return false;
if (!(lo(w) <= lo(v)) && !(hi(w) == 0) && hi(v) == 0 && hi(w) <= lo(v) && !new_bound(i, w, lo(w), 0, vlo, wlo, vhi, whi)) if (!(lo(w) <= lo(v)) && !(hi(w) == 0) && hi(v) == 0 && hi(w) <= lo(v) && !new_bound(i, w, lo(w), 0, vlo, wlo, vhi, whi))
return false; return false;
if (value(v) > value(w) && m_vars[w].contains(value(v)))
update_value(w, value(v) - value(w));
return true; return true;
} }
@ -1486,7 +1500,7 @@ namespace polysat {
template<typename Ext> template<typename Ext>
void fixplex<Ext>::conflict(ineq const& i, u_dependency* a, u_dependency* b, u_dependency* c, u_dependency* d) { void fixplex<Ext>::conflict(ineq const& i, u_dependency* a, u_dependency* b, u_dependency* c, u_dependency* d) {
conflict(a, m_deps.mk_join(mk_leaf(i.dep), m_deps.mk_join(b, m_deps.mk_join(c, d)))); conflict(a, m_deps.mk_join(i.dep, m_deps.mk_join(b, m_deps.mk_join(c, d))));
} }
template<typename Ext> template<typename Ext>
@ -1514,7 +1528,7 @@ namespace polysat {
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 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); bool was_fixed = lo(x) + 1 == hi(x);
SASSERT(!inconsistent()); 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)))); u_dependency* dep = m_deps.mk_join(i.dep, m_deps.mk_join(a, m_deps.mk_join(b, m_deps.mk_join(c, d))));
update_bounds(x, l, h, dep); update_bounds(x, l, h, dep);
if (inconsistent()) if (inconsistent())
return false; return false;