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

Properties

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

- 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

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.

76  {
77  return Context.MkApp(ConstDecl(inx));
78  }

◆ 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.

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

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 100 of file EnumSort.cs.

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

Property Documentation

◆ ConstDecls

FuncDecl [] ConstDecls
get

The function declarations of the constants in the enumeration.

Definition at line 34 of file EnumSort.cs.

34  {
35  get
36  {
37  uint n = Native.Z3_get_datatype_sort_num_constructors(Context.nCtx, NativeObject);
38  FuncDecl[] t = new FuncDecl[n];
39  for (uint i = 0; i < n; i++)
40  t[i] = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, i));
41  return t;
42  }
43  }

◆ Consts

Expr [] Consts
get

The constants in the enumeration.

Definition at line 59 of file EnumSort.cs.

59  {
60  get
61  {
62  FuncDecl[] cds = ConstDecls;
63  Expr[] t = new Expr[cds.Length];
64  for (uint i = 0; i < t.Length; i++)
65  t[i] = Context.MkApp(cds[i]);
66  return t;
67  }
68  }

◆ TesterDecls

FuncDecl [] TesterDecls
get

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

Definition at line 84 of file EnumSort.cs.

84  {
85  get
86  {
87  uint n = Native.Z3_get_datatype_sort_num_constructors(Context.nCtx, NativeObject);
88  FuncDecl[] t = new FuncDecl[n];
89  for (uint i = 0; i < n; i++)
90  t[i] = new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, i));
91  return t;
92  }
93  }
Microsoft.Z3.EnumSort.ConstDecl
FuncDecl ConstDecl(uint inx)
Retrieves the inx'th constant declaration in the enumeration.
Definition: EnumSort.cs:50
Microsoft.Z3.Context.MkApp
Expr MkApp(FuncDecl f, params Expr[] args)
Create a new function application.
Definition: Context.cs:788
Microsoft.Z3.EnumSort.ConstDecls
FuncDecl[] ConstDecls
The function declarations of the constants in the enumeration.
Definition: EnumSort.cs:34