20using System.Diagnostics;
93 return new FuncDecl(
Context, Native.Z3_get_datatype_sort_constructor_accessor(
Context.nCtx, NativeObject, 1, 0));
104 return new FuncDecl(
Context, Native.Z3_get_datatype_sort_constructor_accessor(
Context.nCtx, NativeObject, 1, 1));
110 : base(ctx, IntPtr.Zero)
112 Debug.Assert(ctx !=
null);
113 Debug.Assert(name !=
null);
114 Debug.Assert(elemSort !=
null);
116 IntPtr inil = IntPtr.Zero, iisnil = IntPtr.Zero,
117 icons = IntPtr.Zero, iiscons = IntPtr.Zero,
118 ihead = IntPtr.Zero, itail = IntPtr.Zero;
120 NativeObject = Native.Z3_mk_list_sort(ctx.nCtx, name.NativeObject, elemSort.NativeObject,
121 ref inil, ref iisnil, ref icons, ref iiscons, ref ihead, ref itail);
The main interaction with Z3 happens via the Context.
Expr MkApp(FuncDecl f, params Expr[] args)
Create a new function application.
FuncDecl HeadDecl
The declaration of the head function of this list sort.
FuncDecl IsConsDecl
The declaration of the isCons function of this list sort.
FuncDecl NilDecl
The declaration of the nil function of this list sort.
FuncDecl TailDecl
The declaration of the tail function of this list sort.
FuncDecl IsNilDecl
The declaration of the isNil function of this list sort.
FuncDecl ConsDecl
The declaration of the cons function of this list sort.
The Sort class implements type information for ASTs.
Symbols are used to name several term and type constructors.