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

Public Member Functions

boolean contains (AST k) throws Z3Exception
AST find (AST k) throws Z3Exception
void insert (AST k, AST v) throws Z3Exception
void erase (AST k) throws Z3Exception
void reset () throws Z3Exception
int size () throws Z3Exception
ASTVector getKeys () throws Z3Exception
String toString ()

Package Functions

 ASTMap (Context ctx, long obj) throws Z3Exception
 ASTMap (Context ctx) throws Z3Exception
void incRef (long o) throws Z3Exception
void decRef (long o) throws Z3Exception

Detailed Description

Map from AST to AST

Definition at line 23 of file ASTMap.java.


Constructor & Destructor Documentation

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

Definition at line 114 of file ASTMap.java.

    {
        super(ctx, obj);
    }
ASTMap ( Context  ctx) throws Z3Exception [inline, package]

Definition at line 119 of file ASTMap.java.

    {
        super(ctx, Native.mkAstMap(ctx.nCtx()));
    }

Member Function Documentation

boolean contains ( AST  k) throws Z3Exception [inline]

Checks whether the map contains the key k .

Parameters:
kAn AST
Returns:
True if k is a key in the map, false otherwise.

Definition at line 32 of file ASTMap.java.

    {

        return Native.astMapContains(getContext().nCtx(), getNativeObject(),
                k.getNativeObject());
    }
void decRef ( long  o) throws Z3Exception [inline, package]

Reimplemented from Z3Object.

Definition at line 130 of file ASTMap.java.

    {
        getContext().astmap_DRQ().add(o);
        super.decRef(o);
    }
void erase ( AST  k) throws Z3Exception [inline]

Erases the key k from the map.

Parameters:
kAn AST

Definition at line 67 of file ASTMap.java.

    {

        Native.astMapErase(getContext().nCtx(), getNativeObject(), k.getNativeObject());
    }
AST find ( AST  k) throws Z3Exception [inline]

Finds the value associated with the key k . This function signs an error when k is not a key in the map.

Parameters:
kAn AST
Exceptions:
Z3Exception

Definition at line 46 of file ASTMap.java.

    {
        return new AST(getContext(), Native.astMapFind(getContext().nCtx(),
                getNativeObject(), k.getNativeObject()));
    }
ASTVector getKeys ( ) throws Z3Exception [inline]

The keys stored in the map.

Exceptions:
Z3Exception

Definition at line 94 of file ASTMap.java.

    {
        return new ASTVector(getContext(), Native.astMapKeys(getContext().nCtx(),
                getNativeObject()));
    }
void incRef ( long  o) throws Z3Exception [inline, package]

Reimplemented from Z3Object.

Definition at line 124 of file ASTMap.java.

    {
        getContext().astmap_DRQ().incAndClear(getContext(), o);
        super.incRef(o);
    }
void insert ( AST  k,
AST  v 
) throws Z3Exception [inline]

Stores or replaces a new key/value pair in the map.

Parameters:
kThe key AST
vThe value AST

Definition at line 56 of file ASTMap.java.

    {

        Native.astMapInsert(getContext().nCtx(), getNativeObject(), k.getNativeObject(),
                v.getNativeObject());
    }
void reset ( ) throws Z3Exception [inline]

Removes all keys from the map.

Definition at line 76 of file ASTMap.java.

    {
        Native.astMapReset(getContext().nCtx(), getNativeObject());
    }
int size ( ) throws Z3Exception [inline]

The size of the map

Definition at line 84 of file ASTMap.java.

    {
        return Native.astMapSize(getContext().nCtx(), getNativeObject());
    }
String toString ( ) [inline]

Retrieves a string representation of the map.

Definition at line 103 of file ASTMap.java.

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