Z3
Lambda.cs
Go to the documentation of this file.
1/*++
2Copyright (c) 2017 Microsoft Corporation
3
4Module Name:
5
6 Lambda.cs
7
8Abstract:
9
10 Z3 Managed API: Lambda
11
12Author:
13
14 Christoph Wintersteiger (cwinter) 2012-03-19
15
16Notes:
17
18--*/
19
20using System;
21using System.Diagnostics;
22using System.Linq;
23
24namespace Microsoft.Z3
25{
29 public class Lambda : ArrayExpr
30 {
34 public uint NumBound
35 {
36 get { return Native.Z3_get_quantifier_num_bound(Context.nCtx, NativeObject); }
37 }
38
43 {
44 get
45 {
46
47 uint n = NumBound;
48 Symbol[] res = new Symbol[n];
49 for (uint i = 0; i < n; i++)
50 res[i] = Symbol.Create(Context, Native.Z3_get_quantifier_bound_name(Context.nCtx, NativeObject, i));
51 return res;
52 }
53 }
54
59 {
60 get
61 {
62
63 uint n = NumBound;
64 Sort[] res = new Sort[n];
65 for (uint i = 0; i < n; i++)
66 res[i] = Sort.Create(Context, Native.Z3_get_quantifier_bound_sort(Context.nCtx, NativeObject, i));
67 return res;
68 }
69 }
70
74 public Expr Body
75 {
76 get
77 {
78
79 return Expr.Create(Context, Native.Z3_get_quantifier_body(Context.nCtx, NativeObject));
80 }
81 }
82
88 new public Lambda Translate(Context ctx)
89 {
90 return (Lambda)base.Translate(ctx);
91 }
92
93 #region Internal
94 internal Lambda(Context ctx, Sort[] sorts, Symbol[] names, Expr body)
95 : base(ctx, IntPtr.Zero)
96 {
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));
104 Context.CheckContextMatch<Sort>(sorts);
105 Context.CheckContextMatch<Symbol>(names);
106 Context.CheckContextMatch(body);
107
108 if (sorts.Length != names.Length)
109 throw new Z3Exception("Number of sorts does not match number of names");
110
111 NativeObject = Native.Z3_mk_lambda(ctx.nCtx,
112 AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
113 Symbol.ArrayToNative(names),
114 body.NativeObject);
115
116 }
117
118 internal Lambda(Context ctx, Expr[] bound, Expr body)
119 : base(ctx, IntPtr.Zero)
120 {
121 Debug.Assert(ctx != null);
122 Debug.Assert(body != null);
123
124 Debug.Assert(bound != null && bound.Length > 0 && bound.All(n => n != null));
125
126 Context.CheckContextMatch<Expr>(bound);
127 Context.CheckContextMatch(body);
128
129 NativeObject = Native.Z3_mk_lambda_const(ctx.nCtx,
130 AST.ArrayLength(bound), AST.ArrayToNative(bound),
131 body.NativeObject);
132 }
133
134
135 internal Lambda(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
136
137#if DEBUG
138 internal override void CheckNativeObject(IntPtr obj)
139 {
140 if ((Z3_ast_kind)Native.Z3_get_ast_kind(Context.nCtx, obj) != Z3_ast_kind.Z3_QUANTIFIER_AST)
141 throw new Z3Exception("Underlying object is not a quantifier");
142 base.CheckNativeObject(obj);
143 }
144#endif
145 #endregion
146 }
147}
The abstract syntax tree (AST) class.
Definition: AST.cs:31
Array expressions
Definition: ArrayExpr.cs:32
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Expressions are terms.
Definition: Expr.cs:31
Expr(Context ctx, IntPtr obj)
Constructor for Expr
Definition: Expr.cs:1821
Lambda expressions.
Definition: Lambda.cs:30
uint NumBound
The number of bound variables.
Definition: Lambda.cs:35
Symbol[] BoundVariableNames
The symbols for the bound variables.
Definition: Lambda.cs:43
Sort[] BoundVariableSorts
The sorts of the bound variables.
Definition: Lambda.cs:59
Expr Body
The body of the lambda.
Definition: Lambda.cs:75
new Lambda Translate(Context ctx)
Translates (copies) the lambda to the Context ctx .
Definition: Lambda.cs:88
The Sort class implements type information for ASTs.
Definition: Sort.cs:29
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:32
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition: z3_api.h:180