38 Contract.Requires(a != null);
51 Contract.Requires(f != null);
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);
72 Contract.Requires(f != null);
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)
112 public uint NumConsts
114 get {
return Native.Z3_model_get_num_consts(
Context.nCtx, NativeObject); }
124 Contract.Ensures(Contract.Result<
FuncDecl[]>() != null);
128 for (uint i = 0; i < n; i++)
139 get {
return Native.Z3_model_get_num_funcs(
Context.nCtx, NativeObject); }
149 Contract.Ensures(Contract.Result<
FuncDecl[]>() != null);
153 for (uint i = 0; i < n; i++)
166 Contract.Ensures(Contract.Result<
FuncDecl[]>() != null);
168 uint nFuncs = NumFuncs;
169 uint nConsts = NumConsts;
170 uint n = nFuncs + nConsts;
172 for (uint i = 0; i < nConsts; i++)
174 for (uint i = 0; i < nFuncs; i++)
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)
222 Contract.Requires(t != null);
223 Contract.Ensures(Contract.Result<
Expr>() != null);
225 return Eval(t, completion);
231 public uint NumSorts {
get {
return Native.Z3_model_get_num_sorts(
Context.nCtx, NativeObject); } }
247 Contract.Ensures(Contract.Result<
Sort[]>() != null);
251 for (uint i = 0; i < n; i++)
252 res[i] =
Sort.Create(
Context, Native.Z3_model_get_sort(
Context.nCtx, NativeObject, i));
265 Contract.Requires(s != null);
266 Contract.Ensures(Contract.Result<
Expr[]>() != null);
278 return Native.Z3_model_to_string(
Context.nCtx, NativeObject);
285 Contract.Requires(ctx != null);
290 public DecRefQueue() : base() { }
291 public DecRefQueue(uint move_limit) : base(move_limit) { }
292 internal override void IncRef(
Context ctx, IntPtr obj)
294 Native.Z3_model_inc_ref(ctx.nCtx, obj);
297 internal override void DecRef(
Context ctx, IntPtr obj)
299 Native.Z3_model_dec_ref(ctx.nCtx, obj);
303 internal override void IncRef(IntPtr o)
309 internal override void DecRef(IntPtr o)
Z3_sort_kind
The different kinds of Z3 types (See #Z3_get_sort_kind).
A ModelEvaluationFailedException is thrown when an expression cannot be evaluated by the model...
Expr Eval(Expr t, bool completion=false)
Evaluates the expression t in the current model.
Expr ConstInterp(FuncDecl f)
Retrieves the interpretation (the assignment) of f in the model.
Expr [] SortUniverse(Sort s)
The finite set of distinct values that represent the interpretation for sort s .
uint Arity
The arity of the function declaration
Expr ConstInterp(Expr a)
Retrieves the interpretation (the assignment) of a in the model.
IDecRefQueue Model_DRQ
Model DRQ
FuncInterp FuncInterp(FuncDecl f)
Retrieves the interpretation (the assignment) of a non-constant f in the model.
Expr Evaluate(Expr t, bool completion=false)
Alias for Eval.
A Model contains interpretations (assignments) of constants and functions.
The main interaction with Z3 happens via the Context.
The Sort class implements type information for ASTs.
The exception base class for error reporting from Z3
Expr [] ToExprArray()
Translates an ASTVector into an Expr[]
override string ToString()
Conversion of models to strings.
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Internal base class for interfacing with native Z3 objects. Should not be used externally.
ModelEvaluationFailedException()
An exception that is thrown when model evaluation fails.
A function interpretation is represented as a finite map and an 'else' value. Each entry in the finit...