mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

adding level2var

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-22 11:51:04 -08:00
parent 58be42d2a9
commit 25b98f497a
4 changed files with 50 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -544,6 +544,14 @@ namespace dd {
reserve_var(i);
return pdd(m_var2pdd[i], this);
}
void pdd_manager::set_level2var(unsigned_vector const& level2var) {
SASSERT(level2var.size() == m_level2var.size());
for (unsigned i = 0; i < level2var.size(); ++i) {
m_var2level[level2var[i]] = i;
m_level2var[i] = level2var[i];
}
}
unsigned pdd_manager::dag_size(pdd const& b) {
init_mark();

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

@ -225,7 +225,8 @@ namespace dd {
void set_mod2_semantics() { m_mod2_semantics = true; }
void set_max_num_nodes(unsigned n) { m_max_num_pdd_nodes = n; }
void set_var_order(unsigned_vector const& levels); // TBD: set variable order (m_var2level, m_level2var) before doing anything else.
void set_level2var(unsigned_vector const& level2var);
unsigned_vector const& get_level2var() const { return m_level2var; }
pdd mk_var(unsigned i);
pdd mk_val(rational const& r);

34
src/math/grobner/pdd_grobner.cpp
View file

@ -139,7 +139,6 @@ namespace dd {
unsigned j = 0;
for (equation* target : m_processed) {
if (superpose(eq, *target)) {
// remove from watch lists
retire(target);
}
else {
@ -189,6 +188,11 @@ namespace dd {
retire(&target);
}
else if (simplified && !check_conflict(target) && changed_leading_term) {
SASSERT(target.is_processed());
target.set_processed(false);
if (is_tuned()) {
m_levelp1 = std::max(m_var2level[target.poly().var()]+1, m_levelp1);
}
push_equation(target, m_to_simplify);
}
else {
@ -217,10 +221,6 @@ namespace dd {
target = r;
target = m_dep_manager.mk_join(target.dep(), source.dep());
update_stats_max_degree_and_size(target);
if (changed_leading_term) {
target.set_processed(false);
}
TRACE("grobner", tout << "simplified " << target.poly() << "\n";);
return true;
}
@ -255,8 +255,13 @@ namespace dd {
}
void grobner::tuned_init() {
// TBD: extract free variables, order them, set pointer into variable list.
NOT_IMPLEMENTED_YET();
unsigned_vector const& l2v = m.get_level2var();
m_level2var.resize(l2v.size());
m_var2level.resize(l2v.size());
for (unsigned i = 0; i < l2v.size(); ++i) {
m_level2var[i] = l2v[i];
m_var2level[l2v[i]] = i;
}
m_watch.reserve(m_level2var.size());
m_levelp1 = m_level2var.size();
for (equation* eq : m_to_simplify) add_to_watch(*eq);
@ -278,17 +283,20 @@ namespace dd {
for (equation* _target : watch) {
equation& target = *_target;
SASSERT(!target.is_processed());
SASSERT(target.poly().var() == v);
bool changed_leading_term = false;
bool simplified = !done() && simplify_source_target(eq, target, changed_leading_term);
if (simplified && is_trivial(target)) {
if (!done()) simplify_source_target(eq, target, changed_leading_term);
if (is_trivial(target)) {
retire(&target);
}
else if (simplified && !check_conflict(target) && changed_leading_term) {
SASSERT(!target.is_processed());
pop_equation(target.idx(), m_processed);
push_equation(target, m_to_simplify);
else if (check_conflict(target)) {
// remove from watch
} else if (target.poly().var() != v) {
// move to other watch list
m_watch[target.poly().var()].push_back(_target);
}
else {
// keep watching same variable
watch[++j] = _target;
}
}

19
src/test/pdd_grobner.cpp
View file

@ -36,6 +36,7 @@ namespace dd {
print_eqs(gb.equations());
gb.reset();
// stop early on contradiction
gb.add(v1*v3*v3 + v3*v1 + 2);
gb.add(v1*v3*v3 + v3*v1);
gb.add(v3*v1 + v1*v2 + v2*v3);
@ -45,6 +46,24 @@ namespace dd {
print_eqs(gb.equations());
gb.reset();
// result is v1 = 0, v2 = 0.
gb.add(v1*v3*v3 + v3*v1);
gb.add(v3*v1 + v1*v2 + v2*v3);
gb.add(v3*v1 + v1*v2 + v2*v3 + v1);
gb.add(v3*v1 + v1*v2 + v2*v3 + v2);
gb.saturate();
print_eqs(gb.equations());
gb.reset();
// everything rewrites to a multiple of v0
gb.add(v3 - 2*v2);
gb.add(v2 - 2*v1);
gb.add(v1 - 2*v0);
gb.saturate();
print_eqs(gb.equations());
gb.reset();
//
}
}