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

Detailed Description

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

Definition at line 25 of file Model.java.

Member Function Documentation

◆ eval()

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
tthe expression to evaluate
completionAn 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 208 of file Model.java.

209 {
210 Native.LongPtr v = new Native.LongPtr();
211 if (!Native.modelEval(getContext().nCtx(), getNativeObject(),
212 t.getNativeObject(), (completion), v))
213 throw new ModelEvaluationFailedException();
214 else
215 return Expr.create(getContext(), v.value);
216 }

Referenced by Model.evaluate(), and ModelRef.evaluate().

◆ evaluate()

Expr evaluate ( Expr  t,
boolean  completion 
)
inline

Alias for Eval.

Exceptions
Z3Exception

Definition at line 223 of file Model.java.

224 {
225 return eval(t, completion);
226 }
Expr eval(Expr t, boolean completion)
Definition: Model.java:208

◆ getConstDecls()

FuncDecl[] getConstDecls ( )
inline

The function declarations of the constants in the model.

Exceptions
Z3Exception

Definition at line 126 of file Model.java.

127 {
128 int n = getNumConsts();
129 FuncDecl[] res = new FuncDecl[n];
130 for (int i = 0; i < n; i++)
131 res[i] = new FuncDecl(getContext(), Native.modelGetConstDecl(getContext()
132 .nCtx(), getNativeObject(), i));
133 return res;
134 }

◆ getConstInterp() [1/2]

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 35 of file Model.java.

36 {
37 getContext().checkContextMatch(a);
38 return getConstInterp(a.getFuncDecl());
39 }
Expr getConstInterp(Expr a)
Definition: Model.java:35

Referenced by Model.getConstInterp().

◆ getConstInterp() [2/2]

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 50 of file Model.java.

51 {
52 getContext().checkContextMatch(f);
53 if (f.getArity() != 0)
54 throw new Z3Exception(
55 "Non-zero arity functions have FunctionInterpretations as a model. Use getFuncInterp.");
56
57 long n = Native.modelGetConstInterp(getContext().nCtx(), getNativeObject(),
58 f.getNativeObject());
59 if (n == 0)
60 return null;
61 else
62 return Expr.create(getContext(), n);
63 }

◆ getDecls()

FuncDecl[] getDecls ( )
inline

All symbols that have an interpretation in the model.

Exceptions
Z3Exception

Definition at line 164 of file Model.java.

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

◆ getFuncDecls()

FuncDecl[] getFuncDecls ( )
inline

The function declarations of the function interpretations in the model.

Exceptions
Z3Exception

Definition at line 149 of file Model.java.

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

◆ getFuncInterp()

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 73 of file Model.java.

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

Referenced by Model.getFuncInterp().

◆ getNumConsts()

int getNumConsts ( )
inline

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

Definition at line 116 of file Model.java.

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

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

◆ getNumFuncs()

int getNumFuncs ( )
inline

The number of function interpretations in the model.

Definition at line 139 of file Model.java.

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

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

◆ getNumSorts()

int getNumSorts ( )
inline

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

Definition at line 232 of file Model.java.

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

Referenced by Model.getSorts().

◆ 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 248 of file Model.java.

249 {
250
251 int n = getNumSorts();
252 Sort[] res = new Sort[n];
253 for (int i = 0; i < n; i++)
254 res[i] = Sort.create(getContext(),
255 Native.modelGetSort(getContext().nCtx(), getNativeObject(), i));
256 return res;
257 }

◆ getSortUniverse()

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 268 of file Model.java.

269 {
270
271 ASTVector nUniv = new ASTVector(getContext(), Native.modelGetSortUniverse(
272 getContext().nCtx(), getNativeObject(), s.getNativeObject()));
273 return nUniv.ToExprArray();
274 }

◆ toString()

String toString ( )
inline

Conversion of models to strings.

Returns
A string representation of the model.

Definition at line 282 of file Model.java.

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