ExprIteEliminator { static <T extends Type> Expr<T> eliminateIte(final Expr<T> expr) { return removeIte(propagateIte(expr)); } private  ExprIteEliminator();   }
@Test public void testSimple() { assertEquals(eliminateIte(Ite(a, b, c)), And(Or(Not(a), b), Or(a, c))); assertEquals(eliminateIte(Ite(a, Ite(b, c, d), e)), And(Or(Not(a), And(Or(Not(b), c), Or(b, d))), Or(a, e))); }
@Test public void testUnary() { assertEquals(eliminateIte(Not(Ite(a, b, c))), Not(And(Or(Not(a), b), Or(a, c)))); }
@Test public void testBinary() { assertEquals(eliminateIte(Imply(a, Ite(b, c, d))), Imply(a, And(Or(Not(b), c), Or(b, d)))); assertEquals(eliminateIte(Imply(Ite(b, c, d), a)), Imply(And(Or(Not(b), c), Or(b, d)), a)); assertEquals(eliminateIte(Iff(a, Ite(b, c, d))), Iff(a, And(Or(Not(b), c), Or(b, d)))); assertEquals(eliminateIte(Eq(x, Ite(a, y, z))), And(Or(Not(a), Eq(x, y)), Or(a, Eq(x, z)))); assertEquals(eliminateIte(Eq(Ite(a, y, z), x)), And(Or(Not(a), Eq(y, x)), Or(a, Eq(z, x)))); assertEquals(eliminateIte(Eq(x, Ite(a, Ite(b, y, z), t))), And(Or(Not(a), And(Or(Not(b), Eq(x, y)), Or(b, Eq(x, z)))), Or(a, Eq(x, t)))); assertEquals(eliminateIte(Eq(Ite(a, Ite(b, y, z), t), x)), And(Or(Not(a), And(Or(Not(b), Eq(y, x)), Or(b, Eq(z, x)))), Or(a, Eq(t, x)))); assertEquals(eliminateIte(Eq(Ite(a, x, y), Ite(b, z, t))), And(Or(Not(a), And(Or(Not(b), Eq(x, z)), Or(b, Eq(x, t)))), Or(a, And(Or(Not(b), Eq(y, z)), Or(b, Eq(y, t)))))); }
@Test public void testMultiary() { assertEquals(eliminateIte(Or(a, b, Ite(c, d, e))), Or(a, b, And(Or(Not(c), d), Or(c, e)))); assertEquals(eliminateIte(Eq(i1, Add(i2, Ite(a, i3, i4), i5))), And(Or(Not(a), Eq(i1, Add(i2, i3, i5))), Or(a, Eq(i1, Add(i2, i4, i5))))); assertEquals(eliminateIte(Eq(i1, Add(i2, Ite(a, i3, i4), Ite(b, x, y)))), And(Or(Not(a), And(Or(Not(b), Eq(i1, Add(i2, i3, x))), Or(b, Eq(i1, Add(i2, i3, y))))), Or(a, And(Or(Not(b), Eq(i1, Add(i2, i4, x))), Or(b, Eq(i1, Add(i2, i4, y))))))); }
@Test public void testNothingHappening() { final List<Expr<BoolType>> expressions = new ArrayList<>(); expressions.add(And(a, b, d)); expressions.add(Eq(x, Neg(y))); expressions.add(Geq(Sub(x, y), Add(x, z, t))); for (final Expr<BoolType> expr : expressions) { assertEquals(expr, eliminateIte(expr)); } }
@Test public void testPrime() { assertEquals(eliminateIte(Eq(z, Prime(Ite(a, x, y)))), And(Or(Not(a), Eq(z, Prime(x))), Or(a, Eq(z, Prime(y))))); }