mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 05:18:44 +00:00
debug order lemma, introduce sign for factors
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
parent
218e155603
commit
54ba889b7b
|
|
@ -493,6 +493,8 @@ namespace smt {
|
|||
TRACE("lemma", tout << strm.str() << "\n";);
|
||||
display_lemma_as_smt_problem(out, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic);
|
||||
out.close();
|
||||
if (m_lemma_id==6184)
|
||||
exit(0);
|
||||
return m_lemma_id;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -14,7 +14,7 @@ void const_iterator_mon::init_vars_by_the_mask(unsigned_vector & k_vars, unsigne
|
|||
}
|
||||
}
|
||||
}
|
||||
|
||||
// todo : do we need the sign?
|
||||
bool const_iterator_mon::get_factors(factor& k, factor& j, rational& sign) const {
|
||||
unsigned_vector k_vars;
|
||||
unsigned_vector j_vars;
|
||||
|
|
@ -30,7 +30,7 @@ bool const_iterator_mon::get_factors(factor& k, factor& j, rational& sign) const
|
|||
if (!m_ff->find_rm_monomial_of_vars(k_vars, i)) {
|
||||
return false;
|
||||
}
|
||||
k.set(i, factor_type::RM);
|
||||
k.set(i, factor_type::MON);
|
||||
}
|
||||
|
||||
if (j_vars.size() == 1) {
|
||||
|
|
@ -40,7 +40,7 @@ bool const_iterator_mon::get_factors(factor& k, factor& j, rational& sign) const
|
|||
if (!m_ff->find_rm_monomial_of_vars(j_vars, i)) {
|
||||
return false;
|
||||
}
|
||||
j.set(i, factor_type::RM);
|
||||
j.set(i, factor_type::MON);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -27,14 +27,16 @@ namespace nla {
|
|||
struct factorization_factory;
|
||||
typedef unsigned lpvar;
|
||||
|
||||
enum class factor_type { VAR, RM }; // RM stands for rooted monomial
|
||||
enum class factor_type { VAR, MON };
|
||||
|
||||
class factor {
|
||||
lpvar m_var;
|
||||
factor_type m_type;
|
||||
bool m_sign;
|
||||
public:
|
||||
factor(): m_var(UINT_MAX), m_type(factor_type::VAR) {}
|
||||
explicit factor(lpvar v, factor_type t) : m_var(v), m_type(t) {}
|
||||
factor(): factor(false) {}
|
||||
factor(bool sign): m_var(UINT_MAX), m_type(factor_type::VAR), m_sign(sign) {}
|
||||
explicit factor(lpvar v, factor_type t) : m_var(v), m_type(t), m_sign(false) {}
|
||||
unsigned var() const { return m_var; }
|
||||
factor_type type() const { return m_type; }
|
||||
void set(lpvar v, factor_type t) { m_var = v; m_type = t; }
|
||||
|
|
@ -45,6 +47,9 @@ public:
|
|||
bool operator!=(factor const& other) const {
|
||||
return m_var != other.var() || m_type != other.type();
|
||||
}
|
||||
bool sign() const { return m_sign; }
|
||||
bool& sign() { return m_sign; }
|
||||
rational rsign() const { return m_sign? rational(-1) : rational(1); }
|
||||
};
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -36,7 +36,6 @@ template <typename T> rational common::val(T const& t) const { return c().val(t)
|
|||
template rational common::val<monomial>(monomial const& t) const;
|
||||
template rational common::val<factor>(factor const& t) const;
|
||||
rational common::val(lpvar t) const { return c().val(t); }
|
||||
rational common::rval(const monomial& m) const { return c().rval(m); }
|
||||
template <typename T> lpvar common::var(T const& t) const { return c().var(t); }
|
||||
template lpvar common::var<factor>(factor const& t) const;
|
||||
template lpvar common::var<monomial>(monomial const& t) const;
|
||||
|
|
|
|||
|
|
@ -76,10 +76,14 @@ bool core::lemma_holds(const lemma& l) const {
|
|||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
lpvar core::map_to_root(lpvar j) const {
|
||||
return m_evars.find(j).var();
|
||||
}
|
||||
|
||||
svector<lpvar> core::sorted_vars(const factor& f) const {
|
||||
svector<lpvar> core::sorted_rvars(const factor& f) const {
|
||||
if (f.is_var()) {
|
||||
svector<lpvar> r; r.push_back(f.var());
|
||||
svector<lpvar> r; r.push_back(map_to_root(f.var()));
|
||||
return r;
|
||||
}
|
||||
TRACE("nla_solver", tout << "nv";);
|
||||
|
|
@ -89,14 +93,23 @@ svector<lpvar> core::sorted_vars(const factor& f) const {
|
|||
// the value of the factor is equal to the value of the variable multiplied
|
||||
// by the canonize_sign
|
||||
rational core::canonize_sign(const factor& f) const {
|
||||
return f.is_var()? canonize_sign_of_var(f.var()) : m_emons[f.var()].rsign();
|
||||
return f.rsign() * (f.is_var()? canonize_sign_of_var(f.var()) : m_emons[f.var()].rsign());
|
||||
}
|
||||
|
||||
rational core::canonize_sign_of_var(lpvar j) const {
|
||||
return m_evars.find(j).rsign();
|
||||
}
|
||||
|
||||
|
||||
bool core::canonize_sign_is_correct(const monomial& m) const {
|
||||
rational r(1);
|
||||
for (lpvar j : m.vars()) {
|
||||
r *= canonize_sign_of_var(j);
|
||||
}
|
||||
return r == m.rsign();
|
||||
}
|
||||
|
||||
rational core::canonize_sign(const monomial& m) const {
|
||||
SASSERT(canonize_sign_is_correct(m));
|
||||
return m.rsign();
|
||||
}
|
||||
|
||||
|
|
@ -157,11 +170,13 @@ std::ostream& core::print_product(const T & m, std::ostream& out) const {
|
|||
}
|
||||
|
||||
std::ostream & core::print_factor(const factor& f, std::ostream& out) const {
|
||||
if (f.sign())
|
||||
out << "- ";
|
||||
if (f.is_var()) {
|
||||
out << "VAR, ";
|
||||
print_var(f.var(), out);
|
||||
} else {
|
||||
out << "PROD, ";
|
||||
out << "MON, ";
|
||||
print_product(m_emons[f.var()].rvars(), out);
|
||||
}
|
||||
out << "\n";
|
||||
|
|
@ -1372,30 +1387,38 @@ std::unordered_set<lpvar> core::collect_vars(const lemma& l) const {
|
|||
return vars;
|
||||
}
|
||||
|
||||
// divides bc by c, so bc = b*c
|
||||
bool core::divide(const monomial& bc, const factor& c, factor & b) const {
|
||||
svector<lpvar> c_vars = sorted_vars(c);
|
||||
TRACE("nla_solver_div",
|
||||
tout << "c_vars = ";
|
||||
print_product(c_vars, tout);
|
||||
tout << "\nbc_vars = ";
|
||||
svector<lpvar> c_rvars = sorted_rvars(c);
|
||||
TRACE("nla_solver",
|
||||
tout << "c_rvars = ";
|
||||
print_product(c_rvars, tout);
|
||||
tout << "\nbc_rvars = ";
|
||||
print_product(bc.rvars(), tout););
|
||||
if (!lp::is_proper_factor(c_vars, bc.rvars()))
|
||||
if (!lp::is_proper_factor(c_rvars, bc.rvars()))
|
||||
return false;
|
||||
|
||||
auto b_vars = lp::vector_div(bc.rvars(), c_vars);
|
||||
TRACE("nla_solver_div", tout << "b_vars = "; print_product(b_vars, tout););
|
||||
SASSERT(b_vars.size() > 0);
|
||||
if (b_vars.size() == 1) {
|
||||
b = factor(b_vars[0], factor_type::VAR);
|
||||
return true;
|
||||
auto b_rvars = lp::vector_div(bc.rvars(), c_rvars);
|
||||
TRACE("nla_solver_div", tout << "b_rvars = "; print_product(b_rvars, tout););
|
||||
SASSERT(b_rvars.size() > 0);
|
||||
if (b_rvars.size() == 1) {
|
||||
b = factor(b_rvars[0], factor_type::VAR);
|
||||
} else {
|
||||
monomial const* sv = m_emons.find_canonical(b_rvars);
|
||||
if (!sv) {
|
||||
TRACE("nla_solver_div", tout << "not in rooted";);
|
||||
return false;
|
||||
}
|
||||
b = factor(sv->var(), factor_type::MON);
|
||||
}
|
||||
monomial const* sv = m_emons.find_canonical(b_vars);
|
||||
if (!sv) {
|
||||
TRACE("nla_solver_div", tout << "not in rooted";);
|
||||
return false;
|
||||
}
|
||||
b = factor(sv->var(), factor_type::RM);
|
||||
TRACE("nla_solver_div", tout << "success div:"; print_factor(b, tout););
|
||||
SASSERT(!b.sign());
|
||||
// we should have bc.vars()*canonize_sign(bc) = bc.rvar() = b.rvars()*c.rvars() =
|
||||
// = canonize_sign(b)*b.vars()* canonize_sign(c)*c.vars().
|
||||
// so bc.vars()*canonize_sign(bc) = canonize_sign(b)*b.vars()* canonize_sign(c)*c.vars().
|
||||
// but canonize_sign(b) now is canonize_sign_of_var(b.m_var) or canonize_sign(m_monomials[b.m_var])
|
||||
// so we are adjusting it
|
||||
b.sign() = (canonize_sign(b) * canonize_sign(c) * canonize_sign(bc) == rational(1))? false: true;
|
||||
TRACE("nla_solver", tout << "success div:"; print_factor(b, tout););
|
||||
return true;
|
||||
}
|
||||
|
||||
|
|
@ -1468,8 +1491,8 @@ void core::maybe_add_a_factor(lpvar i,
|
|||
}
|
||||
} else {
|
||||
if (try_insert(i, found_rm)) {
|
||||
r.push_back(factor(i, factor_type::RM));
|
||||
TRACE("nla_solver", tout << "inserting factor = "; print_factor_with_vars(factor(i, factor_type::RM), tout); );
|
||||
r.push_back(factor(i, factor_type::MON));
|
||||
TRACE("nla_solver", tout << "inserting factor = "; print_factor_with_vars(factor(i, factor_type::MON), tout); );
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -100,17 +100,17 @@ public:
|
|||
|
||||
rational val(const monomial& m) const { return m_lar_solver.get_column_value_rational(m.var()); }
|
||||
|
||||
rational rval(const monomial& m) const { return val(m)*m.rsign(); }
|
||||
bool canonize_sign_is_correct(const monomial& m) const;
|
||||
|
||||
lpvar var(monomial const& sv) const { return sv.var(); }
|
||||
|
||||
rational val_rooted(const monomial& m) const { return m.rsign()*val(m.var()); }
|
||||
|
||||
rational val(const factor& f) const { return f.is_var()? val(f.var()) : val(m_emons[f.var()]); }
|
||||
rational val(const factor& f) const { return f.rsign() * (f.is_var()? val(f.var()) : val(m_emons[f.var()])); }
|
||||
|
||||
lpvar var(const factor& f) const { return f.var(); }
|
||||
|
||||
svector<lpvar> sorted_vars(const factor& f) const;
|
||||
svector<lpvar> sorted_rvars(const factor& f) const;
|
||||
bool done() const;
|
||||
|
||||
void add_empty_lemma();
|
||||
|
|
@ -338,6 +338,7 @@ public:
|
|||
bool no_lemmas_hold() const;
|
||||
|
||||
lbool test_check(vector<lemma>& l);
|
||||
lpvar map_to_root(lpvar) const;
|
||||
}; // end of core
|
||||
|
||||
struct pp_mon {
|
||||
|
|
|
|||
|
|
@ -95,14 +95,15 @@ void order::order_lemma_on_binomial_sign(const monomial& xy, lpvar x, lpvar y, i
|
|||
}
|
||||
|
||||
// We look for monomials e = m.rvars()[k]*d and see if we can create an order lemma for m and e
|
||||
void order::order_lemma_on_factor_binomial_explore(const monomial& m, bool k) {
|
||||
TRACE("nla_solver", tout << "m = " << pp_rmon(c(), m););
|
||||
SASSERT(m.size() == 2);
|
||||
lpvar c = m.vars()[k];
|
||||
void order::order_lemma_on_factor_binomial_explore(const monomial& ac, bool k) {
|
||||
TRACE("nla_solver", tout << "ac = " << pp_rmon(c(), ac););
|
||||
SASSERT(ac.size() == 2);
|
||||
lpvar c = ac.vars()[k];
|
||||
|
||||
for (monomial const& m2 : _().m_emons.get_products_of(c)) {
|
||||
TRACE("nla_solver", tout << "m2 = " << pp_rmon(_(), m2););
|
||||
order_lemma_on_factor_binomial_rm(m, k, m2);
|
||||
for (monomial const& bd : _().m_emons.get_products_of(c)) {
|
||||
if (bd.var() == ac.var()) continue;
|
||||
TRACE("nla_solver", tout << "bd = " << pp_rmon(_(), bd););
|
||||
order_lemma_on_factor_binomial_rm(ac, k, bd);
|
||||
if (done()) {
|
||||
break;
|
||||
}
|
||||
|
|
@ -118,18 +119,19 @@ void order::order_lemma_on_factor_binomial_rm(const monomial& ac, bool k, const
|
|||
tout << "bd=" << pp_rmon(_(), bd) << "\n";
|
||||
);
|
||||
factor d(_().m_evars.find(ac.vars()[k]).var(), factor_type::VAR);
|
||||
factor b;
|
||||
factor b(false);
|
||||
if (c().divide(bd, d, b)) {
|
||||
order_lemma_on_binomial_ac_bd(ac, k, bd, b, d.var());
|
||||
}
|
||||
}
|
||||
|
||||
// suppose ac >= bd and |c| = |d| => then ac/|c| >= bd/|d|
|
||||
// ac >= bd && |c| = |d| => ac/|c| >= bd/|d|
|
||||
void order::order_lemma_on_binomial_ac_bd(const monomial& ac, bool k, const monomial& bd, const factor& b, lpvar d) {
|
||||
TRACE("nla_solver",
|
||||
tout << "ac=" << pp_rmon(_(), ac) << "\nrm= " << pp_rmon(_(), bd) << ", b= " << pp_fac(_(), b) << ", d= " << pp_var(_(), d) << "\n";);
|
||||
lpvar a = ac.vars()[!k];
|
||||
lpvar c = ac.vars()[k];
|
||||
TRACE("nla_solver",
|
||||
tout << "ac = " << pp_mon(_(), ac) << "a = " << pp_var(_(), a) << "c = " << pp_var(_(), c) << "\nbd = " << pp_mon(_(), bd) << "b = " << pp_fac(_(), b) << "d = " << pp_var(_(), d) << "\n";
|
||||
);
|
||||
SASSERT(_().m_evars.find(c).var() == d);
|
||||
rational acv = val(ac);
|
||||
rational av = val(a);
|
||||
|
|
@ -139,7 +141,10 @@ void order::order_lemma_on_binomial_ac_bd(const monomial& ac, bool k, const mono
|
|||
rational bv = val(b);
|
||||
// Notice that ac/|c| = a*c_sign , and bd/|d| = b*d_sign
|
||||
auto av_c_s = av*c_sign; auto bv_d_s = bv*d_sign;
|
||||
|
||||
TRACE("nla_solver",
|
||||
tout << "acv = " << acv << ", av = " << av << ", c_sign = " << c_sign << ", d_sign = " << d_sign << ", bdv = " << bdv <<
|
||||
"\nbv = " << bv << ", av_c_s = " << av_c_s << ", bv_d_s = " << bv_d_s << "\n";);
|
||||
|
||||
if (acv >= bdv && av_c_s < bv_d_s)
|
||||
generate_mon_ol(ac, a, c_sign, c, bd, b, d_sign, d, llc::LT);
|
||||
else if (acv <= bdv && av_c_s > bv_d_s)
|
||||
|
|
@ -198,7 +203,7 @@ bool order::order_lemma_on_ac_and_bc(const monomial& rm_ac,
|
|||
tout << "rm_bd = " << pp_rmon(_(), rm_bd) << "\n";
|
||||
tout << "ac_f[k] = ";
|
||||
c().print_factor_with_vars(ac_f[k], tout););
|
||||
factor b;
|
||||
factor b(false);
|
||||
return
|
||||
c().divide(rm_bd, ac_f[k], b) &&
|
||||
order_lemma_on_ac_and_bc_and_factors(rm_ac, ac_f[!k], ac_f[k], rm_bd, b);
|
||||
|
|
@ -218,7 +223,7 @@ void order::order_lemma_on_factorization(const monomial& m, const factorization&
|
|||
if (mv == fv)
|
||||
return;
|
||||
bool gt = mv > fv;
|
||||
TRACE("nla_solver_f", tout << "m="; _().print_monomial_with_vars(m, tout); tout << "\nfactorization="; _().print_factorization(ab, tout););
|
||||
TRACE("nla_solver", tout << "m="; _().print_monomial_with_vars(m, tout); tout << "\nfactorization="; _().print_factorization(ab, tout););
|
||||
for (unsigned j = 0, k = 1; j < 2; j++, k--) {
|
||||
order_lemma_on_ab(m, sign, var(ab[k]), var(ab[j]), gt);
|
||||
explain(ab); explain(m);
|
||||
|
|
|
|||
|
|
@ -1,251 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2017 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
<name>
|
||||
|
||||
Abstract:
|
||||
|
||||
<abstract>
|
||||
|
||||
Author:
|
||||
Nikolaj Bjorner (nbjorner)
|
||||
Lev Nachmanson (levnach)
|
||||
|
||||
Revision History:
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
namespace nla {
|
||||
|
||||
typedef lp::constraint_index lpci;
|
||||
typedef lp::explanation expl_set;
|
||||
typedef lp::var_index lpvar;
|
||||
struct hash_svector {
|
||||
size_t operator()(const unsigned_vector & v) const {
|
||||
return svector_hash<unsigned_hash>()(v);
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
|
||||
struct vars_equivalence {
|
||||
|
||||
struct equiv {
|
||||
lpvar m_i;
|
||||
lpvar m_j;
|
||||
rational m_sign;
|
||||
lpci m_c0;
|
||||
lpci m_c1;
|
||||
|
||||
equiv(lpvar i, lpvar j, rational const& sign, lpci c0, lpci c1) :
|
||||
m_i(i),
|
||||
m_j(j),
|
||||
m_sign(sign),
|
||||
m_c0(c0),
|
||||
m_c1(c1) {
|
||||
SASSERT(m_i != m_j);
|
||||
}
|
||||
};
|
||||
|
||||
struct node {
|
||||
unsigned m_parent; // points to m_equivs
|
||||
svector<unsigned> m_children; // point to m_equivs
|
||||
node() : m_parent(-1) {}
|
||||
};
|
||||
|
||||
//fields
|
||||
|
||||
// The map from the variables to m_nodes
|
||||
// m_tree is a spanning tree of the graph of equivs represented by m_equivs
|
||||
std::unordered_map<unsigned, node> m_tree;
|
||||
// If m_tree[v] == -1 then the variable is a root.
|
||||
// if m_tree[v] is not equal to -1 then m_equivs[m_tree[v]] = (k, v) or (v, k), where k is the parent of v
|
||||
vector<equiv> m_equivs; // all equivalences extracted from constraints
|
||||
std::function<rational(lpvar)> m_val;
|
||||
|
||||
|
||||
// constructor
|
||||
vars_equivalence(std::function<rational(lpvar)> val) : m_val(val) {}
|
||||
|
||||
void clear() {
|
||||
m_equivs.clear();
|
||||
m_tree.clear();
|
||||
}
|
||||
|
||||
// j itself is also included
|
||||
svector<lpvar> eq_vars(lpvar j) const {
|
||||
svector<lpvar> r = path_to_root(j);
|
||||
r.append(children(j));
|
||||
r.push_back(j);
|
||||
return r;
|
||||
}
|
||||
|
||||
svector<lpvar> children(lpvar j) const {
|
||||
svector<lpvar> r;
|
||||
auto it = m_tree.find(j);
|
||||
if (it == m_tree.end())
|
||||
return r;
|
||||
|
||||
const node& n = it->second;
|
||||
for (unsigned e_k: n.m_children) {
|
||||
const equiv & e = m_equivs[e_k];
|
||||
lpvar oj = e.m_i == j? e.m_j : e.m_i;
|
||||
r.push_back(oj);
|
||||
for (lpvar k : children(oj)) {
|
||||
r.push_back(k);
|
||||
}
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
||||
|
||||
|
||||
svector<lpvar> path_to_root(lpvar j) const {
|
||||
svector<lpvar> r;
|
||||
while (true) {
|
||||
auto it = m_tree.find(j);
|
||||
if (it == m_tree.end() || it->second.m_parent == static_cast<unsigned>(-1))
|
||||
return r;
|
||||
|
||||
const equiv & e = m_equivs[it->second.m_parent];
|
||||
j = get_parent_node(j, e);
|
||||
r.push_back(j);
|
||||
}
|
||||
SASSERT(false);
|
||||
}
|
||||
|
||||
|
||||
unsigned size() const { return static_cast<unsigned>(m_tree.size()); }
|
||||
|
||||
// we create a spanning tree on all variables participating in an equivalence
|
||||
void create_tree() {
|
||||
for (unsigned k = 0; k < m_equivs.size(); k++)
|
||||
connect_equiv_to_tree(k);
|
||||
}
|
||||
|
||||
void add_equiv(lpvar i, lpvar j, rational const& sign, lpci c0, lpci c1) {
|
||||
m_equivs.push_back(equiv(i, j, sign, c0, c1));
|
||||
}
|
||||
|
||||
void connect_equiv_to_tree(unsigned k) {
|
||||
// m_tree is the tree with the edges formed by m_equivs
|
||||
const equiv &e = m_equivs[k];
|
||||
TRACE("nla_vars_eq", tout << "m_i = " << e.m_i << ", " << "m_j = " << e.m_j ;);
|
||||
auto it_i = m_tree.find(e.m_i);
|
||||
auto it_j = m_tree.find(e.m_j);
|
||||
bool i_is_in = it_i != m_tree.end();
|
||||
bool j_is_in = it_j != m_tree.end();
|
||||
|
||||
if (!(i_is_in || j_is_in)) {
|
||||
// none of the edge vertices is in the tree
|
||||
// let m_i be the parent, and m_j be the child
|
||||
TRACE("nla_vars_eq", tout << "create nodes for " << e.m_i << " and " << e.m_j; );
|
||||
node parent;
|
||||
node child;
|
||||
child.m_parent = k;
|
||||
parent.m_children.push_back(k);
|
||||
m_tree.emplace(e.m_i, parent);
|
||||
m_tree.emplace(e.m_j, child);
|
||||
} else if (i_is_in && (!j_is_in)) {
|
||||
// create a node for m_j, with m_i is the parent
|
||||
node child;
|
||||
child.m_parent = k;
|
||||
TRACE("nla_vars_eq", tout << "create a node for " << e.m_j; );
|
||||
m_tree.emplace(e.m_j, child);
|
||||
it_i->second.m_children.push_back(k);
|
||||
} else if ((!i_is_in) && j_is_in) {
|
||||
TRACE("nla_vars_eq", tout << "create a node for " << e.m_i; );
|
||||
node child;
|
||||
child.m_parent = k;
|
||||
m_tree.emplace(e.m_i, child);
|
||||
it_j->second.m_children.push_back(k);
|
||||
} else {
|
||||
TRACE("nla_vars_eq", tout << "both vertices are in the tree";);
|
||||
}
|
||||
}
|
||||
|
||||
bool empty() const {
|
||||
return m_tree.empty();
|
||||
}
|
||||
|
||||
bool is_root(unsigned j) const {
|
||||
auto it = m_tree.find(j);
|
||||
if (it == m_tree.end())
|
||||
return true;
|
||||
|
||||
return it->second.m_parent == static_cast<unsigned>(-1);
|
||||
}
|
||||
|
||||
static unsigned get_parent_node(unsigned j, const equiv& e) {
|
||||
SASSERT(e.m_i == j || e.m_j == j);
|
||||
return e.m_i == j? e.m_j : e.m_i;
|
||||
}
|
||||
|
||||
bool vars_are_equiv(lpvar a, lpvar b) const {
|
||||
return map_to_root(a) == map_to_root(b);
|
||||
}
|
||||
|
||||
|
||||
// Finds the root var which is equivalent to j.
|
||||
// The sign is flipped if needed
|
||||
lpvar map_to_root(lpvar j, rational& sign) const {
|
||||
TRACE("nla_vars_eq", tout << "j = " << j << "\n";);
|
||||
while (true) {
|
||||
auto it = m_tree.find(j);
|
||||
if (it == m_tree.end())
|
||||
return j;
|
||||
if (it->second.m_parent == static_cast<unsigned>(-1)) {
|
||||
TRACE("nla_vars_eq", tout << "mapped to " << j << "\n";);
|
||||
return j;
|
||||
}
|
||||
const equiv & e = m_equivs[it->second.m_parent];
|
||||
sign *= e.m_sign;
|
||||
j = get_parent_node(j, e);
|
||||
}
|
||||
}
|
||||
|
||||
// Finds the root var which is equivalent to j.
|
||||
// The sign is flipped if needed
|
||||
lpvar map_to_root(lpvar j) const {
|
||||
while (true) {
|
||||
auto it = m_tree.find(j);
|
||||
if (it == m_tree.end())
|
||||
return j;
|
||||
if (it->second.m_parent == static_cast<unsigned>(-1))
|
||||
return j;
|
||||
const equiv & e = m_equivs[it->second.m_parent];
|
||||
j = get_parent_node(j, e);
|
||||
}
|
||||
}
|
||||
|
||||
template <typename T>
|
||||
void explain(const T& collection, expl_set & exp) const {
|
||||
for (lpvar j : collection) {
|
||||
explain(j, exp);
|
||||
}
|
||||
}
|
||||
void explain(lpvar j, expl_set& exp) const {
|
||||
while (true) {
|
||||
auto it = m_tree.find(j);
|
||||
if (it == m_tree.end())
|
||||
return;
|
||||
if (it->second.m_parent == static_cast<unsigned>(-1))
|
||||
return;
|
||||
const equiv & e = m_equivs[it->second.m_parent];
|
||||
exp.add(e.m_c0);
|
||||
exp.add(e.m_c1);
|
||||
j = get_parent_node(j, e);
|
||||
}
|
||||
}
|
||||
|
||||
template <typename T>
|
||||
void add_explanation_of_reducing_to_rooted_monomial(const T & m, expl_set & exp) const {
|
||||
for (lpvar j : m)
|
||||
explain(j, exp);
|
||||
}
|
||||
|
||||
}; // end of vars_equivalence
|
||||
}
|
||||
Loading…
Reference in a new issue