Method eval

src/api/java/Model.java:211–219

Evaluates the expression t in the current model. Remarks: This function may fail if t contains quantifiers, is partial (MODEL_PARTIAL enabled), or if t is not well-sorted. In this case a ModelEvaluationFailedException is thrown. @param t the expression to evaluate @p

(Expr<R> t, boolean completion)

     * @throws Z3Exception
     **/
    public <R extends Sort> Expr<R> eval(Expr<R> t, boolean completion)
    {
        Native.LongPtr v = new Native.LongPtr();
        if (!Native.modelEval(getContext().nCtx(), getNativeObject(),
            t.getNativeObject(), (completion), v))
            throw new ModelEvaluationFailedException();
        else
            return (Expr<R>) Expr.create(getContext(), v.value);
    }

    /**
     * Alias for {@code Eval}.