Skip to content

Commit

Permalink
fix exception safety in pdd-solver
Browse files Browse the repository at this point in the history
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Oct 18, 2023
1 parent c9c5dbc commit 3fa6777
Show file tree
Hide file tree
Showing 5 changed files with 146 additions and 151 deletions.
31 changes: 16 additions & 15 deletions src/math/dd/dd_pdd.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -62,6 +62,10 @@ namespace dd {
init_nodes(level2var);
}

void pdd_manager::set_max_num_nodes(unsigned n) {
m_max_num_nodes = n + m_level2var.size();
}

void pdd_manager::init_nodes(unsigned_vector const& l2v) {
// add dummy nodes for operations, and 0, 1 pdds.
for (unsigned i = 0; i < pdd_no_op; ++i) {
Expand Down Expand Up @@ -1352,9 +1356,8 @@ namespace dd {
e->get_data().m_refcount = 0;
}
if (do_gc) {
if (m_nodes.size() > m_max_num_nodes) {
throw mem_out();
}
if (m_nodes.size() > m_max_num_nodes)
throw mem_out();
alloc_free_nodes(m_nodes.size()/2);
}
SASSERT(e->get_data().m_lo == n.m_lo);
Expand Down Expand Up @@ -1600,7 +1603,8 @@ namespace dd {
for (unsigned i = m_nodes.size(); i-- > pdd_no_op; ) {
if (!reachable[i]) {
if (is_val(i)) {
if (m_freeze_value == val(i)) continue;
if (m_freeze_value == val(i))
continue;
m_free_values.push_back(m_mpq_table.find(val(i)).m_value_index);
m_mpq_table.remove(val(i));
}
Expand All @@ -1615,20 +1619,17 @@ namespace dd {

ptr_vector<op_entry> to_delete, to_keep;
for (auto* e : m_op_cache) {
if (e->m_result != null_pdd) {
to_delete.push_back(e);
}
else {
to_keep.push_back(e);
}
if (e->m_result != null_pdd)
to_delete.push_back(e);
else
to_keep.push_back(e);
}
m_op_cache.reset();
for (op_entry* e : to_delete) {
for (op_entry* e : to_delete)
m_alloc.deallocate(sizeof(*e), e);
}
for (op_entry* e : to_keep) {
m_op_cache.insert(e);
}

for (op_entry* e : to_keep)
m_op_cache.insert(e);

m_factor_cache.reset();

Expand Down
3 changes: 2 additions & 1 deletion src/math/dd/dd_pdd.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -324,8 +324,9 @@ namespace dd {
semantics get_semantics() const { return m_semantics; }

void reset(unsigned_vector const& level2var);
void set_max_num_nodes(unsigned n) { m_max_num_nodes = n; }
void set_max_num_nodes(unsigned n);
unsigned_vector const& get_level2var() const { return m_level2var; }
unsigned num_nodes() const { return m_nodes.size() - m_free_nodes.size(); }

pdd mk_var(unsigned i);
pdd mk_val(rational const& r);
Expand Down
185 changes: 87 additions & 98 deletions src/math/grobner/pdd_simplifier.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,7 @@ namespace dd {
}
}
catch (pdd_manager::mem_out) {
IF_VERBOSE(2, verbose_stream() << "simplifier memout\n");
IF_VERBOSE(1, verbose_stream() << "simplifier memout\n");
// done reduce
DEBUG_CODE(s.invariant(););
}
Expand All @@ -94,7 +94,8 @@ namespace dd {
for (equation* e : s.m_to_simplify) {
pdd p = e->poly();
if (binary) {
if (p.is_binary()) linear.push_back(e);
if (p.is_binary())
linear.push_back(e);
}
else if (p.is_linear()) {
linear.push_back(e);
Expand All @@ -112,39 +113,42 @@ namespace dd {
use_list_t use_list = get_use_list();
compare_top_var ctv;
std::stable_sort(linear.begin(), linear.end(), ctv);
equation_vector trivial;
struct trivial {
solver& s;
equation_vector elems;
trivial(solver& s) : s(s) {}
~trivial () {
for (auto* e : elems)
s.del_equation(e);
}
};
trivial trivial(s);
unsigned j = 0;
bool has_conflict = false;
for (equation* src : linear) {
if (has_conflict) {
break;
}
if (s.is_trivial(*src)) {
continue;
}
if (has_conflict)
break;
if (s.is_trivial(*src))
continue;
unsigned v = src->poly().var();
equation_vector const& uses = use_list[v];
TRACE("dd.solver",
s.display(tout << "uses of: ", *src) << "\n";
for (equation* e : uses) {
s.display(tout, *e) << "\n";
});
for (equation* e : uses) s.display(tout, *e) << "\n";);
bool changed_leading_term;
bool all_reduced = true;
for (equation* dst : uses) {
if (src == dst || s.is_trivial(*dst)) {
continue;
}
if (src == dst || s.is_trivial(*dst))
continue;
pdd q = dst->poly();
if (!src->poly().is_binary() && !q.is_linear()) {
all_reduced = false;
continue;
}
remove_from_use(dst, use_list, v);
s.simplify_using(*dst, *src, changed_leading_term);
if (s.is_trivial(*dst)) {
trivial.push_back(dst);
}
if (s.is_trivial(*dst))
trivial.elems.push_back(dst);
else if (s.is_conflict(dst)) {
s.pop_equation(dst);
s.set_conflict(dst);
Expand All @@ -158,9 +162,8 @@ namespace dd {
// SASSERT(!dst->poly().free_vars().contains(v));
add_to_use(dst, use_list);
}
if (all_reduced) {
linear[j++] = src;
}
if (all_reduced)
linear[j++] = src;
}
if (!has_conflict) {
linear.shrink(j);
Expand All @@ -169,9 +172,7 @@ namespace dd {
s.push_equation(solver::solved, src);
}
}
for (equation* e : trivial) {
s.del_equation(e);
}

DEBUG_CODE(s.invariant(););
return j > 0 || has_conflict;
}
Expand All @@ -187,8 +188,9 @@ namespace dd {
IF_VERBOSE(3, verbose_stream() << "cc\n");
u_map<equation*> los;
bool reduced = false;
unsigned j = 0;
for (equation* eq1 : s.m_to_simplify) {
solver::scoped_update sc(s.m_to_simplify);
for (; sc.i < sc.sz; ++sc.i) {
auto* eq1 = sc.get();
SASSERT(eq1->state() == solver::to_simplify);
pdd p = eq1->poly();
equation* eq2 = los.insert_if_not_there(p.lo().index(), eq1);
Expand All @@ -201,14 +203,11 @@ namespace dd {
s.retire(eq1);
continue;
}
else if (s.check_conflict(*eq1)) {
continue;
}
else if (s.check_conflict(*eq1))
continue;
}
s.m_to_simplify[j] = eq1;
eq1->set_index(j++);
sc.nextj();
}
s.m_to_simplify.shrink(j);
return reduced;
}

Expand All @@ -225,15 +224,12 @@ namespace dd {
pdd p = e->poly();
if (p.is_val())
continue;
if (!p.hi().is_val()) {
continue;
}
if (!p.hi().is_val())
continue;
leaves.reset();
for (equation* e2 : use_list[p.var()]) {
if (e != e2 && e2->poly().var_is_leaf(p.var())) {
leaves.push_back(e2);
}
}
for (equation* e2 : use_list[p.var()])
if (e != e2 && e2->poly().var_is_leaf(p.var()))
leaves.push_back(e2);
for (equation* e2 : leaves) {
bool changed_leading_term;
remove_from_use(e2, use_list);
Expand Down Expand Up @@ -263,23 +259,20 @@ namespace dd {
bool simplifier::simplify_elim_pure_step() {
TRACE("dd.solver", tout << "pure\n";);
IF_VERBOSE(3, verbose_stream() << "pure\n");
use_list_t use_list = get_use_list();
unsigned j = 0;
for (equation* e : s.m_to_simplify) {
use_list_t use_list = get_use_list();
solver::scoped_update sc(s.m_to_simplify);
bool has_solved = false;
for (; sc.i < sc.sz; ++sc.i) {
equation* e = sc.get();
pdd p = e->poly();
if (!p.is_val() && p.hi().is_val() && use_list[p.var()].size() == 1) {
s.push_equation(solver::solved, e);
has_solved = true;
}
else {
s.m_to_simplify[j] = e;
e->set_index(j++);
}
else
sc.nextj();
}
if (j != s.m_to_simplify.size()) {
s.m_to_simplify.shrink(j);
return true;
}
return false;
return has_solved;
}

/**
Expand All @@ -288,63 +281,59 @@ namespace dd {
*/
bool simplifier::simplify_elim_dual_step() {
use_list_t use_list = get_use_list();
unsigned j = 0;
bool reduced = false;
for (unsigned i = 0; i < s.m_to_simplify.size(); ++i) {
equation* e = s.m_to_simplify[i];
pdd p = e->poly();
// check that e is linear in top variable.
if (e->state() != solver::to_simplify) {
reduced = true;
}
else if (!s.done() && !s.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);
s.simplify_using(*e2, *e, changed_leading_term);
if (s.is_conflict(e2)) {
s.pop_equation(e2);
s.set_conflict(e2);
}
// when e2 is trivial, leading term is changed
SASSERT(!s.is_trivial(*e2) || changed_leading_term);
if (changed_leading_term) {
s.pop_equation(e2);
s.push_equation(solver::to_simplify, e2);
{
solver::scoped_update sc(s.m_to_simplify);
for (; sc.i < sc.sz; ++sc.i) {
equation* e = sc.get();
pdd p = e->poly();
// check that e is linear in top variable.
if (e->state() != solver::to_simplify) {
reduced = true;
}
else if (!s.done() && !s.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);
s.simplify_using(*e2, *e, changed_leading_term);
if (s.is_conflict(e2)) {
s.pop_equation(e2);
s.set_conflict(e2);
}
// when e2 is trivial, leading term is changed
SASSERT(!s.is_trivial(*e2) || changed_leading_term);
if (changed_leading_term) {
s.pop_equation(e2);
s.push_equation(solver::to_simplify, e2);
}
add_to_use(e2, use_list);
break;
}
add_to_use(e2, use_list);
break;
reduced = true;
s.push_equation(solver::solved, e);
}
reduced = true;
s.push_equation(solver::solved, e);
}
else {
s.m_to_simplify[j] = e;
e->set_index(j++);
else
sc.nextj();
}
}
if (reduced) {
// clean up elements in s.m_to_simplify
// they may have moved.
s.m_to_simplify.shrink(j);
j = 0;
for (equation* e : s.m_to_simplify) {
if (s.is_trivial(*e)) {
s.retire(e);
}
else if (e->state() == solver::to_simplify) {
s.m_to_simplify[j] = e;
e->set_index(j++);
}
solver::scoped_update sc(s.m_to_simplify);
for (; sc.i < sc.sz; ++sc.i) {
equation* e = sc.get();
if (s.is_trivial(*e))
s.retire(e);
else if (e->state() == solver::to_simplify)
sc.nextj();
}
s.m_to_simplify.shrink(j);
return true;
}
else {
return false;
}
else
return false;
}

void simplifier::add_to_use(equation* e, use_list_t& use_list) {
Expand Down

0 comments on commit 3fa6777

Please sign in to comment.