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:

k

An 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:

k

An 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:

k

An 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:

k	The key AST
v	The 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();
        }
    }