Method mkITE

src/api/java/Context.java:915–922

Create an expression representing an if-then-else: ite(t1, t2, t3). @param t1 An expression with Boolean sort @param t2 An expression @param t3 An expression with the same sort as t2

(Expr<BoolSort> t1, Expr<? extends R> t2, Expr<? extends R> t3)

     * @param t3 An expression with the same sort as {@code t2}
     **/
    public final <R extends Sort> Expr<R> mkITE(Expr<BoolSort> t1, Expr<? extends R> t2, Expr<? extends R> t3)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        checkContextMatch(t3);
        return (Expr<R>) Expr.create(this, Native.mkIte(nCtx(), t1.getNativeObject(),
                t2.getNativeObject(), t3.getNativeObject()));
    }

    /**
     * Create an expression representing {@code t1 iff t2}.