mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

add dummy implementations

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-04-20 14:02:12 -07:00
parent fc60690742
commit ce8184382d
3 changed files with 61 additions and 53 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -81,7 +81,6 @@ namespace polysat {
uint_set m_left_basis; uint_set m_left_basis;
unsigned m_infeasible_var; unsigned m_infeasible_var;
unsigned_vector m_base_vars; unsigned_vector m_base_vars;
unsigned_vector m_to_fix_base;
stats m_stats; stats m_stats;
public: public:
@ -133,48 +132,46 @@ namespace polysat {
private: private:
void gauss_jordan(); void gauss_jordan();
bool gauss_jordan(row const& r); void make_basic(var_t v, row const& r);
#if 0 void del_row(row const& r) {}
void del_row(row const& r); var_t select_var_to_fix() { throw nullptr; }
var_t select_var_to_fix(); pivot_strategy_t pivot_strategy() { throw nullptr; }
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_smallest_var() { return m_to_patch.empty()?null_var:m_to_patch.erase_min(); }
var_t select_error_var(bool least); var_t select_error_var(bool least) { throw nullptr; }
void check_blands_rule(var_t v, unsigned& num_repeated); void check_blands_rule(var_t v, unsigned& num_repeated) {}
bool make_var_feasible(var_t x_i); bool make_var_feasible(var_t x_i) { return false; }
void update_and_pivot(var_t x_i, var_t x_j, numeral const& a_ij, numeral const& new_value); 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(var_t v, numeral const& delta) {}
void update_value_core(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 pivot(var_t x_i, var_t x_j, numeral const& a_ij) {}
void move_to_bound(var_t x, bool to_lower); 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(var_t x_i, bool is_below, scoped_numeral& out_a_ij) { throw nullptr; }
var_t select_pivot_blands(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) { throw nullptr; }
var_t select_pivot_core(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) { throw nullptr; }
int get_num_non_free_dep_vars(var_t x_j, int best_so_far); 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, var_t pick_var_to_leave(var_t x_j, bool is_pos,
scoped_numeral& gain, scoped_numeral& new_a_ij, bool& inc); scoped_numeral& gain, scoped_numeral& new_a_ij, bool& inc) { throw nullptr; }
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); 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_lower(var_t v) const { return false; }
bool at_upper(var_t v) const; bool at_upper(var_t v) const { return false; }
bool above_lower(var_t v) const; bool above_lower(var_t v) const { return false; }
bool below_upper(var_t v) const; bool below_upper(var_t v) const { return false; }
bool outside_bounds(var_t v) const { return below_lower(v) || above_upper(v); } 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_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_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_base(var_t x) const { return m_vars[x].m_is_base; }
void add_patch(var_t v); void add_patch(var_t v) {}
bool well_formed() const; bool well_formed() const { return false; }
bool well_formed_row(row const& r) const; bool well_formed_row(row const& r) const { return false; }
bool is_feasible() const; bool is_feasible() const { return false; }
#endif
}; };
struct uint64_ext { struct uint64_ext {

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

@ -80,6 +80,7 @@ namespace polysat {
template<typename Ext> template<typename Ext>
typename fixplex<Ext>::row typename fixplex<Ext>::row
fixplex<Ext>::add_row(var_t base_var, unsigned num_vars, var_t const* vars, numeral const* coeffs) { fixplex<Ext>::add_row(var_t base_var, unsigned num_vars, var_t const* vars, numeral const* coeffs) {
m_base_vars.reset();
row r = M.mk_row(); row r = M.mk_row();
for (unsigned i = 0; i < num_vars; ++i) for (unsigned i = 0; i < num_vars; ++i)
if (coeffs[i] != 0) if (coeffs[i] != 0)
@ -87,13 +88,13 @@ namespace polysat {
numeral base_coeff = 0; numeral base_coeff = 0;
numeral value = 0; numeral value = 0;
bool has_base = false;
for (auto const& e : M.row_entries(r)) { for (auto const& e : M.row_entries(r)) {
var_t v = e.m_var; var_t v = e.m_var;
if (v == base_var) if (v == base_var)
base_coeff = e.m_coeff; base_coeff = e.m_coeff;
else { else {
has_base |= is_base(v); if (is_base(v))
m_base_vars.push_back(v);
value += e.m_coeff * m_vars[v].m_value; value += e.m_coeff * m_vars[v].m_value;
} }
} }
@ -108,8 +109,7 @@ namespace polysat {
m_vars[base_vars].m_value = value / base_coeff; m_vars[base_vars].m_value = value / base_coeff;
// TBD: record when base_coeff does not divide value // TBD: record when base_coeff does not divide value
add_patch(base_var); add_patch(base_var);
if (has_base) { if (!m_base_vars.empty()) {
m_to_fix_base.push_back(r.id());
gauss_jordan(); gauss_jordan();
} }
SASSERT(well_formed_row(r)); SASSERT(well_formed_row(r));
@ -119,32 +119,31 @@ namespace polysat {
template<typename Ext> template<typename Ext>
void fixplex<Ext>::gauss_jordan() { void fixplex<Ext>::gauss_jordan() {
while (!m_to_fix_base.empty()) { while (!m_base_vars.empty.empty()) {
auto rid = m_to_fix_base.back(); auto v = m_base_vars.back();
if (gauss_jordan(m_rows[rid])) { auto rid = m_vars[v].m_base2row;
m_to_fix_base.pop_back(); auto const& row = m_rows[rid];
} make_basic(v, row);
} }
} }
/**
* make v a basic variable.
* If v is already a basic variable in preferred_row, skip
* If v
*/
template<typename Ext> template<typename Ext>
bool fixplex<Ext>::gauss_jordan(row const& r) { void fixplex<Ext>::make_basic(var_t v, row const& preferred_row) {
auto base_var = m_row2base[r.id()]; numeral c1 = 0;
unsigned other_base = null_var; for (auto const& e : M.row_entries(preferred_row)) {
numeral c1; if (e.m_var == v) {
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; c1 = e.m_coeff;
break; break;
} }
} }
if (null_var == other_base) auto c2 = m_vars[v].m_base_coeff;
return true; auto r2 = m_vars[v].m_base2row;
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 exp1 = trailing_zeros(c1); // exponent of two for v in r
unsigned exp2 = trailing_zeros(c2); // exponent of two for v in r2 unsigned exp2 = trailing_zeros(c2); // exponent of two for v in r2
if (exp1 >= exp2) { if (exp1 >= exp2) {
@ -157,9 +156,10 @@ namespace polysat {
} }
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
return false;
} }
#if 0 #if 0
/** /**
\brief Make x_j the new base variable for row of x_i. \brief Make x_j the new base variable for row of x_i.

11
src/math/simplex/sparse_matrix.h
View file

@ -256,6 +256,17 @@ namespace simplex {
col_iterator col_begin(int v) const { return col_iterator(m_columns[v], m_rows, true); } col_iterator col_begin(int v) const { return col_iterator(m_columns[v], m_rows, true); }
col_iterator col_end(int v) const { return col_iterator(m_columns[v], m_rows, false); } col_iterator col_end(int v) const { return col_iterator(m_columns[v], m_rows, false); }
class col_entries_t {
sparse_matrix const& m;
int v;
public:
col_entries_t(sparse_matrix const& m, int v): m(m), v(v) {}
col_iterator begin() { return m.col_begin(v); }
col_iterator end() { return m.col_end(v); }
};
col_entries_t col_entries(int v) { return col_entries_t(*this, v); }
void display(std::ostream& out); void display(std::ostream& out);
void display_row(std::ostream& out, row const& r); void display_row(std::ostream& out, row const& r);
bool well_formed() const; bool well_formed() const;