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  }

◆ 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  }

◆ 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(R s)
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  }

◆ 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  }