Z3 |

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

## Data Structures
class | ModelEvaluationFailedException

## Public Member Functions
int | getNumConsts ()
FuncDecl<?>[] | getConstDecls ()
int | getNumFuncs ()
FuncDecl<?>[] | getFuncDecls ()
FuncDecl<?>[] | getDecls ()
int | getNumSorts ()
Sort[] | getSorts ()
String | toString ()

## Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[] | arrayToNative (Z3Object[] a)
static int | arrayLength (Z3Object[] a)

## Detailed Description

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

Definition at line 26 of file Model.java.

## Member Function Documentation

## ◆ getConstDecls()

FuncDecl<?>[] getConstDecls | ( |  | ) |
| inline

The function declarations of the constants in the model.

Exceptions

  Z3Exception |

Definition at line 127 of file Model.java.

128 {
129 int n = getNumConsts();
130 FuncDecl<?>[] res = new FuncDecl[n];
131 for (int i = 0; i < n; i++)
132 res[i] = new FuncDecl<>(getContext(), Native.modelGetConstDecl(getContext()
133 .nCtx(), getNativeObject(), i));
134 return res;
135 }
com.microsoft.z3.FuncDecl<?>
com.microsoft.z3.Model.getNumConsts
int getNumConsts()
Definition: Model.java:117

## ◆ getDecls()

FuncDecl<?>[] getDecls | ( |  | ) |
| inline

All symbols that have an interpretation in the model.

Exceptions

  Z3Exception |

Definition at line 165 of file Model.java.

166 {
167 int nFuncs = getNumFuncs();
168 int nConsts = getNumConsts();
169 int n = nFuncs + nConsts;
170 FuncDecl<?>[] res = new FuncDecl[n];
171 for (int i = 0; i < nConsts; i++)
172 res[i] = new FuncDecl<>(getContext(), Native.modelGetConstDecl(getContext()
173 .nCtx(), getNativeObject(), i));
174 for (int i = 0; i < nFuncs; i++)
175 res[nConsts + i] = new FuncDecl<>(getContext(), Native.modelGetFuncDecl(
176 getContext().nCtx(), getNativeObject(), i));
177 return res;
178 }
com.microsoft.z3.Model.getNumFuncs
int getNumFuncs()
Definition: Model.java:140

## ◆ getFuncDecls()

FuncDecl<?>[] getFuncDecls | ( |  | ) |
| inline

The function declarations of the function interpretations in the model.

Exceptions

  Z3Exception |

Definition at line 150 of file Model.java.

151 {
152 int n = getNumFuncs();
153 FuncDecl<?>[] res = new FuncDecl[n];
154 for (int i = 0; i < n; i++)
155 res[i] = new FuncDecl<>(getContext(), Native.modelGetFuncDecl(getContext()
156 .nCtx(), getNativeObject(), i));
157 return res;
158 }

## ◆ getNumConsts()

int getNumConsts | ( |  | ) |
| inline

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

Definition at line 117 of file Model.java.

118 {
119 return Native.modelGetNumConsts(getContext().nCtx(), getNativeObject());
120 }

## ◆ getNumFuncs()

int getNumFuncs | ( |  | ) |
| inline

The number of function interpretations in the model.

Definition at line 140 of file Model.java.

141 {
142 return Native.modelGetNumFuncs(getContext().nCtx(), getNativeObject());
143 }

## ◆ getNumSorts()

int getNumSorts | ( |  | ) |
| inline

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

Definition at line 233 of file Model.java.

234 {
235 return Native.modelGetNumSorts(getContext().nCtx(), getNativeObject());
236 }

## ◆ getSorts()

Sort[] getSorts | ( |  | ) |
| inline

The uninterpreted sorts that the model has an interpretation for. Remarks: Z3 also provides an interpretation 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 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 }
com.microsoft.z3.Model.getNumSorts
int getNumSorts()
Definition: Model.java:233

## ◆ toString()

String toString | ( |  | ) |
| inline

Conversion of models to strings.

Returns
  A string representation of the model.

Definition at line 283 of file Model.java.

283 {
284 return Native.modelToString(getContext().nCtx(), getNativeObject());
285 }