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.

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

getBoundVariableNames()

Symbol [] getBoundVariableNames ( )

inline

The symbols for the bound variables.

Exceptions

Z3Exception

Definition at line 42 of file Lambda.java.

    {
        int n = getNumBound();
        Symbol[] res = new Symbol[n];
        for (int i = 0; i < n; i++)
            res[i] = Symbol.create(getContext(), Native.getQuantifierBoundName(
                    getContext().nCtx(), getNativeObject(), i));
        return res;
    }

getBoundVariableSorts()

Sort [] getBoundVariableSorts ( )

inline

The sorts of the bound variables.

Exceptions

Z3Exception

Definition at line 57 of file Lambda.java.

    {
        int n = getNumBound();
        Sort[] res = new Sort[n];
        for (int i = 0; i < n; i++)
            res[i] = Sort.create(getContext(), Native.getQuantifierBoundSort(
                    getContext().nCtx(), getNativeObject(), i));
        return res;
    }

getNumBound()

int getNumBound ( )

inline

The number of bound variables.

Definition at line 32 of file Lambda.java.

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

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

ctx	Context to create the lambda on.
bound	Bound variables.
body	Body of the lambda expression.

Definition at line 118 of file Lambda.java.

                                                                                            {
        ctx.checkContextMatch(body);
 
              
       long nativeObject = Native.mkLambdaConst(ctx.nCtx(),
                                           AST.arrayLength(bound), AST.arrayToNative(bound),
                                           body.getNativeObject());
       return new Lambda<>(ctx, nativeObject);
   }

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.

    {
        ctx.checkContextMatch(sorts);
        ctx.checkContextMatch(names);
        ctx.checkContextMatch(body);
        
        if (sorts.length != names.length) 
            throw new Z3Exception("Number of sorts does not match number of names");
        
        
        long nativeObject = Native.mkLambda(ctx.nCtx(), 
                                            AST.arrayLength(sorts), AST.arrayToNative(sorts),
                                            Symbol.arrayToNative(names),
                                            body.getNativeObject());
        
        return new Lambda<>(ctx, nativeObject);
    }

translate()

Lambda<R> translate ( Context  ctx )

inline

Translates (copies) the quantifier to the Context

ctx 

.

Parameters

ctx

A context

Returns

A copy of the quantifier which is associated with

ctx 

Exceptions

Z3Exception

on error

Definition at line 88 of file Lambda.java.

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

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