mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

fix exception safety in pdd-solver

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-10-17 19:50:13 -07:00
parent c9c5dbc347
commit 3fa67777e5
5 changed files with 147 additions and 152 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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) {
@ -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);
@ -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));
}
@ -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();

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

@ -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);

187
src/math/grobner/pdd_simplifier.cpp
View file

@ -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(););
}
@ -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);
@ -112,29 +113,33 @@ 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;
@ -142,9 +147,8 @@ namespace dd {
}
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);
@ -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);
@ -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;
}
@ -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);
@ -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;
}
@ -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);
@ -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;
}
/**
@ -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);
}
add_to_use(e2, use_list);
break;
{
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;
}
reduced = true;
s.push_equation(solver::solved, e);
}
else {
s.m_to_simplify[j] = e;
e->set_index(j++);
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;
}
reduced = true;
s.push_equation(solver::solved, e);
}
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) {

77
src/math/grobner/pdd_solver.cpp
View file

@ -90,11 +90,9 @@ namespace dd {
}
void solver::saturate() {
simplify();
if (done()) {
return;
}
init_saturate();
if (done())
return;
init_saturate();
TRACE("dd.solver", display(tout););
try {
while (!done() && step()) {
@ -105,7 +103,7 @@ namespace dd {
DEBUG_CODE(invariant(););
}
catch (pdd_manager::mem_out) {
IF_VERBOSE(2, verbose_stream() << "mem-out\n");
IF_VERBOSE(1, verbose_stream() << "mem-out saturate\n");
// don't reduce further
}
}
@ -124,7 +122,7 @@ namespace dd {
solver::scoped_process::~scoped_process() {
if (e) {
pdd p = e->poly();
pdd const& p = e->poly();
SASSERT(!p.is_val());
g.push_equation(processed, e);
}
@ -137,9 +135,8 @@ namespace dd {
void solver::superpose(equation const & eq) {
for (equation* target : m_processed) {
superpose(eq, *target);
}
for (equation* target : m_processed)
superpose(eq, *target);
}
/*
@ -166,32 +163,28 @@ namespace dd {
TRACE("dd.solver", display(tout << "simplification result: ", eq););
}
void solver::well_formed() {
auto& set = m_to_simplify;
for (unsigned k = 0; k < set.size(); ++k)
for (unsigned l = k + 1; l < set.size(); ++l) {
if (!set[l] || !set[k] || set[k] != set[l])
continue;
verbose_stream() << k << " " << l << " " << set[k] << "\n";
for (auto* s : set)
verbose_stream() << s->idx() << "\n";
VERIFY(set[k] != set[l]);
}
}
/*
Use the given equation to simplify equations in set
*/
void solver::simplify_using(equation_vector& set, std::function<bool(equation&, bool&)>& simplifier) {
struct scoped_update {
equation_vector& set;
unsigned i, j, sz;
scoped_update(equation_vector& set): set(set), i(0), j(0), sz(set.size()) {}
void nextj() {
set[j] = set[i];
set[i]->set_index(j++);
}
~scoped_update() {
for (; i < sz; ++i)
nextj();
set.shrink(j);
}
};
void solver::simplify_using(equation_vector& set, std::function<bool(equation&, bool&)>& simplifier) {
scoped_update sr(set);
for (; sr.i < sr.sz; ++sr.i) {
equation& target = *set[sr.i];
bool changed_leading_term = false;
bool simplified = true;
simplified = !done() && simplifier(target, changed_leading_term);
if (simplified && is_trivial(target))
retire(&target);
@ -286,21 +279,32 @@ namespace dd {
m_stats.m_compute_steps++;
IF_VERBOSE(3, if (m_stats.m_compute_steps % 100 == 0) verbose_stream() << "compute steps = " << m_stats.m_compute_steps << "\n";);
equation* e = pick_next();
if (!e) return false;
if (!e)
return false;
scoped_process sd(*this, e);
equation& eq = *e;
SASSERT(eq.state() == to_simplify);
simplify_using(eq, m_processed);
if (is_trivial(eq)) { sd.e = nullptr; retire(e); return true; }
if (check_conflict(eq)) { sd.e = nullptr; return false; }
if (is_trivial(eq)) {
sd.e = nullptr;
retire(e);
return true;
}
if (check_conflict(eq)) {
sd.e = nullptr;
return false;
}
m_too_complex = false;
simplify_using(m_processed, eq);
if (done()) return false;
if (done())
return false;
TRACE("dd.solver", display(tout << "eq = ", eq););
superpose(eq);
simplify_using(m_to_simplify, eq);
if (done()) return false;
if (!m_too_complex) sd.done();
if (done())
return false;
if (!m_too_complex)
sd.done();
return true;
}
@ -345,9 +349,9 @@ namespace dd {
}
void solver::reset() {
for (equation* e : m_solved) dealloc(e);
for (equation* e : m_to_simplify) dealloc(e);
for (equation* e : m_processed) dealloc(e);
for (equation* e : m_solved) dealloc(e);
for (equation* e : m_to_simplify) dealloc(e);
for (equation* e : m_processed) dealloc(e);
m_subst.reset();
m_solved.reset();
m_processed.reset();
@ -445,7 +449,6 @@ namespace dd {
#endif
}
void solver::pop_equation(equation& eq) {
equation_vector& v = get_queue(eq);
unsigned idx = eq.idx();

1
src/math/grobner/pdd_solver.h
View file

@ -108,6 +108,7 @@ public:
private:
typedef ptr_vector<equation> equation_vector;
for (; i < sz; ++i)
typedef std::function<void (u_dependency* d, std::ostream& out)> print_dep_t;
pdd_manager& m;