Z3
Data Structures | Public Member Functions | Properties
Model Class Reference

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

+ Inheritance diagram for Model:

Data Structures

class  DecRefQueue
 
class  ModelEvaluationFailedException
 A ModelEvaluationFailedException is thrown when an expression cannot be evaluated by the model. More...
 

Public Member Functions

Expr ConstInterp (Expr a)
 Retrieves the interpretation (the assignment) of a in the model. More...
 
Expr ConstInterp (FuncDecl f)
 Retrieves the interpretation (the assignment) of f in the model. More...
 
FuncInterp FuncInterp (FuncDecl f)
 Retrieves the interpretation (the assignment) of a non-constant f in the model. More...
 
Expr Eval (Expr t, bool completion=false)
 Evaluates the expression t in the current model. More...
 
Expr Evaluate (Expr t, bool completion=false)
 Alias for Eval. More...
 
double Double (Expr t)
 Evaluate expression to a double, assuming it is a numeral already. More...
 
Expr[] SortUniverse (Sort s)
 The finite set of distinct values that represent the interpretation for sort s . More...
 
override string ToString ()
 Conversion of models to strings. More...
 
- Public Member Functions inherited from Z3Object
void Dispose ()
 Disposes of the underlying native Z3 object. More...
 

Properties

uint NumConsts [get]
 The number of constants that have an interpretation in the model. More...
 
FuncDecl[] ConstDecls [get]
 The function declarations of the constants in the model. More...
 
IEnumerable< KeyValuePair< FuncDecl, Expr > > Consts [get]
 Enumerate constants in model. More...
 
uint NumFuncs [get]
 The number of function interpretations in the model. More...
 
FuncDecl[] FuncDecls [get]
 The function declarations of the function interpretations in the model. More...
 
FuncDecl[] Decls [get]
 All symbols that have an interpretation in the model. More...
 
uint NumSorts [get]
 The number of uninterpreted sorts that the model has an interpretation for. More...
 
Sort[] Sorts [get]
 The uninterpreted sorts that the model has an interpretation for. More...
 

Detailed Description

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

Definition at line 29 of file Model.cs.

Member Function Documentation

◆ ConstInterp() [1/2]

Expr ConstInterp ( 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.

Definition at line 36 of file Model.cs.

37  {
38  Debug.Assert(a != null);
39 
40  Context.CheckContextMatch(a);
41  return ConstInterp(a.FuncDecl);
42  }

◆ ConstInterp() [2/2]

Expr ConstInterp ( 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.


Definition at line 49 of file Model.cs.

50  {
51  Debug.Assert(f != null);
52 
53  Context.CheckContextMatch(f);
54  if (f.Arity != 0)
55  throw new Z3Exception("Non-zero arity functions have FunctionInterpretations as a model. Use FuncInterp.");
56 
57  IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject);
58  if (n == IntPtr.Zero)
59  return null;
60  else
61  return Expr.Create(Context, n);
62  }

◆ Double()

double Double ( Expr  t)
inline

Evaluate expression to a double, assuming it is a numeral already.

Definition at line 243 of file Model.cs.

243  {
244  var r = Eval(t, true);
245  return Native.Z3_get_numeral_double(Context.nCtx, r.NativeObject);
246  }

◆ Eval()

Expr Eval ( Expr  t,
bool  completion = false 
)
inline

Evaluates the expression t in the current model.

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
tAn expression
completionWhen 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.


Definition at line 219 of file Model.cs.

220  {
221  Debug.Assert(t != null);
222 
223  IntPtr v = IntPtr.Zero;
224  if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (byte)(completion ? 1 : 0), ref v) == (byte)0)
225  throw new ModelEvaluationFailedException();
226  else
227  return Expr.Create(Context, v);
228  }

Referenced by Model.Double(), and Model.Evaluate().

◆ Evaluate()

Expr Evaluate ( Expr  t,
bool  completion = false 
)
inline

Alias for Eval.


Definition at line 233 of file Model.cs.

234  {
235  Debug.Assert(t != null);
236 
237  return Eval(t, completion);
238  }

◆ FuncInterp()

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.


Definition at line 69 of file Model.cs.

70  {
71  Debug.Assert(f != null);
72 
73  Context.CheckContextMatch(f);
74 
75  Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_range(Context.nCtx, f.NativeObject));
76 
77  if (f.Arity == 0)
78  {
79  IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject);
80 
81  if (sk == Z3_sort_kind.Z3_ARRAY_SORT)
82  {
83  if (n == IntPtr.Zero)
84  return null;
85  else
86  {
87  if (Native.Z3_is_as_array(Context.nCtx, n) == 0)
88  throw new Z3Exception("Argument was not an array constant");
89  IntPtr fd = Native.Z3_get_as_array_func_decl(Context.nCtx, n);
90  return FuncInterp(new FuncDecl(Context, fd));
91  }
92  }
93  else
94  {
95  throw new Z3Exception("Constant functions do not have a function interpretation; use ConstInterp");
96  }
97  }
98  else
99  {
100  IntPtr n = Native.Z3_model_get_func_interp(Context.nCtx, NativeObject, f.NativeObject);
101  if (n == IntPtr.Zero)
102  return null;
103  else
104  return new FuncInterp(Context, n);
105  }
106  }

