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

Rename confusing methods

Browse source 
avoid difference between c.is_eq() and c->is_eq()
This commit is contained in:
Jakob Rath 2023-06-23 11:59:18 +02:00
parent 8a50467ba8
commit 0c62b81a56
9 changed files with 27 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -28,15 +28,6 @@ namespace polysat {
return eval(s.get_assignment());
}
bool signed_constraint::is_eq() const {
return is_positive() && m_constraint->is_eq();
}
pdd const& signed_constraint::eq() const {
SASSERT(is_eq());
return m_constraint->to_ule().lhs();
}
inequality inequality::from_ule(signed_constraint src)
{
ule_constraint& c = src->to_ule();
@ -91,6 +82,11 @@ namespace polysat {
return { std::move(lhs), std::move(rhs), m_src };
}
pdd const& constraint::to_eq() const {
SASSERT(is_eq());
return to_ule().lhs();
}
ule_constraint& constraint::to_ule() {
return *dynamic_cast<ule_constraint*>(this);
}

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

@ -90,6 +90,7 @@ namespace polysat {
*/
virtual clause_ref produce_lemma(solver& s, assignment const& a, bool is_positive) { return {}; }
pdd const& to_eq() const;
ule_constraint& to_ule();
ule_constraint const& to_ule() const;
umul_ovfl_constraint& to_umul_ovfl();
@ -180,10 +181,8 @@ namespace polysat {
constraint& operator*() { return *m_constraint; }
constraint const& operator*() const { return *m_constraint; }
bool is_eq() const;
bool is_diseq() const { return negated().is_eq(); }
pdd const& eq() const;
pdd const& diseq() const { return negated().eq(); }
bool is_pos_eq() const { return is_positive() && m_constraint->is_eq(); }
bool is_neg_eq() const { return is_negative() && m_constraint->is_eq(); }
signed_constraint& operator=(std::nullptr_t) { m_constraint = nullptr; return *this; }

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

@ -45,7 +45,7 @@ namespace polysat {
}
bool eq_explain::try_explain1(pvar v, signed_constraint c, conflict& core) {
if (!c.is_eq())
if (!c.is_pos_eq())
return false;
if (!c.is_currently_false(s))
return false;

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

@ -106,7 +106,7 @@ namespace polysat {
*/
bool simplify_clause::try_remove_equations(clause& cl) {
LOG_H2("Remove superfluous equations from: " << cl);
bool const has_eqn = any_of(cl, [&](sat::literal lit) { return s.lit2cnstr(lit).is_eq(); });
bool const has_eqn = any_of(cl, [&](sat::literal lit) { return !lit.sign() && s.lit2cnstr(lit)->is_eq(); });
if (!has_eqn)
return false;
bool any_removed = false;
@ -189,8 +189,8 @@ namespace polysat {
return false;
}
SASSERT(v != null_var); // constraints without unassigned variables would be evaluated at this point
if (c.is_diseq() && c.diseq().is_unilinear()) {
pdd const& p = c.diseq();
if (c.is_negative() && c->is_eq() && c->to_eq().is_unilinear()) {
pdd const& p = c->to_eq();
if (p.hi().is_one()) {
eq = lit;
k = (-p.lo()).val();
@ -589,7 +589,7 @@ namespace polysat {
trailing_bits mask;
single_bit bit;
pdd p = c->to_ule().lhs();
if ((c.is_eq() || c.is_diseq()) && get_lsb(c->to_ule().lhs(), c->to_ule().rhs(), p, mask, c.is_positive())) {
if (c->is_eq() && get_lsb(c->to_ule().lhs(), c->to_ule().rhs(), p, mask, c.is_positive())) {
if (mask.bits.bitsize() > mask.length) {
removed[i] = true; // skip this constraint. e.g., 2^(k-3)*x = 9*2^(k-3) is false as 9 >= 2^3
continue;

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

@ -37,8 +37,8 @@ namespace polysat {
LOG_H3("Resolving upon v" << v);
LOG("c1: " << lit_pp(s, c1));
LOG("c2: " << lit_pp(s, c2));
pdd a = c1.eq();
pdd b = c2.eq();
pdd a = c1->to_eq();
pdd b = c2->to_eq();
unsigned degree_a = a.degree();
unsigned degree_b = b.degree();
pdd r = a;
@ -67,7 +67,7 @@ namespace polysat {
for (auto c1 : s.m_viable.get_constraints(v)) {
if (!c1->contains_var(v)) // side conditions do not contain v; skip them here
continue;
if (!c1.is_eq())
if (!c1.is_pos_eq())
continue;
SASSERT(c1.is_currently_true(s));
SASSERT(c2.is_currently_false(s));
@ -102,7 +102,7 @@ namespace polysat {
// true = done, false = abort, undef = continue
lbool ex_polynomial_superposition::try_explain1(pvar v, conflict& core) {
for (auto c2 : core) {
if (!c2.is_eq())
if (!c2.is_pos_eq())
continue;
if (!c2->contains_var(v))
continue;
@ -128,7 +128,7 @@ namespace polysat {
for (auto c : core) {
if (!c->contains_var(v))
continue;
if (!c.is_eq())
if (!c.is_pos_eq())
continue;
#if 0
if (!c.is_currently_true(s))
@ -151,7 +151,7 @@ namespace polysat {
continue;
if (!c->contains_var(v))
continue;
if (c.is_eq())
if (c.is_pos_eq())
continue;
LOG("try-reduce: " << c << " " << c.is_currently_false(s));
if (!c->is_ule())

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

@ -8,7 +8,7 @@ Module Name:
Author:
Nikolaj Bjorner (nbjorner) 2021-03-19
Jakob Rath 2021-04-6
Jakob Rath 2021-04-06
Notes:

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

@ -8,7 +8,7 @@ Module Name:
Author:
Nikolaj Bjorner (nbjorner) 2021-03-19
Jakob Rath 2021-04-6
Jakob Rath 2021-04-06
--*/
#pragma once

6
src/math/polysat/variable_elimination.cpp
View file

@ -279,9 +279,9 @@ namespace polysat {
// find constraint that allows computing v from other variables
// (currently, consider only equations that contain v with degree 1)
for (signed_constraint c : core) {
if (!c.is_eq())
if (!c.is_pos_eq())
continue;
if (c.eq().degree(v) != 1)
if (c->to_eq().degree(v) != 1)
continue;
find_lemma(v, c, core);
}
@ -289,7 +289,7 @@ namespace polysat {
void free_variable_elimination::find_lemma(pvar v, signed_constraint c, conflict& core) {
LOG_H3("Free Variable Elimination for v" << v << " using equation " << c);
pdd const& p = c.eq();
pdd const& p = c->to_eq();
SASSERT_EQ(p.degree(v), 1);
auto& m = p.manager();
pdd fac = m.zero();

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

@ -985,8 +985,8 @@ namespace {
justifications[bit.position].clear();
justifications[bit.position].push_back(e1);
}
else if ((src->is_eq() || src.is_diseq()) &&
simplify_clause::get_lsb(s.subst(src->to_ule().lhs()), s.subst(src->to_ule().rhs()), p, lsb, src.is_positive()) && p.is_var()) {
else if (src->is_eq() &&
simplify_clause::get_lsb(s.subst(src->to_ule().lhs()), s.subst(src->to_ule().rhs()), p, lsb, src.is_positive()) && p.is_var()) {
if (src.is_positive()) {
for (unsigned i = 0; i < lsb.length; i++) {
lbool prev = fixed[i];
@ -1179,7 +1179,7 @@ namespace {
justifications[bit.position].clear();
justifications[bit.position].push_back(src);
}
else if ((src->is_eq() || src.is_diseq()) &&
else if (src->is_eq() &&
simplify_clause::get_lsb(src->to_ule().lhs(), src->to_ule().rhs(), p, mask, src.is_positive()) && p.is_var()) {
if (src.is_positive()) {
for (unsigned i = 0; i < mask.length; i++) {