Z3
Model.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
21 
25 public class Model extends Z3Object {
36  {
37  getContext().checkContextMatch(a);
38  return getConstInterp(a.getFuncDecl());
39  }
40 
51  {
52  getContext().checkContextMatch(f);
53  if (f.getArity() != 0)
54  throw new Z3Exception(
55  "Non-zero arity functions have FunctionInterpretations as a model. Use getFuncInterp.");
56 
57  long n = Native.modelGetConstInterp(getContext().nCtx(), getNativeObject(),
58  f.getNativeObject());
59  if (n == 0)
60  return null;
61  else
62  return Expr.create(getContext(), n);
63  }
64 
74  {
75  getContext().checkContextMatch(f);
76 
78  .nCtx(), Native.getRange(getContext().nCtx(), f.getNativeObject())));
79 
80  if (f.getArity() == 0)
81  {
82  long n = Native.modelGetConstInterp(getContext().nCtx(),
83  getNativeObject(), f.getNativeObject());
84 
85  if (sk == Z3_sort_kind.Z3_ARRAY_SORT)
86  {
87  if (n == 0)
88  return null;
89  else
90  {
91  if (Native.isAsArray(getContext().nCtx(), n)) {
92  long fd = Native.getAsArrayFuncDecl(getContext().nCtx(), n);
93  return getFuncInterp(new FuncDecl(getContext(), fd));
94  }
95  return null;
96  }
97  } else
98  {
99  throw new Z3Exception(
100  "Constant functions do not have a function interpretation; use getConstInterp");
101  }
102  } else
103  {
104  long n = Native.modelGetFuncInterp(getContext().nCtx(),
105  getNativeObject(), f.getNativeObject());
106  if (n == 0)
107  return null;
108  else
109  return new FuncInterp(getContext(), n);
110  }
111  }
112 
116  public int getNumConsts()
117  {
118  return Native.modelGetNumConsts(getContext().nCtx(), getNativeObject());
119  }
120 
127  {
128  int n = getNumConsts();
129  FuncDecl[] res = new FuncDecl[n];
130  for (int i = 0; i < n; i++)
131  res[i] = new FuncDecl(getContext(), Native.modelGetConstDecl(getContext()
132  .nCtx(), getNativeObject(), i));
133  return res;
134  }
135 
139  public int getNumFuncs()
140  {
141  return Native.modelGetNumFuncs(getContext().nCtx(), getNativeObject());
142  }
143 
150  {
151  int n = getNumFuncs();
152  FuncDecl[] res = new FuncDecl[n];
153  for (int i = 0; i < n; i++)
154  res[i] = new FuncDecl(getContext(), Native.modelGetFuncDecl(getContext()
155  .nCtx(), getNativeObject(), i));
156  return res;
157  }
158 
164  public FuncDecl[] getDecls()
165  {
166  int nFuncs = getNumFuncs();
167  int nConsts = getNumConsts();
168  int n = nFuncs + nConsts;
169  FuncDecl[] res = new FuncDecl[n];
170  for (int i = 0; i < nConsts; i++)
171  res[i] = new FuncDecl(getContext(), Native.modelGetConstDecl(getContext()
172  .nCtx(), getNativeObject(), i));
173  for (int i = 0; i < nFuncs; i++)
174  res[nConsts + i] = new FuncDecl(getContext(), Native.modelGetFuncDecl(
175  getContext().nCtx(), getNativeObject(), i));
176  return res;
177  }
178 
183  @SuppressWarnings("serial")
185  {
190  {
191  super();
192  }
193  }
194 
208  public Expr eval(Expr t, boolean completion)
209  {
210  Native.LongPtr v = new Native.LongPtr();
211  if (!Native.modelEval(getContext().nCtx(), getNativeObject(),
212  t.getNativeObject(), (completion), v))
213  throw new ModelEvaluationFailedException();
214  else
215  return Expr.create(getContext(), v.value);
216  }
217 
223  public Expr evaluate(Expr t, boolean completion)
224  {
225  return eval(t, completion);
226  }
227 
232  public int getNumSorts()
233  {
234  return Native.modelGetNumSorts(getContext().nCtx(), getNativeObject());
235  }
236 
248  public Sort[] getSorts()
249  {
250 
251  int n = getNumSorts();
252  Sort[] res = new Sort[n];
253  for (int i = 0; i < n; i++)
254  res[i] = Sort.create(getContext(),
255  Native.modelGetSort(getContext().nCtx(), getNativeObject(), i));
256  return res;
257  }
258 
269  {
270 
271  ASTVector nUniv = new ASTVector(getContext(), Native.modelGetSortUniverse(
272  getContext().nCtx(), getNativeObject(), s.getNativeObject()));
273  return nUniv.ToExprArray();
274  }
275 
281  @Override
282  public String toString() {
283  return Native.modelToString(getContext().nCtx(), getNativeObject());
284  }
285 
286  Model(Context ctx, long obj)
287  {
288  super(ctx, obj);
289  }
290 
291  @Override
292  void incRef() {
293  Native.modelIncRef(getContext().nCtx(), getNativeObject());
294  }
295 
296  @Override
297  void addToReferenceQueue() {
298  getContext().getModelDRQ().storeReference(getContext(), this);
299  }
300 }
Expr evaluate(Expr t, boolean completion)
Definition: Model.java:223
Expr getConstInterp(Expr a)
Definition: Model.java:35
static long modelGetSort(long a0, long a1, int a2)
Definition: Native.java:3607
Sort [] getSorts()
Definition: Model.java:248
Expr [] getSortUniverse(Sort s)
Definition: Model.java:268
Expr getConstInterp(FuncDecl f)
Definition: Model.java:50
static int modelGetNumSorts(long a0, long a1)
Definition: Native.java:3598
static int modelGetNumConsts(long a0, long a1)
Definition: Native.java:3562
static long getAsArrayFuncDecl(long a0, long a1)
Definition: Native.java:3643
static int getSortKind(long a0, long a1)
Definition: Native.java:2682
static final Z3_sort_kind fromInt(int v)
FuncDecl [] getFuncDecls()
Definition: Model.java:149
Expr eval(Expr t, boolean completion)
Definition: Model.java:208
IDecRefQueue< Model > getModelDRQ()
Definition: Context.java:4063
static boolean isAsArray(long a0, long a1)
Definition: Native.java:3634
void storeReference(Context ctx, T obj)
FuncDecl [] getConstDecls()
Definition: Model.java:126
static boolean modelEval(long a0, long a1, long a2, boolean a3, LongPtr a4)
Definition: Native.java:3526
static long modelGetFuncDecl(long a0, long a1, int a2)
Definition: Native.java:3589
FuncDecl getFuncDecl()
Definition: Expr.java:72
static long modelGetSortUniverse(long a0, long a1, long a2)
Definition: Native.java:3616
static long modelGetConstDecl(long a0, long a1, int a2)
Definition: Native.java:3571
static long modelGetConstInterp(long a0, long a1, long a2)
Definition: Native.java:3535
static int modelGetNumFuncs(long a0, long a1)
Definition: Native.java:3580
FuncDecl [] getDecls()
Definition: Model.java:164
static String modelToString(long a0, long a1)
Definition: Native.java:3845
static long getRange(long a0, long a1)
Definition: Native.java:2934
static long modelGetFuncInterp(long a0, long a1, long a2)
Definition: Native.java:3553
def String(name, ctx=None)
Definition: z3py.py:10087
FuncInterp getFuncInterp(FuncDecl f)
Definition: Model.java:73