Z3
Data Structures | Public Member Functions
Model Class Reference
+ Inheritance diagram for Model:

Data Structures

class  ModelEvaluationFailedException
 

Public Member Functions

Expr getConstInterp (Expr a) throws Z3Exception
 
Expr getConstInterp (FuncDecl f) throws Z3Exception
 
FuncInterp getFuncInterp (FuncDecl f) throws Z3Exception
 
int getNumConsts () throws Z3Exception
 
FuncDecl[] getConstDecls () throws Z3Exception
 
int getNumFuncs () throws Z3Exception
 
FuncDecl[] getFuncDecls () throws Z3Exception
 
FuncDecl[] getDecls () throws Z3Exception
 
Expr eval (Expr t, boolean completion) throws Z3Exception
 
Expr evaluate (Expr t, boolean completion) throws Z3Exception
 
int getNumSorts () throws Z3Exception
 
Sort[] getSorts () throws Z3Exception
 
Expr[] getSortUniverse (Sort s) throws Z3Exception
 
String toString ()
 
- Public Member Functions inherited from Z3Object
void dispose () throws Z3Exception
 
- Public Member Functions inherited from IDisposable
void dispose () throws Z3Exception
 

Additional Inherited Members

- Protected Member Functions inherited from Z3Object
void finalize () throws Z3Exception
 

Detailed Description

A Model contains interpretations (assignments) of constants and functions.

Definition at line 25 of file Model.java.

Member Function Documentation

Expr eval ( Expr  t,
boolean  completion 
) throws Z3Exception
inline

Evaluates the expression t in the current model.

This function may fail if t contains quantifiers, is partial (MODEL_PARTIAL enabled), or if t is not well-sorted. In this case a

ModelEvaluationFailedException

is thrown.

Parameters
tAn expression
completionWhen this flag is enabled, a model value will be assigned to any constant or function that does not have an interpretation in the model.
Returns
The evaluation of t in the model.
Exceptions
Z3Exception

Definition at line 211 of file Model.java.

Referenced by Model.evaluate().

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  }
Expr evaluate ( Expr  t,
boolean  completion 
) throws Z3Exception
inline

Alias for Eval.

Exceptions
Z3Exception

Definition at line 226 of file Model.java.

227  {
228  return eval(t, completion);
229  }
Expr eval(Expr t, boolean completion)
Definition: Model.java:211
FuncDecl [] getConstDecls ( ) throws Z3Exception
inline

The function declarations of the constants in the model.

Exceptions
Z3Exception

Definition at line 129 of file Model.java.

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  }
Expr getConstInterp ( Expr  a) throws Z3Exception
inline

Retrieves the interpretation (the assignment) of a in the model.

Parameters
aA Constant
Returns
An expression if the constant has an interpretation in the model, null otherwise.
Exceptions
Z3Exception

Definition at line 35 of file Model.java.

36  {
37  getContext().checkContextMatch(a);
38  return getConstInterp(a.getFuncDecl());
39  }
Expr getConstInterp(Expr a)
Definition: Model.java:35
Expr getConstInterp ( FuncDecl  f) throws Z3Exception
inline

Retrieves the interpretation (the assignment) of f in the model.

Parameters
fA function declaration of zero arity
Returns
An expression if the function has an interpretation in the model, null otherwise.
Exceptions
Z3Exception

Definition at line 49 of file Model.java.

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  }
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:186
FuncDecl [] getDecls ( ) throws Z3Exception
inline

All symbols that have an interpretation in the model.

Exceptions
Z3Exception

Definition at line 167 of file Model.java.

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  }
FuncDecl [] getFuncDecls ( ) throws Z3Exception
inline

The function declarations of the function interpretations in the model.

Exceptions
Z3Exception

Definition at line 152 of file Model.java.

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  }
FuncInterp getFuncInterp ( FuncDecl  f) throws Z3Exception
inline

Retrieves the interpretation (the assignment) of a non-constant f in the model.

Parameters
fA function declaration of non-zero arity
Returns
A FunctionInterpretation if the function has an interpretation in the model, null otherwise.
Exceptions
Z3Exception

Definition at line 76 of file Model.java.

77  {
78  getContext().checkContextMatch(f);
79 
80  Z3_sort_kind sk = Z3_sort_kind.fromInt(Native.getSortKind(getContext()
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  }
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:186
FuncInterp getFuncInterp(FuncDecl f)
Definition: Model.java:76
int getNumConsts ( ) throws Z3Exception
inline

The number of constants that have an interpretation in the model.

Definition at line 119 of file Model.java.

Referenced by Model.getConstDecls(), and Model.getDecls().

120  {
121  return Native.modelGetNumConsts(getContext().nCtx(), getNativeObject());
122  }
int getNumFuncs ( ) throws Z3Exception
inline

The number of function interpretations in the model.

Definition at line 142 of file Model.java.

Referenced by Model.getDecls(), and Model.getFuncDecls().

143  {
144  return Native.modelGetNumFuncs(getContext().nCtx(), getNativeObject());
145  }
int getNumSorts ( ) throws Z3Exception
inline

The number of uninterpreted sorts that the model has an interpretation for.

Definition at line 235 of file Model.java.

Referenced by Model.getSorts().

236  {
237  return Native.modelGetNumSorts(getContext().nCtx(), getNativeObject());
238  }
Sort [] getSorts ( ) throws Z3Exception
inline

The uninterpreted sorts that the model has an interpretation for.

Z3 also provides an intepretation for uninterpreted sorts used in a formula. The interpretation for a sort is a finite set of distinct values. We say this finite set is the "universe" of the sort.

See also
NumSorts, SortUniverse
Exceptions
Z3Exception

Definition at line 249 of file Model.java.

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  }
Expr [] getSortUniverse ( Sort  s) throws Z3Exception
inline

The finite set of distinct values that represent the interpretation for sort s .

See also
Sorts
Parameters
sAn uninterpreted sort
Returns
An array of expressions, where each is an element of the universe of s
Exceptions
Z3Exception

Definition at line 269 of file Model.java.

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  }
String toString ( )
inline

Conversion of models to strings.

Returns
A string representation of the model.

Definition at line 286 of file Model.java.

287  {
288  try
289  {
290  return Native.modelToString(getContext().nCtx(), getNativeObject());
291  } catch (Z3Exception e)
292  {
293  return "Z3Exception: " + e.getMessage();
294  }
295  }