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

◆ getDecls()

FuncDecl<?> [] getDecls ( )
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  }

◆ getFuncDecls()

FuncDecl<?> [] getFuncDecls ( )
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  }

◆ getNumConsts()

int getNumConsts ( )
inline

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

Definition at line 119 of file Model.java.

120  {
121  return Native.modelGetNumConsts(getContext().nCtx(), getNativeObject());
122  }

◆ getNumFuncs()

int getNumFuncs ( )
inline

The number of function interpretations in the model.

Definition at line 142 of file Model.java.

143  {
144  return Native.modelGetNumFuncs(getContext().nCtx(), getNativeObject());
145  }

◆ getNumSorts()

int getNumSorts ( )
inline

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

Definition at line 235 of file Model.java.

236  {
237  return Native.modelGetNumSorts(getContext().nCtx(), getNativeObject());
238  }

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

◆ toString()

String toString ( )
inline

Conversion of models to strings.

Returns
A string representation of the model.

Definition at line 285 of file Model.java.

285  {
286  return Native.modelToString(getContext().nCtx(), getNativeObject());
287  }