minor code simplifications
MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -1274,9 +1274,9 @@ expr expr::funo(const expr &rhs) const {
static expr get_bool(const expr &e) {
expr cond, then, els;
if (e.isIf(cond, then, els)) {
- if ((then == 1).isTrue() && (els == 0).isTrue())
+ if (then.isOne() && els.isZero())
return cond;
- if ((then == 0).isTrue() && (els == 1).isTrue())
+ if (then.isZero() && els.isOne())
return !cond;
}
return {};
@@ -2228,7 +2228,7 @@ string expr::numeral_string() const {
string expr::fn_name() const {
if (isApp())
return Z3_get_symbol_string(ctx(), Z3_get_decl_name(ctx(), decl()));
- return "";
+ return {};
}
unsigned expr::getFnNumArgs() const {

MODIFY
smt/expr.h
smt/expr.h
@@ -21,7 +21,7 @@ typedef struct _Z3_sort* Z3_sort;
namespace smt {
class expr {
- uintptr_t ptr;
+ uintptr_t ptr = 0;
expr(Z3_ast ast) noexcept;
bool isZ3Ast() const;
@@ -61,9 +61,9 @@ class expr {
bool isTernaryOp(expr &a, expr &b, expr &c, int z3op) const;
public:
- expr() : ptr(0) {}
+ expr() = default;
- expr(expr &&other) noexcept : ptr(0) {
+ expr(expr &&other) noexcept {
std::swap(ptr, other.ptr);
}

minor code simplifications