Method mkFPRoundingModeSort

src/api/java/Context.java:3633–3636

Create the floating-point RoundingMode sort. @throws Z3Exception

()

     * @throws Z3Exception
     **/
    public FPRMSort mkFPRoundingModeSort()
    {
        return new FPRMSort(this);
    }

    /**
     * Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.