mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 06:13:40 +00:00
Code Activity

add simplification routines

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-25 19:31:18 -08:00
parent de6409f558
commit 65d818437a
5 changed files with 297 additions and 96 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -87,7 +87,7 @@ namespace dd {
} }
} }
SASSERT(well_formed()); SASSERT(well_formed());
return 0; return null_pdd;
} }
bool pdd_manager::check_result(op_entry*& e1, op_entry const* e2, PDD a, PDD b, PDD c) { bool pdd_manager::check_result(op_entry*& e1, op_entry const* e2, PDD a, PDD b, PDD c) {
@ -112,21 +112,21 @@ namespace dd {
if (is_zero(p)) return q; if (is_zero(p)) return q;
if (is_zero(q)) return p; if (is_zero(q)) return p;
if (is_val(p) && is_val(q)) return imk_val(val(p) + val(q)); if (is_val(p) && is_val(q)) return imk_val(val(p) + val(q));
if (!is_val(p) && level(p) < level(q)) std::swap(p, q);
if (is_val(p)) std::swap(p, q); if (is_val(p)) std::swap(p, q);
else if (!is_val(q) && level(p) < level(q)) std::swap(p, q);
break; break;
case pdd_mul_op: case pdd_mul_op:
if (is_zero(p) || is_zero(q)) return zero_pdd; if (is_zero(p) || is_zero(q)) return zero_pdd;
if (is_one(p)) return q; if (is_one(p)) return q;
if (is_one(q)) return p; if (is_one(q)) return p;
if (is_val(p) && is_val(q)) return imk_val(val(p) * val(q)); if (is_val(p) && is_val(q)) return imk_val(val(p) * val(q));
if (!is_val(p) && level(p) < level(q)) std::swap(p, q);
if (is_val(p)) std::swap(p, q); if (is_val(p)) std::swap(p, q);
else if (!is_val(q) && level(p) < level(q)) std::swap(p, q);
break; break;
case pdd_reduce_op: case pdd_reduce_op:
if (is_zero(q)) return p; if (is_zero(q)) return p;
if (is_val(p)) return p; if (is_val(p)) return p;
if (level(p) < level(q)) return p; if (!is_val(q) && level(p) < level(q)) return p;
break; break;
default: default:
UNREACHABLE(); UNREACHABLE();
@ -156,14 +156,12 @@ namespace dd {
push(apply_rec(hi(p), hi(q), op)); push(apply_rec(hi(p), hi(q), op));
r = make_node(level_p, read(2), read(1)); r = make_node(level_p, read(2), read(1));
} }
else if (level_p > level_q) { else {
SASSERT(level_p > level_q);
push(apply_rec(lo(p), q, op)); push(apply_rec(lo(p), q, op));
r = make_node(level_p, read(1), hi(p)); r = make_node(level_p, read(1), hi(p));
npop = 1; npop = 1;
} }
else {
UNREACHABLE();
}
break; break;
case pdd_mul_op: case pdd_mul_op:
SASSERT(!is_val(p)); SASSERT(!is_val(p));
@ -179,7 +177,7 @@ namespace dd {
// == x((a+b)(c+d)+bd) + bd // == x((a+b)(c+d)+bd) + bd
// //
push(apply_rec(lo(p), lo(q), pdd_mul_op)); push(apply_rec(lo(p), lo(q), pdd_mul_op));
unsigned bd = read(3); unsigned bd = read(1);
push(apply_rec(hi(p), lo(p), pdd_add_op)); push(apply_rec(hi(p), lo(p), pdd_add_op));
push(apply_rec(hi(q), lo(q), pdd_add_op)); push(apply_rec(hi(q), lo(q), pdd_add_op));
push(apply_rec(read(1), read(2), pdd_mul_op)); push(apply_rec(read(1), read(2), pdd_mul_op));
@ -239,9 +237,7 @@ namespace dd {
UNREACHABLE(); UNREACHABLE();
} }
pop(npop); pop(npop);
e1->m_result = r; e1->m_result = r;
// SASSERT(well_formed());
SASSERT(!m_free_nodes.contains(r)); SASSERT(!m_free_nodes.contains(r));
return r; return r;
} }
@ -852,6 +848,7 @@ namespace dd {
out << "v" << v; out << "v" << v;
} }
} }
if (first) out << "0";
return out; return out;
} }

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

