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 {
36  {
37  getContext().checkContextMatch(a);
38  return getConstInterp(a.getFuncDecl());
39  }
40 
50  {
51  getContext().checkContextMatch(f);
52  if (f.getArity() != 0
53  || Native.getSortKind(getContext().nCtx(),
54  Native.getRange(getContext().nCtx(), f.getNativeObject())) == Z3_sort_kind.Z3_ARRAY_SORT
55  .toInt())
56  throw new Z3Exception(
57  "Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.");
58 
59  long n = Native.modelGetConstInterp(getContext().nCtx(), getNativeObject(),
60  f.getNativeObject());
61  if (n == 0)
62  return null;
63  else
64  return Expr.create(getContext(), n);
65  }
66 
77  {
78  getContext().checkContextMatch(f);
79 
81  .nCtx(), Native.getRange(getContext().nCtx(), f.getNativeObject())));
82 
83  if (f.getArity() == 0)
84  {
85  long n = Native.modelGetConstInterp(getContext().nCtx(),
86  getNativeObject(), f.getNativeObject());
87 
88  if (sk == Z3_sort_kind.Z3_ARRAY_SORT)
89  {
90  if (n == 0)
91  return null;
92  else
93  {
94  if (Native.isAsArray(getContext().nCtx(), n) ^ true)
95  throw new Z3Exception(
96  "Argument was not an array constant");
97  long fd = Native.getAsArrayFuncDecl(getContext().nCtx(), n);
98  return getFuncInterp(new FuncDecl(getContext(), fd));
99  }
100  } else
101  {
102  throw new Z3Exception(
103  "Constant functions do not have a function interpretation; use ConstInterp");
104  }
105  } else
106  {
107  long n = Native.modelGetFuncInterp(getContext().nCtx(),
108  getNativeObject(), f.getNativeObject());
109  if (n == 0)
110  return null;
111  else
112  return new FuncInterp(getContext(), n);
113  }
114  }
115 
119  public int getNumConsts() throws Z3Exception
120  {
121  return Native.modelGetNumConsts(getContext().nCtx(), getNativeObject());
122  }
123 
130  {
131  int n = getNumConsts();
132  FuncDecl[] res = new FuncDecl[n];
133  for (int i = 0; i < n; i++)
134  res[i] = new FuncDecl(getContext(), Native.modelGetConstDecl(getContext()
135  .nCtx(), getNativeObject(), i));
136  return res;
137  }
138 
142  public int getNumFuncs() throws Z3Exception
143  {
144  return Native.modelGetNumFuncs(getContext().nCtx(), getNativeObject());
145  }
146 
153  {
154  int n = getNumFuncs();
155  FuncDecl[] res = new FuncDecl[n];
156  for (int i = 0; i < n; i++)
157  res[i] = new FuncDecl(getContext(), Native.modelGetFuncDecl(getContext()
158  .nCtx(), getNativeObject(), i));
159  return res;
160  }
161 
167  public FuncDecl[] getDecls() throws Z3Exception
168  {
169  int nFuncs = getNumFuncs();
170  int nConsts = getNumConsts();
171  int n = nFuncs + nConsts;
172  FuncDecl[] res = new FuncDecl[n];
173  for (int i = 0; i < nConsts; i++)
174  res[i] = new FuncDecl(getContext(), Native.modelGetConstDecl(getContext()
175  .nCtx(), getNativeObject(), i));
176  for (int i = 0; i < nFuncs; i++)
177  res[nConsts + i] = new FuncDecl(getContext(), Native.modelGetFuncDecl(
178  getContext().nCtx(), getNativeObject(), i));
179  return res;
180  }
181 
186  @SuppressWarnings("serial")
188  {
193  {
194  super();
195  }
196  }
197 
211  public Expr eval(Expr t, boolean completion) throws Z3Exception
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) throws Z3Exception
227  {
228  return eval(t, completion);
229  }
230 
235  public int getNumSorts() throws Z3Exception
236  {
237  return Native.modelGetNumSorts(getContext().nCtx(), getNativeObject());
238  }
239 
249  public Sort[] getSorts() throws Z3Exception
250  {
251 
252  int n = getNumSorts();
253  Sort[] res = new Sort[n];
254  for (int i = 0; i < n; i++)
255  res[i] = Sort.create(getContext(),
256  Native.modelGetSort(getContext().nCtx(), getNativeObject(), i));
257  return res;
258  }
259 
270  {
271 
272  ASTVector nUniv = new ASTVector(getContext(), Native.modelGetSortUniverse(
273  getContext().nCtx(), getNativeObject(), s.getNativeObject()));
274  int n = nUniv.size();
275  Expr[] res = new Expr[n];
276  for (int i = 0; i < n; i++)
277  res[i] = Expr.create(getContext(), nUniv.get(i).getNativeObject());
278  return res;
279  }
280 
286  public String toString()
287  {
288  try
289  {
290  return Native.modelToString(getContext().nCtx(), getNativeObject());
291  } catch (Z3Exception e)
292  {
293  return "Z3Exception: " + e.getMessage();
294  }
295  }
296 
297  Model(Context ctx, long obj) throws Z3Exception
298  {
299  super(ctx, obj);
300  }
301 
302  void incRef(long o) throws Z3Exception
303  {
304  getContext().model_DRQ().incAndClear(getContext(), o);
305  super.incRef(o);
306  }
307 
308  void decRef(long o) throws Z3Exception
309  {
310  getContext().model_DRQ().add(o);
311  super.decRef(o);
312  }
313 }
Expr evaluate(Expr t, boolean completion)
Definition: Model.java:226
Expr getConstInterp(Expr a)
Definition: Model.java:35
static long modelGetSort(long a0, long a1, int a2)
Definition: Native.java:2829
Expr[] getSortUniverse(Sort s)
Definition: Model.java:269
Expr getConstInterp(FuncDecl f)
Definition: Model.java:49
static int modelGetNumSorts(long a0, long a1)
Definition: Native.java:2820
static int modelGetNumConsts(long a0, long a1)
Definition: Native.java:2784
static long getAsArrayFuncDecl(long a0, long a1)
Definition: Native.java:2856
static int getSortKind(long a0, long a1)
Definition: Native.java:1994
static final Z3_sort_kind fromInt(int v)
FuncDecl[] getFuncDecls()
Definition: Model.java:152
Expr eval(Expr t, boolean completion)
Definition: Model.java:211
static boolean isAsArray(long a0, long a1)
Definition: Native.java:2847
FuncDecl[] getConstDecls()
Definition: Model.java:129
static boolean modelEval(long a0, long a1, long a2, boolean a3, LongPtr a4)
Definition: Native.java:2748
static long modelGetFuncDecl(long a0, long a1, int a2)
Definition: Native.java:2811
static long modelGetSortUniverse(long a0, long a1, long a2)
Definition: Native.java:2838
static long modelGetConstDecl(long a0, long a1, int a2)
Definition: Native.java:2793
static long modelGetConstInterp(long a0, long a1, long a2)
Definition: Native.java:2757
static int modelGetNumFuncs(long a0, long a1)
Definition: Native.java:2802
FuncDecl[] getDecls()
Definition: Model.java:167
static String modelToString(long a0, long a1)
Definition: Native.java:3025
static long getRange(long a0, long a1)
Definition: Native.java:2192
static long modelGetFuncInterp(long a0, long a1, long a2)
Definition: Native.java:2775
FuncInterp getFuncInterp(FuncDecl f)
Definition: Model.java:76