21using System.Diagnostics;
36 get {
return Native.Z3_get_quantifier_num_bound(
Context.nCtx, NativeObject); }
49 for (uint i = 0; i < n; i++)
50 res[i] =
Symbol.Create(
Context, Native.Z3_get_quantifier_bound_name(
Context.nCtx, NativeObject, i));
65 for (uint i = 0; i < n; i++)
66 res[i] =
Sort.Create(
Context, Native.Z3_get_quantifier_bound_sort(
Context.nCtx, NativeObject, i));
79 return Expr.Create(
Context, Native.Z3_get_quantifier_body(
Context.nCtx, NativeObject));
95 : base(ctx, IntPtr.Zero)
97 Debug.Assert(ctx !=
null);
98 Debug.Assert(sorts !=
null);
99 Debug.Assert(names !=
null);
100 Debug.Assert(body !=
null);
101 Debug.Assert(sorts.Length == names.Length);
102 Debug.Assert(sorts.All(s => s !=
null));
103 Debug.Assert(names.All(n => n !=
null));
106 Context.CheckContextMatch(body);
108 if (sorts.Length != names.Length)
109 throw new Z3Exception(
"Number of sorts does not match number of names");
111 NativeObject = Native.Z3_mk_lambda(ctx.nCtx,
112 AST.ArrayLength(sorts),
AST.ArrayToNative(sorts),
113 Symbol.ArrayToNative(names),
118 internal Lambda(Context ctx,
Expr[] bound,
Expr body)
119 : base(ctx, IntPtr.Zero)
121 Debug.Assert(ctx !=
null);
122 Debug.Assert(body !=
null);
124 Debug.Assert(bound !=
null && bound.Length > 0 && bound.All(n => n !=
null));
126 Context.CheckContextMatch<
Expr>(bound);
127 Context.CheckContextMatch(body);
129 NativeObject = Native.Z3_mk_lambda_const(ctx.nCtx,
130 AST.ArrayLength(bound), AST.ArrayToNative(bound),
135 internal Lambda(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx !=
null); }
138 internal override void CheckNativeObject(IntPtr obj)
141 throw new Z3Exception(
"Underlying object is not a quantifier");
142 base.CheckNativeObject(obj);
The abstract syntax tree (AST) class.
The main interaction with Z3 happens via the Context.
Expr(Context ctx, IntPtr obj)
Constructor for Expr
uint NumBound
The number of bound variables.
Symbol[] BoundVariableNames
The symbols for the bound variables.
Sort[] BoundVariableSorts
The sorts of the bound variables.
Expr Body
The body of the lambda.
new Lambda Translate(Context ctx)
Translates (copies) the lambda to the Context ctx .
The Sort class implements type information for ASTs.
Symbols are used to name several term and type constructors.
The exception base class for error reporting from Z3
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.