mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

Test and memoize pdd factoring (#5163)

Browse source 
* Test and fix pdd_manager::factor

* Memoize pdd_manager::factor

* Fix Windows build (maybe)
This commit is contained in:
Jakob Rath 2021-04-09 19:13:39 +02:00 • committed by Nikolaj Bjorner
parent f8562380d6
commit 75c87a2869
3 changed files with 102 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/math/dd/dd_pdd.cpp
View file

@ -50,6 +50,7 @@ namespace dd {
void pdd_manager::reset(unsigned_vector const& level2var) {
reset_op_cache();
m_factor_cache.reset();
m_node_table.reset();
m_nodes.reset();
m_free_nodes.reset();
@ -691,27 +692,36 @@ namespace dd {
* factor p into lc*v^degree + rest
* such that degree(rest, v) < degree
* Initial implementation is very naive
* - memoize intermediary results
*/
void pdd_manager::factor(pdd const& p, unsigned v, unsigned degree, pdd& lc, pdd& rest) {
unsigned level_v = m_var2level[v];
if (degree == 0) {
lc = p;
rest = zero();
return;
}
else if (level(p.root) < level_v) {
if (level(p.root) < level_v) {
lc = zero();
rest = p;
return;
}
else if (level(p.root) > level_v) {
// Memoize nontrivial cases
auto* et = m_factor_cache.insert_if_not_there2({p.root, v, degree});
factor_entry& e = et->get_data();
if (e.is_valid()) {
lc = pdd(e.m_lc, this);
rest = pdd(e.m_rest, this);
return;
}
if (level(p.root) > level_v) {
pdd lc1 = zero(), rest1 = zero();
pdd vv = mk_var(p.var());
factor(p.hi(), v, degree, lc, rest);
factor(p.lo(), v, degree, lc1, rest1);
lc += lc1;
rest += rest1;
lc *= vv;
rest *= vv;
lc += lc1;
rest += rest1;
}
else {
unsigned d = 0;
@ -733,6 +743,8 @@ namespace dd {
rest = p;
}
}
e.m_lc = lc.root;
e.m_rest = rest.root;
}
@ -1169,6 +1181,8 @@ namespace dd {
m_op_cache.insert(e);
}
m_factor_cache.reset();
m_node_table.reset();
// re-populate node cache
for (unsigned i = m_nodes.size(); i-- > 2; ) {

37
src/math/dd/dd_pdd.h
View file

@ -140,9 +140,44 @@ namespace dd {
typedef ptr_hashtable<op_entry, hash_entry, eq_entry> op_table;
struct factor_entry {
factor_entry(PDD p, unsigned v, unsigned degree):
m_p(p),
m_v(v),
m_degree(degree),
m_lc(UINT_MAX),
m_rest(UINT_MAX)
{}
factor_entry(): m_p(0), m_v(0), m_degree(0), m_lc(UINT_MAX), m_rest(UINT_MAX) {}
PDD m_p; // input
unsigned m_v; // input
unsigned m_degree; // input
PDD m_lc; // output
PDD m_rest; // output
bool is_valid() { return m_lc != UINT_MAX; }
unsigned hash() const { return mk_mix(m_p, m_v, m_degree); }
};
struct hash_factor_entry {
unsigned operator()(factor_entry const& e) const { return e.hash(); }
};
struct eq_factor_entry {
bool operator()(factor_entry const& a, factor_entry const& b) const {
return a.m_p == b.m_p && a.m_v == b.m_v && a.m_degree == b.m_degree;
}
};
typedef hashtable<factor_entry, hash_factor_entry, eq_factor_entry> factor_table;
svector<node> m_nodes;
vector<rational> m_values;
op_table m_op_cache;
factor_table m_factor_cache;
node_table m_node_table;
mpq_table m_mpq_table;
svector<PDD> m_pdd_stack;
@ -361,7 +396,7 @@ namespace dd {
pdd rev_sub(rational const& r) const { return m.sub(m.mk_val(r), *this); }
pdd reduce(pdd const& other) const { return m.reduce(*this, other); }
bool different_leading_term(pdd const& other) const { return m.different_leading_term(*this, other); }
void factor(unsigned v, unsigned degree, pdd& lc, pdd& rest) { m.factor(*this, v, degree, lc, rest); }
void factor(unsigned v, unsigned degree, pdd& lc, pdd& rest) const { m.factor(*this, v, degree, lc, rest); }
pdd subst_val(vector<std::pair<unsigned, rational>> 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); }