Sort

java.lang.Object

com.microsoft.z3.Z3Object

com.microsoft.z3.AST

com.microsoft.z3.Sort

All Implemented Interfaces:: Comparable<AST>

Direct Known Subclasses:: ArithSort, ArraySort, BitVecSort, BoolSort, CharSort, DatatypeSort, EnumSort, FiniteDomainSort, FPRMSort, FPSort, ListSort, RelationSort, ReSort, SeqSort, TupleSort, UninterpretedSort

public class Sort extends AST

The Sort class implements type information for ASTs.

Method Summary

Modifier and Type

Method

Description

boolean

equals(Object o)

Equality operator for objects of type Sort.

int

getId()

Returns a unique identifier for the sort.

Symbol

getName()

The name of the sort

Z3_sort_kind

getSortKind()

The kind of the sort.

int

hashCode()

Hash code generation for Sorts

String

toString()

A string representation of the sort.

Sort

translate(Context ctx)

Translates (copies) the sort to the Context ctx.

Methods inherited from class com.microsoft.z3.AST
compareTo, getASTKind, getSExpr, isApp, isExpr, isFuncDecl, isQuantifier, isSort, isVar

Methods inherited from class com.microsoft.z3.Z3Object
arrayLength, arrayToNative

Methods inherited from class java.lang.Object
clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Method Details
- equals
  
  public boolean equals(Object o)
  
  Equality operator for objects of type Sort.
  
  Overrides:
  
  equals in class AST
  
  Parameters:
  
  o - another AST
- hashCode
  
  public int hashCode()
  
  Hash code generation for Sorts
  
  Overrides:
  
  hashCode in class AST
  
  Returns:
  
  A hash code
- getId
  
  public int getId()
  
  Returns a unique identifier for the sort.
  
  Overrides:
  
  getId in class AST
- getSortKind
  
  public Z3_sort_kind getSortKind()
  
  The kind of the sort.
- getName
  
  public Symbol getName()
  
  The name of the sort
- toString
  
  public String toString()
  
  A string representation of the sort.
  
  Overrides:
  
  toString in class AST
- translate
  
  public Sort translate(Context ctx)
  
  Translates (copies) the sort to the Context ctx.
  
  Overrides:
  
  translate in class AST
  
  Parameters:
  
  ctx - A context
  
  Returns:
  
  A copy of the sort which is associated with ctx
  
  Throws:
  
  Z3Exception - on error