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

Referenced by Model.evaluate().

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

§ evaluate()

Expr evaluate ( Expr  t,
boolean  completion 
)
inline

Alias for

Eval

.

Exceptions
Z3Exception

Definition at line 226 of file Model.java.

227  {
228  return eval(t, completion);
229  }
Expr eval(Expr t, boolean completion)
Definition: Model.java:211

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

§ 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

§ 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  || Native.getSortKind(getContext().nCtx(),
55  Native.getRange(getContext().nCtx(), f.getNativeObject())) == Z3_sort_kind.Z3_ARRAY_SORT
56  .toInt())
57  throw new Z3Exception(
58  "Non-zero arity functions and arrays have FunctionInterpretations as a model. Use getFuncInterp.");
59 
60  long n = Native.modelGetConstInterp(getContext().nCtx(), getNativeObject(),
61  f.getNativeObject());
62  if (n == 0)
63  return null;
64  else
65  return Expr.create(getContext(), n);
66  }
Z3_sort_kind
The different kinds of Z3 types (See #Z3_get_sort_kind).
Definition: z3_api.h:153

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

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

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

§ getNumConsts()

int getNumConsts ( )
inline

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

Definition at line 119 of file Model.java.

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

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.

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

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.

Referenced by Model.getSorts().

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

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

272  {
273 
274  ASTVector nUniv = new ASTVector(getContext(), Native.modelGetSortUniverse(
275  getContext().nCtx(), getNativeObject(), s.getNativeObject()));
276  return nUniv.ToExprArray();
277  }

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