mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-05-01 14:43:58 -07:00
parent 501dbd9475
commit 6520f43f9d
2 changed files with 20 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -138,12 +138,12 @@ namespace polysat {
var_t select_smallest_var() { return m_to_patch.empty()?null_var:m_to_patch.erase_min(); }
lbool make_var_feasible(var_t x_i);
bool is_infeasible_row(var_t x);
void pivot(var_t x_i, var_t x_j, numeral const& b, numeral const& new_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;
void update_value(var_t v, numeral const& delta);
bool can_pivot(var_t x_i, numeral const& new_value, numeral const& a_ij, var_t x_j);
bool has_minimal_trailing_zeros(var_t y, numeral const& b);
var_t select_pivot_core(var_t x, numeral const& delta, numeral const& new_value, numeral& out_b);
numeral new_value(var_t v) const;
var_t select_pivot_core(var_t x, numeral const& new_value, numeral& out_b);
bool in_bounds(var_t v) const { return in_bounds(v, value(v)); }
bool in_bounds(var_t v, numeral const& b) const { return in_bounds(b, lo(v), hi(v)); }
bool in_bounds(numeral const& val, numeral const& lo, numeral const& hi) const;

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

@ -205,17 +205,10 @@ namespace polysat {
if (in_bounds(x))
return l_true;
auto val = value(x);
numeral new_value, b, delta;
if (lo(x) - val < val - hi(x)) {
new_value = lo(x);
delta = new_value - val;
}
else {
new_value = hi(x) - 1;
delta = val - new_value;
}
var_t y = select_pivot_core(x, delta, new_value, b);
numeral delta = value2delta(x, value(x));
numeral new_value = value(x) + delta;
numeral b;
var_t y = select_pivot_core(x, new_value, b);
if (y == null_var) {
if (is_infeasible_row(x))
@ -238,7 +231,7 @@ namespace polysat {
number of trailing zeros.
*/
template<typename Ext>
var_t fixplex<Ext>::select_pivot_core(var_t x, numeral const& delta,
var_t fixplex<Ext>::select_pivot_core(var_t x,
numeral const& new_value, numeral & out_b) {
SASSERT(is_base(x));
var_t max = get_num_vars();
@ -266,7 +259,7 @@ namespace polysat {
if (lo(y) - new_y_value < new_y_value - hi(y))
delta_y = new_y_value - lo(y);
else
delta_y = hi(y) - new_y_value - 1;
delta_y = new_y_value - hi(y) - 1;
}
int num = get_num_non_free_dep_vars(y, best_so_far);
unsigned col_sz = M.column_size(y);
@ -306,6 +299,16 @@ namespace polysat {
return result < max ? result : null_var;
}
template<typename Ext>
typename fixplex<Ext>::numeral
fixplex<Ext>::value2delta(var_t v, numeral const& value) const {
if (lo(v) - value < value - hi(v))
return lo(v) - value;
else
return hi(v) - value - 1;
}
template<typename Ext>
void fixplex<Ext>::set_bounds(var_t v, numeral const& lo, numeral const& hi) {
m_vars[v].m_lo = lo;
@ -314,10 +317,8 @@ namespace polysat {
return;
if (is_base(v))
add_patch(v);
else if (lo - value(v) < value(v) - hi)
update_value(v, lo - value(v));
else
update_value(v, hi - value(v) - 1);
update_value(v, value2delta(v, value(v)));
}
template<typename Ext>