Z3
ASTVector.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
23 class ASTVector extends Z3Object
24 {
28  public int size() throws Z3Exception
29  {
30  return Native.astVectorSize(getContext().nCtx(), getNativeObject());
31  }
32 
41  public AST get(int i) throws Z3Exception
42  {
43  return new AST(getContext(), Native.astVectorGet(getContext().nCtx(),
44  getNativeObject(), i));
45  }
46 
47  public void set(int i, AST value) throws Z3Exception
48  {
49 
50  Native.astVectorSet(getContext().nCtx(), getNativeObject(), i,
51  value.getNativeObject());
52  }
53 
58  public void resize(int newSize) throws Z3Exception
59  {
60  Native.astVectorResize(getContext().nCtx(), getNativeObject(), newSize);
61  }
62 
67  public void push(AST a) throws Z3Exception
68  {
69  Native.astVectorPush(getContext().nCtx(), getNativeObject(), a.getNativeObject());
70  }
71 
79  public ASTVector translate(Context ctx) throws Z3Exception
80  {
81  return new ASTVector(getContext(), Native.astVectorTranslate(getContext()
82  .nCtx(), getNativeObject(), ctx.nCtx()));
83  }
84 
88  public String toString()
89  {
90  try
91  {
92  return Native.astVectorToString(getContext().nCtx(), getNativeObject());
93  } catch (Z3Exception e)
94  {
95  return "Z3Exception: " + e.getMessage();
96  }
97  }
98 
99  ASTVector(Context ctx, long obj) throws Z3Exception
100  {
101  super(ctx, obj);
102  }
103 
104  ASTVector(Context ctx) throws Z3Exception
105  {
106  super(ctx, Native.mkAstVector(ctx.nCtx()));
107  }
108 
109  void incRef(long o) throws Z3Exception
110  {
111  getContext().astvector_DRQ().incAndClear(getContext(), o);
112  super.incRef(o);
113  }
114 
115  void decRef(long o) throws Z3Exception
116  {
117  getContext().astvector_DRQ().add(o);
118  super.decRef(o);
119  }
120 }