A Model contains interpretations (assignments) of constants and functions. More...
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. | |
Expr | ConstInterp (FuncDecl f) |
Retrieves the interpretation (the assignment) of f in the model. | |
FuncInterp | FuncInterp (FuncDecl f) |
Retrieves the interpretation (the assignment) of a non-constant f in the model. | |
Expr | Eval (Expr t, bool completion=false) |
Evaluates the expression t in the current model. | |
Expr | Evaluate (Expr t, bool completion=false) |
Alias for Eval . | |
Expr[] | SortUniverse (Sort s) |
The finite set of distinct values that represent the interpretation for sort s . | |
override string | ToString () |
Conversion of models to strings. | |
Properties | |
uint | NumConsts [get] |
The number of constants that have an interpretation in the model. | |
FuncDecl[] | ConstDecls [get] |
The function declarations of the constants in the model. | |
uint | NumFuncs [get] |
The number of function interpretations in the model. | |
FuncDecl[] | FuncDecls [get] |
The function declarations of the function interpretations in the model. | |
FuncDecl[] | Decls [get] |
All symbols that have an interpretation in the model. | |
uint | NumSorts [get] |
The number of uninterpreted sorts that the model has an interpretation for. | |
Sort[] | Sorts [get] |
The uninterpreted sorts that the model has an interpretation for. |
A Model contains interpretations (assignments) of constants and functions.
Expr ConstInterp | ( | Expr | a | ) | [inline] |
Retrieves the interpretation (the assignment) of a in the model.
a | A Constant |
Definition at line 36 of file Model.cs.
{ Contract.Requires(a != null); Context.CheckContextMatch(a); return ConstInterp(a.FuncDecl); }
Expr ConstInterp | ( | FuncDecl | f | ) | [inline] |
Retrieves the interpretation (the assignment) of f in the model.
f | A function declaration of zero arity |
Definition at line 49 of file Model.cs.
{ Contract.Requires(f != null); Context.CheckContextMatch(f); if (f.Arity != 0 || Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_range(Context.nCtx, f.NativeObject)) == (uint)Z3_sort_kind.Z3_ARRAY_SORT) throw new Z3Exception("Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp."); IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject); if (n == IntPtr.Zero) return null; else return Expr.Create(Context, n); }
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.
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. |
Definition at line 205 of file Model.cs.
{ Contract.Requires(t != null); Contract.Ensures(Contract.Result<Expr>() != null); IntPtr v = IntPtr.Zero; if (Native.Z3_model_eval(Context.nCtx, NativeObject, t.NativeObject, (completion) ? 1 : 0, ref v) == 0) throw new ModelEvaluationFailedException(); else return Expr.Create(Context, v); }
FuncInterp FuncInterp | ( | FuncDecl | f | ) | [inline] |
Retrieves the interpretation (the assignment) of a non-constant f in the model.
f | A function declaration of non-zero arity |
Definition at line 70 of file Model.cs.
{ Contract.Requires(f != null); Context.CheckContextMatch(f); Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_range(Context.nCtx, f.NativeObject)); if (f.Arity == 0) { IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject); if (sk == Z3_sort_kind.Z3_ARRAY_SORT) { if (n == IntPtr.Zero) return null; else { if (Native.Z3_is_as_array(Context.nCtx, n) == 0) throw new Z3Exception("Argument was not an array constant"); IntPtr fd = Native.Z3_get_as_array_func_decl(Context.nCtx, n); return FuncInterp(new FuncDecl(Context, fd)); } } else { throw new Z3Exception("Constant functions do not have a function interpretation; use ConstInterp"); } } else { IntPtr n = Native.Z3_model_get_func_interp(Context.nCtx, NativeObject, f.NativeObject); if (n == IntPtr.Zero) return null; else return new FuncInterp(Context, n); } }
Expr [] SortUniverse | ( | Sort | s | ) | [inline] |
The finite set of distinct values that represent the interpretation for sort s .
s | An uninterpreted sort |
Definition at line 263 of file Model.cs.
{ Contract.Requires(s != null); Contract.Ensures(Contract.Result<Expr[]>() != null); ASTVector nUniv = new ASTVector(Context, Native.Z3_model_get_sort_universe(Context.nCtx, NativeObject, s.NativeObject)); uint n = nUniv.Size; Expr[] res = new Expr[n]; for (uint i = 0; i < n; i++) res[i] = Expr.Create(Context, nUniv[i].NativeObject); return res; }
override string ToString | ( | ) | [inline] |
FuncDecl [] ConstDecls [get] |
uint NumConsts [get] |
uint NumFuncs [get] |
uint NumSorts [get] |
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.