Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
Public Member Functions
Model Class Reference
+ Inheritance diagram for Model:

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

Detailed Description

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

Definition at line 25 of file Model.java.

Member Function Documentation

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  }
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
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:146
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  }
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  }
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  long fd = Native.getAsArrayFuncDecl(getContext().nCtx(), n);
96  return getFuncInterp(new FuncDecl(getContext(), fd));
97  }
98  return null;
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:146
FuncInterp getFuncInterp(FuncDecl f)
Definition: Model.java:76
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  }
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  }