smt expr: use bvnot for 'x xor -1'
MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -702,6 +702,10 @@ expr expr::fdiv(const expr &rhs) const {
return Z3_mk_fpa_div(ctx(), rm, ast(), rhs());
}
+expr expr::fneg() const {
+ return unop_fold(Z3_mk_fpa_neg);
+}
+
expr expr::foeq(const expr &rhs) const {
return ford(rhs) && binop_fold(rhs, Z3_mk_fpa_eq);
}
@@ -758,10 +762,6 @@ expr expr::funo(const expr &rhs) const {
return !ford(rhs());
}
-expr expr::fneg() const {
- return unop_fold(Z3_mk_fpa_neg);
-}
-
expr expr::operator&(const expr &rhs) const {
if (eq(rhs))
return *this;
@@ -806,6 +806,10 @@ expr expr::operator|(const expr &rhs) const {
expr expr::operator^(const expr &rhs) const {
if (eq(rhs))
return mkUInt(0, sort());
+ if (isAllOnes())
+ return ~rhs;
+ if (rhs.isAllOnes())
+ return ~*this;
return binopc(Z3_mk_bvxor, isZero, alwaysFalse);
}
@@ -823,8 +827,7 @@ expr expr::operator!() const {
}
expr expr::operator~() const {
- C();
- return mkInt(-1, sort()) - *this;
+ return unop_fold(Z3_mk_bvnot);
}
expr expr::operator==(const expr &rhs) const {

MODIFY
smt/expr.h
smt/expr.h
@@ -171,6 +171,7 @@ public:
expr fsub(const expr &rhs) const;
expr fmul(const expr &rhs) const;
expr fdiv(const expr &rhs) const;
+ expr fneg() const;
expr foeq(const expr &rhs) const;
expr fogt(const expr &rhs) const;
@@ -186,7 +187,6 @@ public:
expr fule(const expr &rhs) const;
expr fune(const expr &rhs) const;
expr funo(const expr &rhs) const;
- expr fneg() const;
expr operator&(const expr &rhs) const;
expr operator|(const expr &rhs) const;

smt expr: use bvnot for 'x xor -1'