smt expr: merge isNegative() and isSigned()
MODIFY
ir/type.cpp
ir/type.cpp
@@ -358,7 +358,7 @@ void IntType::printVal(ostream &os, State &s, const expr &e) const {
e.printHexadecimal(os);
os << " (";
e.printUnsigned(os);
- if (e.bits() > 1 && e.isSigned()) {
+ if (e.bits() > 1 && e.isNegative().isTrue()) {
os << ", ";
e.printSigned(os);
}

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -336,9 +336,10 @@ bool expr::isSMax() const {
return eq(IntSMax(bits()));
}
-bool expr::isSigned() const {
+expr expr::isNegative() const {
+ C();
auto bit = bits() - 1;
- return extract(bit, bit).isOne();
+ return extract(bit, bit) == 1;
}
unsigned expr::bits() const {
@@ -879,11 +880,6 @@ expr expr::abs() const {
return mkIf(sge(mkUInt(0, s)), *this, mkInt(-1, s) * *this);
}
-expr expr::isNegative() const {
- C();
- return this->slt(mkInt(0, *this));
-}
-
expr expr::isNaN() const {
return unop_fold(Z3_mk_fpa_is_nan);
}
@@ -1745,7 +1741,7 @@ void expr::printUnsigned(ostream &os) const {
}
void expr::printSigned(ostream &os) const {
- if (isSigned()) {
+ if (isNegative().isTrue()) {
os << '-';
(~*this + mkUInt(1, sort())).printUnsigned(os);
} else {

MODIFY
smt/expr.h
smt/expr.h
@@ -120,7 +120,7 @@ public:
bool isAllOnes() const;
bool isSMin() const;
bool isSMax() const;
- bool isSigned() const;
+ expr isNegative() const;
unsigned bits() const;
bool isUInt(uint64_t &n) const;
@@ -196,7 +196,6 @@ public:
expr abs() const;
- expr isNegative() const;
expr isNaN() const;
expr isInf() const;
expr isFPZero() const;

smt expr: merge isNegative() and isSigned()