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	IsApp [get]
	Indicates whether the AST is an application.
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.
Properties inherited from Z3Object
Context	Context [get]
	Access Context object.

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.
new Sort	Translate (Context ctx)
	Translates (copies) the sort to the Context ctx .
Public Member Functions inherited from AST
override bool	Equals (object o)
	Object comparison.
virtual int	CompareTo (object other)
	Object Comparison.
override int	GetHashCode ()
	The AST's hash code.
AST	Translate (Context ctx)
	Translates (copies) the AST to the Context ctx .
override string	ToString ()
	A string representation of the AST.
string	SExpr ()
	A string representation of the AST in s-expression notation.
Public Member Functions inherited from Z3Object
void	Dispose ()
	Disposes of the underlying native Z3 object.
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.
Static Public Member Functions inherited from AST
static bool	operator== (AST a, AST b)
	Comparison operator.
static bool	operator!= (AST a, AST b)
	Comparison operator.

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.

        {
            get
            {
                return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, 1));
            }
        }

HeadDecl

FuncDecl HeadDecl

get

The declaration of the head function of this list sort.

Definition at line 89 of file ListSort.cs.

        {
            get
            {
                return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor_accessor(Context.nCtx, NativeObject, 1, 0));
            }
        }

IsConsDecl

FuncDecl IsConsDecl

get

The declaration of the isCons function of this list sort.

Definition at line 78 of file ListSort.cs.

        {
            get
            {
                return new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, 1));
            }
        }

IsNilDecl

FuncDecl IsNilDecl

get

The declaration of the isNil function of this list sort.

Definition at line 55 of file ListSort.cs.

        {
            get
            {
                return new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, 0));
            }
        }

Nil

Expr Nil

get

The empty list.

Definition at line 44 of file ListSort.cs.

        {
            get
            {
                return Context.MkApp(NilDecl);
            }
        }

NilDecl

FuncDecl NilDecl

get

The declaration of the nil function of this list sort.

Definition at line 33 of file ListSort.cs.

        {
            get
            {
                return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, 0));                                
            }
        }

TailDecl

FuncDecl TailDecl

get

The declaration of the tail function of this list sort.

Definition at line 100 of file ListSort.cs.

        {
            get
            {
                return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor_accessor(Context.nCtx, NativeObject, 1, 1));
            }
        }