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 |
Definition at line 23 of file ASTMap.java.
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())); }
boolean contains | ( | AST | k | ) | throws Z3Exception [inline] |
Checks whether the map contains the key k .
k | An AST |
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.
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.
k | An AST |
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.
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.
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(); } }