◆ SortUniverse()

Expr [] SortUniverse ( Sort  s)
inline

The finite set of distinct values that represent the interpretation for sort s .

See also
Sorts
Parameters
sAn uninterpreted sort
Returns
An array of expressions, where each is an element of the universe of s

Definition at line 282 of file Model.cs.

283  {
284  Debug.Assert(s != null);
285 
286  ASTVector av = new ASTVector(Context, Native.Z3_model_get_sort_universe(Context.nCtx, NativeObject, s.NativeObject));
287  return av.ToExprArray();
288  }

◆ ToString()

override string ToString ( )
inline

Conversion of models to strings.

Returns
A string representation of the model.

Definition at line 294 of file Model.cs.

295  {
296  return Native.Z3_model_to_string(Context.nCtx, NativeObject);
297  }

Property Documentation

◆ ConstDecls

FuncDecl [] ConstDecls
get

The function declarations of the constants in the model.

Definition at line 120 of file Model.cs.

120  {
121  get
122  {
123 
124  uint n = NumConsts;
125  FuncDecl[] res = new FuncDecl[n];
126  for (uint i = 0; i < n; i++)
127  res[i] = new FuncDecl(Context, Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i));
128  return res;
129  }
130  }

◆ Consts

IEnumerable<KeyValuePair<FuncDecl, Expr> > Consts
get

Enumerate constants in model.

Definition at line 136 of file Model.cs.

136  {
137  get
138  {
139  uint nc = NumConsts;
140  for (uint i = 0; i < nc; ++i)
141  {
142  var f = new FuncDecl(Context, Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i));
143  IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject);
144  if (n == IntPtr.Zero) continue;
145  yield return new KeyValuePair<FuncDecl, Expr>(f, Expr.Create(Context, n));
146  }
147  }
148  }

◆ Decls

FuncDecl [] Decls
get

All symbols that have an interpretation in the model.

Definition at line 178 of file Model.cs.

178  {
179  get
180  {
181 
182  uint nFuncs = NumFuncs;
183  uint nConsts = NumConsts;
184  uint n = nFuncs + nConsts;
185  FuncDecl[] res = new FuncDecl[n];
186  for (uint i = 0; i < nConsts; i++)
187  res[i] = new FuncDecl(Context, Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i));
188  for (uint i = 0; i < nFuncs; i++)
189  res[nConsts + i] = new FuncDecl(Context, Native.Z3_model_get_func_decl(Context.nCtx, NativeObject, i));
190  return res;
191  }
192  }

◆ FuncDecls

FuncDecl [] FuncDecls
get

The function declarations of the function interpretations in the model.

Definition at line 162 of file Model.cs.

162  {
163  get
164  {
165 
166  uint n = NumFuncs;
167  FuncDecl[] res = new FuncDecl[n];
168  for (uint i = 0; i < n; i++)
169  res[i] = new FuncDecl(Context, Native.Z3_model_get_func_decl(Context.nCtx, NativeObject, i));
170  return res;
171  }
172  }

◆ NumConsts

uint NumConsts
get

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

Definition at line 112 of file Model.cs.

112  {
113  get { return Native.Z3_model_get_num_consts(Context.nCtx, NativeObject); }
114  }

◆ NumFuncs

uint NumFuncs
get

The number of function interpretations in the model.

Definition at line 154 of file Model.cs.

154  {
155  get { return Native.Z3_model_get_num_funcs(Context.nCtx, NativeObject); }
156  }

◆ NumSorts

uint NumSorts
get

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


Definition at line 251 of file Model.cs.

251 { get { return Native.Z3_model_get_num_sorts(Context.nCtx, NativeObject); } }

◆ Sorts

Sort [] Sorts
get

The uninterpreted sorts that the model has an interpretation for.

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
NumSorts, SortUniverse

Definition at line 264 of file Model.cs.

264  {
265  get
266  {
267 
268  uint n = NumSorts;
269  Sort[] res = new Sort[n];
270  for (uint i = 0; i < n; i++)
271  res[i] = Sort.Create(Context, Native.Z3_model_get_sort(Context.nCtx, NativeObject, i));
272  return res;
273  }
274  }
Microsoft.Z3.Model.NumFuncs
uint NumFuncs
The number of function interpretations in the model.
Definition: Model.cs:154
Microsoft.Z3.Model.Eval
Expr Eval(Expr t, bool completion=false)
Evaluates the expression t in the current model.
Definition: Model.cs:219
Microsoft.Z3.Model.ConstInterp
Expr ConstInterp(Expr a)
Retrieves the interpretation (the assignment) of a in the model.
Definition: Model.cs:36
Microsoft.Z3.Model.NumConsts
uint NumConsts
The number of constants that have an interpretation in the model.
Definition: Model.cs:112
Z3_sort_kind
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:149
Microsoft.Z3.Model.NumSorts
uint NumSorts
The number of uninterpreted sorts that the model has an interpretation for.
Definition: Model.cs:251
Microsoft.Z3.Model.FuncInterp
FuncInterp FuncInterp(FuncDecl f)
Retrieves the interpretation (the assignment) of a non-constant f in the model.
Definition: Model.cs:69