mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

elem

Browse source
This commit is contained in:
Jakob Rath 2023-02-07 09:57:32 +01:00
parent 984e98c88f
commit bf03886a87
3 changed files with 18 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -340,6 +340,18 @@ namespace polysat {
return ult(a + shift, b + shift); return ult(a + shift, b + shift);
} }
/** Membership test t \in [lo; hi[ is equivalent to t - lo < hi - lo. */
signed_constraint constraint_manager::elem(pdd const& t, pdd const& lo, pdd const& hi) {
return ult(t - lo, hi - lo);
}
signed_constraint constraint_manager::elem(pdd const& t, interval const& i) {
if (i.is_full())
return eq(t.manager().zero());
else
return elem(t, i.lo(), i.hi());
}
/** unsigned quotient/remainder */ /** unsigned quotient/remainder */
std::pair<pdd, pdd> constraint_manager::quot_rem(pdd const& a, pdd const& b) { std::pair<pdd, pdd> constraint_manager::quot_rem(pdd const& a, pdd const& b) {
auto& m = a.manager(); auto& m = a.manager();

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

@ -117,6 +117,9 @@ namespace polysat {
signed_constraint smul_udfl(pdd const& p, pdd const& q); signed_constraint smul_udfl(pdd const& p, pdd const& q);
signed_constraint bit(pdd const& p, unsigned i); signed_constraint bit(pdd const& p, unsigned i);
signed_constraint elem(pdd const& t, pdd const& lo, pdd const& hi);
signed_constraint elem(pdd const& t, interval const& i);
std::pair<pdd, pdd> quot_rem(pdd const& a, pdd const& b); std::pair<pdd, pdd> quot_rem(pdd const& a, pdd const& b);
pdd bnot(pdd const& p); pdd bnot(pdd const& p);

17
src/math/polysat/viable.cpp
View file

@ -945,14 +945,8 @@ namespace {
} }
} }
else if (!e->interval.is_full()) { else if (!e->interval.is_full()) {
auto const& hi = e->interval.hi(); signed_constraint c = s.m_constraints.elem(e->interval.hi(), n->interval.symbolic());
auto const& next_lo = n->interval.lo();
auto const& next_hi = n->interval.hi();
auto lhs = hi - next_lo;
auto rhs = next_hi - next_lo;
signed_constraint c = s.m_constraints.ult(lhs, rhs);
out_c.push_back(c); out_c.push_back(c);
// verbose_stream() << "C: " << lhs << " < " << rhs << " -> " << lit_pp(s, c) << "\n";
} }
if (e != e0) { if (e != e0) {
for (auto sc : e->side_cond) { for (auto sc : e->side_cond) {
@ -1296,13 +1290,8 @@ namespace {
// verbose_stream() << e->interval << " " << e->side_cond << " " << e->src << ";\n"; // verbose_stream() << e->interval << " " << e->side_cond << " " << e->src << ";\n";
if (!e->interval.is_full()) { if (!e->interval.is_full()) {
auto const& hi = e->interval.hi(); signed_constraint c = s.m_constraints.elem(e->interval.hi(), n->interval.symbolic());
auto const& next_lo = n->interval.lo(); lemma.insert_try_eval(~c);
auto const& next_hi = n->interval.hi();
auto lhs = hi - next_lo;
auto rhs = next_hi - next_lo;
signed_constraint c = s.m_constraints.ult(lhs, rhs);
lemma.insert_try_eval(~c); // "try" because linking constraint may contain unassigned variables, see test_polysat::test_bench23_fi_lemma for an example.
} }
for (auto sc : e->side_cond) for (auto sc : e->side_cond)
lemma.insert_eval(~sc); lemma.insert_eval(~sc);