minor SMT encoding simpl to expr::abs()
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -593,14 +593,13 @@ StateValue BinOp::toSMT(State &s) const {
default:
UNREACHABLE();
}
- return {std::move(v), ap && bp};
+ return { move(v), ap && bp };
};
break;
case Abs:
fn = [&](auto a, auto ap, auto b, auto bp) -> StateValue {
- auto AbsA = a.abs();
- return {expr(AbsA), ap && (b == 0 || !AbsA.isNegative())};
+ return { a.abs(), ap && bp && (b == 0 || a != expr::IntSMin(a.bits())) };
};
break;
}

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -860,12 +860,8 @@ expr expr::smax(const expr &rhs) const {
expr expr::abs() const {
C();
- return mkIf(isNegative(), mkInt(0, *this) - *this, *this);
-}
-
-expr expr::isNegative() const {
- C();
- return this->slt(mkInt(0, *this));
+ auto s = sort();
+ return mkIf(sge(mkUInt(0, s)), *this, mkInt(-1, s) * *this);
}
expr expr::isNaN() const {

MODIFY
smt/expr.h
smt/expr.h
@@ -192,8 +192,6 @@ public:
expr abs() const;
- expr isNegative() const;
-
expr isNaN() const;
expr isInf() const;
expr isFPZero() const;

minor SMT encoding simpl to expr::abs()