THEORY bitvectors-cast; LOGIC QF_UFBV; SOLVER external; SIGNATURE Xor, icmp_sge, icmp_ugt, lshr, icmp_sgt, icmp_uge, icmp_ne, select, icmp_eq, sub, add, zext_11, True, trunc_11, add_i29, sext_11, sext, sext_i1, icmp, Or, trunc, And, icmp_ult, False, icmp_slt, icmp_ule, zext, shl, ashr, RULES And(Xor(X, C1), C2) -> Xor(And(X, C2), CL0) [ ((C1 &.32 C2) =.32 CL0)] ; /* AndOrXor:135*/ And(Or(X, C1), C2) -> And(Or(X, CL0), C2) [ ((C1 &.32 C2) =.32 CL0)] ; /* AndOrXor:144*/ And(Or(X, C1), C2) -> Or(And(X, CL0), C1) [ (((C2 ^.32 (C1 &.32 C2)) =.32 CL0) /\ ((C1 &.32 C2) =.32 C1))] ; /* AndOrXor:151*/ And(add(X, C1), C2) -> And(X, C2) [ (isPowerOf2.32(C2) /\ (((C1 &.32 (C2 -.32 bv32"#x00000001")) =.32 bv32"#x00000000") /\ ((C2 &.32 C1) =.32 bv32"#x00000000")))] ; /* AndOrXor:185*/ And(add(X, C1), C2) -> Xor(And(X, C2), C2) [ (isPowerOf2.32(C2) /\ (((C1 &.32 (C2 -.32 bv32"#x00000001")) =.32 bv32"#x00000000") /\ ((C2 &.32 C1) !=.32 bv32"#x00000000")))] ; /* AndOrXor:190*/ And(shl(X, C1), C2) -> shl(X, C1) [ ((C2 &.32 (bv32"#xffffffff" <<.32 C1)) =.32 (bv32"#xffffffff" <<.32 C1))] ; /* AndOrXor:206*/ And(shl(X, C1), C2) -> And(shl(X, C1), CL0) [ (((C2 &.32 (bv32"#xffffffff" <<.32 C1)) =.32 CL0) /\ (((C2 &.32 (bv32"#xffffffff" <<.32 C1)) !=.32 (bv32"#xffffffff" <<.32 C1)) /\ ((C2 &.32 (bv32"#xffffffff" <<.32 C1)) !=.32 C2)))] ; /* AndOrXor:210*/ And(lshr(X, C1), C2) -> lshr(X, C1) [ ((C2 &.32 (bv32"#xffffffff" >>u.32 C1)) =.32 (bv32"#xffffffff" >>u.32 C1))] ; /* AndOrXor:226*/ And(lshr(X, C1), C2) -> And(lshr(X, C1), CL0) [ (((C2 &.32 (bv32"#xffffffff" >>u.32 C1)) =.32 CL0) /\ ((C2 &.32 (bv32"#xffffffff" >>u.32 C1)) !=.32 (bv32"#xffffffff" >>u.32 C1)))] ; /* AndOrXor:230*/ And(ashr(X, C1), C2) -> And(lshr(X, C1), C2) [ (hasOneUse.32 /\ ((C2 &.32 (bv32"#xffffffff" >>u.32 C1)) =.32 C2))] ; /* AndOrXor:246*/ And(icmp_sge(X, C1), icmp_slt(X, C2)) -> False [ ((C1 <=s.32 C2) /\ (C1 =.32 C2))] ; /* AndOrXor:270*/ And(icmp_sge(X, C1), icmp_slt(X, C2)) -> icmp_slt(X, C2) [ ((C1 <=s.32 C2) /\ (C1 =.32 (bv32"#x00000001" <<.32 (width.32(C1) -.32 bv32"#x00000001"))))] ; /* AndOrXor:273*/ And(icmp_sge(X, C1), icmp_slt(X, C2)) -> icmp_ult(add(X, neg.32(C1)), CL0) [ (((neg.32(C1) +.32 C2) =.32 CL0) /\ (C1 <=s.32 C2))] ; /* AndOrXor:280*/ Or(icmp_slt(X, C1), icmp_sge(X, C2)) -> True [ ((C1 <=s.32 C2) /\ (C1 =.32 C2))] ; /* AndOrXor:287*/ Or(icmp_slt(X, C1), icmp_sge(X, C2)) -> icmp_sgt(X, CL0) [ (((C2 -.32 bv32"#x00000001") =.32 CL0) /\ ((C1 <=s.32 C2) /\ ((C1 !=.32 C2) /\ (C1 =.32 (bv32"#x00000001" <<.32 (width.32(C1) -.32 bv32"#x00000001"))))))] ; /* AndOrXor:290*/ Or(icmp_slt(X, C1), icmp_sge(X, C2)) -> icmp_ugt(add(X, neg.32(C1)), CL0) [ (((neg.32(C1) +.32 (C2 -.32 bv32"#x00000001")) =.32 CL0) /\ ((C1 <=s.32 C2) /\ (C1 !=.32 C2)))] ; /* AndOrXor:298*/ And(add(And(A, C1), B), C2) -> And(add(A, B), C2) [ (((C1 &.32 C2) =.32 C2) /\ (isPowerOf2OrZero.32((C2 +.32 bv32"#x00000001")) \/ (isShiftedMask.32(C2) /\ MaskedValueIsZero.32(B, ((bv32"#x00000001" <<.32 (width.32(C2) -.32 countLeadingZeros.32(((C2 -.32 bv32"#x00000001") ^.32 C2)))) -.32 bv32"#x00000001")))))] ; /* AndOrXor:343*/ And(add(Or(A, C1), B), C2) -> And(add(A, B), C2) [ (isPowerOf2OrZero.32((C2 +.32 bv32"#x00000001")) /\ ((C1 &.32 C2) =.32 bv32"#x00000000"))] ; /* AndOrXor:363*/ And(sub(Xor(A, C1), B), C2) -> And(sub(A, B), C2) [ (isPowerOf2OrZero.32((C2 +.32 bv32"#x00000001")) /\ ((C1 &.32 C2) =.32 bv32"#x00000000"))] ; /* AndOrXor:364*/ icmp_slt(X, bv32"#x00000000") -> icmp_ne(And(X, CL0), bv32"#x00000000") [ ((bv32"#x00000001" <<.32 (width.32(X) -.32 bv32"#x00000001")) =.32 CL0)] ; /* AndOrXor:516*/ icmp_sgt(X, bv32"#xffffffff") -> icmp_eq(And(X, CL0), bv32"#x00000000") [ ((bv32"#x00000001" <<.32 (width.32(X) -.32 bv32"#x00000001")) =.32 CL0)] ; /* AndOrXor:523*/ icmp_ult(X, C) -> icmp_eq(And(X, neg.32(C)), bv32"#x00000000") [ isPowerOf2.32(C)] ; /* AndOrXor:530*/ icmp_ugt(X, C) -> icmp_ne(And(X, ~.32(C)), bv32"#x00000000") [ isPowerOf2.32((C +.32 bv32"#x00000001"))] ; /* AndOrXor:537*/ And(icmp_eq(And(a, b), bv32"#x00000000"), icmp_eq(And(a, d), bv32"#x00000000")) -> icmp_eq(And(a, Or(b, d)), bv32"#x00000000"); /* AndOrXor:698*/ And(icmp_eq(And(a, b), b), icmp_eq(And(a, d), d)) -> icmp_eq(And(a, Or(b, d)), Or(b, d)); /* AndOrXor:709*/ And(icmp_eq(And(a, b), a), icmp_eq(And(a, d), a)) -> icmp_eq(And(a, And(b, d)), a); /* AndOrXor:716*/ And(icmp_ne(And(a, C1), bv32"#x00000000"), icmp_ne(And(a, C2), bv32"#x00000000")) -> icmp_ne(And(a, C1), bv32"#x00000000") [ ((C1 &.32 C2) =.32 C1)] ; /* AndOrXor:732-1*/ And(icmp_ne(And(a, C1), C1), icmp_ne(And(a, C2), C2)) -> icmp_ne(And(a, C1), C1) [ ((C1 &.32 C2) =.32 C1)] ; /* AndOrXor:732-2*/ And(icmp_ne(And(a, C1), a), icmp_ne(And(a, C2), a)) -> icmp_ne(And(a, C1), a) [ ((C1 |.32 C2) =.32 C1)] ; /* AndOrXor:745*/ And(icmp_eq(And(a, C1), C2), icmp_eq(And(a, C3), C4)) -> icmp_eq(And(a, CL0), CL1) [ (((C1 |.32 C3) =.32 CL0) /\ (((C2 |.32 C4) =.32 CL1) /\ ((((C1 &.32 C3) &.32 (C2 ^.32 C4)) =.32 bv32"#x00000000") /\ (((C1 &.32 C2) =.32 C2) /\ ((C3 &.32 C4) =.32 C4)))))] ; /* AndOrXor:757*/ And(icmp_sgt(a, b), icmp_ne(a, b)) -> icmp_sgt(a, b); /* AndOrXor:794*/ And(icmp_ult(a, C), icmp_ult(b, C)) -> icmp_ult(Or(a, b), C) [ isPowerOf2.32(C)] ; /* AndOrXor:819*/ And(icmp_eq(a, bv32"#x00000000"), icmp_eq(b, bv32"#x00000000")) -> icmp_eq(Or(a, b), bv32"#x00000000"); /* AndOrXor:827*/ And(icmp_eq(CL0, C1), icmp_eq(And(x, C3), C2)) -> icmp_eq(And(x, CL1), CL2) [ (((zext.32(C1) |.32 C2) =.32 CL2) /\ ((trunc.32(x) =.32 CL0) /\ (((C3 |.32 ((bv32"#x00000001" <<.32 width.32(C1)) -.32 bv32"#x00000001")) =.32 CL1) /\ (((((bv32"#x00000001" <<.32 width.32(C1)) -.32 bv32"#x00000001") &.32 C3) =.32 bv32"#x00000000") /\ ((((bv32"#x00000001" <<.32 width.32(C1)) -.32 bv32"#x00000001") &.32 C2) =.32 bv32"#x00000000")))))] ; /* AndOrXor:842*/ And(icmp_eq(a, C1), icmp_eq(a, C2)) -> False [ (C1 !=.32 C2)] ; /* AndOrXor:887-1*/ And(icmp_eq(a, C1), icmp_ne(a, C1)) -> False; /* AndOrXor:887-2*/ And(icmp_eq(a, C1), icmp_ne(a, C2)) -> icmp_eq(a, C1) [ (C1 <u.32 C2)] ; /* AndOrXor:922*/ And(icmp_eq(a, C1), icmp_ult(a, C2)) -> icmp_eq(a, C1) [ (C1 <u.32 C2)] ; /* AndOrXor:923*/ And(icmp_eq(a, C1), icmp_slt(a, C2)) -> icmp_eq(a, C1) [ (C1 <s.32 C2)] ; /* AndOrXor:924*/ And(icmp_ne(a, C1), icmp_ult(a, C2)) -> icmp_ult(a, C1) [ ((C1 <u.32 C2) /\ (C1 =.32 (C2 -.32 bv32"#x00000001")))] ; /* AndOrXor:931*/ And(icmp_ne(a, C1), icmp_slt(a, C2)) -> icmp_slt(a, C1) [ ((C1 <s.32 C2) /\ (C1 =.32 (C2 -.32 bv32"#x00000001")))] ; /* AndOrXor:937*/ And(icmp_ne(a, C1), icmp_eq(a, C2)) -> icmp_eq(a, C2) [ (C1 <u.32 C2)] ; /* AndOrXor:940*/ And(icmp_ne(a, C1), icmp_ugt(a, C2)) -> icmp_ugt(a, C2) [ (C1 <u.32 C2)] ; /* AndOrXor:941*/ And(icmp_ne(a, C1), icmp_sgt(a, C2)) -> icmp_sgt(a, C2) [ (C1 <s.32 C2)] ; /* AndOrXor:942*/ And(icmp_ne(a, C1), icmp_ne(a, C2)) -> icmp_ugt(add(a, neg.32(C1)), bv32"#x00000001") [ ((C1 <u.32 C2) /\ (C1 =.32 (C2 -.32 bv32"#x00000001")))] ; /* AndOrXor:949*/ And(icmp_ult(a, C1), icmp_eq(a, C2)) -> False [ (C1 <u.32 C2)] ; /* AndOrXor:961*/ And(icmp_ult(a, C1), icmp_ugt(a, C2)) -> False [ (C1 <u.32 C2)] ; /* AndOrXor:962*/ And(icmp_ult(a, C1), icmp_ne(a, C2)) -> icmp_ult(a, C1) [ (C1 <u.32 C2)] ; /* AndOrXor:966*/ And(icmp_ult(a, C1), icmp_ult(a, C2)) -> icmp_ult(a, C1) [ (C1 <u.32 C2)] ; /* AndOrXor:967*/ And(icmp_slt(a, C1), icmp_ne(a, C2)) -> icmp_slt(a, C1) [ (C1 <s.32 C2)] ; /* AndOrXor:978*/ And(icmp_slt(a, C1), icmp_slt(a, C2)) -> icmp_slt(a, C1) [ (C1 <s.32 C2)] ; /* AndOrXor:979*/ And(icmp_ugt(a, C1), icmp_eq(a, C2)) -> icmp_eq(a, C2) [ (C1 <u.32 C2)] ; /* AndOrXor:988*/ And(icmp_ugt(a, C1), icmp_ugt(a, C2)) -> icmp_ugt(a, C2) [ (C1 <u.32 C2)] ; /* AndOrXor:989*/ And(icmp_ugt(a, C1), icmp_ne(a, C2)) -> icmp_ugt(a, C2) [ ((C1 <u.32 C2) /\ (C2 =.32 (C1 +.32 bv32"#x00000001")))] ; /* AndOrXor:994*/ And(icmp_sgt(a, C1), icmp_eq(a, C2)) -> icmp_eq(a, C2) [ (C1 <s.32 C2)] ; /* AndOrXor:1006*/ And(icmp_sgt(a, C1), icmp_sgt(a, C2)) -> icmp_sgt(a, C2) [ (C1 <s.32 C2)] ; /* AndOrXor:1007*/ And(icmp_sgt(a, C1), icmp_ne(a, C2)) -> icmp_sgt(a, C2) [ ((C1 <s.32 C2) /\ (C2 =.32 (C1 +.32 bv32"#x00000001")))] ; /* AndOrXor:1012*/ And(Xor(op0LHS, op0RHS), C) -> Xor(op0LHS, And(op0RHS, C)) [ MaskedValueIsZero.32(op0LHS, ~.32(C))] ; /* AndOrXor:1140-1*/ And(Or(op0LHS, op0RHS), C) -> Or(op0LHS, And(op0RHS, C)) [ MaskedValueIsZero.32(op0LHS, ~.32(C))] ; /* AndOrXor:1140-2*/ And(Xor(op0LHS, op0RHS), C) -> Xor(And(op0LHS, C), op0RHS) [ MaskedValueIsZero.32(op0RHS, ~.32(C))] ; /* AndOrXor:1146-1*/ And(Or(op0LHS, op0RHS), C) -> Or(And(op0LHS, C), op0RHS) [ MaskedValueIsZero.32(op0RHS, ~.32(C))] ; /* AndOrXor:1146-2*/ And(sub(A, B), C) -> And(sub(bv32"#x00000000", B), C) [ MaskedValueIsZero.32(A, (bv32"#xffffffff" >>u.32 countLeadingZeros.32(C)))] ; /* AndOrXor:1175*/ And(shl(bv32"#x00000001", op0RHS), bv32"#x00000001") -> zext(icmp_eq(op0RHS, bv32"#x00000000")); /* AndOrXor:1191-1*/ And(lshr(bv32"#x00000001", op0RHS), bv32"#x00000001") -> zext(icmp_eq(op0RHS, bv32"#x00000000")); /* AndOrXor:1191-2*/ And(trunc(And(x, C1)), C2) -> And(trunc(x), CL0) [ ((trunc.32(C1) &.32 C2) =.32 CL0)] ; /* AndOrXor:1207*/ And(Xor(notOp0, bv32"#xffffffff"), Xor(notOp1, bv32"#xffffffff")) -> Xor(Or(notOp0, notOp1), bv32"#xffffffff"); /* AndOrXor:1230 ~A & ~B -> ~(A | B)*/ And(Or(A, B), Xor(And(A, B), bv32"#xffffffff")) -> Xor(A, B); /* AndOrXor:1241 (A|B) & ~(A&B) => A^B*/ And(Xor(And(A, B), bv32"#xffffffff"), Or(A, B)) -> Xor(A, B); /* AndOrXor:1247 ~(A&B) & (A|B) => A^B*/ And(Xor(A, B), A) -> And(A, Xor(B, bv32"#xffffffff")); /* AndOrXor:1253 A & (A^B) -> A & ~B*/ And(Or(Xor(A, bv32"#xffffffff"), B), A) -> And(A, B); /* AndOrXor:1280 (~A|B)&A -> A&B*/ And(Xor(A, B), Xor(Xor(B, C), A)) -> And(Xor(A, B), Xor(C, bv32"#xffffffff")); /* AndOrXor:1288 (A ^ B) & ((B ^ C) ^ A) -> (A ^ B) & ~C*/ And(Or(A, B), Xor(Xor(A, bv32"#xffffffff"), B)) -> And(A, B); /* AndOrXor:1294 (A | B) & ((~A) ^ B) -> (A & B)*/ And(sext(x), sext(y)) -> sext(And(x, y)); /* AndOrXor:1346 (sext)*/ And(zext(x), zext(y)) -> zext(And(x, y)); /* AndOrXor:1346 (zext)*/ And(trunc(x), trunc(y)) -> trunc(And(x, y)); /* AndOrXor:1346 (trunc)*/ And(sext_i1(a), b) -> select(a, b, bv32"#x00000000"); /* AndOrXor:1388*/ And(Xor(sext_i1(a), bv32"#xffffffff"), b) -> select(a, bv32"#x00000000", b); /* AndOrXor:1395*/ Or(And(sext(Cond), C), And(B, Xor(sext(Cond), bv32"#xffffffff"))) -> select(Cond, C, B); /* AndOrXor:1574*/ Or(And(sext(Cond), C), And(B, sext(Xor(Cond, bv32"#xffffffff")))) -> select(Cond, C, B); /* AndOrXor:1577*/ Or(And(sext(Cond), C), And(Xor(sext(Cond), bv32"#xffffffff"), D)) -> select(Cond, C, D); /* AndOrXor:1581*/ Or(And(sext(Cond), C), And(sext(Xor(Cond, bv32"#xffffffff")), D)) -> select(Cond, C, D); /* AndOrXor:1583*/ Or(icmp_eq(And(A, K1), bv32"#x00000000"), icmp_eq(And(A, K2), bv32"#x00000000")) -> icmp_ne(And(A, Or(K1, K2)), Or(K1, K2)) [ (isPowerOf2.32(K1) /\ isPowerOf2.32(K2))] ; /* AndOrXor:1593*/ Or(icmp_ult(add_i29(A, C1), C3), icmp_ult(add(A, C2), C3)) -> icmp_ult(add(And(A, ~.32(CL0)), CL1), C3) [ (((C1 ^.32 C2) =.32 CL0) /\ ((umax.32(C1, C2) =.32 CL1) /\ ((C1 >u.32 C3) /\ ((C2 >u.32 C3) /\ (isPowerOf2.32((C1 ^.32 C2)) /\ (isPowerOf2.32((neg.32(C2) ^.32 neg.32(C1))) /\ (((neg.32(C2) ^.32 neg.32(C1)) =.32 ((C3 -.32 C2) ^.32 (C3 -.32 C1))) /\ (abs.32((C1 -.32 C2)) >u.32 C3))))))))] ; /* AndOrXor:1628-1*/ Or(icmp_ule(add_i29(A, C1), C3), icmp_ule(add(A, C2), C3)) -> icmp_ule(add(And(A, ~.32(CL0)), CL1), C3) [ (((C1 ^.32 C2) =.32 CL0) /\ ((umax.32(C1, C2) =.32 CL1) /\ ((C1 >u.32 C3) /\ ((C2 >u.32 C3) /\ (isPowerOf2.32((C1 ^.32 C2)) /\ (isPowerOf2.32((neg.32(C2) ^.32 neg.32(C1))) /\ (((neg.32(C2) ^.32 neg.32(C1)) =.32 ((C3 -.32 C2) ^.32 (C3 -.32 C1))) /\ (abs.32((C1 -.32 C2)) >u.32 C3))))))))] ; /* AndOrXor:1628-2*/ Or(icmp_ugt(a, b), icmp_eq(a, b)) -> icmp_uge(a, b); /* AndOrXor:1683-1*/ Or(icmp_uge(a, b), icmp_ne(a, b)) -> True; /* AndOrXor:1683-2*/ Or(icmp_eq(B, bv32"#x00000000"), icmp_ult(A, B)) -> icmp_uge(add(B, bv32"#xffffffff"), A); /* AndOrXor:1704*/ Or(icmp_eq(B, bv32"#x00000000"), icmp_ugt(B, A)) -> icmp_uge(add(B, bv32"#xffffffff"), A); /* AndOrXor:1705*/ Or(icmp_ne(A, bv32"#x00000000"), icmp_ne(B, bv32"#x00000000")) -> icmp_ne(Or(A, B), bv32"#x00000000"); /* AndOrXor:1733*/ Or(icmp_ult(add(X, C3), C1), icmp_eq(X, C2)) -> icmp_ule(add(X, C3), C1) [ ((C2 +.32 C3) =.32 C1)] ; /* AndOrXor:1740*/ Or(icmp_eq(X, C1), icmp_eq(X, C2)) -> icmp_eq(And(X, ~.32(CL0)), C1) [ (((C1 ^.32 C2) =.32 CL0) /\ ((C1 <u.32 C2) /\ isPowerOf2.32((C1 ^.32 C2))))] ; /* AndOrXor:1795*/ Or(icmp_eq(X, C1), icmp_eq(X, C2)) -> icmp_ult(add(X, neg.32(C1)), bv32"#x00000002") [ (C1 =.32 (C2 -.32 bv32"#x00000001"))] ; /* AndOrXor:1806*/ Or(icmp_eq(X, C1), icmp_ne(X, C2)) -> icmp_ne(X, C2) [ (C1 <u.32 C2)] ; /* AndOrXor:1818*/ Or(icmp_eq(X, C1), icmp_ult(X, C2)) -> icmp_ult(X, C2) [ (C1 <u.32 C2)] ; /* AndOrXor:1819*/ Or(icmp_eq(X, C1), icmp_slt(X, C2)) -> icmp_slt(X, C2) [ (C1 <s.32 C2)] ; /* AndOrXor:1820*/ Or(icmp_ne(X, C1), icmp_eq(X, C2)) -> icmp_ne(X, C1) [ (C1 <u.32 C2)] ; /* AndOrXor:1827*/ Or(icmp_ne(X, C1), icmp_ugt(X, C2)) -> icmp_ne(X, C1) [ (C1 <u.32 C2)] ; /* AndOrXor:1828*/ Or(icmp_ne(X, C1), icmp_sgt(X, C2)) -> icmp_ne(X, C1) [ (C1 <s.32 C2)] ; /* AndOrXor:1829*/ Or(icmp_ne(X, C1), icmp_ne(X, C2)) -> True [ (C1 <u.32 C2)] ; /* AndOrXor:1831*/ Or(icmp_ne(X, C1), icmp_ult(X, C2)) -> True [ (C1 <u.32 C2)] ; /* AndOrXor:1832*/ Or(icmp_ne(X, C1), icmp_slt(X, C2)) -> True [ (C1 <s.32 C2)] ; /* AndOrXor:1833*/ Or(icmp_ult(X, C1), icmp_ugt(X, C2)) -> icmp_ult(X, C1) [ ((C1 <u.32 C2) /\ (C2 =.32 bv32"#xffffffff"))] ; /* AndOrXor:1844*/ Or(icmp_ult(X, C1), icmp_ne(X, C2)) -> icmp_ne(X, C2) [ (C1 <u.32 C2)] ; /* AndOrXor:1849*/ Or(icmp_ult(X, C1), icmp_ult(X, C2)) -> icmp_ult(X, C2) [ (C1 <u.32 C2)] ; /* AndOrXor:1850*/ Or(icmp_slt(X, C1), icmp_sgt(X, C2)) -> icmp_slt(X, C1) [ ((C1 <s.32 C2) /\ (C2 =.32 (bv32"#x00000001" <<.32 (width.32(C2) -.32 bv32"#x00000001"))))] ; /* AndOrXor:1864*/ Or(icmp_slt(X, C1), icmp_ne(X, C2)) -> icmp_ne(X, C2) [ (C1 <s.32 C2)] ; /* AndOrXor:1869*/ Or(icmp_slt(X, C1), icmp_slt(X, C2)) -> icmp_slt(X, C2) [ (C1 <s.32 C2)] ; /* AndOrXor:1870*/ Or(icmp_ugt(X, C1), icmp_eq(X, C2)) -> icmp_ugt(X, C1) [ (C1 <u.32 C2)] ; /* AndOrXor:1879*/ Or(icmp_ugt(X, C1), icmp_ugt(X, C2)) -> icmp_ugt(X, C1) [ (C1 <u.32 C2)] ; /* AndOrXor:1880*/ Or(icmp_ugt(X, C1), icmp_ne(X, C2)) -> True [ (C1 <u.32 C2)] ; /* AndOrXor:1884*/ Or(icmp_ugt(X, C1), icmp_ult(X, C2)) -> True [ (C1 <u.32 C2)] ; /* AndOrXor:1885*/ Or(icmp_sgt(X, C1), icmp_eq(X, C2)) -> icmp_sgt(X, C1) [ (C1 <s.32 C2)] ; /* AndOrXor:1894*/ Or(icmp_sgt(X, C1), icmp_sgt(X, C2)) -> icmp_sgt(X, C1) [ (C1 <s.32 C2)] ; /* AndOrXor:1895*/ Or(icmp_sgt(X, C1), icmp_ne(X, C2)) -> True [ (C1 <s.32 C2)] ; /* AndOrXor:1899*/ Or(icmp_sgt(X, C1), icmp_slt(X, C2)) -> True [ (C1 <s.32 C2)] ; /* AndOrXor:1900*/ Or(And(Or(A, B), C1), And(B, C2)) -> Or(And(A, C1), B) [ ((C1 ^.32 C2) =.32 bv32"#xffffffff")] ; /* AndOrXor:1979*/ Or(And(Xor(A, B), C1), And(B, C2)) -> Xor(And(A, C1), B) [ ((C1 ^.32 C2) =.32 bv32"#xffffffff")] ; /* AndOrXor:2008*/ Or(And(x, C1), C) -> And(Or(x, C), CL0) [ (((C |.32 C1) =.32 CL0) /\ ((C &.32 C1) !=.32 bv32"#x00000000"))] ; /* AndOrXor:2052 (X & C1) | C2 --> (X | C2) & (C1|C2)*/ Or(Xor(x, C1), C) -> Xor(Or(x, C), CL0) [ ((C1 &.32 ~.32(C)) =.32 CL0)] ; /* AndOrXor:2063 (X ^ C1) | C2 --> (X | C2) ^ (C1 & ~C2)*/ Or(Xor(A, C1), op1) -> Xor(Or(A, op1), C1) [ MaskedValueIsZero.32(op1, C1)] ; /* AndOrXor:2095 (X^C)|Y -> (X|Y)^C iff Y&C == 0*/ Or(And(Xor(A, bv32"#xffffffff"), B), A) -> Or(A, B); /* AndOrXor:2113 ((~A & B) | A) -> (A | B)*/ Or(And(A, B), Xor(A, bv32"#xffffffff")) -> Or(Xor(A, bv32"#xffffffff"), B); /* AndOrXor:2118 ((A & B) | ~A) -> (~A | B)*/ Or(And(A, Xor(B, bv32"#xffffffff")), Xor(A, B)) -> Xor(A, B); /* AndOrXor:2123 (A & (~B)) | (A ^ B) -> (A ^ B)*/ Or(And(Or(B, V2), C1), And(B, C2)) -> And(Or(B, V2), CL0) [ (((C1 |.32 C2) =.32 CL0) /\ (((C1 &.32 C2) =.32 bv32"#x00000000") /\ MaskedValueIsZero.32(V2, ~.32(C1))))] ; /* AndOrXor:2142*/ Or(And(Or(V1, C3), C1), And(Or(V1, C4), C2)) -> And(Or(V1, CL0), CL1) [ (((C1 |.32 C2) =.32 CL1) /\ (((C3 |.32 C4) =.32 CL0) /\ (((C1 &.32 C2) =.32 bv32"#x00000000") /\ (((C3 &.32 ~.32(C1)) =.32 bv32"#x00000000") /\ ((C4 &.32 ~.32(C2)) =.32 bv32"#x00000000")))))] ; /* AndOrXor:2160*/ Or(And(A, Xor(D, bv32"#xffffffff")), And(Xor(A, bv32"#xffffffff"), D)) -> Xor(A, D); /* AndOrXor:2188*/ Or(Xor(A, B), Xor(Xor(B, C), A)) -> Or(Xor(A, B), C); /* AndOrXor:2231 (A ^ B) | ((B ^ C) ^ A) -> (A ^ B) | C*/ Or(And(Or(B, C), A), B) -> Or(B, And(A, C)); /* AndOrXor:2243 ((B | C) & A) | B -> B | (A & C)*/ Or(Xor(A, bv32"#xffffffff"), Xor(B, bv32"#xffffffff")) -> Xor(And(A, B), bv32"#xffffffff"); /* AndOrXor:2247 (~A | ~B) == (~(A & B))*/ Or(op0, Xor(op0, B)) -> Or(op0, B); /* AndOrXor:2263*/ Or(A, Xor(Xor(A, bv32"#xffffffff"), B)) -> Or(A, Xor(B, bv32"#xffffffff")); /* AndOrXor:2264*/ Or(And(A, B), Xor(A, B)) -> Or(A, B); /* AndOrXor:2265*/ Or(A, Xor(Or(A, B), bv32"#xffffffff")) -> Or(A, Xor(B, bv32"#xffffffff")); /* AndOrXor:2284*/ Or(A, Xor(Xor(A, B), bv32"#xffffffff")) -> Or(A, Xor(B, bv32"#xffffffff")); /* AndOrXor:2285*/ Or(And(A, B), Xor(Xor(A, bv32"#xffffffff"), B)) -> Xor(Xor(A, bv32"#xffffffff"), B); /* AndOrXor:2297*/ Or(zext(A), zext(B)) -> zext(Or(A, B)); /* AndOrXor:2321-1*/ Or(sext(A), sext(B)) -> sext(Or(A, B)); /* AndOrXor:2321-2*/ Or(trunc(A), trunc(B)) -> trunc(Or(A, B)); /* AndOrXor:2321-3*/ Or(sext_i1(A), op1) -> select(A, bv32"#xffffffff", op1); /* AndOrXor:2356*/ Or(Or(A, C1), op1) -> Or(Or(A, op1), C1); /* AndOrXor:2367*/ Or(select(x, A, B), select(x, C, D)) -> select(x, Or(A, C), Or(B, D)); /* AndOrXor:2375*/ Xor(And(Xor(nx, bv32"#xffffffff"), y), bv32"#xffffffff") -> Or(nx, Xor(y, bv32"#xffffffff")); /* AndOrXor:2416*/ Xor(Or(Xor(nx, bv32"#xffffffff"), y), bv32"#xffffffff") -> And(nx, Xor(y, bv32"#xffffffff")); /* AndOrXor:2417*/ Xor(And(x, y), bv32"#xffffffff") -> Or(Xor(x, bv32"#xffffffff"), Xor(y, bv32"#xffffffff")); /* AndOrXor:2429*/ Xor(Or(x, y), bv32"#xffffffff") -> And(Xor(x, bv32"#xffffffff"), Xor(y, bv32"#xffffffff")); /* AndOrXor:2430*/ Xor(ashr(Xor(x, bv32"#xffffffff"), y), bv32"#xffffffff") -> ashr(x, y); /* AndOrXor:2443*/ Xor(icmp_slt(x, y), bv32"#xffffffff") -> icmp_sge(x, y); /* AndOrXor:2453*/ Xor(CL0, bv32"#x00000001") -> zext(icmp_sge(x, y)) [ (zext.32(icmp_slt.32(x, y)) =.32 CL0)] ; /* AndOrXor:2459-1*/ Xor(CL0, bv32"#xffffffff") -> sext(icmp_sge(x, y)) [ (sext.32(icmp_slt.32(x, y)) =.32 CL0)] ; /* AndOrXor:2459-2*/ Xor(sub(C, x), bv32"#xffffffff") -> add(x, CL0) [ ((bv32"#xffffffff" -.32 C) =.32 CL0)] ; /* AndOrXor:2475*/ Xor(add(x, C), bv32"#xffffffff") -> sub(CL0, x) [ ((bv32"#xffffffff" -.32 C) =.32 CL0)] ; /* AndOrXor:2486*/ Xor(add(x, C), C1) -> add(x, CL0) [ (((C +.32 C1) =.32 CL0) /\ isSignBit.32(C1))] ; /* AndOrXor:2494*/ Xor(Or(x, C1), C2) -> Xor(x, CL0) [ (((C1 ^.32 C2) =.32 CL0) /\ MaskedValueIsZero.32(x, C1))] ; /* AndOrXor:2500*/ Xor(lshr(Xor(x, C1), C2), C3) -> Xor(lshr(x, C2), CL0) [ (((C1 >>u.32 C2) ^.32 C3) =.32 CL0)] ; /* AndOrXor:2515 ((X^C1) >> C2)^C3 -> (X>>C2) ^ ((C1>>C2)^C3)*/ Xor(Or(a, op1), op1) -> And(a, Xor(op1, bv32"#xffffffff")); /* AndOrXor:2581 (B|A)^B -> A & ~B*/ Xor(And(a, op1), op1) -> And(Xor(a, bv32"#xffffffff"), op1); /* AndOrXor:2587 (B&A)^A -> ~B & A*/ Xor(And(a, b), Or(a, b)) -> Xor(a, b); /* AndOrXor:2595*/ Xor(Or(a, Xor(b, bv32"#xffffffff")), Or(Xor(a, bv32"#xffffffff"), b)) -> Xor(a, b); /* AndOrXor:2607*/ Xor(And(a, Xor(b, bv32"#xffffffff")), And(Xor(a, bv32"#xffffffff"), b)) -> Xor(a, b); /* AndOrXor:2617*/ Xor(Xor(a, c), Or(a, b)) -> Xor(And(Xor(a, bv32"#xffffffff"), b), c); /* AndOrXor:2627*/ Xor(And(a, b), Xor(a, b)) -> Or(a, b); /* AndOrXor:2647*/ Xor(And(a, Xor(b, bv32"#xffffffff")), Xor(a, bv32"#xffffffff")) -> Xor(And(a, b), bv32"#xffffffff"); /* AndOrXor:2658*/ Xor(icmp_ule(a, b), icmp_ne(a, b)) -> icmp_uge(a, b); /* AndOrXor:2663*/ Xor(zext(a), zext(b)) -> zext(Xor(a, b)); /* AndOrXor:2681-1*/ Xor(sext(a), sext(b)) -> sext(Xor(a, b)); /* AndOrXor:2681-2*/ Xor(trunc(a), trunc(b)) -> trunc(Xor(a, b)); /* AndOrXor:2681-3*/ zext_11(X0) -> zext(X0); /**/ icmp_ugt(X0, X1) -> icmp(X0, X1); /**/ add_i29(X0, X1) -> add(X0, X1); /**/ sext_i1(X0) -> sext(X0); /**/ icmp_sgt(X0, X1) -> icmp(X0, X1); /**/ sext_11(X0) -> sext(X0); /**/ icmp_slt(X0, X1) -> icmp(X0, X1); /**/ icmp_ule(X0, X1) -> icmp(X0, X1); /**/ icmp_uge(X0, X1) -> icmp(X0, X1); /**/ trunc_11(X0) -> trunc(X0); /**/ icmp_eq(X0, X1) -> icmp(X0, X1); /**/ icmp_ne(X0, X1) -> icmp(X0, X1); /**/ icmp_sge(X0, X1) -> icmp(X0, X1); /**/ icmp_ult(X0, X1) -> icmp(X0, X1); /**/ NON-STANDARD IRREGULAR QUERY loops