EnumSort Class Reference

Enumeration sorts. More...

Inheritance diagram for EnumSort:

Public Member Functions
FuncDecl	ConstDecl (uint inx)
	Retrieves the inx'th constant declaration in the enumeration.
Expr	Const (uint inx)
	Retrieves the inx'th constant in the enumeration.
FuncDecl	TesterDecl (uint inx)
	Retrieves the inx'th tester/recognizer declaration in the enumeration.
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.

Properties
FuncDecl[]	ConstDecls [get]
	The function declarations of the constants in the enumeration.
Expr[]	Consts [get]
	The constants in the enumeration.
FuncDecl[]	TesterDecls [get]
	The test predicates (recognizers) for the constants in the enumeration.
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
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

Enumeration sorts.

Definition at line 28 of file EnumSort.cs.

Member Function Documentation

Const()

Expr Const ( uint  inx )

inline

Retrieves the inx'th constant in the enumeration.

Parameters

inx

Returns

Definition at line 75 of file EnumSort.cs.

        {
            using var decl = ConstDecl(inx);
            return Context.MkApp(decl);
        }

ConstDecl()

FuncDecl ConstDecl ( uint  inx )

inline

Retrieves the inx'th constant declaration in the enumeration.

Parameters

inx

Returns

Definition at line 50 of file EnumSort.cs.

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

Referenced by EnumSort.Const().

TesterDecl()

FuncDecl TesterDecl ( uint  inx )

inline

Retrieves the inx'th tester/recognizer declaration in the enumeration.

Parameters

inx

Returns

Definition at line 101 of file EnumSort.cs.

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

Property Documentation

ConstDecls

FuncDecl [] ConstDecls

get

The function declarations of the constants in the enumeration.

Definition at line 33 of file EnumSort.cs.

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

Consts

Expr [] Consts

get

The constants in the enumeration.

Definition at line 58 of file EnumSort.cs.

        {
            get
            {
                FuncDecl[] cds = ConstDecls;
                Expr[] t = new Expr[cds.Length];
                for (uint i = 0; i < t.Length; i++)
                    t[i] = Context.MkApp(cds[i]);
                return t;
            }
        }

TesterDecls

FuncDecl [] TesterDecls

get

The test predicates (recognizers) for the constants in the enumeration.

Definition at line 84 of file EnumSort.cs.

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