Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Data Structures | Public Member Functions | Package Functions
FuncDecl Class Reference
+ Inheritance diagram for FuncDecl:

Data Structures

class  Parameter

Public Member Functions

boolean equals (Object o)
int hashCode ()
String toString ()
int getId () throws Z3Exception
int getArity () throws Z3Exception
int getDomainSize () throws Z3Exception
Sort[] getDomain () throws Z3Exception
Sort getRange () throws Z3Exception
Z3_decl_kind getDeclKind () throws Z3Exception
Symbol getName () throws Z3Exception
int getNumParameters () throws Z3Exception
Parameter[] getParameters () throws Z3Exception
Expr apply (Expr...args) throws Z3Exception

Package Functions

 FuncDecl (Context ctx, long obj) throws Z3Exception
 FuncDecl (Context ctx, Symbol name, Sort[] domain, Sort range) throws Z3Exception
 FuncDecl (Context ctx, String prefix, Sort[] domain, Sort range) throws Z3Exception
void checkNativeObject (long obj) throws Z3Exception

Detailed Description

Function declarations.

Definition at line 27 of file FuncDecl.java.


Constructor & Destructor Documentation

FuncDecl ( Context  ctx,
long  obj 
) throws Z3Exception [inline, package]

Definition at line 344 of file FuncDecl.java.

Referenced by FuncDecl.equals(), and FuncDecl.getParameters().

    {
        super(ctx, obj);

    }
FuncDecl ( Context  ctx,
Symbol  name,
Sort[]  domain,
Sort  range 
) throws Z3Exception [inline, package]

Definition at line 350 of file FuncDecl.java.

    {
        super(ctx, Native.mkFuncDecl(ctx.nCtx(), name.getNativeObject(),
                AST.arrayLength(domain), AST.arrayToNative(domain),
                range.getNativeObject()));

    }
FuncDecl ( Context  ctx,
String  prefix,
Sort[]  domain,
Sort  range 
) throws Z3Exception [inline, package]

Definition at line 359 of file FuncDecl.java.

    {
        super(ctx, Native.mkFreshFuncDecl(ctx.nCtx(), prefix,
                AST.arrayLength(domain), AST.arrayToNative(domain),
                range.getNativeObject()));

    }

Member Function Documentation

Expr apply ( Expr...  args) throws Z3Exception [inline]

Create expression that applies function to arguments.

Parameters:
args
Returns:

Definition at line 383 of file FuncDecl.java.

Referenced by Tactic.__call__().

    {
        getContext().checkContextMatch(args);
        return Expr.create(getContext(), this, args);
    }
void checkNativeObject ( long  obj) throws Z3Exception [inline, package]

Reimplemented from Z3Object.

Definition at line 368 of file FuncDecl.java.

    {
        if (Native.getAstKind(getContext().nCtx(), obj) != Z3_ast_kind.Z3_FUNC_DECL_AST
                .toInt())
            throw new Z3Exception(
                    "Underlying object is not a function declaration");
        super.checkNativeObject(obj);
    }
boolean equals ( Object  o) [inline]

Comparison operator.

Returns:
True if a and b share the same context and are equal, false otherwise. Comparison operator.
True if a and b do not share the same context or are not equal, false otherwise. Object comparison.

Reimplemented from AST.

Definition at line 48 of file FuncDecl.java.

    {
        FuncDecl casted = (FuncDecl) o;
        if (casted == null)
            return false;
        return this == casted;
    }
int getArity ( ) throws Z3Exception [inline]

The arity of the function declaration

Definition at line 89 of file FuncDecl.java.

    {
        return Native.getArity(getContext().nCtx(), getNativeObject());
    }
Z3_decl_kind getDeclKind ( ) throws Z3Exception [inline]

The kind of the function declaration.

Definition at line 131 of file FuncDecl.java.

