Z3
ASTMap.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
23 class ASTMap extends Z3Object
24 {
32  public boolean contains(AST k) throws Z3Exception
33  {
34 
35  return Native.astMapContains(getContext().nCtx(), getNativeObject(),
36  k.getNativeObject());
37  }
38 
46  public AST find(AST k) throws Z3Exception
47  {
48  return new AST(getContext(), Native.astMapFind(getContext().nCtx(),
49  getNativeObject(), k.getNativeObject()));
50  }
51 
56  public void insert(AST k, AST v) throws Z3Exception
57  {
58 
59  Native.astMapInsert(getContext().nCtx(), getNativeObject(), k.getNativeObject(),
60  v.getNativeObject());
61  }
62 
67  public void erase(AST k) throws Z3Exception
68  {
69 
70  Native.astMapErase(getContext().nCtx(), getNativeObject(), k.getNativeObject());
71  }
72 
76  public void reset() throws Z3Exception
77  {
78  Native.astMapReset(getContext().nCtx(), getNativeObject());
79  }
80 
84  public int size() throws Z3Exception
85  {
86  return Native.astMapSize(getContext().nCtx(), getNativeObject());
87  }
88 
94  public ASTVector getKeys() throws Z3Exception
95  {
96  return new ASTVector(getContext(), Native.astMapKeys(getContext().nCtx(),
97  getNativeObject()));
98  }
99 
103  public String toString()
104  {
105  try
106  {
107  return Native.astMapToString(getContext().nCtx(), getNativeObject());
108  } catch (Z3Exception e)
109  {
110  return "Z3Exception: " + e.getMessage();
111  }
112  }
113 
114  ASTMap(Context ctx, long obj) throws Z3Exception
115  {
116  super(ctx, obj);
117  }
118 
119  ASTMap(Context ctx) throws Z3Exception
120  {
121  super(ctx, Native.mkAstMap(ctx.nCtx()));
122  }
123 
124  void incRef(long o) throws Z3Exception
125  {
126  getContext().astmap_DRQ().incAndClear(getContext(), o);
127  super.incRef(o);
128  }
129 
130  void decRef(long o) throws Z3Exception
131  {
132  getContext().astmap_DRQ().add(o);
133  super.decRef(o);
134  }
135 }