21 using System.Diagnostics.Contracts;
28 [ContractVerification(
true)]
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);
111 Contract.Ensures(Contract.Result<
FuncDecl>() != null);
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;
129 ref inil, ref iisnil, ref icons, ref iiscons, ref ihead, ref itail);
static Z3_sort Z3_mk_list_sort(Z3_context a0, IntPtr a1, Z3_sort a2, [In, Out] ref Z3_func_decl a3, [In, Out] ref Z3_func_decl a4, [In, Out] ref Z3_func_decl a5, [In, Out] ref Z3_func_decl a6, [In, Out] ref Z3_func_decl a7, [In, Out] ref Z3_func_decl a8)
Expr MkApp(FuncDecl f, params Expr[] args)
Create a new function application.
static Z3_func_decl Z3_get_datatype_sort_recognizer(Z3_context a0, Z3_sort a1, uint a2)
The main interaction with Z3 happens via the Context.
The Sort class implements type information for ASTs.
static Z3_func_decl Z3_get_datatype_sort_constructor(Z3_context a0, Z3_sort a1, uint a2)
Symbols are used to name several term and type constructors.
static Z3_func_decl Z3_get_datatype_sort_constructor_accessor(Z3_context a0, Z3_sort a1, uint a2, uint a3)