Referenced by Expr.isAdd(), Expr.isAnd(), Expr.isArithmeticNumeral(), Expr.isArrayMap(), Expr.isAsArray(), Expr.isBVAdd(), Expr.isBVAND(), Expr.isBVBitOne(), Expr.isBVBitZero(), Expr.isBVCarry(), Expr.isBVComp(), Expr.isBVConcat(), Expr.isBVExtract(), Expr.isBVMul(), Expr.isBVNAND(), Expr.isBVNOR(), Expr.isBVNOT(), Expr.isBVNumeral(), Expr.isBVOR(), Expr.isBVReduceAND(), Expr.isBVReduceOR(), Expr.isBVRepeat(), Expr.isBVRotateLeft(), Expr.isBVRotateLeftExtended(), Expr.isBVRotateRight(), Expr.isBVRotateRightExtended(), Expr.isBVSDiv(), Expr.IsBVSDiv0(), Expr.isBVSGE(), Expr.isBVSGT(), Expr.isBVShiftLeft(), Expr.isBVShiftRightArithmetic(), Expr.isBVShiftRightLogical(), Expr.isBVSignExtension(), Expr.isBVSLE(), Expr.isBVSLT(), Expr.isBVSMod(), Expr.IsBVSMod0(), Expr.isBVSRem(), Expr.IsBVSRem0(), Expr.isBVSub(), Expr.isBVToInt(), Expr.isBVUDiv(), Expr.IsBVUDiv0(), Expr.isBVUGE(), Expr.isBVUGT(), Expr.isBVULE(), Expr.isBVULT(), Expr.isBVUMinus(), Expr.isBVURem(), Expr.IsBVURem0(), Expr.isBVXNOR(), Expr.isBVXOR(), Expr.isBVXOR3(), Expr.isBVZeroExtension(), Expr.isConstantArray(), Expr.isDefaultArray(), Expr.isDistinct(), Expr.isDiv(), Expr.isEmptyRelation(), Expr.isEq(), Expr.isFalse(), Expr.isFiniteDomainLT(), Expr.isGE(), Expr.isGT(), Expr.isIDiv(), Expr.isIff(), Expr.isImplies(), Expr.isIntToBV(), Expr.isIntToReal(), Expr.isIsEmptyRelation(), Expr.isITE(), Expr.isLabel(), Expr.isLabelLit(), Expr.isLE(), Expr.isLT(), Expr.isModulus(), Expr.isMul(), Expr.isNot(), Expr.isOEQ(), Expr.isOr(), Expr.isProofAndElimination(), Expr.isProofApplyDef(), Expr.isProofAsserted(), Expr.isProofCNFStar(), Expr.isProofCommutativity(), Expr.isProofDefAxiom(), Expr.isProofDefIntro(), Expr.isProofDER(), Expr.isProofDistributivity(), Expr.isProofElimUnusedVars(), Expr.isProofGoal(), Expr.isProofHypothesis(), Expr.isProofIFFFalse(), Expr.isProofIFFOEQ(), Expr.isProofIFFTrue(), Expr.isProofLemma(), Expr.isProofModusPonens(), Expr.isProofModusPonensOEQ(), Expr.isProofMonotonicity(), Expr.isProofNNFNeg(), Expr.isProofNNFPos(), Expr.isProofNNFStar(), Expr.isProofOrElimination(), Expr.isProofPullQuant(), Expr.isProofPullQuantStar(), Expr.isProofPushQuant(), Expr.isProofQuantInst(), Expr.isProofQuantIntro(), Expr.isProofReflexivity(), Expr.isProofRewrite(), Expr.isProofRewriteStar(), Expr.isProofSkolemize(), Expr.isProofSymmetry(), Expr.isProofTheoryLemma(), Expr.isProofTransitivity(), Expr.isProofTransitivityStar(), Expr.isProofTrue(), Expr.isProofUnitResolution(), Expr.isRealIsInt(), Expr.isRealToInt(), Expr.isRelationalJoin(), Expr.isRelationClone(), Expr.isRelationComplement(), Expr.isRelationFilter(), Expr.isRelationNegationFilter(), Expr.isRelationProject(), Expr.isRelationRename(), Expr.isRelationSelect(), Expr.isRelationStore(), Expr.isRelationUnion(), Expr.isRelationWiden(), Expr.isRemainder(), Expr.isSelect(), Expr.isSetComplement(), Expr.isSetDifference(), Expr.isSetIntersect(), Expr.isSetSubset(), Expr.isSetUnion(), Expr.isStore(), Expr.isSub(), Expr.isTrue(), Expr.isUMinus(), and Expr.isXor().

    {
        return Z3_decl_kind.fromInt(Native.getDeclKind(getContext().nCtx(),
                getNativeObject()));
    }
Sort [] getDomain ( ) throws Z3Exception [inline]

The domain of the function declaration

Definition at line 106 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;
    }
int getDomainSize ( ) throws Z3Exception [inline]

The size of the domain of the function declaration

See also:
Arity

Definition at line 98 of file FuncDecl.java.

Referenced by DatatypeSort.getAccessors(), FuncDecl.getDomain(), and Expr.isConst().

    {
        return Native.getDomainSize(getContext().nCtx(), getNativeObject());
    }
int getId ( ) throws Z3Exception [inline]

Returns a unique identifier for the function declaration.

Reimplemented from AST.

Definition at line 81 of file FuncDecl.java.

    {
        return Native.getFuncDeclId(getContext().nCtx(), getNativeObject());
    }
Symbol getName ( ) throws Z3Exception [inline]

The name of the function declaration

Definition at line 140 of file FuncDecl.java.

    {

        return Symbol.create(getContext(),
                Native.getDeclName(getContext().nCtx(), getNativeObject()));
    }
int getNumParameters ( ) throws Z3Exception [inline]

The number of parameters of the function declaration

Definition at line 150 of file FuncDecl.java.

Referenced by FuncDecl.getParameters().

    {
        return Native.getDeclNumParameters(getContext().nCtx(), getNativeObject());
    }
Parameter [] getParameters ( ) throws Z3Exception [inline]

The parameters of the function declaration

Definition at line 158 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;
    }
Sort getRange ( ) throws Z3Exception [inline]

The range of the function declaration

Definition at line 121 of file FuncDecl.java.

    {

        return Sort.create(getContext(),
                Native.getRange(getContext().nCtx(), getNativeObject()));
    }
int hashCode ( ) [inline]

A hash code.

Reimplemented from AST.

Definition at line 59 of file FuncDecl.java.

    {
        return super.hashCode();
    }
String toString ( ) [inline]

A string representations of the function declaration.

Reimplemented from AST.

Definition at line 67 of file FuncDecl.java.

    {
        try
        {
            return Native.funcDeclToString(getContext().nCtx(), getNativeObject());
        } catch (Z3Exception e)
        {
            return "Z3Exception: " + e.getMessage();
        }
    }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines