18 package com.microsoft.z3;
23 class ASTMap
extends Z3Object
32 public boolean contains(AST k)
throws Z3Exception
35 return Native.astMapContains(getContext().nCtx(), getNativeObject(),
46 public AST find(AST k)
throws Z3Exception
48 return new AST(getContext(), Native.astMapFind(getContext().nCtx(),
49 getNativeObject(), k.getNativeObject()));
56 public void insert(AST k, AST v)
throws Z3Exception
59 Native.astMapInsert(getContext().nCtx(), getNativeObject(), k.getNativeObject(),
67 public void erase(AST k)
throws Z3Exception
70 Native.astMapErase(getContext().nCtx(), getNativeObject(), k.getNativeObject());
76 public void reset() throws Z3Exception
78 Native.astMapReset(getContext().nCtx(), getNativeObject());
84 public int size() throws Z3Exception
86 return Native.astMapSize(getContext().nCtx(), getNativeObject());
94 public ASTVector getKeys() throws Z3Exception
96 return new ASTVector(getContext(), Native.astMapKeys(getContext().nCtx(),
103 public String toString()
107 return Native.astMapToString(getContext().nCtx(), getNativeObject());
108 }
catch (Z3Exception e)
110 return "Z3Exception: " + e.getMessage();
114 ASTMap(Context ctx,
long obj)
throws Z3Exception
119 ASTMap(Context ctx)
throws Z3Exception
121 super(ctx, Native.mkAstMap(ctx.nCtx()));
124 void incRef(
long o)
throws Z3Exception
126 getContext().astmap_DRQ().incAndClear(getContext(), o);
130 void decRef(
long o)
throws Z3Exception
132 getContext().astmap_DRQ().add(o);