| 2125 | } |
| 2126 | |
| 2127 | expr expr::mkIf(const expr &cond, const expr &then, const expr &els) { |
| 2128 | C2(cond, then, els); |
| 2129 | if (cond.isTrue() || then.eq(els)) |
| 2130 | return then; |
| 2131 | if (cond.isFalse()) |
| 2132 | return els; |
| 2133 | |
| 2134 | if (then.isTrue() || cond.eq(then)) |
| 2135 | return cond || els; |
| 2136 | if (then.isFalse()) |
| 2137 | return !cond && els; |
| 2138 | if (els.isTrue()) |
| 2139 | return !cond || then; |
| 2140 | if (els.isFalse()) |
| 2141 | return cond && then; |
| 2142 | |
| 2143 | expr notcond; |
| 2144 | if (cond.isNot(notcond)) |
| 2145 | return mkIf(notcond, els, then); |
| 2146 | |
| 2147 | expr lhs, rhs; |
| 2148 | // (ite (= x 1) 1 0) -> x |
| 2149 | // (ite (= x 1) 0 1) -> (not x) |
| 2150 | if (then.isBV() && then.bits() == 1 && cond.isEq(lhs, rhs) && |
| 2151 | lhs.isBV() && lhs.bits() == 1) { |
| 2152 | if (then.isOne() && els.isZero()) { |
| 2153 | if (lhs.isOne()) |
| 2154 | return rhs; |
| 2155 | if (rhs.isOne()) |
| 2156 | return lhs; |
| 2157 | } |
| 2158 | if (then.isZero() && els.isOne()) { |
| 2159 | if (lhs.isOne()) |
| 2160 | return ~rhs; |
| 2161 | if (rhs.isOne()) |
| 2162 | return ~lhs; |
| 2163 | } |
| 2164 | } |
| 2165 | |
| 2166 | // (ite c a (ite c2 a b)) -> (ite (or c c2) a b) |
| 2167 | expr cond2, then2, else2; |
| 2168 | if (els.isIf(cond2, then2, else2) && then.eq(then2)) |
| 2169 | return mkIf(cond || cond2, then, else2); |
| 2170 | |
| 2171 | return Z3_mk_ite(ctx(), cond(), then(), els()); |
| 2172 | } |
| 2173 | |
| 2174 | expr expr::mkForAll(const set<expr> &vars, expr &&val) { |
| 2175 | if (vars.empty() || val.isConst() || !val.isValid()) |