|
Z3
|
|
All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
|
Z3
|
|
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. | |
| 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.
1.7.6.1