Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
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.
 
Expr Nil [get]
 The empty list.
 
FuncDecl IsNilDecl [get]
 The declaration of the isNil function of this list sort.
 
FuncDecl ConsDecl [get]
 The declaration of the cons function of this list sort.
 
FuncDecl IsConsDecl [get]
 The declaration of the isCons function of this list sort.
 
FuncDecl HeadDecl [get]
 The declaration of the head function of this list sort.
 
FuncDecl TailDecl [get]
 The declaration of the tail function of this list sort.
 
- Properties inherited from Sort
new uint Id [get]
 Returns a unique identifier for the sort.
 
Z3_sort_kind SortKind [get]
 The kind of the sort.
 
Symbol Name [get]
 The name of the sort
 
- Properties inherited from AST
uint Id [get]
 A unique identifier for the AST (unique among all ASTs).
 
Z3_ast_kind ASTKind [get]
 The kind of the AST.
 
bool IsExpr [get]
 Indicates whether the AST is an Expr
 
bool IsVar [get]
 Indicates whether the AST is a BoundVariable
 
bool IsQuantifier [get]
 Indicates whether the AST is a Quantifier
 
bool IsSort [get]
 Indicates whether the AST is a Sort
 
bool IsFuncDecl [get]
 Indicates whether the AST is a FunctionDeclaration
 

Additional Inherited Members

- Public Member Functions inherited from Sort
override bool Equals (object o)
 Equality operator for objects of type Sort.
 
override int GetHashCode ()
 Hash code generation for Sorts
 
override string ToString ()
 A string representation of the sort.
 
- Static Public Member Functions inherited from Sort
static bool operator== (Sort a, Sort b)
 Comparison operator.
 
static bool operator!= (Sort a, Sort b)
 Comparison operator.
 
- Protected Member Functions inherited from Sort
 Sort (Context ctx)
 Sort constructor
 

Detailed Description

List sorts.

Definition at line 520 of file Sort.cs.

Property Documentation

FuncDecl ConsDecl
get

The declaration of the cons function of this list sort.

Definition at line 557 of file Sort.cs.

FuncDecl HeadDecl
get

The declaration of the head function of this list sort.

Definition at line 582 of file Sort.cs.

FuncDecl IsConsDecl
get

The declaration of the isCons function of this list sort.

Definition at line 570 of file Sort.cs.

FuncDecl IsNilDecl
get

The declaration of the isNil function of this list sort.

Definition at line 545 of file Sort.cs.

Expr Nil
get

The empty list.

Definition at line 533 of file Sort.cs.

FuncDecl NilDecl
get

The declaration of the nil function of this list sort.

Definition at line 525 of file Sort.cs.

FuncDecl TailDecl
get

The declaration of the tail function of this list sort.

Definition at line 594 of file Sort.cs.