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 }