21using System.Diagnostics;
22using System.Collections.Generic;
38 Debug.Assert(a !=
null);
51 Debug.Assert(f !=
null);
55 throw new Z3Exception(
"Non-zero arity functions have FunctionInterpretations as a model. Use FuncInterp.");
57 IntPtr n = Native.Z3_model_get_const_interp(
Context.nCtx, NativeObject, f.NativeObject);
71 Debug.Assert(f !=
null);
79 IntPtr n = Native.Z3_model_get_const_interp(
Context.nCtx, NativeObject, f.NativeObject);
87 if (Native.Z3_is_as_array(
Context.nCtx, n) == 0)
88 throw new Z3Exception(
"Argument was not an array constant");
89 IntPtr fd = Native.Z3_get_as_array_func_decl(
Context.nCtx, n);
95 throw new Z3Exception(
"Constant functions do not have a function interpretation; use ConstInterp");
100 IntPtr n = Native.Z3_model_get_func_interp(
Context.nCtx, NativeObject, f.NativeObject);
101 if (n == IntPtr.Zero)
113 get {
return Native.Z3_model_get_num_consts(
Context.nCtx, NativeObject); }
126 for (uint i = 0; i < n; i++)
135 public IEnumerable<KeyValuePair<FuncDecl, Expr>>
Consts
140 for (uint i = 0; i < nc; ++i)
143 IntPtr n = Native.Z3_model_get_const_interp(
Context.nCtx, NativeObject, f.NativeObject);
144 if (n == IntPtr.Zero)
continue;
145 yield
return new KeyValuePair<FuncDecl, Expr>(f,
Expr.Create(
Context, n));
155 get {
return Native.Z3_model_get_num_funcs(
Context.nCtx, NativeObject); }
168 for (uint i = 0; i < n; i++)
184 uint n = nFuncs + nConsts;
186 for (uint i = 0; i < nConsts; i++)
188 for (uint i = 0; i < nFuncs; i++)
221 Debug.Assert(t !=
null);
223 IntPtr v = IntPtr.Zero;
224 if (Native.Z3_model_eval(
Context.nCtx, NativeObject, t.NativeObject, (
byte)(completion ? 1 : 0), ref v) == (
byte)0)
235 Debug.Assert(t !=
null);
237 return Eval(t, completion);
244 var r =
Eval(t,
true);
245 return Native.Z3_get_numeral_double(
Context.nCtx, r.NativeObject);
251 public uint
NumSorts {
get {
return Native.Z3_model_get_num_sorts(
Context.nCtx, NativeObject); } }
270 for (uint i = 0; i < n; i++)
271 res[i] =
Sort.Create(
Context, Native.Z3_model_get_sort(
Context.nCtx, NativeObject, i));
284 Debug.Assert(s !=
null);
296 return Native.Z3_model_to_string(
Context.nCtx, NativeObject);
303 Debug.Assert(ctx !=
null);
306 internal class DecRefQueue : IDecRefQueue
308 public DecRefQueue() : base() { }
309 public DecRefQueue(uint move_limit) : base(move_limit) { }
310 internal override void IncRef(Context ctx, IntPtr obj)
312 Native.Z3_model_inc_ref(ctx.nCtx, obj);
315 internal override void DecRef(Context ctx, IntPtr obj)
317 Native.Z3_model_dec_ref(ctx.nCtx, obj);
321 internal override void IncRef(IntPtr o)
323 Context.
Model_DRQ.IncAndClear(Context, o);
327 internal override void DecRef(IntPtr o)
Expr[] ToExprArray()
Translates an ASTVector into an Expr[]
The main interaction with Z3 happens via the Context.
IDecRefQueue Model_DRQ
Model DRQ
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
uint Arity
The arity of the function declaration
A function interpretation is represented as a finite map and an 'else' value. Each entry in the finit...
A ModelEvaluationFailedException is thrown when an expression cannot be evaluated by the model.
ModelEvaluationFailedException()
An exception that is thrown when model evaluation fails.
A Model contains interpretations (assignments) of constants and functions.
FuncDecl[] Decls
All symbols that have an interpretation in the model.
Expr ConstInterp(Expr a)
Retrieves the interpretation (the assignment) of a in the model.
Expr Evaluate(Expr t, bool completion=false)
Alias for Eval.
FuncDecl[] FuncDecls
The function declarations of the function interpretations in the model.
double Double(Expr t)
Evaluate expression to a double, assuming it is a numeral already.
FuncInterp FuncInterp(FuncDecl f)
Retrieves the interpretation (the assignment) of a non-constant f in the model.
Expr[] SortUniverse(Sort s)
The finite set of distinct values that represent the interpretation for sort s .
Sort[] Sorts
The uninterpreted sorts that the model has an interpretation for.
IEnumerable< KeyValuePair< FuncDecl, Expr > > Consts
Enumerate constants in model.
FuncDecl[] ConstDecls
The function declarations of the constants in the model.
override string ToString()
Conversion of models to strings.
uint NumFuncs
The number of function interpretations in the model.
Expr ConstInterp(FuncDecl f)
Retrieves the interpretation (the assignment) of f in the model.
Expr Eval(Expr t, bool completion=false)
Evaluates the expression t in the current model.
uint NumConsts
The number of constants that have an interpretation in the model.
uint NumSorts
The number of uninterpreted sorts that the model has an interpretation for.
The Sort class implements type information for ASTs.
The exception base class for error reporting from Z3
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).