mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +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 13:58:34 -07:00
parent 20277f4a3f
commit 57a7bef96b
3 changed files with 12 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -116,7 +116,7 @@ namespace polysat {
lbool make_feasible(); 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; std::ostream& display(std::ostream& out) const;
void display_row(std::ostream& out, row const& r, bool values = true); std::ostream& display_row(std::ostream& out, row const& r, bool values = true);
void collect_statistics(::statistics & st) const; void collect_statistics(::statistics & st) const;
row get_infeasible_row(); row get_infeasible_row();

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

@ -155,10 +155,11 @@ namespace polysat {
template<typename Ext> template<typename Ext>
void fixplex<Ext>::gauss_jordan() { void fixplex<Ext>::gauss_jordan() {
#if 0
while (!m_base_vars.empty()) { while (!m_base_vars.empty()) {
auto v = m_base_vars.back(); auto v = m_base_vars.back();
auto rid = m_vars[v].m_base2row; auto rid = m_vars[v].m_base2row;
#if 0
auto const& row = m_rows[rid]; auto const& row = m_rows[rid];
make_basic(v, row); make_basic(v, row);
#endif #endif
@ -265,7 +266,7 @@ namespace polysat {
if (lo(y) - new_y_value < new_y_value - hi(y)) if (lo(y) - new_y_value < new_y_value - hi(y))
delta_y = new_y_value - lo(y); delta_y = new_y_value - lo(y);
else else
delta_y = hi(y) - new_y_value; delta_y = hi(y) - new_y_value - 1;
} }
int num = get_num_non_free_dep_vars(y, best_so_far); int num = get_num_non_free_dep_vars(y, best_so_far);
unsigned col_sz = M.column_size(y); unsigned col_sz = M.column_size(y);
@ -291,6 +292,7 @@ namespace polysat {
best_so_far = num; best_so_far = num;
best_col_sz = col_sz; best_col_sz = col_sz;
best_in_bounds = _in_bounds; best_in_bounds = _in_bounds;
delta_best = delta_y;
n = 1; n = 1;
} }
else if (is_plateau) { else if (is_plateau) {
@ -312,12 +314,12 @@ namespace polysat {
return; return;
if (is_base(v)) if (is_base(v))
add_patch(v); add_patch(v);
else { else if (lo - value(v) < value(v) - hi)
NOT_IMPLEMENTED_YET(); update_value(v, lo - value(v));
} else
update_value(v, hi - value(v) - 1);
} }
template<typename Ext> template<typename Ext>
bool fixplex<Ext>::has_minimal_trailing_zeros(var_t y, numeral const& b) { bool fixplex<Ext>::has_minimal_trailing_zeros(var_t y, numeral const& b) {
unsigned tz1 = trailing_zeros(b); unsigned tz1 = trailing_zeros(b);
@ -332,7 +334,6 @@ namespace polysat {
return true; return true;
} }
template<typename Ext> template<typename Ext>
bool fixplex<Ext>::is_infeasible_row(var_t x) { bool fixplex<Ext>::is_infeasible_row(var_t x) {
SASSERT(is_base(x)); SASSERT(is_base(x));
@ -446,8 +447,7 @@ namespace polysat {
typename fixplex<Ext>::row typename fixplex<Ext>::row
fixplex<Ext>::get_infeasible_row() { fixplex<Ext>::get_infeasible_row() {
SASSERT(is_base(m_infeasible_var)); SASSERT(is_base(m_infeasible_var));
unsigned row_id = m_vars[m_infeasible_var].m_base2row; return row(m_vars[m_infeasible_var].m_base2row);
return row(row_id);
} }
/** /**
@ -541,7 +541,7 @@ namespace polysat {
} }
template<typename Ext> template<typename Ext>
void fixplex<Ext>::display_row(std::ostream& out, row const& r, bool values) { std::ostream& fixplex<Ext>::display_row(std::ostream& out, row const& r, bool values) {
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 (e.m_coeff != 1) if (e.m_coeff != 1)

2
src/test/fixplex.cpp
View file

@ -8,7 +8,7 @@ namespace polysat {
static void test1() { static void test1() {
reslimit lim; reslimit lim;
fixplex<uint64_ext> fp(lim); fixplex<uint64_ext> fp(lim);
var_t x = 0, y = 1, z = 2, u = 3; var_t x = 0, y = 1, z = 2;
var_t ys[3] = { x, y, z }; var_t ys[3] = { x, y, z };
numeral coeffs[3] = { 2, 1, 4 }; numeral coeffs[3] = { 2, 1, 4 };