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

Data Structures

class  ModelEvaluationFailedException
 

Public Member Functions

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

Additional Inherited Members

- Protected Member Functions inherited from Z3Object
void finalize ()
 

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 
)
inline

Evaluates the expression

t

in the current model. Remarks: 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
completion
When 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 
)
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 ( )
inline

The function declarations of the constants in the model.

Exceptions
Z3Exception

Definition at line 130 of file Model.java.

131  {
132  int n = getNumConsts();
133  FuncDecl[] res = new FuncDecl[n];
134  for (int i = 0; i < n; i++)
135  res[i] = new FuncDecl(getContext(), Native.modelGetConstDecl(getContext()
136  .nCtx(), getNativeObject(), i));
137  return res;
138  }
Expr getConstInterp ( Expr  a)
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 36 of file Model.java.

37  {
38  getContext().checkContextMatch(a);
39  return getConstInterp(a.getFuncDecl());
40  }
Expr getConstInterp(Expr a)
Definition: Model.java:36
Expr getConstInterp ( FuncDecl  f)
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 51 of file Model.java.

52  {
53  getContext().checkContextMatch(f);
54  if (f.getArity() != 0
55  || Native.getSortKind(getContext().nCtx(),
56  Native.getRange(getContext().nCtx(), f.getNativeObject())) == Z3_sort_kind.Z3_ARRAY_SORT
57  .toInt())
58  throw new Z3Exception(
59  "Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.");
60 
61  long n = Native.modelGetConstInterp(getContext().nCtx(), getNativeObject(),
62  f.getNativeObject());
63  if (n == 0)
64  return null;
65  else
66  return Expr.create(getContext(), n);
67  }
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:194
FuncDecl [] getDecls ( )
inline

All symbols that have an interpretation in the model.

Exceptions
Z3Exception

Definition at line 168 of file Model.java.

169  {
170  int nFuncs = getNumFuncs();
171  int nConsts = getNumConsts();
172  int n = nFuncs + nConsts;
173  FuncDecl[] res = new FuncDecl[n];
174  for (int i = 0; i < nConsts; i++)
175  res[i] = new FuncDecl(getContext(), Native.modelGetConstDecl(getContext()
176  .nCtx(), getNativeObject(), i));
177  for (int i = 0; i < nFuncs; i++)
178  res[nConsts + i] = new FuncDecl(getContext(), Native.modelGetFuncDecl(
179  getContext().nCtx(), getNativeObject(), i));
180  return res;
181  }
FuncDecl [] getFuncDecls ( )
inline

The function declarations of the function interpretations in the model.

Exceptions
Z3Exception

Definition at line 153 of file Model.java.

154  {
155  int n = getNumFuncs();
156  FuncDecl[] res = new FuncDecl[n];
157  for (int i = 0; i < n; i++)
158  res[i] = new FuncDecl(getContext(), Native.modelGetFuncDecl(getContext()
159  .nCtx(), getNativeObject(), i));
160  return res;
161  }
FuncInterp getFuncInterp ( FuncDecl  f)
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 77 of file Model.java.

78  {
79  getContext().checkContextMatch(f);
80 
81  Z3_sort_kind sk = Z3_sort_kind.fromInt(Native.getSortKind(getContext()
82  .nCtx(), Native.getRange(getContext().nCtx(), f.getNativeObject())));
83 
84  if (f.getArity() == 0)
85  {
86  long n = Native.modelGetConstInterp(getContext().nCtx(),
87  getNativeObject(), f.getNativeObject());
88 
89  if (sk == Z3_sort_kind.Z3_ARRAY_SORT)
90  {
91  if (n == 0)
92  return null;
93  else
94  {
95  if (Native.isAsArray(getContext().nCtx(), n) ^ true)
96  throw new Z3Exception(
97  "Argument was not an array constant");
98  long fd = Native.getAsArrayFuncDecl(getContext().nCtx(), n);
99  return getFuncInterp(new FuncDecl(getContext(), fd));
100  }
101  } else
102  {
103  throw new Z3Exception(
104  "Constant functions do not have a function interpretation; use ConstInterp");
105  }
106  } else
107  {
108  long n = Native.modelGetFuncInterp(getContext().nCtx(),
109  getNativeObject(), f.getNativeObject());
110  if (n == 0)
111  return null;
112  else
113  return new FuncInterp(getContext(), n);
114  }
115  }
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:194
FuncInterp getFuncInterp(FuncDecl f)
Definition: Model.java:77
int getNumConsts ( )
inline

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

Definition at line 120 of file Model.java.

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

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

The number of function interpretations in the model.

Definition at line 143 of file Model.java.

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

144  {
145  return Native.modelGetNumFuncs(getContext().nCtx(), getNativeObject());
146  }
int getNumSorts ( )
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 ( )
inline

The uninterpreted sorts that the model has an interpretation for. Remarks: 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
getNumSorts
getSortUniverse
Exceptions
Z3Exception

Definition at line 251 of file Model.java.

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

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

s

.

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

Definition at line 271 of file Model.java.

272  {
273 
274  ASTVector nUniv = new ASTVector(getContext(), Native.modelGetSortUniverse(
275  getContext().nCtx(), getNativeObject(), s.getNativeObject()));
276  return nUniv.ToExprArray();
277  }
String toString ( )
inline

Conversion of models to strings.

Returns
A string representation of the model.

Definition at line 284 of file Model.java.

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