Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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  long fd = Native.getAsArrayFuncDecl(getContext().nCtx(), n);
96  return getFuncInterp(new FuncDecl(getContext(), fd));
97  }
98  return null;
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")
187  public class ModelEvaluationFailedException extends Z3Exception
188  {
192  public ModelEvaluationFailedException()
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 
271  public Expr[] getSortUniverse(Sort s)
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 getConstInterp(Expr a)
Definition: Model.java:35
Expr getConstInterp(FuncDecl f)
Definition: Model.java:50
static int modelGetNumConsts(long a0, long a1)
Definition: Native.java:3542
static long getAsArrayFuncDecl(long a0, long a1)
Definition: Native.java:3623
static int getSortKind(long a0, long a1)
Definition: Native.java:2662
static final Z3_sort_kind fromInt(int v)
FuncDecl[] getFuncDecls()
Definition: Model.java:152
def String
Definition: z3py.py:10043
IDecRefQueue< Model > getModelDRQ()
Definition: Context.java:4061
static boolean isAsArray(long a0, long a1)
Definition: Native.java:3614
FuncDecl[] getConstDecls()
Definition: Model.java:129
static long modelGetFuncDecl(long a0, long a1, int a2)
Definition: Native.java:3569
FuncDecl getFuncDecl()
Definition: Expr.java:72
static long modelGetConstDecl(long a0, long a1, int a2)
Definition: Native.java:3551
def Model
Definition: z3py.py:6216
static long modelGetConstInterp(long a0, long a1, long a2)
Definition: Native.java:3515
static int modelGetNumFuncs(long a0, long a1)
Definition: Native.java:3560
FuncDecl[] getDecls()
Definition: Model.java:167
static long getRange(long a0, long a1)
Definition: Native.java:2914
static long modelGetFuncInterp(long a0, long a1, long a2)
Definition: Native.java:3533
FuncInterp getFuncInterp(FuncDecl f)
Definition: Model.java:76