mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
cheap_eqs - work on fixed_phase
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
parent
cb3ebac3dd
commit
29b3f438bc
|
|
@ -25,24 +25,19 @@ class lp_bound_propagator {
|
|||
vertex* m_parent;
|
||||
unsigned m_level; // the distance in hops to the root;
|
||||
// it is handy to find the common ancestor
|
||||
bool m_neg; // false if grows with the root, true if grows with -root
|
||||
public:
|
||||
vertex() {}
|
||||
vertex(unsigned row,
|
||||
unsigned column,
|
||||
bool neg) :
|
||||
unsigned column) :
|
||||
m_row(row),
|
||||
m_column(column),
|
||||
m_parent(nullptr),
|
||||
m_level(0),
|
||||
m_neg(neg)
|
||||
m_level(0)
|
||||
{}
|
||||
unsigned column() const { return m_column; }
|
||||
unsigned row() const { return m_row; }
|
||||
vertex* parent() const { return m_parent; }
|
||||
unsigned level() const { return m_level; }
|
||||
bool neg() const { return m_neg; }
|
||||
bool& neg() { return m_neg; }
|
||||
void add_child(vertex* child) {
|
||||
SASSERT(!(*this == *child));
|
||||
child->m_parent = this;
|
||||
|
|
@ -50,17 +45,24 @@ class lp_bound_propagator {
|
|||
child->m_level = m_level + 1;
|
||||
}
|
||||
const ptr_vector<vertex> & children() const { return m_children; }
|
||||
std::ostream& print(std::ostream & out) const {
|
||||
out << "r = " << m_row << ", c = " << m_column << ", P = {";
|
||||
if (m_parent) { out << "(" << m_parent->row() << ", " << m_parent->column() << ")";}
|
||||
else { out << "null"; }
|
||||
out << "} , lvl = " << m_level << (neg()? " -":" +");
|
||||
return out;
|
||||
}
|
||||
bool operator==(const vertex& o) const {
|
||||
return m_row == o.m_row && m_column == o.m_column;
|
||||
}
|
||||
};
|
||||
|
||||
std::ostream& print(std::ostream & out, const vertex* v) const {
|
||||
out << "r = " << v->row() << ", c = " << v->column() << ", P = {";
|
||||
if (v->parent()) { out << "(" << v->parent()->row() << ", " << v->parent()->column() << ")";}
|
||||
else { out << "null"; }
|
||||
out << "} , lvl = " << v->level();
|
||||
if (m_pol.contains(v->column())) {
|
||||
tout << (pol(v) == -1? " -":" +");
|
||||
} else {
|
||||
tout << " not in m_pol";
|
||||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
hashtable<unsigned, u_hash, u_eq> m_visited_rows;
|
||||
hashtable<unsigned, u_hash, u_eq> m_visited_columns;
|
||||
vertex* m_root;
|
||||
|
|
@ -69,26 +71,20 @@ class lp_bound_propagator {
|
|||
// by adjusting the vertices offsets, so they become absolute.
|
||||
// If the tree is fixed then in addition to checking with the m_vals_to_verts
|
||||
// we are going to check with the m_fixed_var_tables.
|
||||
vertex* m_fixed_vertex;
|
||||
const vertex* m_fixed_vertex;
|
||||
explanation m_fixed_vertex_explanation;
|
||||
// a pair (o, j) belongs to m_vals_to_verts iff x[j] = x[m_root->column()] + o
|
||||
map<mpq, vertex*, obj_hash<mpq>, default_eq<mpq>> m_vals_to_verts;
|
||||
// a pair (o, j) belongs to m_vals_to_verts_neg iff -x[j] = x[m_root->column()] + o
|
||||
map<mpq, vertex*, obj_hash<mpq>, default_eq<mpq>> m_vals_to_verts_neg;
|
||||
// x[m_root->column()] - m_pol[j]*x[j] == const;
|
||||
u_map<int> m_pol;
|
||||
// if m_pos.contains(j) then x[j] = x[m_root->column()] + o
|
||||
uint_set m_pos;
|
||||
|
||||
// these maps map a column index to the corresponding index in ibounds
|
||||
std::unordered_map<unsigned, unsigned> m_improved_lower_bounds;
|
||||
std::unordered_map<unsigned, unsigned> m_improved_upper_bounds;
|
||||
class signed_column {
|
||||
bool m_sign;
|
||||
unsigned m_column;
|
||||
public:
|
||||
signed_column() : m_column(UINT_MAX) {}
|
||||
bool not_set() const { return m_column == UINT_MAX; }
|
||||
bool is_set() const { return m_column != UINT_MAX; }
|
||||
bool sign() const { return m_sign; }
|
||||
bool& sign() { return m_sign; }
|
||||
unsigned column() const { return m_column; }
|
||||
unsigned& column() { return m_column; }
|
||||
};
|
||||
|
||||
T& m_imp;
|
||||
vector<implied_bound> m_ibounds;
|
||||
|
|
@ -172,19 +168,6 @@ public:
|
|||
m_imp.consume(a, ci);
|
||||
}
|
||||
|
||||
bool set_sign_and_column(signed_column& i, const row_cell<mpq> & c) const {
|
||||
if (c.coeff().is_one()) {
|
||||
i.sign() = false;
|
||||
i.column() = c.var();
|
||||
return true;
|
||||
}
|
||||
else if (c.coeff().is_minus_one()){
|
||||
i.sign() = true;
|
||||
i.column() = c.var();
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
const mpq& val(unsigned j) const {
|
||||
return lp().get_column_value(j).x;
|
||||
}
|
||||
|
|
@ -200,11 +183,11 @@ public:
|
|||
if (!lp().find_in_fixed_tables(val(v_j), is_int(v_j), j))
|
||||
return;
|
||||
TRACE("cheap_eq", tout << "found j=" << j << " for v=";
|
||||
v->print(tout) << "\n in lp.fixed tables\n";);
|
||||
ptr_vector<vertex> path;
|
||||
print(tout, v) << "\n in lp.fixed tables\n";);
|
||||
ptr_vector<const vertex> path;
|
||||
find_path_on_tree(path, v, m_fixed_vertex);
|
||||
explanation ex = get_explanation_from_path(path);
|
||||
explain_fixed_column(ex, j);
|
||||
ex.add_expl(m_fixed_vertex_explanation);
|
||||
add_eq_on_columns(ex, j, v->column());
|
||||
}
|
||||
|
||||
|
|
@ -217,6 +200,47 @@ public:
|
|||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
// pol for polarity
|
||||
int pol(const vertex* v) const { return pol(v->column()); }
|
||||
int pol(unsigned j) const { return m_pol[j]; }
|
||||
void set_polarity(unsigned j, int p) {
|
||||
SASSERT(p == 1 || p == -1);
|
||||
SASSERT(!m_pol.contains(j));
|
||||
m_pol.insert(j, p);
|
||||
}
|
||||
|
||||
void check_polarity(vertex* v, int polarity) {
|
||||
int prev_pol;
|
||||
if (!m_pol.find(v->column(), prev_pol)) {
|
||||
m_pol.insert(v->column(), polarity);
|
||||
return;
|
||||
}
|
||||
if (prev_pol == polarity)
|
||||
return;
|
||||
TRACE("cheap_eq", tout << "polarity switch:"; print(tout , v) << "\n";);
|
||||
const vertex *u = find_other_vertex_with_same_column(v);
|
||||
ptr_vector<const vertex> path;
|
||||
find_path_on_tree(path, u, v);
|
||||
m_fixed_vertex_explanation = get_explanation_from_path(path);
|
||||
set_fixed_vertex(v);
|
||||
}
|
||||
|
||||
const vertex* find_other_vertex_with_same_column(const vertex* t) const {
|
||||
return find_other_vertex_with_same_column_under(m_root, t);
|
||||
}
|
||||
|
||||
const vertex * find_other_vertex_with_same_column_under(const vertex* v, const vertex* t) const {
|
||||
if (v != t && v->column() == t->column())
|
||||
return v;
|
||||
for (const vertex* c : v->children()) {
|
||||
auto u = find_other_vertex_with_same_column_under(c, t);
|
||||
if (u)
|
||||
return u;
|
||||
}
|
||||
UNREACHABLE();
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
bool tree_contains(vertex *v) const {
|
||||
if (!m_root)
|
||||
|
|
@ -224,28 +248,34 @@ public:
|
|||
return tree_contains_r(m_root, v);
|
||||
}
|
||||
|
||||
vertex * alloc_v(unsigned row_index, unsigned column, bool neg) {
|
||||
vertex * v = alloc(vertex, row_index, column, neg);
|
||||
vertex * alloc_v(unsigned row_index, unsigned column) {
|
||||
vertex * v = alloc(vertex, row_index, column);
|
||||
SASSERT(!tree_contains(v));
|
||||
return v;
|
||||
}
|
||||
|
||||
static bool not_set(unsigned j) { return j == UINT_MAX; }
|
||||
static bool is_set(unsigned j) { return j != UINT_MAX; }
|
||||
|
||||
void create_root(unsigned row_index) {
|
||||
SASSERT(!m_root && !m_fixed_vertex);
|
||||
signed_column x, y;
|
||||
unsigned x, y;
|
||||
int polarity;
|
||||
TRACE("cheap_eq", print_row(tout, row_index););
|
||||
if (!is_tree_offset_row(row_index, x, y)) {
|
||||
if (!is_tree_offset_row(row_index, x, y, polarity)) {
|
||||
TRACE("cheap_eq", tout << "not an offset row\n";);
|
||||
return;
|
||||
}
|
||||
const mpq& r = val(x.column());
|
||||
m_root = alloc_v(row_index, x.column(), false);
|
||||
if (y.not_set()) {
|
||||
set_fixed_vertex(m_root);
|
||||
const mpq& r = val(x);
|
||||
m_root = alloc_v(row_index, x);
|
||||
set_polarity(x, 1);
|
||||
if (not_set(y)) {
|
||||
set_fixed_vertex(m_root);
|
||||
explain_fixed_in_row(row_index, m_fixed_vertex_explanation);
|
||||
} else {
|
||||
bool neg = x.sign() == y.sign();
|
||||
vertex *v = alloc_v(row_index, y.column(), neg);
|
||||
vertex *v = alloc_v(row_index, y);
|
||||
m_root->add_child(v);
|
||||
set_polarity(y, polarity);
|
||||
}
|
||||
// keep root in the positive table
|
||||
m_vals_to_verts.insert(r, m_root);
|
||||
|
|
@ -261,29 +291,33 @@ public:
|
|||
// It is assumed that parent->column() is present in the row
|
||||
vertex* add_child_from_row(unsigned row_index, vertex* parent) {
|
||||
TRACE("cheap_eq", print_row(tout, row_index););
|
||||
signed_column x, y;
|
||||
if (!is_tree_offset_row(row_index, x, y)) {
|
||||
unsigned x, y; int polarity;
|
||||
if (!is_tree_offset_row(row_index, x, y, polarity)) {
|
||||
TRACE("cheap_eq", tout << "not an offset row\n"; );
|
||||
return nullptr;
|
||||
}
|
||||
if (y.not_set()) {
|
||||
SASSERT(parent->column() == x.column());
|
||||
vertex *v = alloc_v( row_index, x.column(), parent->neg());
|
||||
if (not_set(y)) {
|
||||
SASSERT(parent->column() == x);
|
||||
vertex *v = alloc_v(row_index, x);
|
||||
parent->add_child(v);
|
||||
set_fixed_vertex(v);
|
||||
if (!fixed_phase()) {
|
||||
set_fixed_vertex(v);
|
||||
explain_fixed_in_row(row_index, m_fixed_vertex_explanation);
|
||||
}
|
||||
return v;
|
||||
}
|
||||
|
||||
SASSERT(x.is_set() && y.is_set());
|
||||
SASSERT(is_set(x) && is_set(y));
|
||||
|
||||
// v is exactly like parent, but the row is different
|
||||
vertex *v = alloc_v(row_index, parent->column(), parent->neg());
|
||||
// v has the column of the parent, but the row is different
|
||||
vertex *v = alloc_v(row_index, parent->column());
|
||||
parent->add_child(v);
|
||||
SASSERT(x.column() == v->column() || y.column() == v->column());
|
||||
unsigned col = v->column() == y.column()? x.column(): y.column();
|
||||
bool neg = x.sign() == y.sign() ? !v->neg(): v->neg();
|
||||
vertex *vy = alloc_v(v->row(), col, neg);
|
||||
SASSERT(x == v->column() || y == v->column());
|
||||
unsigned col = v->column() == y? x : y;
|
||||
vertex *vy = alloc_v(v->row(), col);
|
||||
v->add_child(vy);
|
||||
if (!fixed_phase())
|
||||
check_polarity(vy, polarity * pol(v));
|
||||
return v;
|
||||
}
|
||||
|
||||
|
|
@ -292,25 +326,31 @@ public:
|
|||
}
|
||||
|
||||
void check_for_eq_and_add_to_val_table(vertex* v, map<mpq, vertex*, obj_hash<mpq>, default_eq<mpq>>& table) {
|
||||
TRACE("cheap_eq", tout << "v="; print(tout, v) << "\n";);
|
||||
vertex *k; // the other vertex
|
||||
if (table.find(val(v), k)) {
|
||||
TRACE("cheap_eq", tout << "found k " ; k->print(tout) << "\n";);
|
||||
TRACE("cheap_eq", tout << "found k " ; print(tout, k) << "\n";);
|
||||
if (k->column() != v->column() &&
|
||||
is_int(k->column()) == is_int(v->column()) &&
|
||||
!is_equal(k->column(), v->column()))
|
||||
!is_equal(k->column(), v->column())) {
|
||||
report_eq(k, v);
|
||||
} else {
|
||||
TRACE("cheap_eq", tout << "no report\n";);
|
||||
}
|
||||
} else {
|
||||
TRACE("cheap_eq", tout << "registered: " << val(v) << " -> { "; v->print(tout) << "} \n";);
|
||||
TRACE("cheap_eq", tout << "registered: " << val(v) << " -> { "; print(tout, v) << "} \n";);
|
||||
table.insert(val(v), v);
|
||||
}
|
||||
}
|
||||
|
||||
void check_for_eq_and_add_to_val_tables(vertex* v) {
|
||||
TRACE("cheap_eq_det", v->print(tout) << "\n";);
|
||||
if (v->neg())
|
||||
check_for_eq_and_add_to_val_table(v, m_vals_to_verts_neg);
|
||||
else
|
||||
check_for_eq_and_add_to_val_table(v, m_vals_to_verts);
|
||||
TRACE("cheap_eq_det", print(tout, v) << "\n";);
|
||||
if (!fixed_phase()) {
|
||||
if (pol(v->column()) == -1)
|
||||
check_for_eq_and_add_to_val_table(v, m_vals_to_verts_neg);
|
||||
else
|
||||
check_for_eq_and_add_to_val_table(v, m_vals_to_verts);
|
||||
}
|
||||
}
|
||||
|
||||
void clear_for_eq() {
|
||||
|
|
@ -319,11 +359,11 @@ public:
|
|||
m_root = nullptr;
|
||||
}
|
||||
|
||||
std::ostream& print_path(const ptr_vector<vertex>& path, std::ostream& out) const {
|
||||
std::ostream& print_path(const ptr_vector<const vertex>& path, std::ostream& out) const {
|
||||
unsigned pr = UINT_MAX;
|
||||
out << "path = \n";
|
||||
for (vertex* k : path) {
|
||||
k->print(out) << "\n";
|
||||
for (const vertex* k : path) {
|
||||
print(out, k) << "\n";
|
||||
if (k->row() != pr) {
|
||||
print_row(out, pr = k->row());
|
||||
}
|
||||
|
|
@ -336,13 +376,13 @@ public:
|
|||
SASSERT(v_i != v_j);
|
||||
SASSERT(lp().get_column_value(v_i->column()) == lp().get_column_value(v_j->column()));
|
||||
TRACE("cheap_eq", tout << v_i->column() << " = " << v_j->column() << "\nu = ";
|
||||
v_i->print(tout) << "\nv = "; v_j->print(tout) <<"\n";
|
||||
print(tout, v_i) << "\nv = "; print(tout, v_j) <<"\n";
|
||||
display_row_of_vertex(v_i, tout);
|
||||
if (v_j->row() != v_i->row())
|
||||
display_row_of_vertex(v_j, tout);
|
||||
);
|
||||
|
||||
ptr_vector<vertex> path;
|
||||
ptr_vector<const vertex> path;
|
||||
find_path_on_tree(path, v_i, v_j);
|
||||
lp::explanation exp = get_explanation_from_path(path);
|
||||
add_eq_on_columns(exp, v_i->column(), v_j->column());
|
||||
|
|
@ -364,19 +404,6 @@ public:
|
|||
lp().settings().stats().m_cheap_eqs++;
|
||||
}
|
||||
|
||||
/**
|
||||
The table functionality:
|
||||
Cheap propagation of equalities x_i = x_j, when
|
||||
x_i = y + k
|
||||
x_j = y + k
|
||||
|
||||
This equalities are detected by maintaining a map:
|
||||
(y, k) -> row_id when a row is of the form x = y + k
|
||||
If x = k, then y is null_lpvar
|
||||
This methods checks whether the given row is an offset row (is_offset_row())
|
||||
and uses the map to find new equalities if that is the case.
|
||||
Some equalities, those spreading more than two rows, can be missed
|
||||
*/
|
||||
// column to theory_var
|
||||
unsigned col_to_imp(unsigned j) const {
|
||||
return lp().local_to_external(lp().column_to_reported_index(j));
|
||||
|
|
@ -391,10 +418,10 @@ public:
|
|||
return lp().column_is_int(j);
|
||||
}
|
||||
|
||||
explanation get_explanation_from_path(const ptr_vector<vertex>& path) const {
|
||||
explanation get_explanation_from_path(const ptr_vector<const vertex>& path) const {
|
||||
explanation ex;
|
||||
unsigned prev_row = UINT_MAX;
|
||||
for (vertex* k : path) {
|
||||
for (const vertex* k : path) {
|
||||
unsigned row = k->row();
|
||||
if (row == prev_row)
|
||||
continue;
|
||||
|
|
@ -423,11 +450,11 @@ public:
|
|||
return print_row(out, k->row());
|
||||
}
|
||||
|
||||
void find_path_on_tree(ptr_vector<vertex> & path, vertex* u, vertex* v) const {
|
||||
TRACE("cheap_eq_details", tout << "u = " ;u->print(tout); tout << "\nv = ";v->print(tout) << "\n";);
|
||||
void find_path_on_tree(ptr_vector<const vertex> & path, const vertex* u, const vertex* v) const {
|
||||
TRACE("cheap_eq_details", tout << "u = " ; print(tout, u); tout << "\nv = ";print(tout, v) << "\n";);
|
||||
vertex* up; // u parent
|
||||
vertex* vp; // v parent
|
||||
ptr_vector<vertex> v_branch;
|
||||
vector<const vertex*> v_branch;
|
||||
path.push_back(u);
|
||||
v_branch.push_back(v);
|
||||
// equalize the levels
|
||||
|
|
@ -445,7 +472,7 @@ public:
|
|||
v = vp;
|
||||
}
|
||||
SASSERT(u->level() == v->level());
|
||||
TRACE("cheap_eq_details", tout << "u = " ;u->print(tout); tout << "\nv = ";v->print(tout) << "\n";);
|
||||
TRACE("cheap_eq_details", tout << "u = " ; print(tout, u); tout << "\nv = "; print(tout, v) << "\n";);
|
||||
while (u != v) {
|
||||
up = u->parent();
|
||||
vp = v->parent();
|
||||
|
|
@ -457,7 +484,7 @@ public:
|
|||
}
|
||||
|
||||
for (unsigned i = v_branch.size(); i--; ) {
|
||||
vertex * bv = v_branch[i];
|
||||
const vertex * bv = v_branch[i];
|
||||
if (path.back() != bv)
|
||||
path.push_back(bv);
|
||||
}
|
||||
|
|
@ -477,8 +504,8 @@ public:
|
|||
return false;
|
||||
}
|
||||
bool tree_is_correct(vertex* v, ptr_vector<vertex>& vs) const {
|
||||
if (fixed_phase() && v->neg())
|
||||
return false;
|
||||
if (fixed_phase())
|
||||
return true;
|
||||
for (vertex * u : v->children()) {
|
||||
if (contains_vertex(u, vs))
|
||||
return false;
|
||||
|
|
@ -495,7 +522,7 @@ public:
|
|||
return true;
|
||||
}
|
||||
std::ostream& print_tree(std::ostream & out, vertex* v) const {
|
||||
v->print(out);
|
||||
print(out, v);
|
||||
out << "\nchildren :\n";
|
||||
for (auto * c : v->children()) {
|
||||
print_tree(out, c);
|
||||
|
|
@ -514,16 +541,15 @@ public:
|
|||
TRACE("cheap_eq", tout << "tree = "; print_tree(tout, m_root) << "\n";);
|
||||
SASSERT(tree_is_correct());
|
||||
explore_under(m_root);
|
||||
if (fixed_phase()) {
|
||||
create_fixed_eqs(m_root);
|
||||
}
|
||||
TRACE("cheap_eq", tout << "done for row_index " << row_index << "\n";);
|
||||
TRACE("cheap_eq", tout << "tree size = " << verts_size(););
|
||||
delete_tree(m_root);
|
||||
m_root = nullptr;
|
||||
set_fixed_vertex(nullptr);
|
||||
m_fixed_vertex_explanation.clear();
|
||||
m_vals_to_verts.reset();
|
||||
m_vals_to_verts_neg.reset();
|
||||
m_pol.reset();
|
||||
}
|
||||
|
||||
void create_fixed_eqs(vertex* v) {
|
||||
|
|
@ -533,8 +559,8 @@ public:
|
|||
}
|
||||
|
||||
std::ostream& print_row(std::ostream & out, unsigned row_index) const {
|
||||
signed_column x, y;
|
||||
if (true || !is_tree_offset_row(row_index, x, y))
|
||||
unsigned x, y; int polarity;
|
||||
if (true || !is_tree_offset_row(row_index, x, y, polarity))
|
||||
return lp().get_int_solver()->display_row_info(out, row_index);
|
||||
|
||||
bool first = true;
|
||||
|
|
@ -553,12 +579,13 @@ public:
|
|||
out << "\n";
|
||||
return out;
|
||||
}
|
||||
|
||||
|
||||
void set_fixed_vertex(vertex *v) {
|
||||
TRACE("cheap_eq", if (v) v->print(tout); else tout << "set m_fixed_vertex to nullptr"; tout << "\n";);
|
||||
void set_fixed_vertex(vertex *v) {
|
||||
TRACE("cheap_eq", if (v) print(tout, v); else tout << "set m_fixed_vertex to nullptr"; tout << "\n";);
|
||||
SASSERT(!m_fixed_vertex || v == nullptr);
|
||||
m_fixed_vertex = v;
|
||||
}
|
||||
|
||||
unsigned verts_size() const {
|
||||
return subtree_size(m_root);
|
||||
}
|
||||
|
|
@ -612,23 +639,39 @@ public:
|
|||
// In case of only one non fixed column, and the function returns true,
|
||||
// this column would be represened by x.
|
||||
bool is_tree_offset_row( unsigned row_index,
|
||||
signed_column & x,
|
||||
signed_column & y) const {
|
||||
unsigned & x, unsigned & y, int & polarity ) const {
|
||||
x = y = UINT_MAX;
|
||||
const row_cell<mpq>* x_cell = nullptr;
|
||||
const row_cell<mpq>* y_cell = nullptr;
|
||||
const auto & row = lp().get_row(row_index);
|
||||
for (unsigned k = 0; k < row.size(); k++) {
|
||||
const auto& c = row[k];
|
||||
if (column_is_fixed(c.var()))
|
||||
continue;
|
||||
if (x.not_set()) {
|
||||
if (!set_sign_and_column(x, c))
|
||||
if (not_set(x)) {
|
||||
if (c.coeff().is_one() || c.coeff().is_minus_one()) {
|
||||
x = c.var();
|
||||
x_cell = & c;
|
||||
} else {
|
||||
return false;
|
||||
} else if (y.not_set()) {
|
||||
if (!set_sign_and_column(y, c))
|
||||
}
|
||||
} else if (not_set(y)) {
|
||||
if (c.coeff().is_one() || c.coeff().is_minus_one()) {
|
||||
y = c.var();
|
||||
y_cell = & c;
|
||||
} else
|
||||
return false;
|
||||
} else
|
||||
return false;
|
||||
}
|
||||
return x.is_set() || y.is_set();
|
||||
}
|
||||
if (is_set(x)) {
|
||||
if (is_set(y))
|
||||
polarity = x_cell->coeff().is_pos() == y_cell->coeff().is_pos()? -1 : 1;
|
||||
else
|
||||
polarity = 1;
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
};
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in a new issue