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  || Native.getSortKind(getContext().nCtx(),
55  Native.getRange(getContext().nCtx(), f.getNativeObject())) == Z3_sort_kind.Z3_ARRAY_SORT
56  .toInt())
57  throw new Z3Exception(
58  "Non-zero arity functions and arrays have FunctionInterpretations as a model. Use getFuncInterp.");
59 
60  long n = Native.modelGetConstInterp(getContext().nCtx(), getNativeObject(),
61  f.getNativeObject());
62  if (n == 0)
63  return null;
64  else
65  return Expr.create(getContext(), n);
66  }
67 
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))
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 getConstInterp");
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()
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()
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()
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)
212  {
213  Native.LongPtr v = new Native.LongPtr();
214  if (!Native.modelEval(getContext().nCtx(), getNativeObject(),
215  t.getNativeObject(), (completion), v))
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  @Override
285  public String toString() {
286  return Native.modelToString(getContext().nCtx(), getNativeObject());
287  }
288 
289  Model(Context ctx, long obj)
290  {
291  super(ctx, obj);
292  }
293 
294  @Override
295  void incRef() {
296  Native.modelIncRef(getContext().nCtx(), getNativeObject());
297  }
298 
299  @Override
300  void addToReferenceQueue() {
301  getContext().getModelDRQ().storeReference(getContext(), this);
302  }
303 }
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:3219
Sort [] getSorts()
Definition: Model.java:251
Expr [] getSortUniverse(Sort s)
Definition: Model.java:271
Expr getConstInterp(FuncDecl f)
Definition: Model.java:50
static int modelGetNumSorts(long a0, long a1)
Definition: Native.java:3210
static int modelGetNumConsts(long a0, long a1)
Definition: Native.java:3174
static long getAsArrayFuncDecl(long a0, long a1)
Definition: Native.java:3246
static int getSortKind(long a0, long a1)
Definition: Native.java:2348
static final Z3_sort_kind fromInt(int v)
FuncDecl [] getFuncDecls()
Definition: Model.java:152
Expr eval(Expr t, boolean completion)
Definition: Model.java:211
IDecRefQueue< Model > getModelDRQ()
Definition: Context.java:3969
static boolean isAsArray(long a0, long a1)
Definition: Native.java:3237
void storeReference(Context ctx, T obj)
FuncDecl [] getConstDecls()
Definition: Model.java:129
static boolean modelEval(long a0, long a1, long a2, boolean a3, LongPtr a4)
Definition: Native.java:3138
static long modelGetFuncDecl(long a0, long a1, int a2)
Definition: Native.java:3201
FuncDecl getFuncDecl()
Definition: Expr.java:72
static long modelGetSortUniverse(long a0, long a1, long a2)
Definition: Native.java:3228
static long modelGetConstDecl(long a0, long a1, int a2)
Definition: Native.java:3183
static long modelGetConstInterp(long a0, long a1, long a2)
Definition: Native.java:3147
static void modelIncRef(long a0, long a1)
Definition: Native.java:3122
static int modelGetNumFuncs(long a0, long a1)
Definition: Native.java:3192
FuncDecl [] getDecls()
Definition: Model.java:167
static String modelToString(long a0, long a1)
Definition: Native.java:3415
static long getRange(long a0, long a1)
Definition: Native.java:2582
static long modelGetFuncInterp(long a0, long a1, long a2)
Definition: Native.java:3165
def String(name, ctx=None)
Definition: z3py.py:9443
FuncInterp getFuncInterp(FuncDecl f)
Definition: Model.java:76