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

Add simplify_clause::try_remove_equations

Browse source
This commit is contained in:
Jakob Rath 2022-12-22 14:53:42 +01:00
parent 5bd63ab7c5
commit b5af2164f4
5 changed files with 113 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/math/polysat/constraint_manager.cpp
View file

@ -305,6 +305,11 @@ namespace polysat {
return ~ule(b, a);
}
signed_constraint constraint_manager::find_eq(pdd const& p) /* const */ {
// TODO: implement as lookup rather than allocating/deduping constraint
return eq(p);
}
/**
* encode that the i'th bit of p is 1.
* It holds if p << (K - i - 1) >= 2^{K-1}, where K is the bit-width.

3
src/math/polysat/constraint_manager.h
View file

@ -102,6 +102,9 @@ namespace polysat {
constraint* lookup(sat::bool_var var) const;
signed_constraint lookup(sat::literal lit) const;
/** Find constraint p == 0; returns null if it doesn't exist yet */
signed_constraint find_eq(pdd const& p) /* const */;
signed_constraint eq(pdd const& p);
signed_constraint ule(pdd const& a, pdd const& b);
signed_constraint ult(pdd const& a, pdd const& b);

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

@ -11,21 +11,6 @@ Author:
Notes:
TODO: inspired from bench23, trying to strength weak FI lemma.
If we have both:
p <= q
p - q == 0
Then remove the equality.
If we have both:
p < q
p - q == 0
Then merge into p <= q.
TODO: from test_ineq_basic5: (mod 2^4)
Lemma: -0 \/ -1 \/ 2 \/ 3
-0: -4 > v1 + v0 [ bvalue=l_false @0 pwatched=1 ]
@ -93,6 +78,8 @@ namespace polysat {
bool simplify_clause::apply(clause& cl) {
LOG_H1("Simplifying clause: " << cl);
bool simplified = false;
if (try_remove_equations(cl))
simplified = true;
#if 0
if (try_recognize_bailout(cl))
simplified = true;
@ -102,6 +89,63 @@ namespace polysat {
return simplified;
}
/**
* If we have:
* p <= q
* p - q == 0
* Then remove the equality.
*
* If we have:
* p < q
* p - q == 0
* Then merge into p <= q.
*/
bool simplify_clause::try_remove_equations(clause& cl) {
LOG_H2("Try removing equations");
sat::literal_set eqns;
for (sat::literal lit : cl)
if (s.lit2cnstr(lit).is_eq())
eqns.insert(lit);
sat::literal_set to_remove;
for (unsigned i = cl.size(); i-- > 0; ) {
sat::literal const lit = cl[i];
signed_constraint const c = s.lit2cnstr(lit);
if (!c->is_ule())
continue;
if (c->is_eq())
continue;
LOG_V(10, "Examine: " << lit_pp(s, lit));
pdd const p = c->to_ule().lhs();
pdd const q = c->to_ule().rhs();
signed_constraint const eq = s.m_constraints.find_eq(p - q);
if (!eq)
continue;
if (!eqns.contains(eq.blit()))
continue;
to_remove.insert(eq.blit());
if (c.is_positive()) {
// c: p <= q
// eq: p == q
LOG("Removing " << eq.blit() << ": " << eq << " because it subsumes " << cl[i] << ": " << s.lit2cnstr(cl[i]));
}
else {
// c: p > q
// eq: p == q
cl[i] = s.ule(q, p).blit();
LOG("Merge " << eq.blit() << ": " << eq << " and " << lit << ": " << c << " to obtain " << cl[i] << ": " << s.lit2cnstr(cl[i]));
}
}
// Remove superfluous equations
if (to_remove.empty())
return false;
unsigned j = 0;
for (unsigned i = 0; i < cl.size(); ++i)
if (!to_remove.contains(cl[i]))
cl[j++] = cl[i];
cl.m_literals.shrink(j);
return true;
}
// If x != k appears among the new literals, all others are superfluous.
// TODO: this seems to work for lemmas coming from forbidden intervals, but in general it's too naive (esp. for side lemmas).
bool simplify_clause::try_recognize_bailout(clause& cl) {

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

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

45
src/test/polysat.cpp
View file

@ -630,6 +630,47 @@ namespace polysat {
SASSERT(cl->size() == 2);
}
// p <= q
// p == q (should be removed)
static void test_clause_simplify2() {
scoped_solver s(__func__);
simplify_clause simp(s);
clause_builder cb(s);
auto u = s.var(s.add_var(32));
auto v = s.var(s.add_var(32));
auto w = s.var(s.add_var(32));
auto p = 2*u*v;
auto q = 7*v*w;
cb.insert(s.ule(p, q));
cb.insert(s.eq(p, q));
auto cl = cb.build();
simp.apply(*cl);
std::cout << *cl << "\n";
SASSERT_EQ(cl->size(), 1);
SASSERT_EQ((*cl)[0], s.ule(p, q).blit());
}
// p < q
// p == q
// should be merged into p <= q
static void test_clause_simplify3() {
scoped_solver s(__func__);
simplify_clause simp(s);
clause_builder cb(s);
auto u = s.var(s.add_var(32));
auto v = s.var(s.add_var(32));
auto w = s.var(s.add_var(32));
auto p = 2*u*v;
auto q = 7*v*w;
cb.insert(s.ult(p, q));
cb.insert(s.eq(p, q));
auto cl = cb.build();
simp.apply(*cl);
std::cout << *cl << "\n";
SASSERT_EQ(cl->size(), 1);
SASSERT_EQ((*cl)[0], s.ule(p, q).blit());
}
// 8 * x + 3 == 0 or 8 * x + 5 == 0 is unsat
static void test_parity1() {
scoped_solver s(__func__);
@ -1917,6 +1958,8 @@ void tst_polysat() {
test_max_conflicts = 50;
// test_polysat::test_bench27_viable1(); // TODO: refinement
// test_polysat::test_bench27_viable2(); // TODO: refinement
test_polysat::test_band5(); // TODO: assertion
// test_polysat::test_fixed_point_arith_div_mul_inverse(); // TODO: assertion
return;
#endif
@ -1949,6 +1992,8 @@ void tst_polysat() {
RUN(test_polysat::test_parity4());
RUN(test_polysat::test_clause_simplify1());
RUN(test_polysat::test_clause_simplify2());
RUN(test_polysat::test_clause_simplify3());
RUN(test_polysat::test_add_conflicts());
RUN(test_polysat::test_wlist());