FuncDecl< R extends Sort > Class Template Reference

Inheritance diagram for FuncDecl< R extends Sort >:

Data Structures
class	Parameter

Public Member Functions
boolean	equals (Object o)
String	toString ()
int	getId ()
FuncDecl< R >	translate (Context ctx)
int	getArity ()
int	getDomainSize ()
Sort[]	getDomain ()
R	getRange ()
Z3_decl_kind	getDeclKind ()
Symbol	getName ()
int	getNumParameters ()
Parameter[]	getParameters ()
Expr< R >	apply (Expr<?> ... args)
Public Member Functions inherited from AST
int	compareTo (AST other)
int	hashCode ()
Z3_ast_kind	getASTKind ()
boolean	isExpr ()
boolean	isApp ()
boolean	isVar ()
boolean	isQuantifier ()
boolean	isSort ()
boolean	isFuncDecl ()
String	getSExpr ()

Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[]	arrayToNative (Z3Object[] a)
static int	arrayLength (Z3Object[] a)

Detailed Description

Function declarations.

Definition at line 27 of file FuncDecl.java.

Member Function Documentation

apply()

Expr<R> apply ( Expr<?> ...  args )

inline

Create expression that applies function to arguments.

Definition at line 374 of file FuncDecl.java.

    {
        getContext().checkContextMatch(args);
        return Expr.create(getContext(), this, args);
    }

Referenced by Tactic.__call__().

equals()

boolean equals ( Object  o )

inline

Object comparison.

Reimplemented from AST.

Definition at line 33 of file FuncDecl.java.

    {
        if (o == this) return true;
        if (!(o instanceof FuncDecl)) return false;
        FuncDecl<?> other = (FuncDecl<?>) o;
 
        return
            (getContext().nCtx() == other.getContext().nCtx()) &&
            (Native.isEqFuncDecl(
                getContext().nCtx(),
                getNativeObject(),
                other.getNativeObject()));
    }

getArity()

int getArity ( )

inline

The arity of the function declaration

Definition at line 78 of file FuncDecl.java.

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

getDeclKind()

Z3_decl_kind getDeclKind ( )

inline

The kind of the function declaration.

Definition at line 120 of file FuncDecl.java.

    {
        return Z3_decl_kind.fromInt(Native.getDeclKind(getContext().nCtx(),
                getNativeObject()));
    }

getDomain()

Sort [] getDomain ( )

inline

The domain of the function declaration

Definition at line 95 of file FuncDecl.java.

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

getDomainSize()

int getDomainSize ( )

inline

The size of the domain of the function declaration

See also

getArity

Definition at line 87 of file FuncDecl.java.

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

Referenced by DatatypeSort< R >.getAccessors(), and FuncDecl< R extends Sort >.getDomain().

getId()

int getId ( )

inline

Returns a unique identifier for the function declaration.

Reimplemented from AST.

Definition at line 57 of file FuncDecl.java.

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

getName()

Symbol getName ( )

inline

The name of the function declaration

Definition at line 129 of file FuncDecl.java.

    {
 
        return Symbol.create(getContext(),
                Native.getDeclName(getContext().nCtx(), getNativeObject()));
    }

getNumParameters()

int getNumParameters ( )

inline

The number of parameters of the function declaration

Definition at line 139 of file FuncDecl.java.

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

Referenced by FuncDecl< R extends Sort >.getParameters().

getParameters()

Parameter [] getParameters ( )

inline

The parameters of the function declaration

Definition at line 147 of file FuncDecl.java.

    {
 
        int num = getNumParameters();
        Parameter[] res = new Parameter[num];
        for (int i = 0; i < num; i++)
        {
            Z3_parameter_kind k = Z3_parameter_kind.fromInt(Native
                    .getDeclParameterKind(getContext().nCtx(), getNativeObject(), i));
            switch (k)
            {
            case Z3_PARAMETER_INT:
                res[i] = new Parameter(k, Native.getDeclIntParameter(getContext()
                        .nCtx(), getNativeObject(), i));
                break;
            case Z3_PARAMETER_DOUBLE:
                res[i] = new Parameter(k, Native.getDeclDoubleParameter(
                        getContext().nCtx(), getNativeObject(), i));
                break;
            case Z3_PARAMETER_SYMBOL:
                res[i] = new Parameter(k, Symbol.create(getContext(), Native
                        .getDeclSymbolParameter(getContext().nCtx(),
                                getNativeObject(), i)));
                break;
            case Z3_PARAMETER_SORT:
                res[i] = new Parameter(k, Sort.create(getContext(), Native
                        .getDeclSortParameter(getContext().nCtx(), getNativeObject(),
                                i)));
                break;
            case Z3_PARAMETER_AST:
                res[i] = new Parameter(k, new AST(getContext(),
                        Native.getDeclAstParameter(getContext().nCtx(),
                                getNativeObject(), i)));
                break;
            case Z3_PARAMETER_FUNC_DECL:
                res[i] = new Parameter(k, new FuncDecl<>(getContext(),
                        Native.getDeclFuncDeclParameter(getContext().nCtx(),
                                getNativeObject(), i)));
                break;
            case Z3_PARAMETER_RATIONAL:
                res[i] = new Parameter(k, Native.getDeclRationalParameter(
                        getContext().nCtx(), getNativeObject(), i));
                break;
            default:
                throw new Z3Exception(
                        "Unknown function declaration parameter kind encountered");
            }
        }
        return res;
    }

getRange()

R getRange ( )

inline

The range of the function declaration

Definition at line 111 of file FuncDecl.java.

    {
        return (R) Sort.create(getContext(),
                Native.getRange(getContext().nCtx(), getNativeObject()));
    }

toString()

String toString ( )

inline

A string representation of the AST.

Reimplemented from AST.

Definition at line 48 of file FuncDecl.java.

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

translate()

FuncDecl<R> translate ( Context  ctx )

inline

Translates (copies) the function declaration to the Context

ctx 

.

Parameters

ctx

A context

Returns

A copy of the function declaration which is associated with

ctx 

Exceptions

Z3Exception

on error

Reimplemented from AST.

Definition at line 70 of file FuncDecl.java.

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