mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 17:15:31 +00:00
Shared features from polysat branch (#6567)
* Allow setting default debug action * Fix dlist and add iterator * Add var_queue iterator * Add some helpers * rational: machine_div2k and pseudo_inverse * Basic support for non-copyable types in map * tbv helpers * pdd updates * Remove duplicate functions gcc doesn't like having both versions
This commit is contained in:
Jakob Rath
GitHub
parent
be44ace995
commit
d69155b9e9
13 changed files with 456 additions and 62 deletions
|
|
@ -165,6 +165,47 @@ namespace dd {
|
|||
return true;
|
||||
}
|
||||
|
||||
unsigned pdd_manager::min_parity(PDD p) {
|
||||
if (m_semantics != mod2N_e)
|
||||
return 0;
|
||||
|
||||
if (is_val(p)) {
|
||||
rational v = val(p);
|
||||
if (v.is_zero())
|
||||
return m_power_of_2 + 1;
|
||||
unsigned r = 0;
|
||||
while (v.is_even() && v > 0)
|
||||
r++, v /= 2;
|
||||
return r;
|
||||
}
|
||||
init_mark();
|
||||
PDD q = p;
|
||||
m_todo.push_back(hi(q));
|
||||
while (!is_val(q)) {
|
||||
q = lo(q);
|
||||
m_todo.push_back(hi(q));
|
||||
}
|
||||
unsigned p2 = val(q).trailing_zeros();
|
||||
init_mark();
|
||||
while (p2 != 0 && !m_todo.empty()) {
|
||||
PDD r = m_todo.back();
|
||||
m_todo.pop_back();
|
||||
if (is_marked(r))
|
||||
continue;
|
||||
set_mark(r);
|
||||
if (!is_val(r)) {
|
||||
m_todo.push_back(lo(r));
|
||||
m_todo.push_back(hi(r));
|
||||
}
|
||||
else if (val(r).is_zero())
|
||||
continue;
|
||||
else if (val(r).trailing_zeros() < p2)
|
||||
p2 = val(r).trailing_zeros();
|
||||
}
|
||||
m_todo.reset();
|
||||
return p2;
|
||||
}
|
||||
|
||||
pdd pdd_manager::subst_val(pdd const& p, pdd const& s) {
|
||||
return pdd(apply(p.root, s.root, pdd_subst_val_op), this);
|
||||
}
|
||||
|
|
@ -185,7 +226,20 @@ namespace dd {
|
|||
pdd v_val = mk_var(v) + val;
|
||||
return pdd(apply(s.root, v_val.root, pdd_subst_add_op), this);
|
||||
}
|
||||
|
||||
|
||||
bool pdd_manager::subst_get(pdd const& s, unsigned v, rational& out_val) {
|
||||
unsigned level_v = m_var2level[v];
|
||||
PDD p = s.root;
|
||||
while (/* !is_val(p) && */ level(p) > level_v) {
|
||||
SASSERT(is_val(lo(p)));
|
||||
p = hi(p);
|
||||
}
|
||||
if (!is_val(p) && level(p) == level_v) {
|
||||
out_val = val(lo(p));
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
pdd_manager::PDD pdd_manager::apply(PDD arg1, PDD arg2, pdd_op op) {
|
||||
bool first = true;
|
||||
|
|
@ -1154,6 +1208,11 @@ namespace dd {
|
|||
return true;
|
||||
}
|
||||
|
||||
/** Return true iff p contains no variables other than v. */
|
||||
bool pdd_manager::is_univariate_in(PDD p, unsigned v) {
|
||||
return (is_val(p) || var(p) == v) && is_univariate(p);
|
||||
}
|
||||
|
||||
/**
|
||||
* Push coefficients of univariate polynomial in order of ascending degree.
|
||||
* Example: a*x^2 + b*x + c ==> [ c, b, a ]
|
||||
|
|
@ -1532,7 +1591,6 @@ namespace dd {
|
|||
}
|
||||
|
||||
void pdd_manager::gc() {
|
||||
m_gc_generation++;
|
||||
init_dmark();
|
||||
m_free_nodes.reset();
|
||||
SASSERT(well_formed());
|
||||
|
|
@ -1617,26 +1675,26 @@ namespace dd {
|
|||
std::ostream& pdd_manager::display(std::ostream& out, pdd const& b) {
|
||||
auto mons = to_monomials(b);
|
||||
bool first = true;
|
||||
for (auto& m : mons) {
|
||||
for (auto& [a, vs] : mons) {
|
||||
if (!first)
|
||||
out << " ";
|
||||
if (m.first.is_neg())
|
||||
if (a.is_neg())
|
||||
out << "- ";
|
||||
else if (!first)
|
||||
out << "+ ";
|
||||
first = false;
|
||||
rational c = abs(m.first);
|
||||
m.second.reverse();
|
||||
if (!c.is_one() || m.second.empty()) {
|
||||
if (m_semantics == mod2N_e && mod(-c, m_mod2N) < c)
|
||||
out << -mod(-c, m_mod2N);
|
||||
else
|
||||
rational c = abs(a);
|
||||
vs.reverse();
|
||||
if (!c.is_one() || vs.empty()) {
|
||||
if (m_semantics == mod2N_e)
|
||||
out << val_pp(*this, c, !vs.empty());
|
||||
else
|
||||
out << c;
|
||||
if (!m.second.empty()) out << "*";
|
||||
if (!vs.empty()) out << "*";
|
||||
}
|
||||
unsigned v_prev = UINT_MAX;
|
||||
unsigned pow = 0;
|
||||
for (unsigned v : m.second) {
|
||||
for (unsigned v : vs) {
|
||||
if (v == v_prev) {
|
||||
pow++;
|
||||
continue;
|
||||
|
|
@ -1660,6 +1718,23 @@ namespace dd {
|
|||
return out;
|
||||
}
|
||||
|
||||
std::ostream& val_pp::display(std::ostream& out) const {
|
||||
if (m.get_semantics() != pdd_manager::mod2N_e)
|
||||
return out << val;
|
||||
unsigned pow;
|
||||
if (val.is_power_of_two(pow) && pow > 10)
|
||||
return out << "2^" << pow;
|
||||
for (int offset : {-2, -1, 1, 2})
|
||||
if (val < m.max_value() && (val - offset).is_power_of_two(pow) && pow > 10 && pow < m.power_of_2())
|
||||
return out << lparen() << "2^" << pow << (offset >= 0 ? "+" : "") << offset << rparen();
|
||||
rational neg_val = mod(-val, m.two_to_N());
|
||||
if (neg_val < val) { // keep this condition so we don't suddenly print negative values where we wouldn't otherwise
|
||||
if (neg_val.is_power_of_two(pow) && pow > 10)
|
||||
return out << "-2^" << pow;
|
||||
}
|
||||
return out << m.normalize(val);
|
||||
}
|
||||
|
||||
bool pdd_manager::well_formed() {
|
||||
bool ok = true;
|
||||
for (unsigned n : m_free_nodes) {
|
||||
|
|
@ -1737,6 +1812,13 @@ namespace dd {
|
|||
return p.val();
|
||||
}
|
||||
|
||||
rational const& pdd::offset() const {
|
||||
pdd p = *this;
|
||||
while (!p.is_val())
|
||||
p = p.lo();
|
||||
return p.val();
|
||||
}
|
||||
|
||||
pdd pdd::shl(unsigned n) const {
|
||||
return (*this) * rational::power_of_two(n);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ Abstract:
|
|||
Poly DD package
|
||||
|
||||
It is a mild variant of ZDDs.
|
||||
In PDDs arithmetic is either standard or using mod 2 (over GF2).
|
||||
In PDDs arithmetic is either standard or using mod 2^n.
|
||||
|
||||
Non-leaf nodes are of the form x*hi + lo
|
||||
where
|
||||
|
|
@ -208,7 +208,6 @@ namespace dd {
|
|||
rational m_mod2N;
|
||||
unsigned m_power_of_2 = 0;
|
||||
rational m_max_value;
|
||||
unsigned m_gc_generation = 0; ///< will be incremented on each GC
|
||||
|
||||
void reset_op_cache();
|
||||
void init_nodes(unsigned_vector const& l2v);
|
||||
|
|
@ -254,7 +253,9 @@ namespace dd {
|
|||
inline bool is_val(PDD p) const { return m_nodes[p].is_val(); }
|
||||
inline bool is_internal(PDD p) const { return m_nodes[p].is_internal(); }
|
||||
inline bool is_var(PDD p) const { return !is_val(p) && is_zero(lo(p)) && is_one(hi(p)); }
|
||||
inline bool is_max(PDD p) const { SASSERT(m_semantics == mod2_e || m_semantics == mod2N_e); return is_val(p) && val(p) == max_value(); }
|
||||
bool is_never_zero(PDD p);
|
||||
unsigned min_parity(PDD p);
|
||||
inline unsigned level(PDD p) const { return m_nodes[p].m_level; }
|
||||
inline unsigned var(PDD p) const { return m_level2var[level(p)]; }
|
||||
inline PDD lo(PDD p) const { return m_nodes[p].m_lo; }
|
||||
|
|
@ -315,6 +316,11 @@ namespace dd {
|
|||
pdd_manager(unsigned num_vars, semantics s = free_e, unsigned power_of_2 = 0);
|
||||
~pdd_manager();
|
||||
|
||||
pdd_manager(pdd_manager const&) = delete;
|
||||
pdd_manager(pdd_manager&&) = delete;
|
||||
pdd_manager& operator=(pdd_manager const&) = delete;
|
||||
pdd_manager& operator=(pdd_manager&&) = delete;
|
||||
|
||||
semantics get_semantics() const { return m_semantics; }
|
||||
|
||||
void reset(unsigned_vector const& level2var);
|
||||
|
|
@ -343,6 +349,7 @@ namespace dd {
|
|||
pdd subst_val(pdd const& a, unsigned v, rational const& val);
|
||||
pdd subst_val(pdd const& a, pdd const& s);
|
||||
pdd subst_add(pdd const& s, unsigned v, rational const& val);
|
||||
bool subst_get(pdd const& s, unsigned v, rational& out_val);
|
||||
bool resolve(unsigned v, pdd const& p, pdd const& q, pdd& r);
|
||||
pdd reduce(unsigned v, pdd const& a, pdd const& b);
|
||||
void quot_rem(pdd const& a, pdd const& b, pdd& q, pdd& r);
|
||||
|
|
@ -357,6 +364,7 @@ namespace dd {
|
|||
bool is_monomial(PDD p);
|
||||
|
||||
bool is_univariate(PDD p);
|
||||
bool is_univariate_in(PDD p, unsigned v);
|
||||
void get_univariate_coefficients(PDD p, vector<rational>& coeff);
|
||||
|
||||
// create an spoly r if leading monomials of a and b overlap
|
||||
|
|
@ -375,6 +383,8 @@ namespace dd {
|
|||
unsigned power_of_2() const { return m_power_of_2; }
|
||||
rational const& max_value() const { return m_max_value; }
|
||||
rational const& two_to_N() const { return m_mod2N; }
|
||||
rational normalize(rational const& n) const { return mod(-n, m_mod2N) < n ? -mod(-n, m_mod2N) : n; }
|
||||
|
||||
|
||||
unsigned_vector const& free_vars(pdd const& p);
|
||||
|
||||
|
|
@ -406,21 +416,26 @@ namespace dd {
|
|||
unsigned var() const { return m.var(root); }
|
||||
rational const& val() const { SASSERT(is_val()); return m.val(root); }
|
||||
rational const& leading_coefficient() const;
|
||||
rational const& offset() const;
|
||||
bool is_val() const { return m.is_val(root); }
|
||||
bool is_one() const { return m.is_one(root); }
|
||||
bool is_zero() const { return m.is_zero(root); }
|
||||
bool is_linear() const { return m.is_linear(root); }
|
||||
bool is_var() const { return m.is_var(root); }
|
||||
/** Polynomial is of the form a * x + b for numerals a, b. */
|
||||
bool is_max() const { return m.is_max(root); }
|
||||
/** Polynomial is of the form a * x + b for some numerals a, b. */
|
||||
bool is_unilinear() const { return !is_val() && lo().is_val() && hi().is_val(); }
|
||||
/** Polynomial is of the form a * x for some numeral a. */
|
||||
bool is_unary() const { return !is_val() && lo().is_zero() && hi().is_val(); }
|
||||
bool is_offset() const { return !is_val() && lo().is_val() && hi().is_one(); }
|
||||
bool is_binary() const { return m.is_binary(root); }
|
||||
bool is_monomial() const { return m.is_monomial(root); }
|
||||
bool is_univariate() const { return m.is_univariate(root); }
|
||||
bool is_univariate_in(unsigned v) const { return m.is_univariate_in(root, v); }
|
||||
void get_univariate_coefficients(vector<rational>& coeff) const { m.get_univariate_coefficients(root, coeff); }
|
||||
vector<rational> get_univariate_coefficients() const { vector<rational> coeff; m.get_univariate_coefficients(root, coeff); return coeff; }
|
||||
bool is_never_zero() const { return m.is_never_zero(root); }
|
||||
unsigned min_parity() const { return m.min_parity(root); }
|
||||
bool var_is_leaf(unsigned v) const { return m.var_is_leaf(root, v); }
|
||||
|
||||
pdd operator-() const { return m.minus(*this); }
|
||||
|
|
@ -455,7 +470,8 @@ namespace dd {
|
|||
pdd subst_val0(vector<std::pair<unsigned, rational>> const& s) const { return m.subst_val0(*this, s); }
|
||||
pdd subst_val(pdd const& s) const { return m.subst_val(*this, s); }
|
||||
pdd subst_val(unsigned v, rational const& val) const { return m.subst_val(*this, v, val); }
|
||||
pdd subst_add(unsigned var, rational const& val) { return m.subst_add(*this, var, val); }
|
||||
pdd subst_add(unsigned var, rational const& val) const { return m.subst_add(*this, var, val); }
|
||||
bool subst_get(unsigned var, rational& out_val) const { return m.subst_get(*this, var, out_val); }
|
||||
|
||||
/**
|
||||
* \brief substitute variable v by r.
|
||||
|
|
@ -538,6 +554,18 @@ namespace dd {
|
|||
bool operator!=(pdd_iterator const& other) const { return m_nodes != other.m_nodes; }
|
||||
};
|
||||
|
||||
class val_pp {
|
||||
pdd_manager const& m;
|
||||
rational const& val;
|
||||
bool require_parens;
|
||||
char const* lparen() const { return require_parens ? "(" : ""; }
|
||||
char const* rparen() const { return require_parens ? ")" : ""; }
|
||||
public:
|
||||
val_pp(pdd_manager const& m, rational const& val, bool require_parens = false): m(m), val(val), require_parens(require_parens) {}
|
||||
std::ostream& display(std::ostream& out) const;
|
||||
};
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& out, val_pp const& v) { return v.display(out); }
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue