mirror of
https://github.com/Z3Prover/z3
synced 2025-04-29 03:45:51 +00:00
tidy, initial polysat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
82bc6474a3
commit
fc60690742
8 changed files with 496 additions and 32 deletions
195
src/math/polysat/fixplex.h
Normal file
195
src/math/polysat/fixplex.h
Normal file
|
|
@ -0,0 +1,195 @@
|
|||
/*++
|
||||
Copyright (c) 2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
fixplex.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Fixed-precision unsigned integer simplex tableau.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
||||
Jakob Rath 2021-04-6
|
||||
|
||||
--*/
|
||||
|
||||
#pragma once
|
||||
|
||||
#include "math/simplex/sparse_matrix.h"
|
||||
#include "util/heap.h"
|
||||
#include "util/lbool.h"
|
||||
#include "util/uint_set.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
template<typename Ext>
|
||||
class fixplex {
|
||||
|
||||
typedef unsigned var_t;
|
||||
typedef typename Ext::numeral numeral;
|
||||
typedef typename Ext::scoped_numeral scoped_numeral;
|
||||
typedef typename Ext::manager manager;
|
||||
typedef simplex::sparse_matrix<Ext> matrix;
|
||||
struct var_lt {
|
||||
bool operator()(var_t v1, var_t v2) const { return v1 < v2; }
|
||||
};
|
||||
typedef heap<var_lt> var_heap;
|
||||
|
||||
struct stats {
|
||||
unsigned m_num_pivots;
|
||||
unsigned m_num_infeasible;
|
||||
unsigned m_num_checks;
|
||||
stats() { reset(); }
|
||||
void reset() {
|
||||
memset(this, 0, sizeof(*this));
|
||||
}
|
||||
};
|
||||
|
||||
enum pivot_strategy_t {
|
||||
S_BLAND,
|
||||
S_GREATEST_ERROR,
|
||||
S_LEAST_ERROR,
|
||||
S_DEFAULT
|
||||
};
|
||||
|
||||
struct var_info {
|
||||
unsigned m_base2row:29;
|
||||
unsigned m_is_base:1;
|
||||
numeral m_lo;
|
||||
numeral m_hi;
|
||||
numeral m_value;
|
||||
var_info():
|
||||
m_base2row(0),
|
||||
m_is_base(false)
|
||||
{}
|
||||
};
|
||||
|
||||
static const var_t null_var;
|
||||
reslimit& m_limit;
|
||||
mutable manager m;
|
||||
mutable matrix M;
|
||||
unsigned m_max_iterations;
|
||||
var_heap m_to_patch;
|
||||
vector<var_info> m_vars;
|
||||
svector<var_t> m_row2base;
|
||||
bool m_bland;
|
||||
unsigned m_blands_rule_threshold;
|
||||
random_gen m_random;
|
||||
uint_set m_left_basis;
|
||||
unsigned m_infeasible_var;
|
||||
unsigned_vector m_base_vars;
|
||||
unsigned_vector m_to_fix_base;
|
||||
stats m_stats;
|
||||
|
||||
public:
|
||||
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) {}
|
||||
|
||||
~fixplex();
|
||||
|
||||
typedef typename matrix::row row;
|
||||
typedef typename matrix::row_iterator row_iterator;
|
||||
typedef typename matrix::col_iterator col_iterator;
|
||||
|
||||
var_t get_base_var(row const& r) const { return m_row2base[r.id()]; }
|
||||
numeral const& get_lo(var_t var) const { return m_vars[var].m_lo; }
|
||||
numeral const& get_hi(var_t var) const { return m_vars[var].m_hi; }
|
||||
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);
|
||||
|
||||
#if 0
|
||||
row get_infeasible_row();
|
||||
void del_row(var_t base_var);
|
||||
void set_lo(var_t var, numeral const& b);
|
||||
void set_hi(var_t var, numeral const& b);
|
||||
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);
|
||||
void display(std::ostream& out) const;
|
||||
void display_row(std::ostream& out, row const& r, bool values = true);
|
||||
|
||||
|
||||
|
||||
void collect_statistics(::statistics & st) const;
|
||||
|
||||
#endif
|
||||
|
||||
private:
|
||||
|
||||
void gauss_jordan();
|
||||
bool gauss_jordan(row const& r);
|
||||
|
||||
#if 0
|
||||
void del_row(row const& r);
|
||||
var_t select_var_to_fix();
|
||||
pivot_strategy_t pivot_strategy();
|
||||
var_t select_smallest_var() { return m_to_patch.empty()?null_var:m_to_patch.erase_min(); }
|
||||
var_t select_error_var(bool least);
|
||||
void check_blands_rule(var_t v, unsigned& num_repeated);
|
||||
bool make_var_feasible(var_t x_i);
|
||||
void update_and_pivot(var_t x_i, var_t x_j, numeral const& a_ij, numeral const& new_value);
|
||||
void update_value(var_t v, numeral const& delta);
|
||||
void update_value_core(var_t v, numeral const& delta);
|
||||
void pivot(var_t x_i, var_t x_j, numeral const& a_ij);
|
||||
void move_to_bound(var_t x, bool to_lower);
|
||||
var_t select_pivot(var_t x_i, bool is_below, scoped_numeral& out_a_ij);
|
||||
var_t select_pivot_blands(var_t x_i, bool is_below, scoped_numeral& out_a_ij);
|
||||
var_t select_pivot_core(var_t x_i, bool is_below, scoped_numeral& out_a_ij);
|
||||
int get_num_non_free_dep_vars(var_t x_j, int best_so_far);
|
||||
|
||||
var_t pick_var_to_leave(var_t x_j, bool is_pos,
|
||||
scoped_numeral& gain, scoped_numeral& new_a_ij, bool& inc);
|
||||
|
||||
|
||||
void select_pivot_primal(var_t v, var_t& x_i, var_t& x_j, scoped_numeral& a_ij, bool& inc_x_i, bool& inc_x_j);
|
||||
|
||||
|
||||
bool at_lower(var_t v) const;
|
||||
bool at_upper(var_t v) const;
|
||||
bool above_lower(var_t v) const;
|
||||
bool below_upper(var_t v) const;
|
||||
bool outside_bounds(var_t v) const { return below_lower(v) || above_upper(v); }
|
||||
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;
|
||||
bool well_formed_row(row const& r) const;
|
||||
bool is_feasible() const;
|
||||
|
||||
#endif
|
||||
};
|
||||
|
||||
struct uint64_ext {
|
||||
typedef uint64_t numeral;
|
||||
struct manager {
|
||||
void reset() {}
|
||||
void reset(numeral& n) {}
|
||||
bool is_zero(numeral const& n) const { return n == 0; }
|
||||
};
|
||||
struct scoped_numeral {
|
||||
scoped_numeral(manager& m) { n = 0; }
|
||||
numeral n;
|
||||
numeral& operator()() { return n; }
|
||||
};
|
||||
};
|
||||
|
||||
};
|
||||
|
||||
264
src/math/polysat/fixplex_def.h
Normal file
264
src/math/polysat/fixplex_def.h
Normal file
|
|
@ -0,0 +1,264 @@
|
|||
/*++
|
||||
Copyright (c) 2021 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
fixplex_def.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Fixed-precision unsigned integer simplex tableau.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
||||
Jakob Rath 2021-04-6
|
||||
|
||||
--*/
|
||||
|
||||
#pragma once
|
||||
|
||||
#include "math/polysat/fixplex.h"
|
||||
#include "math/simplex/sparse_matrix_def.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
template<typename Ext>
|
||||
fixplex<Ext>::~fixplex() {
|
||||
reset();
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
void fixplex<Ext>::ensure_var(var_t v) {
|
||||
while (v >= m_vars.size()) {
|
||||
M.ensure_var(m_vars.size());
|
||||
m_vars.push_back(var_info());
|
||||
}
|
||||
if (m_to_patch.get_bounds() <= v)
|
||||
m_to_patch.set_bounds(2*v+1);
|
||||
}
|
||||
|
||||
|
||||
template<typename Ext>
|
||||
void fixplex<Ext>::reset() {
|
||||
M.reset();
|
||||
m_to_patch.reset();
|
||||
m_vars.reset();
|
||||
m_row2base.reset();
|
||||
m_left_basis.reset();
|
||||
m_base_vars.reset();
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
lbool fixplex<Ext>::make_feasible() {
|
||||
++m_stats.m_num_checks;
|
||||
m_left_basis.reset();
|
||||
m_infeasible_var = null_var;
|
||||
unsigned num_iterations = 0;
|
||||
unsigned num_repeated = 0;
|
||||
var_t v = null_var;
|
||||
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) {
|
||||
return l_undef;
|
||||
}
|
||||
check_blands_rule(v, num_repeated);
|
||||
if (!make_var_feasible(v)) {
|
||||
m_to_patch.insert(v);
|
||||
m_infeasible_var = v;
|
||||
++m_stats.m_num_infeasible;
|
||||
return l_false;
|
||||
}
|
||||
++num_iterations;
|
||||
}
|
||||
SASSERT(well_formed());
|
||||
return l_true;
|
||||
}
|
||||
|
||||
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) {
|
||||
row r = M.mk_row();
|
||||
for (unsigned i = 0; i < num_vars; ++i)
|
||||
if (coeffs[i] != 0)
|
||||
M.add_var(r, coeffs[i], vars[i]);
|
||||
|
||||
numeral base_coeff = 0;
|
||||
numeral value = 0;
|
||||
bool has_base = false;
|
||||
for (auto const& e : M.row_entries(r)) {
|
||||
var_t v = e.m_var;
|
||||
if (v == base_var)
|
||||
base_coeff = e.m_coeff;
|
||||
else {
|
||||
has_base |= is_base(v);
|
||||
value += e.m_coeff * m_vars[v].m_value;
|
||||
}
|
||||
}
|
||||
SASSERT(base_coeff != 0);
|
||||
SASSERT(!is_base(base_var));
|
||||
while (m_row2base.size() <= r.id())
|
||||
m_row2base.push_back(null_var);
|
||||
m_row2base[r.id()] = base_var;
|
||||
m_vars[base_var].m_base2row = r.id();
|
||||
m_vars[base_var].m_is_base = true;
|
||||
m_vars[base_var].m_base_coeff = base_coeff;
|
||||
m_vars[base_vars].m_value = value / base_coeff;
|
||||
// TBD: record when base_coeff does not divide value
|
||||
add_patch(base_var);
|
||||
if (has_base) {
|
||||
m_to_fix_base.push_back(r.id());
|
||||
gauss_jordan();
|
||||
}
|
||||
SASSERT(well_formed_row(r));
|
||||
SASSERT(well_formed());
|
||||
return r;
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
void fixplex<Ext>::gauss_jordan() {
|
||||
while (!m_to_fix_base.empty()) {
|
||||
auto rid = m_to_fix_base.back();
|
||||
if (gauss_jordan(m_rows[rid])) {
|
||||
m_to_fix_base.pop_back();
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
bool fixplex<Ext>::gauss_jordan(row const& r) {
|
||||
auto base_var = m_row2base[r.id()];
|
||||
unsigned other_base = null_var;
|
||||
numeral c1;
|
||||
for (auto const& e : M.row_entries(r)) {
|
||||
var_t v = e.m_var;
|
||||
if (is_base(v) && v != base_var) {
|
||||
other_base = v;
|
||||
c1 = e.m_coeff;
|
||||
break;
|
||||
}
|
||||
}
|
||||
if (null_var == other_base)
|
||||
return true;
|
||||
|
||||
auto c2 = m_vars[other_base].m_base_coeff;
|
||||
auto r2 = m_vars[other_base].m_base2row;
|
||||
unsigned exp1 = trailing_zeros(c1); // exponent of two for v in r
|
||||
unsigned exp2 = trailing_zeros(c2); // exponent of two for v in r2
|
||||
if (exp1 >= exp2) {
|
||||
// eliminate v from r
|
||||
}
|
||||
else {
|
||||
// eliminate v from r2,
|
||||
// make v the new base for r
|
||||
// perform gauss-jordan for both r and r2 (add to queue)
|
||||
}
|
||||
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return false;
|
||||
}
|
||||
|
||||
#if 0
|
||||
/**
|
||||
\brief Make x_j the new base variable for row of x_i.
|
||||
x_i is assumed base variable of row r_i.
|
||||
x_j is assumed to have coefficient a_ij in r_i.
|
||||
|
||||
a_ii*x_i + a_ij*x_j + r_i = 0
|
||||
|
||||
current value of x_i is v_i
|
||||
new value of x_i is new_value
|
||||
a_ii*(x_i + new_value - x_i) + a_ij*((x_i - new_value)*a_ii/a_ij + x_j) + r_i = 0
|
||||
|
||||
Let r_k be a row where x_j has coefficient x_kj != 0.
|
||||
r_k <- r_k * a_ij - r_i * a_kj
|
||||
*/
|
||||
template<typename Ext>
|
||||
void fixplex<Ext>::update_and_pivot(var_t x_i, var_t x_j, numeral const& a_ij, numeral const& new_value) {
|
||||
SASSERT(is_base(x_i));
|
||||
SASSERT(!is_base(x_j));
|
||||
var_info& x_iI = m_vars[x_i];
|
||||
numeral const& a_ii = x_iI.m_base_coeff;
|
||||
auto theta = x_iI.m_value - new_value;
|
||||
theta *= a_ii;
|
||||
theta /= a_ij;
|
||||
update_value(x_j, theta);
|
||||
SASSERT(new_value == x_iI.m_value);
|
||||
pivot(x_i, x_j, a_ij);
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
void fixplex<Ext>::pivot(var_t x_i, var_t x_j, numeral const& a_ij) {
|
||||
++m_stats.m_num_pivots;
|
||||
var_info& x_iI = m_vars[x_i];
|
||||
var_info& x_jI = m_vars[x_j];
|
||||
unsigned r_i = x_iI.m_base2row;
|
||||
m_row2base[r_i] = x_j;
|
||||
x_jI.m_base2row = r_i;
|
||||
x_jI.m_base_coeff = a_ij;
|
||||
x_jI.m_is_base = true;
|
||||
x_iI.m_is_base = false;
|
||||
add_patch(x_j);
|
||||
SASSERT(well_formed_row(row(r_i)));
|
||||
|
||||
col_iterator it = M.col_begin(x_j), end = M.col_end(x_j);
|
||||
scoped_numeral a_kj(m), g(m);
|
||||
for (; it != end; ++it) {
|
||||
row r_k = it.get_row();
|
||||
if (r_k.id() != r_i) {
|
||||
a_kj = it.get_row_entry().m_coeff;
|
||||
a_kj.neg();
|
||||
M.mul(r_k, a_ij);
|
||||
M.add(r_k, a_kj, row(r_i));
|
||||
var_t s = m_row2base[r_k.id()];
|
||||
numeral& coeff = m_vars[s].m_base_coeff;
|
||||
m.mul(coeff, a_ij, coeff);
|
||||
M.gcd_normalize(r_k, g);
|
||||
if (!m.is_one(g)) {
|
||||
m.div(coeff, g, coeff);
|
||||
}
|
||||
SASSERT(well_formed_row(row(r_k)));
|
||||
}
|
||||
}
|
||||
SASSERT(well_formed());
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
void fixplex<Ext>::update_value(var_t v, eps_numeral const& delta) {
|
||||
if (em.is_zero(delta)) {
|
||||
return;
|
||||
}
|
||||
update_value_core(v, delta);
|
||||
col_iterator it = M.col_begin(v), end = M.col_end(v);
|
||||
|
||||
// v <- v + delta
|
||||
// s*s_coeff + v*v_coeff + R = 0
|
||||
// ->
|
||||
// (v + delta)*v_coeff + (s - delta*v_coeff/s_coeff)*v + R = 0
|
||||
for (; it != end; ++it) {
|
||||
row r = it.get_row();
|
||||
var_t s = m_row2base[r.id()];
|
||||
var_info& si = m_vars[s];
|
||||
scoped_eps_numeral delta2(em);
|
||||
numeral const& coeff = it.get_row_entry().m_coeff;
|
||||
em.mul(delta, coeff, delta2);
|
||||
em.div(delta2, si.m_base_coeff, delta2);
|
||||
delta2.neg();
|
||||
update_value_core(s, delta2);
|
||||
}
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
void fixplex<Ext>::update_value_core(var_t v, eps_numeral const& delta) {
|
||||
eps_numeral& val = m_vars[v].m_value;
|
||||
em.add(val, delta, val);
|
||||
if (is_base(v)) {
|
||||
add_patch(v);
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
||||
}
|
||||
|
||||
|
|
@ -66,6 +66,7 @@ namespace polysat {
|
|||
solver::solver(reslimit& lim):
|
||||
m_lim(lim),
|
||||
m_bdd(1000),
|
||||
m_fixplex(m_lim),
|
||||
m_dm(m_value_manager, m_alloc),
|
||||
m_free_vars(m_activity) {
|
||||
|
||||
|
|
|
|||
|
|
@ -48,6 +48,7 @@ namespace polysat {
|
|||
scoped_ptr_vector<dd::pdd_manager> m_pdd;
|
||||
scoped_ptr_vector<dd::fdd> m_bits;
|
||||
dd::bdd_manager m_bdd;
|
||||
fixplex<uint64_ext> m_fixplex;
|
||||
dep_value_manager m_value_manager;
|
||||
small_object_allocator m_alloc;
|
||||
poly_dep_manager m_dm;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue