Z3
Model.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
21 
25 public class Model extends Z3Object
26 {
37  {
38  getContext().checkContextMatch(a);
39  return getConstInterp(a.getFuncDecl());
40  }
41 
52  {
53  getContext().checkContextMatch(f);
54  if (f.getArity() != 0
55  || Native.getSortKind(getContext().nCtx(),
56  Native.getRange(getContext().nCtx(), f.getNativeObject())) == Z3_sort_kind.Z3_ARRAY_SORT
57  .toInt())
58  throw new Z3Exception(
59  "Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.");
60 
61  long n = Native.modelGetConstInterp(getContext().nCtx(), getNativeObject(),
62  f.getNativeObject());
63  if (n == 0)
64  return null;
65  else
66  return Expr.create(getContext(), n);
67  }
68 
78  {
79  getContext().checkContextMatch(f);
80 
82  .nCtx(), Native.getRange(getContext().nCtx(), f.getNativeObject())));
83 
84  if (f.getArity() == 0)
85  {
86  long n = Native.modelGetConstInterp(getContext().nCtx(),
87  getNativeObject(), f.getNativeObject());
88 
89  if (sk == Z3_sort_kind.Z3_ARRAY_SORT)
90  {
91  if (n == 0)
92  return null;
93  else
94  {
95  if (Native.isAsArray(getContext().nCtx(), n) ^ true)
96  throw new Z3Exception(
97  "Argument was not an array constant");
98  long fd = Native.getAsArrayFuncDecl(getContext().nCtx(), n);
99  return getFuncInterp(new FuncDecl(getContext(), fd));
100  }
101  } else
102  {
103  throw new Z3Exception(
104  "Constant functions do not have a function interpretation; use ConstInterp");
105  }
106  } else
107  {
108  long n = Native.modelGetFuncInterp(getContext().nCtx(),
109  getNativeObject(), f.getNativeObject());
110  if (n == 0)
111  return null;
112  else
113  return new FuncInterp(getContext(), n);
114  }
115  }
116 
120  public int getNumConsts()
121  {
122  return Native.modelGetNumConsts(getContext().nCtx(), getNativeObject());
123  }
124 
131  {
132  int n = getNumConsts();
133  FuncDecl[] res = new FuncDecl[n];
134  for (int i = 0; i < n; i++)
135  res[i] = new FuncDecl(getContext(), Native.modelGetConstDecl(getContext()
136  .nCtx(), getNativeObject(), i));
137  return res;
138  }
139 
143  public int getNumFuncs()
144  {
145  return Native.modelGetNumFuncs(getContext().nCtx(), getNativeObject());
146  }
147 
154  {
155  int n = getNumFuncs();
156  FuncDecl[] res = new FuncDecl[n];
157  for (int i = 0; i < n; i++)
158  res[i] = new FuncDecl(getContext(), Native.modelGetFuncDecl(getContext()
159  .nCtx(), getNativeObject(), i));
160  return res;
161  }
162 
168  public FuncDecl[] getDecls()
169  {
170  int nFuncs = getNumFuncs();
171  int nConsts = getNumConsts();
172  int n = nFuncs + nConsts;
173  FuncDecl[] res = new FuncDecl[n];
174  for (int i = 0; i < nConsts; i++)
175  res[i] = new FuncDecl(getContext(), Native.modelGetConstDecl(getContext()
176  .nCtx(), getNativeObject(), i));
177  for (int i = 0; i < nFuncs; i++)
178  res[nConsts + i] = new FuncDecl(getContext(), Native.modelGetFuncDecl(
179  getContext().nCtx(), getNativeObject(), i));
180  return res;
181  }
182 
187  @SuppressWarnings("serial")
189  {
194  {
195  super();
196  }
197  }
198 
211  public Expr eval(Expr t, boolean completion)
212  {
213  Native.LongPtr v = new Native.LongPtr();
214  if (Native.modelEval(getContext().nCtx(), getNativeObject(),
215  t.getNativeObject(), (completion) ? true : false, v) ^ true)
216  throw new ModelEvaluationFailedException();
217  else
218  return Expr.create(getContext(), v.value);
219  }
220 
226  public Expr evaluate(Expr t, boolean completion)
227  {
228  return eval(t, completion);
229  }
230 
235  public int getNumSorts()
236  {
237  return Native.modelGetNumSorts(getContext().nCtx(), getNativeObject());
238  }
239 
251  public Sort[] getSorts()
252  {
253 
254  int n = getNumSorts();
255  Sort[] res = new Sort[n];
256  for (int i = 0; i < n; i++)
257  res[i] = Sort.create(getContext(),
258  Native.modelGetSort(getContext().nCtx(), getNativeObject(), i));
259  return res;
260  }
261 
272  {
273 
274  ASTVector nUniv = new ASTVector(getContext(), Native.modelGetSortUniverse(
275  getContext().nCtx(), getNativeObject(), s.getNativeObject()));
276  return nUniv.ToExprArray();
277  }
278 
284  public String toString()
285  {
286  try
287  {
288  return Native.modelToString(getContext().nCtx(), getNativeObject());
289  } catch (Z3Exception e)
290  {
291  return "Z3Exception: " + e.getMessage();
292  }
293  }
294 
295  Model(Context ctx, long obj)
296  {
297  super(ctx, obj);
298  }
299 
300  void incRef(long o)
301  {
302  getContext().getModelDRQ().incAndClear(getContext(), o);
303  super.incRef(o);
304  }
305 
306  void decRef(long o)
307  {
308  getContext().getModelDRQ().add(o);
309  super.decRef(o);
310  }
311 }
Expr evaluate(Expr t, boolean completion)
Definition: Model.java:226
Expr getConstInterp(Expr a)
Definition: Model.java:36
static long modelGetSort(long a0, long a1, int a2)
Definition: Native.java:2952
Expr[] getSortUniverse(Sort s)
Definition: Model.java:271
IDecRefQueue getModelDRQ()
Definition: Context.java:3719
Expr getConstInterp(FuncDecl f)
Definition: Model.java:51
static int modelGetNumSorts(long a0, long a1)
Definition: Native.java:2943
static int modelGetNumConsts(long a0, long a1)
Definition: Native.java:2907
static long getAsArrayFuncDecl(long a0, long a1)
Definition: Native.java:2979
static int getSortKind(long a0, long a1)
Definition: Native.java:2090
static final Z3_sort_kind fromInt(int v)
FuncDecl[] getFuncDecls()
Definition: Model.java:153
Expr eval(Expr t, boolean completion)
Definition: Model.java:211
static boolean isAsArray(long a0, long a1)
Definition: Native.java:2970
FuncDecl[] getConstDecls()
Definition: Model.java:130
void incAndClear(Context ctx, long o)
static boolean modelEval(long a0, long a1, long a2, boolean a3, LongPtr a4)
Definition: Native.java:2871
static long modelGetFuncDecl(long a0, long a1, int a2)
Definition: Native.java:2934
FuncDecl getFuncDecl()
Definition: Expr.java:72
static long modelGetSortUniverse(long a0, long a1, long a2)
Definition: Native.java:2961
static long modelGetConstDecl(long a0, long a1, int a2)
Definition: Native.java:2916
static long modelGetConstInterp(long a0, long a1, long a2)
Definition: Native.java:2880
static int modelGetNumFuncs(long a0, long a1)
Definition: Native.java:2925
FuncDecl[] getDecls()
Definition: Model.java:168
static String modelToString(long a0, long a1)
Definition: Native.java:3148
static long getRange(long a0, long a1)
Definition: Native.java:2315
static long modelGetFuncInterp(long a0, long a1, long a2)
Definition: Native.java:2898
FuncInterp getFuncInterp(FuncDecl f)
Definition: Model.java:77