Z3 |

Properties
ListSort Class Reference

List sorts. More...

Inheritance diagram for ListSort:

## Properties
FuncDecl | NilDecl`[get]`
| The declaration of the nil function of this list sort. More...
Expr | Nil`[get]`
| The empty list. More...
FuncDecl | IsNilDecl`[get]`
| The declaration of the isNil function of this list sort. More...
FuncDecl | ConsDecl`[get]`
| The declaration of the cons function of this list sort. More...
FuncDecl | IsConsDecl`[get]`
| The declaration of the isCons function of this list sort. More...
FuncDecl | HeadDecl`[get]`
| The declaration of the head function of this list sort. More...
FuncDecl | TailDecl`[get]`
| The declaration of the tail function of this list 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

List sorts.

Definition at line 28 of file ListSort.cs.

## Property Documentation

## ◆ ConsDecl

FuncDecl ConsDecl
| get

The declaration of the cons function of this list sort.

Definition at line 66 of file ListSort.cs.

67 {
68 get
69 {
70 return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, 1));
71 }
72 }

## ◆ HeadDecl

FuncDecl HeadDecl
| get

The declaration of the head function of this list sort.

Definition at line 89 of file ListSort.cs.

90 {
91 get
92 {
93 return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor_accessor(Context.nCtx, NativeObject, 1, 0));
94 }
95 }

## ◆ IsConsDecl

FuncDecl IsConsDecl
| get

The declaration of the isCons function of this list sort.

Definition at line 78 of file ListSort.cs.

79 {
80 get
81 {
82 return new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, 1));
83 }
84 }

## ◆ IsNilDecl

FuncDecl IsNilDecl
| get

The declaration of the isNil function of this list sort.

Definition at line 55 of file ListSort.cs.

56 {
57 get
58 {
59 return new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, 0));
60 }
61 }

## ◆ Nil

Expr Nil
| get

The empty list.

Definition at line 44 of file ListSort.cs.

45 {
46 get
47 {
48 return Context.MkApp(NilDecl);
49 }
50 }
Microsoft.Z3.Context.MkApp
Expr MkApp(FuncDecl f, params Expr[] args)
Create a new function application.
Definition: Context.cs:788
Microsoft.Z3.ListSort.NilDecl
FuncDecl NilDecl
The declaration of the nil function of this list sort.
Definition: ListSort.cs:34

## ◆ NilDecl

FuncDecl NilDecl
| get

The declaration of the nil function of this list sort.

Definition at line 33 of file ListSort.cs.

34 {
35 get
36 {
37 return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, 0));
38 }
39 }

## ◆ TailDecl

FuncDecl TailDecl
| get

The declaration of the tail function of this list sort.

Definition at line 100 of file ListSort.cs.

101 {
102 get
103 {
104 return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor_accessor(Context.nCtx, NativeObject, 1, 1));
105 }
106 }