mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +00:00
Code Activity

no need to alloc sets

Browse source
This commit is contained in:
Jakob Rath 2022-12-22 18:55:18 +01:00
parent 29a547e0b4
commit 0cfc0af7ee
2 changed files with 15 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/math/polysat/simplify_clause.cpp
View file

@ -101,12 +101,13 @@ namespace polysat {
* Then merge into p <= q. * Then merge into p <= q.
*/ */
bool simplify_clause::try_remove_equations(clause& cl) { bool simplify_clause::try_remove_equations(clause& cl) {
LOG_H2("Try removing equations"); LOG_H2("Remove superfluous equations from: " << cl);
sat::literal_set eqns; bool const has_eqn = any_of(cl, [&](sat::literal lit) { return s.lit2cnstr(lit).is_eq(); });
for (sat::literal lit : cl) if (!has_eqn)
if (s.lit2cnstr(lit).is_eq()) return false;
eqns.insert(lit); bool any_removed = false;
sat::literal_set to_remove; bool_vector& should_remove = m_bools;
should_remove.fill(cl.size(), false);
for (unsigned i = cl.size(); i-- > 0; ) { for (unsigned i = cl.size(); i-- > 0; ) {
sat::literal const lit = cl[i]; sat::literal const lit = cl[i];
signed_constraint const c = s.lit2cnstr(lit); signed_constraint const c = s.lit2cnstr(lit);
@ -120,9 +121,12 @@ namespace polysat {
signed_constraint const eq = s.m_constraints.find_eq(p - q); signed_constraint const eq = s.m_constraints.find_eq(p - q);
if (!eq) if (!eq)
continue; continue;
if (!eqns.contains(eq.blit())) auto const eq_it = std::find(cl.begin(), cl.end(), eq.blit());
if (eq_it == cl.end())
continue; continue;
to_remove.insert(eq.blit()); unsigned const eq_idx = std::distance(cl.begin(), eq_it);
any_removed = true;
should_remove[eq_idx] = true;
if (c.is_positive()) { if (c.is_positive()) {
// c: p <= q // c: p <= q
// eq: p == q // eq: p == q
@ -136,11 +140,11 @@ namespace polysat {
} }
} }
// Remove superfluous equations // Remove superfluous equations
if (to_remove.empty()) if (!any_removed)
return false; return false;
unsigned j = 0; unsigned j = 0;
for (unsigned i = 0; i < cl.size(); ++i) for (unsigned i = 0; i < cl.size(); ++i)
if (!to_remove.contains(cl[i])) if (!should_remove[i])
cl[j++] = cl[i]; cl[j++] = cl[i];
cl.m_literals.shrink(j); cl.m_literals.shrink(j);
return true; return true;

1
src/math/polysat/simplify_clause.h
View file

@ -28,6 +28,7 @@ namespace polysat {
solver& s; solver& s;
vector<subs_entry> m_entries; vector<subs_entry> m_entries;
bool_vector m_bools;
bool try_remove_equations(clause& cl); bool try_remove_equations(clause& cl);
bool try_recognize_bailout(clause& cl); bool try_recognize_bailout(clause& cl);