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

na

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-12-14 19:42:19 -08:00
parent 134831283f
commit 79bc33b88e
4 changed files with 10 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/polysat/constraint.cpp
View file

@ -233,8 +233,8 @@ namespace polysat {
return { dedup(alloc(mul_ovfl_constraint, *this, a, b)), true };
}
signed_constraint constraint_manager::shr(pdd const& p, pdd const& q) {
return { dedup(alloc(shr_constraint, *this, p, q)), true };
signed_constraint constraint_manager::shr(pdd const& p, pdd const& q, pdd const& r) {
return { dedup(alloc(shr_constraint, *this, p, q, r)), true };
}

2
src/math/polysat/constraint.h
View file

@ -97,7 +97,7 @@ namespace polysat {
signed_constraint slt(pdd const& a, pdd const& b);
signed_constraint mul_ovfl(pdd const& p, pdd const& q);
signed_constraint bit(pdd const& p, unsigned i);
signed_constraint shr(pdd const& p, pdd const& q);
signed_constraint shr(pdd const& p, pdd const& q, pdd const& r);
constraint *const* begin() const { return m_constraints.data(); }
constraint *const* end() const { return m_constraints.data() + m_constraints.size(); }

10
src/math/polysat/shr_constraint.cpp
View file

@ -28,11 +28,13 @@ namespace polysat {
}
lbool shr_constraint::eval(pdd const& p, pdd const& q, pdd const& r) const {
if (p.is_val() && r.is_val()) {
if (p.val() >= p.manager().power_of_2())
if (q.is_val() && r.is_val()) {
auto& m = p.manager();
if (q.val() >= m.power_of_2())
return r.is_zero() ? l_true : l_false;
if (r.is_val()) {
// todo
if (p.is_val()) {
pdd rr = p * m.mk_val(rational::power_of_two(q.val().get_unsigned()));
return rr == r ? l_true : l_false;
}
// other cases when we know lower
// bound of q, e.g, q = 2^k*q1 + q2, where q2 is a constant.

2
src/math/polysat/solver.cpp
View file

@ -139,7 +139,7 @@ namespace polysat {
auto& m = p.manager();
unsigned sz = m.power_of_2();
pdd r = m.mk_var(add_var(sz));
assign_eh(m_constraints.shr(r, p, q));
assign_eh(m_constraints.shr(p, q, r), null_dependency);
return r;
}