TupleSort Class Reference

Tuple sorts. More...

Inheritance diagram for TupleSort:

Properties
FuncDecl	MkDecl [get]
	The constructor function of the tuple. More...
uint	NumFields [get]
	The number of fields in the tuple. More...
FuncDecl[]	FieldDecls [get]
	The field declarations. 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...
Properties inherited from Z3Object
Context	Context [get]
	Access Context object 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

Tuple sorts.

Definition at line 28 of file TupleSort.cs.

Property Documentation

FieldDecls

FuncDecl [] FieldDecls

get

The field declarations.

Definition at line 53 of file TupleSort.cs.

        {
            get
            {
 
                uint n = NumFields;
                FuncDecl[] res = new FuncDecl[n];
                for (uint i = 0; i < n; i++)
                    res[i] = new FuncDecl(Context, Native.Z3_get_tuple_sort_field_decl(Context.nCtx, NativeObject, i));
                return res;
            }
        }

MkDecl

FuncDecl MkDecl

get

The constructor function of the tuple.

Definition at line 33 of file TupleSort.cs.

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

NumFields

uint NumFields

get

The number of fields in the tuple.

Definition at line 45 of file TupleSort.cs.

        {
            get { return Native.Z3_get_tuple_sort_num_fields(Context.nCtx, NativeObject); }
        }