Z3
src/api/java/ASTMap.java
Go to the documentation of this file.
00001 
00018 package com.microsoft.z3;
00019 
00023 class ASTMap extends Z3Object
00024 {
00032     public boolean contains(AST k) throws Z3Exception
00033     {
00034 
00035         return Native.astMapContains(getContext().nCtx(), getNativeObject(),
00036                 k.getNativeObject());
00037     }
00038 
00046     public AST find(AST k) throws Z3Exception
00047     {
00048         return new AST(getContext(), Native.astMapFind(getContext().nCtx(),
00049                 getNativeObject(), k.getNativeObject()));
00050     }
00051 
00056     public void insert(AST k, AST v) throws Z3Exception
00057     {
00058 
00059         Native.astMapInsert(getContext().nCtx(), getNativeObject(), k.getNativeObject(),
00060                 v.getNativeObject());
00061     }
00062 
00067     public void erase(AST k) throws Z3Exception
00068     {
00069 
00070         Native.astMapErase(getContext().nCtx(), getNativeObject(), k.getNativeObject());
00071     }
00072 
00076     public void reset() throws Z3Exception
00077     {
00078         Native.astMapReset(getContext().nCtx(), getNativeObject());
00079     }
00080 
00084     public int size() throws Z3Exception
00085     {
00086         return Native.astMapSize(getContext().nCtx(), getNativeObject());
00087     }
00088 
00094     public ASTVector getKeys() throws Z3Exception
00095     {
00096         return new ASTVector(getContext(), Native.astMapKeys(getContext().nCtx(),
00097                 getNativeObject()));
00098     }
00099 
00103     public String toString()
00104     {
00105         try
00106         {
00107             return Native.astMapToString(getContext().nCtx(), getNativeObject());
00108         } catch (Z3Exception e)
00109         {
00110             return "Z3Exception: " + e.getMessage();
00111         }
00112     }
00113 
00114     ASTMap(Context ctx, long obj) throws Z3Exception
00115     {
00116         super(ctx, obj);
00117     }
00118 
00119     ASTMap(Context ctx) throws Z3Exception
00120     {
00121         super(ctx, Native.mkAstMap(ctx.nCtx()));
00122     }
00123 
00124     void incRef(long o) throws Z3Exception
00125     {
00126         getContext().astmap_DRQ().incAndClear(getContext(), o);
00127         super.incRef(o);
00128     }
00129 
00130     void decRef(long o) throws Z3Exception
00131     {
00132         getContext().astmap_DRQ().add(o);
00133         super.decRef(o);
00134     }
00135 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines