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

  a | A 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 }
Microsoft.Z3.Model.ConstInterp
Expr ConstInterp(Expr a)
Retrieves the interpretation (the assignment) of a in the model.
Definition: Model.cs:36

Referenced by Model.ConstInterp().

## ◆ ConstInterp() [2/2]

Expr ConstInterp | ( | FuncDecl | f | ) |
| inline

Retrieves the interpretation (the assignment) of f in the model.

Parameters

  f | A 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 }
Microsoft.Z3.Model.Eval
Expr Eval(Expr t, bool completion=false)
Evaluates the expression t in the current model.
Definition: Model.cs:219

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

  t | An 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.

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

FuncInterp FuncInterp | ( | FuncDecl | f | ) |
| inline

Retrieves the interpretation (the assignment) of a non-constant f in the model.

Parameters

  f | A 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 }
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
Z3_sort_kind
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:150

Referenced by Model.FuncInterp().

## ◆ SortUniverse()

Expr[] SortUniverse | ( | Sort | s | ) |
| inline

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

See also
  Sorts

Parameters

  s | An 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 119 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 }
Microsoft.Z3.Model.NumConsts
uint NumConsts
The number of constants that have an interpretation in the model.
Definition: Model.cs:112

## ◆ Consts

IEnumerable<KeyValuePair<FuncDecl, Expr> > Consts
| get

Enumerate constants in model.

Definition at line 135 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 177 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 }
Microsoft.Z3.Model.NumFuncs
uint NumFuncs
The number of function interpretations in the model.
Definition: Model.cs:154

## ◆ FuncDecls

FuncDecl [] FuncDecls
| get

The function declarations of the function interpretations in the model.

Definition at line 161 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 111 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 153 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 263 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.NumSorts
uint NumSorts
The number of uninterpreted sorts that the model has an interpretation for.
Definition: Model.cs:251