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

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

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

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

◆ 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  }
com.microsoft.z3.Model.eval
Expr eval(Expr t, boolean completion)
Definition: Model.java:208
com.microsoft.z3.Model.getNumConsts
int getNumConsts()
Definition: Model.java:116
com.microsoft.z3.Model.getNumSorts
int getNumSorts()
Definition: Model.java:232
com.microsoft.z3.Model.getFuncInterp
FuncInterp getFuncInterp(FuncDecl f)
Definition: Model.java:73
com.microsoft.z3.Model.getConstInterp
Expr getConstInterp(Expr a)
Definition: Model.java:35
Z3_sort_kind
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:147
com.microsoft.z3.Model.getNumFuncs
int getNumFuncs()
Definition: Model.java:139