Z3 |

Properties
RelationSort Class Reference

Relation sorts. More...

Inheritance diagram for RelationSort:

## Properties
uint | Arity`[get]`
| The arity of the relation sort. More...
Sort[] | ColumnSorts`[get]`
| The sorts of the columns of the relation sort. More...
Properties inherited from Sort
new uint | Id`[get]`
| Returns a unique identifier for the sort. More...
Z3_sort_kind | SortKind`[get]`
| The kind of the sort. More...
Symbol | Name`[get]`
| The name of the sort More...
Properties inherited from AST
uint | Id`[get]`
| A unique identifier for the AST (unique among all ASTs). More...
Z3_ast_kind | ASTKind`[get]`
| The kind of the AST. More...
bool | IsExpr`[get]`
| Indicates whether the AST is an Expr More...
bool | IsApp`[get]`
| Indicates whether the AST is an application More...
bool | IsVar`[get]`
| Indicates whether the AST is a BoundVariable More...
bool | IsQuantifier`[get]`
| Indicates whether the AST is a Quantifier More...
bool | IsSort`[get]`
| Indicates whether the AST is a Sort More...
bool | IsFuncDecl`[get]`
| Indicates whether the AST is a FunctionDeclaration More...

## Additional Inherited Members
Public Member Functions inherited from Sort
override bool | Equals (object o)
| Equality operator for objects of type Sort. More...
override int | GetHashCode ()
| Hash code generation for Sorts More...
override string | ToString ()
| A string representation of the sort. More...
new Sort | Translate (Context ctx)
| Translates (copies) the sort to the Context ctx . More...
Public Member Functions inherited from AST
override bool | Equals (object o)
| Object comparison. More...
virtual int | CompareTo (object other)
| Object Comparison. More...
override int | GetHashCode ()
| The AST's hash code. More...
AST | Translate (Context ctx)
| Translates (copies) the AST to the Context ctx . More...
override string | ToString ()
| A string representation of the AST. More...
string | SExpr ()
| A string representation of the AST in s-expression notation. More...
Public Member Functions inherited from Z3Object
void | Dispose ()
| Disposes of the underlying native Z3 object. More...
Static Public Member Functions inherited from Sort
static bool | operator== (Sort a, Sort b)
| Comparison operator. More...
static bool | operator!= (Sort a, Sort b)
| Comparison operator. More...
Static Public Member Functions inherited from AST
static bool | operator== (AST a, AST b)
| Comparison operator. More...
static bool | operator!= (AST a, AST b)
| Comparison operator. More...

## Detailed Description

Relation sorts.

Definition at line 28 of file RelationSort.cs.

## Property Documentation

## ◆ Arity

uint Arity
| get

The arity of the relation sort.

Definition at line 33 of file RelationSort.cs.

34 {
35 get { return Native.Z3_get_relation_arity(Context.nCtx, NativeObject); }
36 }

## ◆ ColumnSorts

Sort [] ColumnSorts
| get

The sorts of the columns of the relation sort.

Definition at line 41 of file RelationSort.cs.

42 {
43 get
44 {
45
46 if (m_columnSorts != null)
47 return m_columnSorts;
48
49 uint n = Arity;
50 Sort[] res = new Sort[n];
51 for (uint i = 0; i < n; i++)
52 res[i] = Sort.Create(Context, Native.Z3_get_relation_column(Context.nCtx, NativeObject, i));
53 return res;
54 }
55 }
Microsoft.Z3.RelationSort.Arity
uint Arity
The arity of the relation sort.
Definition: RelationSort.cs:34