identify a couple more patterns for when an expression may be undef
increases number of trivial constraints and reduces timeouts
MODIFY
ir/state.cpp
ir/state.cpp
@@ -159,20 +159,47 @@ static expr strip_undef_and_add_ub(State &s, const Value &val, const expr &e,
return a;
}
- // (ite (= const (ite (= #b0 isundef_%var) %var undef)) #b1 #b0)
- // TODO: generalize to other undef-generating functions other than ==
if (e.isIf(c, a, b) && a.isConst() && b.isConst()) {
- if (c.isEq(lhs, rhs)) {
expr val, not_undef;
- if (rhs.isConst() && is_if_undef(lhs, val, not_undef)) {
+ // (ite (= val (ite (= #b0 isundef_%var) %var undef)) #b1 #b0)
+ if (c.isEq(lhs, rhs)) {
+ if (is_if_undef(lhs, val, not_undef)) {
s.addUB(move(not_undef));
return expr::mkIf(val == rhs, a, b);
}
- if (lhs.isConst() && is_if_undef(rhs, val, not_undef)) {
+ if (is_if_undef(rhs, val, not_undef)) {
s.addUB(move(not_undef));
return expr::mkIf(lhs == val, a, b);
}
}
+
+ if (c.isSLE(lhs, rhs)) {
+ // (ite (bvsle val (ite (= #b0 isundef_%var) %var undef)) #b1 #b0)
+ if (is_if_undef(rhs, val, not_undef)) {
+ s.addUB(not_undef || lhs == expr::IntSMin(lhs.bits()));
+ return expr::mkIf(lhs.sle(val), a, b);
+ }
+
+ // (ite (bvsle (ite (= #b0 isundef_%var) %var undef) val) #b1 #b0)
+ if (is_if_undef(lhs, val, not_undef)) {
+ s.addUB(not_undef || rhs == expr::IntSMax(rhs.bits()));
+ return expr::mkIf(val.sle(rhs), a, b);
+ }
+ }
+
+ if (c.isULE(lhs, rhs)) {
+ // (ite (bvule val (ite (= #b0 isundef_%var) %var undef)) #b1 #b0)
+ if (is_if_undef(rhs, val, not_undef)) {
+ s.addUB(not_undef || lhs == 0);
+ return expr::mkIf(lhs.ule(val), a, b);
+ }
+
+ // (ite (bvule (ite (= #b0 isundef_%var) %var undef) val) #b1 #b0)
+ if (is_if_undef(lhs, val, not_undef)) {
+ s.addUB(not_undef || rhs == expr::mkInt(-1, rhs));
+ return expr::mkIf(val.ule(rhs), a, b);
+ }
+ }
}
// 2) (or (and |isundef_%var| undef) (and %var (not |isundef_%var|)))

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -378,6 +378,14 @@ bool expr::isEq(expr &lhs, expr &rhs) const {
return isBinOp(lhs, rhs, Z3_OP_EQ);
}
+bool expr::isSLE(expr &lhs, expr &rhs) const {
+ return isBinOp(lhs, rhs, Z3_OP_SLEQ);
+}
+
+bool expr::isULE(expr &lhs, expr &rhs) const {
+ return isBinOp(lhs, rhs, Z3_OP_ULEQ);
+}
+
bool expr::isIf(expr &cond, expr &then, expr &els) const {
if (auto app = isAppOf(Z3_OP_ITE)) {
cond = Z3_get_app_arg(ctx(), app, 0);

MODIFY
smt/expr.h
smt/expr.h
@@ -131,6 +131,8 @@ public:
bool isInt(int64_t &n) const;
bool isEq(expr &lhs, expr &rhs) const;
+ bool isSLE(expr &lhs, expr &rhs) const;
+ bool isULE(expr &lhs, expr &rhs) const;
bool isIf(expr &cond, expr &then, expr &els) const;
bool isConcat(expr &a, expr &b) const;
bool isExtract(expr &e, unsigned &high, unsigned &low) const;

identify a couple more patterns for when an expression may be undef
increases number of trivial constraints and reduces timeouts