mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-15 00:35:11 +00:00
Code Activity

Delete unused ineq::operator==

Browse source 
The operator is unused, so there is no need to figure what is
the best fix for it.
This commit is contained in:
Arie Gurfinkel 2026-04-12 13:43:53 -04:00
parent 1576824675
commit a86132095d
1 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/math/lp/nla_types.h
View file

@ -41,9 +41,8 @@ namespace nla {
ineq(const lp::lar_term& term, lp::lconstraint_kind cmp, const rational& rs) : m_cmp(cmp), m_term(term), m_rs(rs) {}
ineq(lpvar v, lp::lconstraint_kind cmp, int i): m_cmp(cmp), m_term(v), m_rs(rational(i)) {}
ineq(lpvar v, lp::lconstraint_kind cmp, rational const& r): m_cmp(cmp), m_term(v), m_rs(r) {}
bool operator==(const ineq& a) const {
return m_cmp == a.m_cmp && &m_term == &a.m_term && m_rs == a.m_rs;
}
bool operator==(const ineq& a) const = delete;
bool operator!=(const ineq& a) const = delete;
const lp::lar_term& term() const { return m_term; };
lp::lconstraint_kind cmp() const { return m_cmp; };
const rational& rs() const { return m_rs; };