@ -281,6 +281,7 @@ namespace dd {
~pdd() { m.dec_ref(root); } ~pdd() { m.dec_ref(root); }
pdd lo() const { return pdd(m.lo(root), m); } pdd lo() const { return pdd(m.lo(root), m); }
pdd hi() const { return pdd(m.hi(root), m); } pdd hi() const { return pdd(m.hi(root), m); }
unsigned index() const { return root; }
unsigned var() const { return m.var(root); } unsigned var() const { return m.var(root); }
rational const& val() const { SASSERT(is_val()); return m.val(root); } rational const& val() const { SASSERT(is_val()); return m.val(root); }
bool is_val() const { return m.is_val(root); } bool is_val() const { return m.is_val(root); }
@ -317,6 +318,8 @@ namespace dd {
inline pdd operator-(pdd const& b, int x) { return b + (-rational(x)); } inline pdd operator-(pdd const& b, int x) { return b + (-rational(x)); }
inline pdd& operator*=(pdd & p, pdd const& q) { p = p * q; return p; } inline pdd& operator*=(pdd & p, pdd const& q) { p = p * q; return p; }
inline pdd& operator|=(pdd & p, pdd const& q) { p = p | q; return p; } inline pdd& operator|=(pdd & p, pdd const& q) { p = p | q; return p; }
inline pdd& operator-=(pdd & p, pdd const& q) { p = p - q; return p; }
inline pdd& operator+=(pdd & p, pdd const& q) { p = p + q; return p; }
std::ostream& operator<<(std::ostream& out, pdd const& b); std::ostream& operator<<(std::ostream& out, pdd const& b);

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

@ -151,10 +151,10 @@ namespace dd {
scoped_detach sd(*this, e); scoped_detach sd(*this, e);
equation& eq = *e; equation& eq = *e;
TRACE("grobner", display(tout << "eq = ", eq); display(tout);); TRACE("grobner", display(tout << "eq = ", eq); display(tout););
SASSERT(!eq.is_processed()); SASSERT(eq.state() == to_simplify);
if (!simplify_using(eq, m_processed)) return false; if (!simplify_using(eq, m_processed)) return false;
if (is_trivial(eq)) { sd.e = nullptr; retire(e); return true; } if (is_trivial(eq)) { sd.e = nullptr; retire(e); return true; }
if (check_conflict(eq)) return false; if (check_conflict(eq)) { sd.e = nullptr; return false; }
if (!simplify_using(m_processed, eq)) return false; if (!simplify_using(m_processed, eq)) return false;
superpose(eq); superpose(eq);
return simplify_using(m_to_simplify, eq); return simplify_using(m_to_simplify, eq);
@ -167,7 +167,7 @@ namespace dd {
eq = curr; eq = curr;
} }
} }
if (eq) pop_equation(eq, m_to_simplify); if (eq) pop_equation(eq);
return eq; return eq;
} }
@ -178,13 +178,13 @@ namespace dd {
eq = curr; eq = curr;
} }
} }
if (eq) pop_equation(eq, m_to_simplify); if (eq) pop_equation(eq);
return eq; return eq;
} }
void grobner::simplify_linear() { void grobner::simplify() {
try { try {
while (simplify_linear_step()) { while (simplify_linear_step() /*|| simplify_cc_step() */ || simplify_elim_step()) {
DEBUG_CODE(invariant();); DEBUG_CODE(invariant(););
} }
} }
@ -207,38 +207,149 @@ namespace dd {
} }
} }
if (linear.empty()) return false; if (linear.empty()) return false;
vector<equation_vector> use_list; use_list_t use_list = get_use_list();
for (equation * e : m_to_simplify) {
add_to_use(e, use_list);
}
for (equation * e : m_processed) {
add_to_use(e, use_list);
}
compare_top_var ctv; compare_top_var ctv;
std::stable_sort(linear.begin(), linear.end(), ctv); std::stable_sort(linear.begin(), linear.end(), ctv);
for (equation* src : linear) { for (equation* src : linear) {
equation_vector const& uses = use_list[src->poly().var()]; equation_vector const& uses = use_list[src->poly().var()];
bool changed_leading_term; bool changed_leading_term;
for (equation* dst : uses) { for (equation* dst : uses) {
if (src == dst || !simplify_source_target(*src, *dst, changed_leading_term)) { if (src == dst) {
continue; continue;
} }
if (dst->is_processed() && changed_leading_term) { simplify_using(*dst, *src, changed_leading_term);
dst->set_processed(false); if (check_conflict(*dst)) {
pop_equation(dst, m_processed); return false;
push_equation(dst, m_to_simplify); }
if (is_trivial(*dst)) {
SASSERT(false);
}
if (changed_leading_term) {
pop_equation(dst);
push_equation(to_simplify, dst);
} }
} }
} }
for (equation* src : linear) { for (equation* src : linear) {
pop_equation(src, m_to_simplify); pop_equation(src);
push_equation(src, m_processed); push_equation(solved, src);
src->set_processed(true);
} }
return true; return true;
} }
void grobner::add_to_use(equation* e, vector<equation_vector>& use_list) { /**
\brief simplify using congruences
replace pair px + q and ry + q by
px + q, px - ry
since px = ry
*/
bool grobner::simplify_cc_step() {
u_map<equation*> los;
bool reduced = false;
unsigned j = 0;
for (equation* eq1 : m_to_simplify) {
SASSERT(eq1->state() == to_simplify);
pdd p = eq1->poly();
auto* e = los.insert_if_not_there2(p.lo().index(), eq1);
equation* eq2 = e->get_data().m_value;
if (eq2 != eq1 && !p.lo().is_val()) {
*eq1 = p - eq2->poly();
*eq1 = m_dep_manager.mk_join(eq1->dep(), eq2->dep());
reduced = true;
if (is_trivial(*eq1)) {
retire(eq1);
continue;
}
else if (check_conflict(*eq1)) {
continue;
}
}
m_to_simplify[j] = eq1;
eq1->set_index(j++);
}
m_to_simplify.shrink(j);
return reduced;
}
/**
\brief treat equations as processed if top variable occurs only once.
reduce equations where top variable occurs only twice and linear in one of the occurrences.
*/
bool grobner::simplify_elim_step() {
use_list_t use_list = get_use_list();
unsigned j = 0;
for (equation* e : m_to_simplify) {
pdd p = e->poly();
if (!p.is_val() && p.hi().is_val() && use_list[p.var()].size() == 1) {
push_equation(solved, e);
}
else {
m_to_simplify[j] = e;
e->set_index(j++);
}
}
if (j != m_to_simplify.size()) {
m_to_simplify.shrink(j);
return true;
}
j = 0;
for (unsigned i = 0; i < m_to_simplify.size(); ++i) {
equation* e = m_to_simplify[i];
pdd p = e->poly();
// check that e is linear in top variable.
if (e->state() != to_simplify) {
// this was moved before this pass
}
else if (!done() && !is_trivial(*e) && p.hi().is_val() && use_list[p.var()].size() == 2) {
for (equation* e2 : use_list[p.var()]) {
if (e2 == e) continue;
bool changed_leading_term;
remove_from_use(e2, use_list);
simplify_using(*e2, *e, changed_leading_term);
if (check_conflict(*e2)) {
break;
}
if (is_trivial(*e2)) {
break;
}
if (changed_leading_term) {
pop_equation(e2);
push_equation(to_simplify, e2);
}
add_to_use(e2, use_list);
break;
}
push_equation(solved, e);
}
else {
m_to_simplify[j] = e;
e->set_index(j++);
}
}
if (j != m_to_simplify.size()) {
// clean up elements in m_to_simplify
// they may have moved.
m_to_simplify.shrink(j);
j = 0;
for (equation* e : m_to_simplify) {
if (is_trivial(*e)) {
retire(e);
}
else if (e->state() == to_simplify) {
m_to_simplify[j] = e;
e->set_index(j++);
}
}
m_to_simplify.shrink(j);
return true;
}
else {
return false;
}
}
void grobner::add_to_use(equation* e, use_list_t& use_list) {
unsigned_vector const& fv = m.free_vars(e->poly()); unsigned_vector const& fv = m.free_vars(e->poly());
for (unsigned v : fv) { for (unsigned v : fv) {
use_list.reserve(v + 1); use_list.reserve(v + 1);
@ -246,6 +357,25 @@ namespace dd {
} }
} }
void grobner::remove_from_use(equation* e, use_list_t& use_list) {
unsigned_vector const& fv = m.free_vars(e->poly());
for (unsigned v : fv) {
use_list.reserve(v + 1);
use_list[v].erase(e);
}
}
grobner::use_list_t grobner::get_use_list() {
use_list_t use_list;
for (equation * e : m_to_simplify) {
add_to_use(e, use_list);
}
for (equation * e : m_processed) {
add_to_use(e, use_list);
}
return use_list;
}
void grobner::superpose(equation const & eq) { void grobner::superpose(equation const & eq) {
for (equation* target : m_processed) { for (equation* target : m_processed) {
superpose(eq, *target); superpose(eq, *target);
@ -257,7 +387,6 @@ namespace dd {
*/ */
bool grobner::simplify_using(equation& eq, equation_vector const& eqs) { bool grobner::simplify_using(equation& eq, equation_vector const& eqs) {
bool simplified, changed_leading_term; bool simplified, changed_leading_term;
TRACE("grobner", display(tout << "simplifying: ", eq); tout << "using equalities of size " << eqs.size() << "\n";);
do { do {
simplified = false; simplified = false;
for (equation* p : eqs) { for (equation* p : eqs) {
@ -273,7 +402,6 @@ namespace dd {
TRACE("grobner", display(tout << "simplification result: ", eq);); TRACE("grobner", display(tout << "simplification result: ", eq););
check_conflict(eq);
return !done(); return !done();
} }
@ -281,7 +409,6 @@ namespace dd {
Use the given equation to simplify equations in set Use the given equation to simplify equations in set
*/ */
bool grobner::simplify_using(equation_vector& set, equation const& eq) { bool grobner::simplify_using(equation_vector& set, equation const& eq) {
TRACE("grobner", tout << "poly " << eq.poly() << "\n";);
unsigned j = 0, sz = set.size(); unsigned j = 0, sz = set.size();
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
equation& target = *set[i]; equation& target = *set[i];
@ -290,13 +417,15 @@ namespace dd {
if (simplified && is_trivial(target)) { if (simplified && is_trivial(target)) {
retire(&target); retire(&target);
} }
else if (simplified && !check_conflict(target) && changed_leading_term) { else if (simplified && check_conflict(target)) {
SASSERT(target.is_processed()); // pushed to solved
target.set_processed(false); }
else if (simplified && changed_leading_term) {
SASSERT(target.state() == processed);
if (is_tuned()) { if (is_tuned()) {
m_levelp1 = std::max(m_var2level[target.poly().var()]+1, m_levelp1); m_levelp1 = std::max(m_var2level[target.poly().var()]+1, m_levelp1);
} }
push_equation(target, m_to_simplify); push_equation(to_simplify, target);
} }
else { else {
set[j] = set[i]; set[j] = set[i];
@ -312,22 +441,44 @@ namespace dd {
return true if the target was simplified. return true if the target was simplified.
set changed_leading_term if the target is in the m_processed set and the leading term changed. set changed_leading_term if the target is in the m_processed set and the leading term changed.
*/ */
bool grobner::simplify_source_target(equation const& source, equation& target, bool& changed_leading_term) { bool grobner::simplify_source_target(equation const& src, equation& dst, bool& changed_leading_term) {
TRACE("grobner", tout << "simplifying: " << target.poly() << "\nusing: " << source.poly() << "\n";); if (&src == &dst) {
m_stats.m_simplified++;
pdd t = source.poly();
pdd r = target.poly().reduce(t);
if (r == target.poly() || is_too_complex(r)) {
return false; return false;
} }
changed_leading_term = target.is_processed() && m.different_leading_term(r, target.poly()); m_stats.m_simplified++;
target = r; pdd t = src.poly();
target = m_dep_manager.mk_join(target.dep(), source.dep()); pdd r = dst.poly().reduce(t);
update_stats_max_degree_and_size(target); if (r == dst.poly() || is_too_complex(r)) {
TRACE("grobner", tout << "simplified " << target.poly() << "\n";); return false;
}
TRACE("grobner",
tout << "reduce: " << dst.poly() << "\n";
tout << "using: " << t << "\n";
tout << "to: " << r << "\n";);
changed_leading_term = dst.state() == processed && m.different_leading_term(r, dst.poly());
dst = r;
dst = m_dep_manager.mk_join(dst.dep(), src.dep());
update_stats_max_degree_and_size(dst);
return true; return true;
} }
void grobner::simplify_using(equation & dst, equation const& src, bool& changed_leading_term) {
if (&src == &dst) return;
m_stats.m_simplified++;
pdd t = src.poly();
pdd r = dst.poly().reduce(t);
changed_leading_term = dst.state() == processed && m.different_leading_term(r, dst.poly());
TRACE("grobner",
tout << "reduce: " << dst.poly() << "\n";
tout << "using: " << t << "\n";
tout << "to: " << r << "\n";);
if (r == dst.poly()) return;
dst = r;
dst = m_dep_manager.mk_join(dst.dep(), src.dep());
update_stats_max_degree_and_size(dst);
}
/* /*
let eq1: ab+q=0, and eq2: ac+e=0, then qc - eb = 0 let eq1: ab+q=0, and eq2: ac+e=0, then qc - eb = 0
*/ */
@ -347,10 +498,10 @@ namespace dd {
scoped_detach sd(*this, e); scoped_detach sd(*this, e);
equation& eq = *e; equation& eq = *e;
SASSERT(!m_watch[eq.poly().var()].contains(e)); SASSERT(!m_watch[eq.poly().var()].contains(e));
SASSERT(!eq.is_processed()); SASSERT(eq.state() == to_simplify);
if (!simplify_using(eq, m_processed)) return false; if (!simplify_using(eq, m_processed)) return false;
if (is_trivial(eq)) { sd.e = nullptr; retire(e); return true; } if (is_trivial(eq)) { sd.e = nullptr; retire(e); return true; }
if (check_conflict(eq)) return false; if (check_conflict(eq)) { sd.e = nullptr; return false; }
if (!simplify_using(m_processed, eq)) return false; if (!simplify_using(m_processed, eq)) return false;
TRACE("grobner", display(tout << "eq = ", eq);); TRACE("grobner", display(tout << "eq = ", eq););
superpose(eq); superpose(eq);
@ -372,7 +523,7 @@ namespace dd {
} }
void grobner::add_to_watch(equation& eq) { void grobner::add_to_watch(equation& eq) {
SASSERT(!eq.is_processed()); SASSERT(eq.state() == to_simplify);
SASSERT(is_tuned()); SASSERT(is_tuned());
pdd const& p = eq.poly(); pdd const& p = eq.poly();
if (!p.is_val()) { if (!p.is_val()) {
@ -386,7 +537,7 @@ namespace dd {
unsigned j = 0; unsigned j = 0;
for (equation* _target : watch) { for (equation* _target : watch) {
equation& target = *_target; equation& target = *_target;
SASSERT(!target.is_processed()); SASSERT(target.state() == to_simplify);
SASSERT(target.poly().var() == v); SASSERT(target.poly().var() == v);
bool changed_leading_term = false; bool changed_leading_term = false;
if (!done()) simplify_source_target(eq, target, changed_leading_term); if (!done()) simplify_source_target(eq, target, changed_leading_term);
@ -394,8 +545,9 @@ namespace dd {
retire(&target); retire(&target);
} }
else if (check_conflict(target)) { else if (check_conflict(target)) {
// remove from watch // pushed to solved
} else if (target.poly().var() != v) { }
else if (target.poly().var() != v) {
// move to other watch list // move to other watch list
m_watch[target.poly().var()].push_back(_target); m_watch[target.poly().var()].push_back(_target);
} }
@ -415,13 +567,13 @@ namespace dd {
equation* eq = nullptr; equation* eq = nullptr;
for (equation* curr : watch) { for (equation* curr : watch) {
pdd const& p = curr->poly(); pdd const& p = curr->poly();
if (!curr->is_processed() && !p.is_val() && p.var() == v) { if (curr->state() == to_simplify && !p.is_val() && p.var() == v) {
if (!eq || is_simpler(*curr, *eq)) if (!eq || is_simpler(*curr, *eq))
eq = curr; eq = curr;
} }
} }
if (eq) { if (eq) {
pop_equation(eq, m_to_simplify); pop_equation(eq);
m_watch[eq->poly().var()].erase(eq); m_watch[eq->poly().var()].erase(eq);
return eq; return eq;
} }
@ -432,14 +584,17 @@ namespace dd {
grobner::equation_vector const& grobner::equations() { grobner::equation_vector const& grobner::equations() {
m_all_eqs.reset(); m_all_eqs.reset();
for (equation* eq : m_solved) m_all_eqs.push_back(eq);
for (equation* eq : m_to_simplify) m_all_eqs.push_back(eq); for (equation* eq : m_to_simplify) m_all_eqs.push_back(eq);
for (equation* eq : m_processed) m_all_eqs.push_back(eq); for (equation* eq : m_processed) m_all_eqs.push_back(eq);
return m_all_eqs; return m_all_eqs;
} }
void grobner::reset() { void grobner::reset() {
for (equation* e : m_solved) dealloc(e);
for (equation* e : m_to_simplify) dealloc(e); for (equation* e : m_to_simplify) dealloc(e);
for (equation* e : m_processed) dealloc(e); for (equation* e : m_processed) dealloc(e);
m_solved.reset();
m_processed.reset(); m_processed.reset();
m_to_simplify.reset(); m_to_simplify.reset();
m_stats.reset(); m_stats.reset();
@ -448,9 +603,13 @@ namespace dd {
void grobner::add(pdd const& p, u_dependency * dep) { void grobner::add(pdd const& p, u_dependency * dep) {
if (p.is_zero()) return; if (p.is_zero()) return;
equation * eq = alloc(equation, p, dep, m_to_simplify.size()); equation * eq = alloc(equation, p, dep);
m_to_simplify.push_back(eq); if (check_conflict(*eq)) {
if (!check_conflict(*eq) && is_tuned()) { return;
}
push_equation(to_simplify, eq);
if (is_tuned()) {
m_levelp1 = std::max(m_var2level[p.var()]+1, m_levelp1); m_levelp1 = std::max(m_var2level[p.var()]+1, m_levelp1);
} }
update_stats_max_degree_and_size(*eq); update_stats_max_degree_and_size(*eq);
@ -467,12 +626,23 @@ namespace dd {
m_conflict != nullptr; m_conflict != nullptr;
} }
grobner::equation_vector& grobner::get_queue(equation const& eq) {
switch (eq.state()) {
case processed: return m_processed;
case to_simplify: return m_to_simplify;
case solved: return m_solved;
}
UNREACHABLE();
return m_to_simplify;
}
void grobner::del_equation(equation& eq) { void grobner::del_equation(equation& eq) {
pop_equation(eq, eq.is_processed() ? m_processed : m_to_simplify); pop_equation(eq);
retire(&eq); retire(&eq);
} }
void grobner::pop_equation(equation& eq, equation_vector& v) { void grobner::pop_equation(equation& eq) {
equation_vector& v = get_queue(eq);
unsigned idx = eq.idx(); unsigned idx = eq.idx();
if (idx != v.size() - 1) { if (idx != v.size() - 1) {
equation* eq2 = v.back(); equation* eq2 = v.back();
@ -482,7 +652,9 @@ namespace dd {
v.pop_back(); v.pop_back();
} }
void grobner::push_equation(equation& eq, equation_vector& v) { void grobner::push_equation(eq_state st, equation& eq) {
eq.set_state(st);
equation_vector& v = get_queue(eq);
eq.set_index(v.size()); eq.set_index(v.size());
v.push_back(&eq); v.push_back(&eq);
} }
@ -507,6 +679,7 @@ namespace dd {
} }
std::ostream& grobner::display(std::ostream& out) const { std::ostream& grobner::display(std::ostream& out) const {
out << "solved\n"; for (auto e : m_solved) display(out, *e);
out << "processed\n"; for (auto e : m_processed) display(out, *e); out << "processed\n"; for (auto e : m_processed) display(out, *e);
out << "to_simplify\n"; for (auto e : m_to_simplify) display(out, *e); out << "to_simplify\n"; for (auto e : m_to_simplify) display(out, *e);
statistics st; statistics st;
@ -520,17 +693,27 @@ namespace dd {
// they are labled as processed // they are labled as processed
unsigned i = 0; unsigned i = 0;
for (auto* e : m_processed) { for (auto* e : m_processed) {
VERIFY(e->is_processed()); VERIFY(e->state() == processed);
VERIFY(e->idx() == i);
VERIFY(!e->poly().is_val());
++i;
}
i = 0;
for (auto* e : m_solved) {
VERIFY(e->state() == solved);
VERIFY(e->idx() == i); VERIFY(e->idx() == i);
++i; ++i;
} }
// equations in to_simplify have correct indices // equations in to_simplify have correct indices
// they are labeled as non-processed // they are labeled as non-processed
// their top-most variable is watched // their top-most variable is watched
i = 0; i = 0;
for (auto* e : m_to_simplify) { for (auto* e : m_to_simplify) {
VERIFY(!e->is_processed());
VERIFY(e->idx() == i); VERIFY(e->idx() == i);
VERIFY(e->state() == to_simplify);
VERIFY(!e->poly().is_val());
if (is_tuned()) { if (is_tuned()) {
pdd const& p = e->poly(); pdd const& p = e->poly();
VERIFY(p.is_val() || m_watch[p.var()].contains(e)); VERIFY(p.is_val() || m_watch[p.var()].contains(e));
@ -544,7 +727,7 @@ namespace dd {
for (equation* e : w) { for (equation* e : w) {
VERIFY(!e->poly().is_val()); VERIFY(!e->poly().is_val());
VERIFY(e->poly().var() == i); VERIFY(e->poly().var() == i);
VERIFY(!e->is_processed()); VERIFY(e->state() == to_simplify);
VERIFY(m_to_simplify.contains(e)); VERIFY(m_to_simplify.contains(e));
} }
++i; ++i;

50
src/math/grobner/pdd_grobner.h
View file

@ -51,15 +51,21 @@ public:
{} {}
}; };
enum eq_state {
solved,
processed,
to_simplify
};
class equation { class equation {
bool m_processed; //!< state eq_state m_state;
unsigned m_idx; //!< unique index unsigned m_idx; //!< unique index
pdd m_poly; //!< polynomial in pdd form pdd m_poly; //!< polynomial in pdd form
u_dependency * m_dep; //!< justification for the equality u_dependency * m_dep; //!< justification for the equality
public: public:
equation(pdd const& p, u_dependency* d, unsigned idx): equation(pdd const& p, u_dependency* d):
m_processed(false), m_state(to_simplify),
m_idx(idx), m_idx(0),
m_poly(p), m_poly(p),
m_dep(d) m_dep(d)
{} {}
@ -69,8 +75,8 @@ public:
unsigned idx() const { return m_idx; } unsigned idx() const { return m_idx; }
void operator=(pdd& p) { m_poly = p; } void operator=(pdd& p) { m_poly = p; }
void operator=(u_dependency* d) { m_dep = d; } void operator=(u_dependency* d) { m_dep = d; }
bool is_processed() const { return m_processed; } eq_state state() const { return m_state; }
void set_processed(bool p) { m_processed = p; } void set_state(eq_state st) { m_state = st; }
void set_index(unsigned idx) { m_idx = idx; } void set_index(unsigned idx) { m_idx = idx; }
}; };
private: private:
@ -83,11 +89,12 @@ private:
stats m_stats; stats m_stats;
config m_config; config m_config;
print_dep_t m_print_dep; print_dep_t m_print_dep;
equation_vector m_solved; // equations with solved variables, triangular
equation_vector m_processed; equation_vector m_processed;
equation_vector m_to_simplify; equation_vector m_to_simplify;
mutable u_dependency_manager m_dep_manager; mutable u_dependency_manager m_dep_manager;
equation_vector m_all_eqs; equation_vector m_all_eqs;
equation const* m_conflict; equation* m_conflict;
public: public:
grobner(reslimit& lim, pdd_manager& m); grobner(reslimit& lim, pdd_manager& m);
~grobner(); ~grobner();
@ -99,7 +106,7 @@ public:
void add(pdd const& p) { add(p, nullptr); } void add(pdd const& p) { add(p, nullptr); }
void add(pdd const& p, u_dependency * dep); void add(pdd const& p, u_dependency * dep);
void simplify_linear(); void simplify();
void saturate(); void saturate();
equation_vector const& equations(); equation_vector const& equations();
@ -120,14 +127,15 @@ private:
void superpose(equation const& eq1, equation const& eq2); void superpose(equation const& eq1, equation const& eq2);
void superpose(equation const& eq); void superpose(equation const& eq);
bool simplify_source_target(equation const& source, equation& target, bool& changed_leading_term); bool simplify_source_target(equation const& source, equation& target, bool& changed_leading_term);
bool simplify_using(equation_vector& set, equation const& eq);
bool simplify_using(equation& eq, equation_vector const& eqs); bool simplify_using(equation& eq, equation_vector const& eqs);
bool simplify_using(equation_vector& set, equation const& eq);
void simplify_using(equation & dst, equation const& src, bool& changed_leading_term);
bool eliminate(equation& eq) { return is_trivial(eq) && (del_equation(eq), true); } bool eliminate(equation& eq) { return is_trivial(eq) && (del_equation(eq), true); }
bool is_trivial(equation const& eq) const { return eq.poly().is_zero(); } bool is_trivial(equation const& eq) const { return eq.poly().is_zero(); }
bool is_simpler(equation const& eq1, equation const& eq2) { return eq1.poly() < eq2.poly(); } bool is_simpler(equation const& eq1, equation const& eq2) { return eq1.poly() < eq2.poly(); }
bool check_conflict(equation const& eq) { return eq.poly().is_val() && !is_trivial(eq) && (set_conflict(eq), true); } bool check_conflict(equation& eq) { return eq.poly().is_val() && !is_trivial(eq) && (set_conflict(eq), true); }
void set_conflict(equation const& eq) { m_conflict = &eq; } void set_conflict(equation& eq) { m_conflict = &eq; push_equation(solved, eq); }
bool is_too_complex(const equation& eq) const { return is_too_complex(eq.poly()); } bool is_too_complex(const equation& eq) const { return is_too_complex(eq.poly()); }
bool is_too_complex(const pdd& p) const { return p.tree_size() > m_config.m_expr_size_limit; } bool is_too_complex(const pdd& p) const { return p.tree_size() > m_config.m_expr_size_limit; }
@ -144,16 +152,22 @@ private:
void add_to_watch(equation& eq); void add_to_watch(equation& eq);
void del_equation(equation& eq); void del_equation(equation& eq);
equation_vector& get_queue(equation const& eq);
void retire(equation* eq) { dealloc(eq); } void retire(equation* eq) { dealloc(eq); }
void pop_equation(equation& eq, equation_vector& v); void pop_equation(equation& eq);
void pop_equation(equation* eq, equation_vector& v) { pop_equation(*eq, v); } void pop_equation(equation* eq) { pop_equation(*eq); }
void push_equation(equation& eq, equation_vector& v); void push_equation(eq_state st, equation& eq);
void push_equation(equation* eq, equation_vector& v) { push_equation(*eq, v); } void push_equation(eq_state st, equation* eq) { push_equation(st, *eq); }
struct compare_top_var; struct compare_top_var;
bool simplify_linear_step(); bool simplify_linear_step();
void add_to_use(equation* e, vector<equation_vector>& use_list); typedef vector<equation_vector> use_list_t;
use_list_t get_use_list();
void add_to_use(equation* e, use_list_t& use_list);
void remove_from_use(equation* e, use_list_t& use_list);
bool simplify_cc_step();
bool simplify_elim_step();
void invariant() const; void invariant() const;
struct scoped_detach { struct scoped_detach {
@ -162,9 +176,7 @@ private:
scoped_detach(grobner& g, equation* e): g(g), e(e) {} scoped_detach(grobner& g, equation* e): g(g), e(e) {}
~scoped_detach() { ~scoped_detach() {
if (e) { if (e) {
e->set_processed(true); g.push_equation(processed, *e);
e->set_index(g.m_processed.size());
g.m_processed.push_back(e);
} }
} }
}; };

22
src/test/pdd_grobner.cpp
View file

@ -3,6 +3,7 @@
#include "ast/bv_decl_plugin.h" #include "ast/bv_decl_plugin.h"
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/reg_decl_plugins.h" #include "ast/reg_decl_plugins.h"
#include "tactic/goal.h" #include "tactic/goal.h"
#include "tactic/tactic.h" #include "tactic/tactic.h"
@ -76,31 +77,33 @@ namespace dd {
void add_def(unsigned_vector const& id2var, app* e, ast_manager& m, pdd_manager& p, grobner& g) { void add_def(unsigned_vector const& id2var, app* e, ast_manager& m, pdd_manager& p, grobner& g) {
expr* a, *b; expr* a, *b;
pdd v1 = p.mk_var(id2var[e->get_id()]); pdd v1 = p.mk_var(id2var[e->get_id()]);
pdd q(p);
if (m.is_and(e)) { if (m.is_and(e)) {
pdd r = p.one(); pdd r = p.one();
for (expr* arg : *e) r *= p.mk_var(id2var[arg->get_id()]); for (expr* arg : *e) r *= p.mk_var(id2var[arg->get_id()]);
g.add(v1 + r + 1); q = v1 + r;
} }
else if (m.is_or(e)) { else if (m.is_or(e)) {
pdd r = p.zero(); pdd r = p.zero();
for (expr* arg : *e) r |= p.mk_var(id2var[arg->get_id()]); for (expr* arg : *e) r |= p.mk_var(id2var[arg->get_id()]);
g.add(v1 + r + 1); q = v1 + r;
} }
else if (m.is_not(e, a)) { else if (m.is_not(e, a)) {
pdd v2 = p.mk_var(id2var[a->get_id()]); pdd v2 = p.mk_var(id2var[a->get_id()]);
g.add(v1 + v2 + 1); q = v1 + v2 + 1;
} }
else if (m.is_eq(e, a, b)) { else if (m.is_eq(e, a, b)) {
pdd v2 = p.mk_var(id2var[a->get_id()]); pdd v2 = p.mk_var(id2var[a->get_id()]);
pdd v3 = p.mk_var(id2var[b->get_id()]); pdd v3 = p.mk_var(id2var[b->get_id()]);
g.add(v1 + v2 + v3 + 1); q = v1 + v2 + v3 + 1;
} }
else if (is_uninterp_const(e)) { else if (is_uninterp_const(e)) {
// pass return;
} }
else { else {
UNREACHABLE(); UNREACHABLE();
} }
g.add(q);
} }
void collect_id2var(unsigned_vector& id2var, expr_ref_vector const& fmls) { void collect_id2var(unsigned_vector& id2var, expr_ref_vector const& fmls) {
@ -133,7 +136,10 @@ namespace dd {
for (expr* e : fmls) { for (expr* e : fmls) {
g.add(p.mk_var(id2var[e->get_id()]) + 1); g.add(p.mk_var(id2var[e->get_id()]) + 1);
} }
g.simplify_linear(); g.display(std::cout);
g.simplify();
g.display(std::cout);
g.saturate();
g.display(std::cout); g.display(std::cout);
} }
@ -141,8 +147,8 @@ namespace dd {
ast_manager m; ast_manager m;
reg_decl_plugins(m); reg_decl_plugins(m);
bv_util bv(m); bv_util bv(m);
expr_ref x(m.mk_const("x", bv.mk_sort(4)), m); expr_ref x(m.mk_const("x", bv.mk_sort(3)), m);
expr_ref y(m.mk_const("y", bv.mk_sort(4)), m); expr_ref y(m.mk_const("y", bv.mk_sort(3)), m);
expr_ref xy(bv.mk_bv_mul(x, y), m); expr_ref xy(bv.mk_bv_mul(x, y), m);
expr_ref yx(bv.mk_bv_mul(y, x), m); expr_ref yx(bv.mk_bv_mul(y, x), m);
expr_ref eq(m.mk_not(m.mk_eq(xy,yx)), m); expr_ref eq(m.mk_not(m.mk_eq(xy,yx)), m);