Z3
Public Member Functions | Static Public Member Functions
Lambda< R extends Sort > Class Template Reference
+ Inheritance diagram for Lambda< R extends Sort >:

Public Member Functions

int getNumBound ()
 
Symbol[] getBoundVariableNames ()
 
Sort[] getBoundVariableSorts ()
 
Expr< R > getBody ()
 
Lambda< R > translate (Context ctx)
 

Static Public Member Functions

static< R extends Sort > Lambda< R > of (Context ctx, Sort[] sorts, Symbol[] names, Expr< R > body)
 
static< R extends Sort > Lambda< R > of (Context ctx, Expr<?>[] bound, Expr< R > body)
 

Detailed Description

Lambda expressions.

Definition at line 26 of file Lambda.java.

Member Function Documentation

◆ getBody()

Expr< R > getBody ( )
inline

The body of the quantifier.

Exceptions
Z3Exception

Definition at line 73 of file Lambda.java.

74 {
75 return (Expr<R>) Expr.create(getContext(), Native.getQuantifierBody(getContext()
76 .nCtx(), getNativeObject()));
77 }

◆ getBoundVariableNames()

Symbol[] getBoundVariableNames ( )
inline

The symbols for the bound variables.

Exceptions
Z3Exception

Definition at line 42 of file Lambda.java.

43 {
44 int n = getNumBound();
45 Symbol[] res = new Symbol[n];
46 for (int i = 0; i < n; i++)
47 res[i] = Symbol.create(getContext(), Native.getQuantifierBoundName(
48 getContext().nCtx(), getNativeObject(), i));
49 return res;
50 }

◆ getBoundVariableSorts()

Sort[] getBoundVariableSorts ( )
inline

The sorts of the bound variables.

Exceptions
Z3Exception

Definition at line 57 of file Lambda.java.

58 {
59 int n = getNumBound();
60 Sort[] res = new Sort[n];
61 for (int i = 0; i < n; i++)
62 res[i] = Sort.create(getContext(), Native.getQuantifierBoundSort(
63 getContext().nCtx(), getNativeObject(), i));
64 return res;
65 }

◆ getNumBound()

int getNumBound ( )
inline

The number of bound variables.

Definition at line 32 of file Lambda.java.

33 {
34 return Native.getQuantifierNumBound(getContext().nCtx(), getNativeObject());
35 }

Referenced by Lambda< R extends Sort >.getBoundVariableNames(), and Lambda< R extends Sort >.getBoundVariableSorts().

◆ of() [1/2]

static< R extends Sort > Lambda< R > of ( Context  ctx,
Expr<?>[]  bound,
Expr< R >  body 
)
inlinestatic
Parameters
ctxContext to create the lambda on.
boundBound variables.
bodyBody of the lambda expression.

Definition at line 118 of file Lambda.java.

118 {
119 ctx.checkContextMatch(body);
120
121
122 long nativeObject = Native.mkLambdaConst(ctx.nCtx(),
123 AST.arrayLength(bound), AST.arrayToNative(bound),
124 body.getNativeObject());
125 return new Lambda<>(ctx, nativeObject);
126 }

◆ of() [2/2]

static< R extends Sort > Lambda< R > of ( Context  ctx,
Sort[]  sorts,
Symbol[]  names,
Expr< R >  body 
)
inlinestatic

Definition at line 94 of file Lambda.java.

95 {
96 ctx.checkContextMatch(sorts);
97 ctx.checkContextMatch(names);
98 ctx.checkContextMatch(body);
99
100 if (sorts.length != names.length)
101 throw new Z3Exception("Number of sorts does not match number of names");
102
103
104 long nativeObject = Native.mkLambda(ctx.nCtx(),
105 AST.arrayLength(sorts), AST.arrayToNative(sorts),
106 Symbol.arrayToNative(names),
107 body.getNativeObject());
108
109 return new Lambda<>(ctx, nativeObject);
110 }

◆ translate()

Lambda< R > translate ( Context  ctx)
inline

Translates (copies) the quantifier to the Context ctx.

Parameters
ctxA context
Returns
A copy of the quantifier which is associated with ctx
Exceptions
Z3Exceptionon error

Definition at line 88 of file Lambda.java.

89 {
90 return (Lambda<R>) super.translate(ctx);
91 }

Referenced by AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), and Solver.__deepcopy__().