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.
§ ConstInterp() [1/2]
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.
§ ConstInterp() [2/2]
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).
§ 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 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);
§ Evaluate()
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.
§ FuncInterp()
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.
§ SortUniverse()
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();
§ ToString()
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);
§ ConstDecls
The function declarations of the constants in the model.
Definition at line 121 of file Model.cs.
§ Decls
All symbols that have an interpretation in the model.
Definition at line 163 of file Model.cs.
§ FuncDecls
The function declarations of the function interpretations in the model.
Definition at line 146 of file Model.cs.
§ NumConsts
The number of constants that have an interpretation in the model.
Definition at line 113 of file Model.cs.
§ NumFuncs
The number of function interpretations in the model.
Definition at line 138 of file Model.cs.
§ NumSorts
The number of uninterpreted sorts that the model has an interpretation for.
Definition at line 231 of file Model.cs.
§ Sorts
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.