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