Public Member Functions | |
Z3_sort_kind (int v) | |
final int | toInt () |
Static Public Member Functions | |
static final Z3_sort_kind | fromInt (int v) |
Data Fields | |
Z3_BV_SORT =(4) | |
Z3_FINITE_DOMAIN_SORT =(8) | |
Z3_ARRAY_SORT =(5) | |
Z3_UNKNOWN_SORT =(1000) | |
Z3_RELATION_SORT =(7) | |
Z3_REAL_SORT =(3) | |
Z3_INT_SORT =(2) | |
Z3_FLOATING_POINT_SORT =(9) | |
Z3_ROUNDING_MODE_SORT =(10) | |
Z3_UNINTERPRETED_SORT =(0) | |
Z3_BOOL_SORT =(1) | |
Z3_DATATYPE_SORT =(6) | |
Definition at line 10 of file Z3_sort_kind.java.
|
inline |
Definition at line 26 of file Z3_sort_kind.java.
|
inlinestatic |
Definition at line 30 of file Z3_sort_kind.java.
Referenced by Expr.Expr(), Model.getFuncInterp(), Sort.getSortKind(), Expr.isArray(), and Sort.toString().
|
inline |
Definition at line 36 of file Z3_sort_kind.java.
Z3_ARRAY_SORT =(5) |
Definition at line 13 of file Z3_sort_kind.java.
Referenced by Model.getConstInterp(), Model.getFuncInterp(), and Expr.isArray().
Z3_BOOL_SORT =(1) |
Definition at line 21 of file Z3_sort_kind.java.
Z3_BV_SORT =(4) |
Definition at line 11 of file Z3_sort_kind.java.
Referenced by Expr.isBV().
Z3_DATATYPE_SORT =(6) |
Definition at line 22 of file Z3_sort_kind.java.
Z3_FINITE_DOMAIN_SORT =(8) |
Definition at line 12 of file Z3_sort_kind.java.
Referenced by Expr.isFiniteDomain().
Z3_FLOATING_POINT_SORT =(9) |
Definition at line 18 of file Z3_sort_kind.java.
Z3_INT_SORT =(2) |
Definition at line 17 of file Z3_sort_kind.java.
Referenced by Expr.isInt().
Z3_REAL_SORT =(3) |
Definition at line 16 of file Z3_sort_kind.java.
Referenced by Expr.isReal().
Z3_RELATION_SORT =(7) |
Definition at line 15 of file Z3_sort_kind.java.
Referenced by Expr.isRelation().
Z3_ROUNDING_MODE_SORT =(10) |
Definition at line 19 of file Z3_sort_kind.java.
Z3_UNINTERPRETED_SORT =(0) |
Definition at line 20 of file Z3_sort_kind.java.
Z3_UNKNOWN_SORT =(1000) |
Definition at line 14 of file Z3_sort_kind.java.