A Model contains interpretations (assignments) of constants and functions.
More...
|
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...
|
|
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...
|
|
A Model contains interpretations (assignments) of constants and functions.
Definition at line 29 of file Model.cs.
Retrieves the interpretation (the assignment) of a in the model.
- Parameters
-
- Returns
- An expression if the constant has an interpretation in the model, null otherwise.
Definition at line 36 of file Model.cs.
38 Contract.Requires(a != null);
40 Context.CheckContextMatch(a);
Expr ConstInterp(Expr a)
Retrieves the interpretation (the assignment) of a in the model.
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.
51 Contract.Requires(f != null);
53 Context.CheckContextMatch(f);
55 Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_range(Context.nCtx, f.NativeObject)) == (uint)
Z3_sort_kind.Z3_ARRAY_SORT)
56 throw new Z3Exception(
"Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.");
58 IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject);
62 return Expr.Create(Context, n);
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
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 205 of file Model.cs.
207 Contract.Requires(t != null);
208 Contract.Ensures(Contract.Result<Expr>() != null);
210 IntPtr v = IntPtr.Zero;
211 if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (completion) ? 1 : 0, ref v) == 0)
212 throw new ModelEvaluationFailedException();
214 return Expr.Create(Context, v);
Expr Evaluate |
( |
Expr |
t, |
|
|
bool |
completion = false |
|
) |
| |
|
inline |
Alias for Eval
.
Definition at line 220 of file Model.cs.
222 Contract.Requires(t != null);
223 Contract.Ensures(Contract.Result<Expr>() != null);
225 return Eval(t, completion);
Expr Eval(Expr t, bool completion=false)
Evaluates the expression t in the current model.
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 70 of file Model.cs.
72 Contract.Requires(f != null);
74 Context.CheckContextMatch(f);
76 Z3_sort_kind sk = (
Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_range(Context.nCtx, f.NativeObject));
80 IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject);
88 if (Native.Z3_is_as_array(Context.nCtx, n) == 0)
89 throw new Z3Exception(
"Argument was not an array constant");
90 IntPtr fd = Native.Z3_get_as_array_func_decl(Context.nCtx, n);
96 throw new Z3Exception(
"Constant functions do not have a function interpretation; use ConstInterp");
101 IntPtr n = Native.Z3_model_get_func_interp(Context.nCtx, NativeObject, f.NativeObject);
102 if (n == IntPtr.Zero)
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
FuncInterp FuncInterp(FuncDecl f)
Retrieves the interpretation (the assignment) of a non-constant f in the model.
The finite set of distinct values that represent the interpretation for sort s .
- See also
- Sorts
- Parameters
-
- Returns
- An array of expressions, where each is an element of the universe of s
Definition at line 263 of file Model.cs.
265 Contract.Requires(s != null);
266 Contract.Ensures(Contract.Result<Expr[]>() != null);
268 ASTVector av =
new ASTVector(Context, Native.Z3_model_get_sort_universe(Context.nCtx, NativeObject, s.NativeObject));
269 return av.ToExprArray();
override string ToString |
( |
| ) |
|
|
inline |
Conversion of models to strings.
- Returns
- A string representation of the model.
Definition at line 276 of file Model.cs.
278 return Native.Z3_model_to_string(Context.nCtx, NativeObject);
The function declarations of the constants in the model.
Definition at line 121 of file Model.cs.
All symbols that have an interpretation in the model.
Definition at line 163 of file Model.cs.
The function declarations of the function interpretations in the model.
Definition at line 146 of file Model.cs.
The number of constants that have an interpretation in the model.
Definition at line 113 of file Model.cs.
The number of function interpretations in the model.
Definition at line 138 of file Model.cs.
The number of uninterpreted sorts that the model has an interpretation for.
Definition at line 231 of file Model.cs.
The uninterpreted sorts that the model has an interpretation for.
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
- NumSorts, SortUniverse
Definition at line 244 of file Model.cs.