Z3
Data Structures | Public Member Functions | Static Public Member Functions | Data Fields
Z3_sort_kind Enum Reference

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_UNINTERPRETED_SORT =(0)
 
 Z3_BOOL_SORT =(1)
 
 Z3_INT_SORT =(2)
 
 Z3_REAL_SORT =(3)
 
 Z3_BV_SORT =(4)
 
 Z3_ARRAY_SORT =(5)
 
 Z3_DATATYPE_SORT =(6)
 
 Z3_RELATION_SORT =(7)
 
 Z3_FINITE_DOMAIN_SORT =(8)
 
 Z3_FLOATING_POINT_SORT =(9)
 
 Z3_ROUNDING_MODE_SORT =(10)
 
 Z3_SEQ_SORT =(11)
 
 Z3_RE_SORT =(12)
 
 Z3_UNKNOWN_SORT =(1000)
 

Detailed Description

Z3_sort_kind

Definition at line 13 of file Z3_sort_kind.java.

Constructor & Destructor Documentation

§ Z3_sort_kind()

Z3_sort_kind ( int  v)
inline

Definition at line 31 of file Z3_sort_kind.java.

31  {
32  this.intValue = v;
33  }

Member Function Documentation

§ fromInt()

static final Z3_sort_kind fromInt ( int  v)
inlinestatic

Definition at line 45 of file Z3_sort_kind.java.

Referenced by Expr.Expr(), Model.getFuncInterp(), Sort.getSortKind(), Expr.isArray(), and Sort.toString().

45  {
46  Z3_sort_kind k = Z3_sort_kind_MappingHolder.intMapping.get(v);
47  if (k != null) return k;
48  throw new IllegalArgumentException("Illegal value " + v + " for Z3_sort_kind");
49  }
Z3_sort_kind
The different kinds of Z3 types (See #Z3_get_sort_kind).
Definition: z3_api.h:153

§ toInt()

final int toInt ( )
inline

Definition at line 51 of file Z3_sort_kind.java.

51 { return this.intValue; }

Field Documentation

§ Z3_ARRAY_SORT

Z3_ARRAY_SORT =(5)

Definition at line 19 of file Z3_sort_kind.java.

Referenced by Model.getConstInterp(), Model.getFuncInterp(), and Expr.isArray().

§ Z3_BOOL_SORT

Z3_BOOL_SORT =(1)

Definition at line 15 of file Z3_sort_kind.java.

§ Z3_BV_SORT

Z3_BV_SORT =(4)

Definition at line 18 of file Z3_sort_kind.java.

Referenced by Expr.isBV().

§ Z3_DATATYPE_SORT

Z3_DATATYPE_SORT =(6)

Definition at line 20 of file Z3_sort_kind.java.

§ Z3_FINITE_DOMAIN_SORT

Z3_FINITE_DOMAIN_SORT =(8)

Definition at line 22 of file Z3_sort_kind.java.

Referenced by Expr.isFiniteDomain().

§ Z3_FLOATING_POINT_SORT

Z3_FLOATING_POINT_SORT =(9)

Definition at line 23 of file Z3_sort_kind.java.

§ Z3_INT_SORT

Z3_INT_SORT =(2)

Definition at line 16 of file Z3_sort_kind.java.

Referenced by Expr.isInt().

§ Z3_RE_SORT

Z3_RE_SORT =(12)

Definition at line 26 of file Z3_sort_kind.java.

§ Z3_REAL_SORT

Z3_REAL_SORT =(3)

Definition at line 17 of file Z3_sort_kind.java.

Referenced by Expr.isReal().

§ Z3_RELATION_SORT

Z3_RELATION_SORT =(7)

Definition at line 21 of file Z3_sort_kind.java.

Referenced by Expr.isRelation().

§ Z3_ROUNDING_MODE_SORT

Z3_ROUNDING_MODE_SORT =(10)

Definition at line 24 of file Z3_sort_kind.java.

§ Z3_SEQ_SORT

Z3_SEQ_SORT =(11)

Definition at line 25 of file Z3_sort_kind.java.

§ Z3_UNINTERPRETED_SORT

Z3_UNINTERPRETED_SORT =(0)

Definition at line 14 of file Z3_sort_kind.java.

§ Z3_UNKNOWN_SORT

Z3_UNKNOWN_SORT =(1000)

Definition at line 27 of file Z3_sort_kind.java.