Method getSorts

src/api/java/Model.java:251–260

The uninterpreted sorts that the model has an interpretation for. Remarks: Z3 also provides an interpretation for uninterpreted sorts used in a formula. The interpretation for a sort is a finite set of distinct values. We say this finite set is the "universe" of the sort. @see #getNumSorts @see #g

()

     * @throws Z3Exception
     **/
    public Sort[] getSorts()
    {

        int n = getNumSorts();
        Sort[] res = new Sort[n];
        for (int i = 0; i < n; i++)
            res[i] = Sort.create(getContext(),
                    Native.modelGetSort(getContext().nCtx(), getNativeObject(), i));
        return res;
    }

    /**
     * The finite set of distinct values that represent the interpretation for