mirror of
https://github.com/Z3Prover/z3
synced 2025-10-31 03:32:28 +00:00
test 1
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
82a364ed7b
commit
20277f4a3f
5 changed files with 250 additions and 72 deletions
|
|
@ -60,9 +60,9 @@ namespace polysat {
|
|||
struct var_info {
|
||||
unsigned m_base2row:29;
|
||||
unsigned m_is_base:1;
|
||||
numeral m_lo;
|
||||
numeral m_hi;
|
||||
numeral m_value;
|
||||
numeral m_lo { 0 };
|
||||
numeral m_hi { 0 };
|
||||
numeral m_value { 0 };
|
||||
var_info():
|
||||
m_base2row(0),
|
||||
m_is_base(false)
|
||||
|
|
@ -75,19 +75,19 @@ namespace polysat {
|
|||
numeral m_base_coeff;
|
||||
};
|
||||
|
||||
static const var_t null_var = 0;
|
||||
static const var_t null_var = UINT_MAX;
|
||||
reslimit& m_limit;
|
||||
mutable manager m;
|
||||
mutable matrix M;
|
||||
unsigned m_max_iterations;
|
||||
unsigned m_max_iterations { UINT_MAX };
|
||||
var_heap m_to_patch;
|
||||
vector<var_info> m_vars;
|
||||
vector<row_info> m_rows;
|
||||
bool m_bland;
|
||||
unsigned m_blands_rule_threshold;
|
||||
bool m_bland { false };
|
||||
unsigned m_blands_rule_threshold { 1000 };
|
||||
random_gen m_random;
|
||||
uint_set m_left_basis;
|
||||
unsigned m_infeasible_var;
|
||||
unsigned m_infeasible_var { null_var };
|
||||
unsigned_vector m_base_vars;
|
||||
stats m_stats;
|
||||
|
||||
|
|
@ -95,10 +95,7 @@ namespace polysat {
|
|||
fixplex(reslimit& lim):
|
||||
m_limit(lim),
|
||||
M(m),
|
||||
m_max_iterations(UINT_MAX),
|
||||
m_to_patch(1024),
|
||||
m_bland(false),
|
||||
m_blands_rule_threshold(1000) {}
|
||||
m_to_patch(1024) {}
|
||||
|
||||
~fixplex();
|
||||
|
||||
|
|
@ -106,33 +103,29 @@ namespace polysat {
|
|||
typedef typename matrix::row_iterator row_iterator;
|
||||
typedef typename matrix::col_iterator col_iterator;
|
||||
|
||||
void set_lo(var_t var, numeral const& b) { m_vars[var].m_lo = b; }
|
||||
void set_hi(var_t var, numeral const& b) { m_vars[var].m_hi = b; }
|
||||
void set_bounds(var_t v, numeral const& lo, numeral const& hi);
|
||||
void unset_bounds(var_t v) { m_vars[v].m_lo = m_vars[v].m_hi; }
|
||||
|
||||
var_t get_base_var(row const& r) const { return m_rows[r.id()].m_base; }
|
||||
numeral const& lo(var_t var) const { return m_vars[var].m_lo; }
|
||||
numeral const& hi(var_t var) const { return m_vars[var].m_hi; }
|
||||
numeral const& value(var_t var) const { return m_vars[var].m_value; }
|
||||
void set_max_iterations(unsigned n) { m_max_iterations = n; }
|
||||
row_iterator row_begin(row const& r) { return M.row_begin(r); }
|
||||
row_iterator row_end(row const& r) { return M.row_end(r); }
|
||||
unsigned get_num_vars() const { return m_vars.size(); }
|
||||
void ensure_var(var_t v);
|
||||
void reset();
|
||||
lbool make_feasible();
|
||||
row add_row(var_t base, unsigned num_vars, var_t const* vars, numeral const* coeffs);
|
||||
row add_row(var_t base, unsigned num_vars, var_t const* vars, numeral const* coeffs);
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
void display_row(std::ostream& out, row const& r, bool values = true);
|
||||
void collect_statistics(::statistics & st) const;
|
||||
|
||||
row get_infeasible_row();
|
||||
|
||||
#if 0
|
||||
// TBD
|
||||
row get_infeasible_row() { throw nullptr; }
|
||||
void del_row(var_t base_var) {}
|
||||
bool in_range(var_t var, numeral const& b) const {}
|
||||
void unset_lo(var_t var) {}
|
||||
void unset_hi(var_t var) {}
|
||||
void set_value(var_t var, numeral const& b) {}
|
||||
numeral const& get_value(var_t v) { throw nullptr; }
|
||||
void display(std::ostream& out) const {}
|
||||
void display_row(std::ostream& out, row const& r, bool values = true) {}
|
||||
void collect_statistics(::statistics & st) const {}
|
||||
void del_row(var_t base_var) {}
|
||||
#endif
|
||||
|
||||
|
||||
private:
|
||||
|
||||
|
|
@ -140,41 +133,45 @@ namespace polysat {
|
|||
void make_basic(var_t v, row const& r);
|
||||
|
||||
void update_value_core(var_t v, numeral const& delta);
|
||||
void ensure_var(var_t v);
|
||||
|
||||
|
||||
// TBD:
|
||||
void del_row(row const& r) {}
|
||||
var_t select_var_to_fix() { throw nullptr; }
|
||||
pivot_strategy_t pivot_strategy() { throw nullptr; }
|
||||
var_t select_smallest_var() { return m_to_patch.empty()?null_var:m_to_patch.erase_min(); }
|
||||
var_t select_error_var(bool least) { throw nullptr; }
|
||||
void check_blands_rule(var_t v, unsigned& num_repeated) {}
|
||||
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 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;
|
||||
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;
|
||||
bool is_free(var_t v) const { return lo(v) == hi(v); }
|
||||
bool is_non_free(var_t v) const { return !is_free(v); }
|
||||
bool is_base(var_t x) const { return m_vars[x].m_is_base; }
|
||||
bool is_feasible() const;
|
||||
int get_num_non_free_dep_vars(var_t x_j, int best_so_far);
|
||||
void add_patch(var_t v);
|
||||
var_t select_var_to_fix();
|
||||
void check_blands_rule(var_t v, unsigned& num_repeated);
|
||||
pivot_strategy_t pivot_strategy() { return m_bland ? S_BLAND : S_DEFAULT; }
|
||||
var_t select_error_var(bool least);
|
||||
|
||||
bool well_formed() const;
|
||||
bool well_formed_row(row const& r) const;
|
||||
|
||||
|
||||
#if 0
|
||||
// TBD:
|
||||
void del_row(row const& r) {}
|
||||
void move_to_bound(var_t x, bool to_lower) {}
|
||||
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(var_t x_i, bool is_below, numeral& out_a_ij) { throw nullptr; }
|
||||
var_t select_pivot_blands(var_t x_i, bool is_below, numeral& out_a_ij) { throw nullptr; }
|
||||
var_t select_pivot_core(var_t x, numeral const& delta, numeral const& new_value, numeral& out_b);
|
||||
int get_num_non_free_dep_vars(var_t x_j, int best_so_far) { throw nullptr; }
|
||||
var_t pick_var_to_leave(var_t x_j, bool is_pos,
|
||||
numeral& gain, numeral& new_a_ij, bool& inc) { throw nullptr; }
|
||||
|
||||
void select_pivot_primal(var_t v, var_t& x_i, var_t& x_j, numeral& a_ij, bool& inc_x_i, bool& inc_x_j) {}
|
||||
numeral new_value(var_t v) const;
|
||||
bool in_bounds(var_t v) const;
|
||||
bool in_bounds(numeral const& val, numeral const& lo, numeral const& hi) const;
|
||||
bool is_free(var_t v) const { return m_vars[v].m_lo == m_vars[v].m_hi; }
|
||||
bool is_non_free(var_t v) const { return !is_free(v); }
|
||||
bool is_base(var_t x) const { return m_vars[x].m_is_base; }
|
||||
void add_patch(var_t v) {}
|
||||
|
||||
bool well_formed() const { return false; }
|
||||
bool well_formed_row(row const& r) const { return false; }
|
||||
bool is_feasible() const { return false; }
|
||||
#endif
|
||||
|
||||
};
|
||||
|
||||
|
|
@ -200,9 +197,15 @@ namespace polysat {
|
|||
// treat numerals as signed and check for overflow/underflow
|
||||
bool signed_mul(numeral& r, numeral const& x, numeral const& y) { r = x * y; return true; }
|
||||
bool signed_add(numeral& r, numeral const& x, numeral const& y) { r = x + y; return true; }
|
||||
std::ostream& display(std::ostream& out, numeral const& x) const { return out << x; }
|
||||
};
|
||||
typedef _scoped_numeral<manager> scoped_numeral;
|
||||
};
|
||||
|
||||
template<typename Ext>
|
||||
inline std::ostream& operator<<(std::ostream& out, fixplex<Ext> const& fp) {
|
||||
return fp.display(out);
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -46,8 +46,6 @@ namespace polysat {
|
|||
m_rows.reset();
|
||||
m_left_basis.reset();
|
||||
m_base_vars.reset();
|
||||
|
||||
// pivot(0,1, 2);
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
|
|
@ -61,10 +59,9 @@ namespace polysat {
|
|||
m_bland = false;
|
||||
SASSERT(well_formed());
|
||||
while ((v = select_var_to_fix()) != null_var) {
|
||||
TRACE("simplex", display(tout << "v" << v << "\n"););
|
||||
if (!m_limit.inc() || num_iterations > m_max_iterations) {
|
||||
TRACE("polysat", display(tout << "v" << v << "\n"););
|
||||
if (!m_limit.inc() || num_iterations > m_max_iterations)
|
||||
return l_undef;
|
||||
}
|
||||
check_blands_rule(v, num_repeated);
|
||||
switch (make_var_feasible(v)) {
|
||||
case l_true:
|
||||
|
|
@ -87,6 +84,9 @@ namespace polysat {
|
|||
template<typename Ext>
|
||||
typename fixplex<Ext>::row
|
||||
fixplex<Ext>::add_row(var_t base_var, unsigned num_vars, var_t const* vars, numeral const* coeffs) {
|
||||
for (unsigned i = 0; i < num_vars; ++i)
|
||||
ensure_var(vars[i]);
|
||||
|
||||
m_base_vars.reset();
|
||||
row r = M.mk_row();
|
||||
for (unsigned i = 0; i < num_vars; ++i)
|
||||
|
|
@ -179,11 +179,6 @@ namespace polysat {
|
|||
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
bool fixplex<Ext>::in_bounds(var_t v) const {
|
||||
return in_bounds(value(v), lo(v), hi(v));
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
bool fixplex<Ext>::in_bounds(numeral const& val, numeral const& lo, numeral const& hi) const {
|
||||
if (lo == hi)
|
||||
|
|
@ -193,7 +188,6 @@ namespace polysat {
|
|||
return val < hi || lo <= val;
|
||||
}
|
||||
|
||||
|
||||
/**
|
||||
* Attempt to improve assigment to make x feasible.
|
||||
*
|
||||
|
|
@ -254,7 +248,7 @@ namespace polysat {
|
|||
int best_so_far = INT_MAX;
|
||||
numeral row_value = m_rows[r.id()].m_value;
|
||||
numeral a = m_rows[r.id()].m_base_coeff;
|
||||
numeral delta_y;
|
||||
numeral delta_y = 0;
|
||||
numeral delta_best = 0;
|
||||
bool best_in_bounds = false;
|
||||
|
||||
|
|
@ -288,7 +282,7 @@ namespace polysat {
|
|||
is_improvement = true;
|
||||
else if (best_in_bounds && _in_bounds && num == best_so_far && col_sz < best_col_sz)
|
||||
is_improvement = true;
|
||||
else if (best_in_bounds && delta_y == delta_best && best_so_far == num && col_sz == best_col_sz)
|
||||
else if (best_in_bounds && !_in_bounds && delta_y == delta_best && best_so_far == num && col_sz == best_col_sz)
|
||||
is_plateau = true;
|
||||
|
||||
if (is_improvement) {
|
||||
|
|
@ -310,6 +304,20 @@ namespace polysat {
|
|||
return result < max ? result : null_var;
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
void fixplex<Ext>::set_bounds(var_t v, numeral const& lo, numeral const& hi) {
|
||||
m_vars[v].m_lo = lo;
|
||||
m_vars[v].m_hi = hi;
|
||||
if (in_bounds(v))
|
||||
return;
|
||||
if (is_base(v))
|
||||
add_patch(v);
|
||||
else {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
template<typename Ext>
|
||||
bool fixplex<Ext>::has_minimal_trailing_zeros(var_t y, numeral const& b) {
|
||||
unsigned tz1 = trailing_zeros(b);
|
||||
|
|
@ -426,6 +434,169 @@ namespace polysat {
|
|||
SASSERT(well_formed());
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
bool fixplex<Ext>::is_feasible() const {
|
||||
for (unsigned i = m_vars.size(); i-- > 0; )
|
||||
if (!in_bounds(i))
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
typename fixplex<Ext>::row
|
||||
fixplex<Ext>::get_infeasible_row() {
|
||||
SASSERT(is_base(m_infeasible_var));
|
||||
unsigned row_id = m_vars[m_infeasible_var].m_base2row;
|
||||
return row(row_id);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Return the number of base variables that are non free and are v dependent.
|
||||
The function adds 1 to the result if v is non free.
|
||||
The function returns with a partial result r if r > best_so_far.
|
||||
This function is used to select the pivot variable.
|
||||
*/
|
||||
template<typename Ext>
|
||||
int fixplex<Ext>::get_num_non_free_dep_vars(var_t x_j, int best_so_far) {
|
||||
int result = is_non_free(x_j);
|
||||
for (auto const& col : M.col_entries(x_j)) {
|
||||
var_t s = m_rows[col.get_row().id()].m_base;
|
||||
result += is_non_free(s);
|
||||
if (result > best_so_far)
|
||||
return result;
|
||||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
void fixplex<Ext>::add_patch(var_t v) {
|
||||
SASSERT(is_base(v));
|
||||
CTRACE("polysat", !in_bounds(v), tout << "Add patch: v" << v << "\n";);
|
||||
if (!in_bounds(v))
|
||||
m_to_patch.insert(v);
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
var_t fixplex<Ext>::select_var_to_fix() {
|
||||
switch (pivot_strategy()) {
|
||||
case S_BLAND:
|
||||
return select_smallest_var();
|
||||
case S_GREATEST_ERROR:
|
||||
return select_error_var(false);
|
||||
case S_LEAST_ERROR:
|
||||
return select_error_var(true);
|
||||
default:
|
||||
return select_smallest_var();
|
||||
}
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
var_t fixplex<Ext>::select_error_var(bool least) {
|
||||
var_t best = null_var;
|
||||
numeral best_error = 0, curr_error = 0;
|
||||
for (var_t v : m_to_patch) {
|
||||
if (in_bounds(v))
|
||||
continue;
|
||||
if (lo(v) - value(v) < value(v) - hi(v))
|
||||
curr_error = lo(v) - value(v);
|
||||
else
|
||||
curr_error = value(v) - hi(v) - 1;
|
||||
if ((best == null_var) ||
|
||||
(least && curr_error < best_error) ||
|
||||
(!least && curr_error > best_error)) {
|
||||
best = v;
|
||||
best_error = curr_error;
|
||||
}
|
||||
}
|
||||
if (best == null_var)
|
||||
m_to_patch.clear(); // all variables are satisfied
|
||||
else
|
||||
m_to_patch.erase(best);
|
||||
return best;
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
void fixplex<Ext>::check_blands_rule(var_t v, unsigned& num_repeated) {
|
||||
if (m_bland)
|
||||
return;
|
||||
if (!m_left_basis.contains(v))
|
||||
m_left_basis.insert(v);
|
||||
else {
|
||||
++num_repeated;
|
||||
m_bland = num_repeated > m_blands_rule_threshold;
|
||||
CTRACE("polysat", m_bland, tout << "using blands rule, " << num_repeated << "\n";);
|
||||
}
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
std::ostream& fixplex<Ext>::display(std::ostream& out) const {
|
||||
M.display(out);
|
||||
for (unsigned i = 0; i < m_vars.size(); ++i) {
|
||||
var_info const& vi = m_vars[i];
|
||||
out << "v" << i << " " << value(i) << " [" << lo(i) << ", " << hi(i) << "[ ";
|
||||
if (vi.m_is_base) out << "b:" << vi.m_base2row << " ";
|
||||
out << "\n";
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
void fixplex<Ext>::display_row(std::ostream& out, row const& r, bool values) {
|
||||
for (auto const& e : M.row_entries(r)) {
|
||||
var_t v = e.m_var;
|
||||
if (e.m_coeff != 1)
|
||||
out << e.m_coeff << " * ";
|
||||
out << "v" << v << " ";
|
||||
if (values)
|
||||
out << value(v) << " [" << lo(v) << ", " << hi(v) << "[ ";
|
||||
}
|
||||
return out << "\n";
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
bool fixplex<Ext>::well_formed() const {
|
||||
SASSERT(M.well_formed());
|
||||
for (unsigned i = 0; i < m_rows.size(); ++i) {
|
||||
var_t s = m_rows[i].m_base;
|
||||
if (s == null_var)
|
||||
continue;
|
||||
SASSERT(i == m_vars[s].m_base2row);
|
||||
VERIFY(well_formed_row(row(i)));
|
||||
}
|
||||
for (unsigned i = 0; i < m_vars.size(); ++i) {
|
||||
SASSERT(is_base(i) || in_bounds(i));
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
bool fixplex<Ext>::well_formed_row(row const& r) const {
|
||||
var_t s = m_rows[r.id()].m_base;
|
||||
(void)s;
|
||||
SASSERT(m_vars[s].m_base2row == r.id());
|
||||
SASSERT(m_vars[s].m_is_base);
|
||||
numeral sum = 0;
|
||||
for (auto const& e : M.row_entries(r)) {
|
||||
sum += value(e.m_var) * e.m_coeff;
|
||||
SASSERT(s != e.m_var || m_rows[r.id()].m_base_coeff == e.m_coeff);
|
||||
}
|
||||
if (sum != 0) {
|
||||
IF_VERBOSE(0, M.display_row(verbose_stream(), r););
|
||||
TRACE("polysat", display(tout << "non-well formed row\n"); M.display_row(tout << "row: ", r););
|
||||
throw default_exception("non-well formed row");
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
void fixplex<Ext>::collect_statistics(::statistics & st) const {
|
||||
M.collect_statistics(st);
|
||||
st.update("fixplex num pivots", m_stats.m_num_pivots);
|
||||
st.update("fixplex num infeasible", m_stats.m_num_infeasible);
|
||||
st.update("fixplex num checks", m_stats.m_num_checks);
|
||||
}
|
||||
|
||||
|
||||
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -238,7 +238,7 @@ namespace simplex {
|
|||
--m_col.m_refs;
|
||||
}
|
||||
|
||||
row get_row() {
|
||||
row get_row() const {
|
||||
return row(m_col.m_entries[m_curr].m_row_id);
|
||||
}
|
||||
row_entry const& get_row_entry() {
|
||||
|
|
|
|||
|
|
@ -9,17 +9,20 @@ namespace polysat {
|
|||
reslimit lim;
|
||||
fixplex<uint64_ext> fp(lim);
|
||||
var_t x = 0, y = 1, z = 2, u = 3;
|
||||
fp.ensure_var(3);
|
||||
|
||||
var_t ys[2] = { y, z };
|
||||
numeral coeffs[2] = { 1, 4 };
|
||||
fp.add_row(x, 2, ys, coeffs);
|
||||
fp.set_lo(x, 1);
|
||||
fp.set_hi(x, 2);
|
||||
var_t ys[3] = { x, y, z };
|
||||
numeral coeffs[3] = { 2, 1, 4 };
|
||||
fp.add_row(x, 3, ys, coeffs);
|
||||
fp.set_bounds(x, 1, 2);
|
||||
std::cout << fp << "\n";
|
||||
fp.make_feasible();
|
||||
std::cout << fp << "\n";
|
||||
statistics st;
|
||||
fp.collect_statistics(st);
|
||||
std::cout << st << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
void tst_fixplex() {
|
||||
|
||||
polysat::test1();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -264,4 +264,5 @@ int main(int argc, char ** argv) {
|
|||
TST(finder);
|
||||
TST(polysat);
|
||||
TST_ARGV(polysat_argv);
|
||||
TST(fixplex);
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue