SMT: use more sort()
MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -523,7 +523,7 @@ expr expr::mul_no_soverflow(const expr &rhs) const {
expr expr::mul_no_uoverflow(const expr &rhs) const {
C(rhs);
auto bw = bits();
- return (zext(bw) * rhs.zext(bw)).extract(2 * bw - 1, bw) == mkUInt(0, bw);
+ return (zext(bw) * rhs.zext(bw)).extract(2*bw - 1, bw) == mkUInt(0, sort());
}
expr expr::sdiv_exact(const expr &rhs) const {
@@ -892,6 +892,36 @@ expr expr::sgt(const expr &rhs) const {
return !sle(rhs);
}
+expr expr::ule(uint64_t rhs) const {
+ C();
+ return ule(mkUInt(rhs, sort()));
+}
+
+expr expr::ult(uint64_t rhs) const {
+ C();
+ return ult(mkUInt(rhs, sort()));
+}
+
+expr expr::uge(uint64_t rhs) const {
+ C();
+ return uge(mkUInt(rhs, sort()));
+}
+
+expr expr::ugt(uint64_t rhs) const {
+ C();
+ return ugt(mkUInt(rhs, sort()));
+}
+
+expr expr::operator==(uint64_t rhs) const {
+ C();
+ return *this == mkUInt(rhs, sort());
+}
+
+expr expr::operator!=(uint64_t rhs) const {
+ C();
+ return *this != mkUInt(rhs, sort());
+}
+
expr expr::sext(unsigned amount) const {
C();
if (amount == 0)

MODIFY
smt/expr.h
smt/expr.h
@@ -176,12 +176,12 @@ public:
expr sge(const expr &rhs) const;
expr sgt(const expr &rhs) const;
- expr ule(uint64_t rhs) const { return ule(mkUInt(rhs, bits())); }
- expr ult(uint64_t rhs) const { return ult(mkUInt(rhs, bits())); }
- expr uge(uint64_t rhs) const { return uge(mkUInt(rhs, bits())); }
- expr ugt(uint64_t rhs) const { return ugt(mkUInt(rhs, bits())); }
- expr operator==(uint64_t rhs) const { return *this == mkUInt(rhs, bits()); }
- expr operator!=(uint64_t rhs) const { return *this != mkUInt(rhs, bits()); }
+ expr ule(uint64_t rhs) const;
+ expr ult(uint64_t rhs) const;
+ expr uge(uint64_t rhs) const;
+ expr ugt(uint64_t rhs) const;
+ expr operator==(uint64_t rhs) const;
+ expr operator!=(uint64_t rhs) const;
expr sext(unsigned amount) const;
expr zext(unsigned amount) const;

SMT: use more sort()