mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

compile

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-04-30 17:53:09 -07:00
parent 0c4824f194
commit 82a364ed7b
4 changed files with 42 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -26,10 +26,11 @@ Author:
namespace polysat {
typedef unsigned var_t;
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;
@ -105,10 +106,13 @@ 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; }
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_values; }
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); }
@ -121,8 +125,6 @@ namespace polysat {
// TBD
row get_infeasible_row() { throw nullptr; }
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) {}

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

@ -243,8 +243,7 @@ namespace polysat {
number of trailing zeros.
*/
template<typename Ext>
typename fixplex<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& delta,
numeral const& new_value, numeral & out_b) {
SASSERT(is_base(x));
var_t max = get_num_vars();
@ -254,7 +253,9 @@ namespace polysat {
unsigned best_col_sz = UINT_MAX;
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_best = 0;
bool best_in_bounds = false;
for (auto const& r : M.row_entries(r)) {
@ -287,7 +288,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 && num_best_so_far && col_sz == best_col_sz)
else if (best_in_bounds && delta_y == delta_best && best_so_far == num && col_sz == best_col_sz)
is_plateau = true;
if (is_improvement) {
@ -298,7 +299,7 @@ namespace polysat {
best_in_bounds = _in_bounds;
n = 1;
}
else if (is_pleateau) {
else if (is_plateau) {
n++;
if (m_random() % n == 0) {
result = y;
@ -327,9 +328,9 @@ namespace polysat {
template<typename Ext>
bool fixplex<Ext>::is_infeasible_row(var_t x) {
SASSERT(is_base(x));
auto& row = m_rows[m_vars[x].m_base2row];
auto r = m_vars[x].m_base2row;
numeral lo_sum = 0, hi_sum = 0, diff = 0;
for (auto const& e : M.row_entries(r)) {
for (auto const& e : M.row_entries(row(r))) {
var_t v = e.m_var;
numeral const& c = e.m_coeff;
if (lo(v) == hi(v))
@ -389,7 +390,7 @@ namespace polysat {
numeral const& a = row_x.m_base_coeff;
numeral old_value_y = yI.m_value;
row_x.m_base = y;
row_x.m_value = row_i.m_value - b*old_value_y + a*new_value;
row_x.m_value = row_x.m_value - b*old_value_y + a*new_value;
row_x.m_base_coeff = b;
yI.m_base2row = rx;
yI.m_is_base = true;
@ -408,7 +409,7 @@ namespace polysat {
if (rz == rx)
continue;
auto& row_z = m_rows[rz];
var_info& zI = m_vars[row_z];
var_info& zI = m_vars[rz];
numeral c = col.get_row_entry().m_coeff;
unsigned tz2 = trailing_zeros(c);
SASSERT(tz1 <= tz2);
@ -420,7 +421,7 @@ namespace polysat {
row_z.m_base_coeff *= b1;
zI.m_value = 0 - row_z.m_value / row_z.m_base_coeff;
SASSERT(well_formed_row(r_z));
add_patch(zI.m_base);
add_patch(row_z.m_base);
}
SASSERT(well_formed());
}

1
src/test/CMakeLists.txt
View file

@ -45,6 +45,7 @@ add_executable(test-z3
f2n.cpp
factor_rewriter.cpp
finder.cpp
fixplex.cpp
fixed_bit_vector.cpp
for_each_file.cpp
get_consequences.cpp

25
src/test/fixplex.cpp Normal file
View file

@ -0,0 +1,25 @@
#include "math/polysat/fixplex.h"
#include "math/polysat/fixplex_def.h"
namespace polysat {
typedef uint64_ext::numeral numeral;
static void test1() {
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);
fp.make_feasible();
}
}
void tst_fixplex() {
}