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 }
com.microsoft.z3.Native.getSortKind
static int getSortKind(long a0, long a1)
Definition: Native.java:2695
com.microsoft.z3.Native.modelGetNumConsts
static int modelGetNumConsts(long a0, long a1)
Definition: Native.java:3575
com.microsoft.z3.Native.modelGetConstInterp
static long modelGetConstInterp(long a0, long a1, long a2)
Definition: Native.java:3548
com.microsoft.z3.enumerations
Definition: Z3_ast_kind.java:5
com.microsoft.z3.Native.modelGetSortUniverse
static long modelGetSortUniverse(long a0, long a1, long a2)
Definition: Native.java:3629
com.microsoft.z3.FuncDecl
Definition: FuncDecl.java:28
com.microsoft.z3.Model.getFuncDecls
FuncDecl[] getFuncDecls()
Definition: Model.java:149
com.microsoft.z3.Sort
Definition: Sort.java:27
com.microsoft.z3.Native.modelGetFuncDecl
static long modelGetFuncDecl(long a0, long a1, int a2)
Definition: Native.java:3602
com.microsoft.z3.Native.modelGetNumSorts
static int modelGetNumSorts(long a0, long a1)
Definition: Native.java:3611
com.microsoft.z3.ASTVector
Definition: ASTVector.java:23
com.microsoft.z3.Model.eval
Expr eval(Expr t, boolean completion)
Definition: Model.java:208
com.microsoft
com.microsoft.z3.ASTVector.ToExprArray
Expr[] ToExprArray()
Definition: ASTVector.java:129
com.microsoft.z3.Model.getDecls
FuncDecl[] getDecls()
Definition: Model.java:164
com.microsoft.z3.Native.modelGetFuncInterp
static long modelGetFuncInterp(long a0, long a1, long a2)
Definition: Native.java:3566
com.microsoft.z3.Model.getConstDecls
FuncDecl[] getConstDecls()
Definition: Model.java:126
com.microsoft.z3.Native.modelGetSort
static long modelGetSort(long a0, long a1, int a2)
Definition: Native.java:3620
com.microsoft.z3.IDecRefQueue.storeReference
void storeReference(Context ctx, T obj)
Definition: IDecRefQueue.java:56
com.microsoft.z3.Model.getSortUniverse
Expr[] getSortUniverse(Sort s)
Definition: Model.java:268
com.microsoft.z3.Model.getNumConsts
int getNumConsts()
Definition: Model.java:116
com.microsoft.z3.Model.getNumSorts
int getNumSorts()
Definition: Model.java:232
com.microsoft.z3.FuncDecl.getArity
int getArity()
Definition: FuncDecl.java:77
com.microsoft.z3.Model.getFuncInterp
FuncInterp getFuncInterp(FuncDecl f)
Definition: Model.java:73
com.microsoft.z3.Native.LongPtr
Definition: Native.java:6
com.microsoft.z3.Model.getConstInterp
Expr getConstInterp(Expr a)
Definition: Model.java:35
com.microsoft.z3.Model.toString
String toString()
Definition: Model.java:282
com.microsoft.z3.Native.isAsArray
static boolean isAsArray(long a0, long a1)
Definition: Native.java:3647
com.microsoft.z3.Model
Definition: Model.java:25
com.microsoft.z3.Native.modelEval
static boolean modelEval(long a0, long a1, long a2, boolean a3, LongPtr a4)
Definition: Native.java:3539
com.microsoft.z3.Model.ModelEvaluationFailedException
Definition: Model.java:185
com.microsoft.z3.Native
Definition: Native.java:4
com.microsoft.z3
Definition: AlgebraicNum.java:18
com.microsoft.z3.Model.getNumFuncs
int getNumFuncs()
Definition: Model.java:139
com.microsoft.z3.Native.modelGetNumFuncs
static int modelGetNumFuncs(long a0, long a1)
Definition: Native.java:3593
com.microsoft.z3.enumerations.Z3_sort_kind.fromInt
static final Z3_sort_kind fromInt(int v)
Definition: Z3_sort_kind.java:45
com.microsoft.z3.Expr
Definition: Expr.java:31
com.microsoft.z3.Native.modelGetConstDecl
static long modelGetConstDecl(long a0, long a1, int a2)
Definition: Native.java:3584
com.microsoft.z3.Z3Exception
Definition: Z3Exception.java:26
com.microsoft.z3.Model.ModelEvaluationFailedException.ModelEvaluationFailedException
ModelEvaluationFailedException()
Definition: Model.java:189
com.microsoft.z3.Context.getModelDRQ
IDecRefQueue< Model > getModelDRQ()
Definition: Context.java:4063
com
com.microsoft.z3.Native.modelToString
static String modelToString(long a0, long a1)
Definition: Native.java:3858
com.microsoft.z3.Expr.getFuncDecl
FuncDecl getFuncDecl()
Definition: Expr.java:72
com.microsoft.z3.Model.getSorts
Sort[] getSorts()
Definition: Model.java:248
com.microsoft.z3.enumerations.Z3_sort_kind
Definition: Z3_sort_kind.java:13
com.microsoft.z3.Context
Definition: Context.java:35
com.microsoft.z3.enumerations.Z3_sort_kind.Z3_ARRAY_SORT
Z3_ARRAY_SORT
Definition: Z3_sort_kind.java:19
com.microsoft.z3.Native.getAsArrayFuncDecl
static long getAsArrayFuncDecl(long a0, long a1)
Definition: Native.java:3656
com.microsoft.z3.Model.evaluate
Expr evaluate(Expr t, boolean completion)
Definition: Model.java:223
com.microsoft.z3.Native.getRange
static long getRange(long a0, long a1)
Definition: Native.java:2947
com.microsoft.z3.FuncInterp
Definition: FuncInterp.java:25
com.microsoft.z3.Model.getConstInterp
Expr getConstInterp(FuncDecl f)
Definition: Model.java:50
com.microsoft.z3.Z3Object
Definition: Z3Object.java:24
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10111