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__().