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

bugfix

Browse source
This commit is contained in:
Jakob Rath 2023-08-11 14:52:26 +02:00
parent 81609ed043
commit 32d66951a8
3 changed files with 6 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1245,6 +1245,8 @@ namespace polysat {
for (auto c : core) {
if (!c->is_ule())
continue;
if (c->to_ule().power_of_2() != m.power_of_2())
continue;
auto i = inequality::from_ule(c);
if (c == a_l_b.as_signed_constraint())
continue;

3
src/math/polysat/ule_constraint.cpp
View file

@ -194,6 +194,8 @@ namespace polysat {
ule_constraint::ule_constraint(pdd const& l, pdd const& r) :
constraint(ckind_t::ule_t), m_lhs(l), m_rhs(r) {
SASSERT_EQ(m_lhs.power_of_2(), m_rhs.power_of_2());
m_vars.append(m_lhs.free_vars());
for (auto v : m_rhs.free_vars())
if (!m_vars.contains(v))
@ -201,6 +203,7 @@ namespace polysat {
}
void ule_constraint::simplify(bool& is_positive, pdd& lhs, pdd& rhs) {
SASSERT_EQ(lhs.power_of_2(), rhs.power_of_2());
#ifndef NDEBUG
bool const old_is_positive = is_positive;
pdd const old_lhs = lhs;

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

@ -45,6 +45,7 @@ namespace polysat {
bool operator==(constraint const& other) const override;
bool is_eq() const override { return m_rhs.is_zero(); }
void add_to_univariate_solver(pvar v, solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override;
unsigned power_of_2() const { return m_lhs.power_of_2(); }
};
struct ule_pp {