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

track

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-05-22 17:57:23 -07:00
parent 79e38c6477
commit befc47902e
2 changed files with 21 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -223,6 +223,7 @@ namespace polysat {
void propagate_bounds(row const& r);
void propagate_bounds(ineq const& i);
void new_bound(row const& r, var_t x, mod_interval<numeral> const& range);
void new_bound(ineq const& i, var_t x, numeral const& lo, numeral const& hi);
void pivot(var_t x_i, var_t x_j, numeral const& b, numeral const& value);
numeral value2delta(var_t v, numeral const& new_value) const;
numeral value2error(var_t v, numeral const& new_value) const;

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

@ -1086,17 +1086,31 @@ namespace polysat {
// v < w => lo(v) < lo(w)
// v <= w => hi(v) <= hi(w)
// v <= w => lo(v) <= lo(w)
// TBD: detect conflicts,
// ensure overflow / underflow conditions
var_t v = i.v, w = i.w;
if (i.strict && hi(v) >= hi(w))
;
new_bound(i, v, lo(v), hi(w) - 1);
if (i.strict && lo(v) >= lo(w))
;
new_bound(i, w, lo(v) + 1, hi(w));
if (!i.strict && hi(v) > hi(w))
;
new_bound(i, v, lo(v), hi(w));
if (!i.strict && lo(v) > lo(w))
;
new_bound(i, w, lo(v), hi(w));
}
template<typename Ext>
void fixplex<Ext>::new_bound(ineq const& i, var_t x, numeral const& l, numeral const& h) {
mod_interval<numeral> r(l, h);
bool was_fixed = lo(x) + 1 == hi(x);
m_vars[x] &= r;
if (m_vars[x].is_empty())
m_infeasible_var = x;
else if (!was_fixed && lo(x) + 1 == hi(x)) {
// TBD: track based on inequality not row
// fixed_var_eh(r, x);
}
}
template<typename Ext>
void fixplex<Ext>::new_bound(row const& r, var_t x, mod_interval<numeral> const& range) {
@ -1107,7 +1121,7 @@ namespace polysat {
IF_VERBOSE(0, verbose_stream() << "new-bound v" << x << " " << m_vars[x] << "\n");
if (m_vars[x].is_empty())
m_infeasible_var = x;
else if (!was_fixed && lo(x) + 1 == hi(x))
else if (!was_fixed && lo(x) + 1 == hi(x))
fixed_var_eh(r, x);
}