mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 13:53:39 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-05-06 18:43:47 -07:00
parent 59221f1d63
commit 5931e0d902
2 changed files with 69 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -164,6 +164,8 @@ namespace polysat {
void get_offset_eqs(row const& r); void get_offset_eqs(row const& r);
void fixed_var_eh(row const& r, var_t x); void fixed_var_eh(row const& r, var_t x);
void eq_eh(var_t x, var_t y, row const& r1, row const& r2); void eq_eh(var_t x, var_t y, row const& r1, row const& r2);
void propagate_bounds(row const& r);
void new_bound(row const& r, var_t x, numeral const& l, numeral const& h);
void pivot(var_t x_i, var_t x_j, numeral const& b, numeral const& value); 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 value2delta(var_t v, numeral const& new_value) const;
void update_value(var_t v, numeral const& delta); void update_value(var_t v, numeral const& delta);

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

@ -726,6 +726,73 @@ namespace polysat {
m_var_eqs.push_back(var_eq(x, y, r1, r2)); m_var_eqs.push_back(var_eq(x, y, r1, r2));
} }
#if 1
template<typename Ext>
void fixplex<Ext>::propagate_bounds(row const& r) {
numeral lo_sum = 0, hi_sum = 0, diff = 0, free_c = 0;
var_t free_v = null_var;
for (auto const& e : M.row_entries(r)) {
var_t v = e.var();
numeral const& c = e.coeff();
if (is_free(v)) {
if (free_v != null_var)
return;
if (c != 1 && c + 1 != 1)
return;
free_v = v;
free_c = c;
continue;
}
lo_sum += lo(v) * c;
hi_sum += (hi(v) - 1) * c;
numeral range = hi(v) - lo(v);
if (!m.signed_mul(range, c, range))
return;
if (!m.signed_add(diff, diff, range))
return;
}
if (free_v != null_var) {
if (c == 1) {
//
// free_v in [lo_sum, hi_sum[
// new_bound(r, free_v, lo_sum, hi_sum);
}
else {
// c = -1
// free_v in [1 - hi_sum, 1 - lo_sum[
// new_bound(r, free_v, 1 - hi_sum, 1 - lo_sum);
}
return;
}
for (auto const& e : M.row_entries(r)) {
var_t v = e.var();
numeral const& c = e.coeff();
numeral lo_other = lo_sum - lo(v) * c;
numeral hi_other = hi_sum - (hi(v) - 1) * c;
//
// compute [lo_other,hi_other[ as range of
// other variables.
//
numeral lo1 = 1 - hi_other;
numeral hi1 = 1 - lo_other;
if (lo(v) < lo1) {
new_bound(r, v, lo1, hi(v));
}
if (hi(v) > hi1) {
new_bound(r, v, lo(v), hi1);
}
}
}
template<typename Ext>
void fixplex<Ext>::new_bound(row const& r, var_t x, numeral const& l, numeral const& h) {
}
#endif
template<typename Ext> template<typename Ext>
std::ostream& fixplex<Ext>::display(std::ostream& out) const { std::ostream& fixplex<Ext>::display(std::ostream& out) const {
M.display(out); M.display(out);