38 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
50 Contract.Ensures(Contract.Result<
Expr>() != null);
62 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
74 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
87 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
99 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
100 return new FuncDecl(
Context, Native.Z3_get_datatype_sort_constructor_accessor(
Context.nCtx, NativeObject, 1, 0));
111 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
112 return new FuncDecl(
Context, Native.Z3_get_datatype_sort_constructor_accessor(
Context.nCtx, NativeObject, 1, 1));
118 : base(ctx, IntPtr.Zero)
120 Contract.Requires(ctx != null);
121 Contract.Requires(name != null);
122 Contract.Requires(elemSort != null);
124 IntPtr inil = IntPtr.Zero, iisnil = IntPtr.Zero,
125 icons = IntPtr.Zero, iiscons = IntPtr.Zero,
126 ihead = IntPtr.Zero, itail = IntPtr.Zero;
128 NativeObject = Native.Z3_mk_list_sort(ctx.nCtx, name.NativeObject, elemSort.NativeObject,
129 ref inil, ref iisnil, ref icons, ref iiscons, ref ihead, ref itail);
Expr MkApp(FuncDecl f, params Expr[] args)
Create a new function application.
The main interaction with Z3 happens via the Context.
The Sort class implements type information for ASTs.
Symbols are used to name several term and type constructors.