diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index 719b186a8..b56983b9b 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -88,6 +88,8 @@ namespace polysat { pdd rhs; bool is_strict; constraint const* src; + inequality(pdd const & lhs, pdd const & rhs, bool is_strict, constraint const* src): + lhs(lhs), rhs(rhs), is_strict(is_strict), src(src) {} }; diff --git a/src/math/polysat/eq_constraint.cpp b/src/math/polysat/eq_constraint.cpp index 0301fd987..f1d96672c 100644 --- a/src/math/polysat/eq_constraint.cpp +++ b/src/math/polysat/eq_constraint.cpp @@ -214,12 +214,12 @@ namespace polysat { inequality eq_constraint::as_inequality() const { SASSERT(!is_undef()); pdd zero = p() - p(); - if (is_positive()) { + if (is_positive()) // p <= 0 - return { .lhs = p(), .rhs = zero, .is_strict = false, .src = this }; - } else { + return inequality(p(), zero, false, this); + else // 0 < p - return { .lhs = zero, .rhs = p(), .is_strict = true, .src = this }; - } + return inequality(zero, p(), true, this); } + } diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp index 05c213f3c..965383365 100644 --- a/src/math/polysat/ule_constraint.cpp +++ b/src/math/polysat/ule_constraint.cpp @@ -290,10 +290,9 @@ namespace polysat { inequality ule_constraint::as_inequality() const { SASSERT(!is_undef()); - if (is_positive()) { - return { .lhs = lhs(), .rhs = rhs(), .is_strict = false, .src = this }; - } else { - return { .lhs = rhs(), .rhs = lhs(), .is_strict = true, .src = this }; - } + if (is_positive()) + return inequality(lhs(), rhs(), false, this); + else + return inequality(rhs(), lhs(), true, this); } }