20using System.Diagnostics;
37 uint n = Native.Z3_get_datatype_sort_num_constructors(
Context.nCtx, NativeObject);
39 for (uint i = 0; i < n; i++)
64 for (uint i = 0; i < t.Length; i++)
87 uint n = Native.Z3_get_datatype_sort_num_constructors(
Context.nCtx, NativeObject);
89 for (uint i = 0; i < n; i++)
107 : base(ctx, IntPtr.Zero)
109 Debug.Assert(ctx !=
null);
110 Debug.Assert(name !=
null);
111 Debug.Assert(enumNames !=
null);
113 int n = enumNames.Length;
114 IntPtr[] n_constdecls =
new IntPtr[n];
115 IntPtr[] n_testers =
new IntPtr[n];
116 NativeObject = Native.Z3_mk_enumeration_sort(ctx.nCtx, name.NativeObject, (uint)n,
117 Symbol.ArrayToNative(enumNames), n_constdecls, n_testers);
The main interaction with Z3 happens via the Context.
Expr MkApp(FuncDecl f, params Expr[] args)
Create a new function application.
FuncDecl TesterDecl(uint inx)
Retrieves the inx'th tester/recognizer declaration in the enumeration.
Expr[] Consts
The constants in the enumeration.
FuncDecl ConstDecl(uint inx)
Retrieves the inx'th constant declaration in the enumeration.
FuncDecl[] ConstDecls
The function declarations of the constants in the enumeration.
FuncDecl[] TesterDecls
The test predicates (recognizers) for the constants in the enumeration.
Expr Const(uint inx)
Retrieves the inx'th constant in the enumeration.
The Sort class implements type information for ASTs.
Symbols are used to name several term and type constructors.