20using System.Diagnostics;
44 return Expr.Create(
Context, Native.Z3_func_entry_get_value(
Context.nCtx, NativeObject));
53 get {
return Native.Z3_func_entry_get_num_args(
Context.nCtx, NativeObject); }
66 for (uint i = 0; i < n; i++)
67 res[i] =
Expr.Create(
Context, Native.Z3_func_entry_get_arg(
Context.nCtx, NativeObject, i));
80 for (uint i = 0; i < n; i++)
81 res += args[i] +
", ";
82 return res +
Value +
"]";
86 internal Entry(
Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx !=
null); }
90 public DecRefQueue() : base() { }
91 public DecRefQueue(uint move_limit) : base(move_limit) { }
92 internal override void IncRef(Context ctx, IntPtr obj)
94 Native.Z3_func_entry_inc_ref(ctx.nCtx, obj);
97 internal override void DecRef(Context ctx, IntPtr obj)
99 Native.Z3_func_entry_dec_ref(ctx.nCtx, obj);
103 internal override void IncRef(IntPtr o)
109 internal override void DecRef(IntPtr o)
122 get {
return Native.Z3_func_interp_get_num_entries(
Context.nCtx, NativeObject); }
135 for (uint i = 0; i < n; i++)
136 res[i] =
new Entry(
Context, Native.Z3_func_interp_get_entry(
Context.nCtx, NativeObject, i));
149 return Expr.Create(
Context, Native.Z3_func_interp_get_else(
Context.nCtx, NativeObject));
158 get {
return Native.Z3_func_interp_get_arity(
Context.nCtx, NativeObject); }
171 if (n > 1) res +=
"[";
173 for (uint i = 0; i < n; i++)
175 if (i != 0) res +=
", ";
178 if (n > 1) res +=
"]";
179 res +=
" -> " + e.
Value +
", ";
181 res +=
"else -> " +
Else;
190 Debug.Assert(ctx !=
null);
193 internal class DecRefQueue : IDecRefQueue
195 public DecRefQueue() : base() { }
196 public DecRefQueue(uint move_limit) : base(move_limit) { }
197 internal override void IncRef(Context ctx, IntPtr obj)
199 Native.Z3_func_interp_inc_ref(ctx.nCtx, obj);
202 internal override void DecRef(Context ctx, IntPtr obj)
204 Native.Z3_func_interp_dec_ref(ctx.nCtx, obj);
208 internal override void IncRef(IntPtr o)
214 internal override void DecRef(IntPtr o)
The main interaction with Z3 happens via the Context.
IDecRefQueue FuncEntry_DRQ
FuncEntry DRQ
IDecRefQueue FuncInterp_DRQ
FuncInterp DRQ
An Entry object represents an element in the finite map used to encode a function interpretation.
uint NumArgs
The number of arguments of the entry.
Expr Value
Return the (symbolic) value of this entry.
Expr[] Args
The arguments of the function entry.
override string ToString()
A string representation of the function entry.
A function interpretation is represented as a finite map and an 'else' value. Each entry in the finit...
uint Arity
The arity of the function interpretation
override string ToString()
A string representation of the function interpretation.
Entry[] Entries
The entries in the function interpretation
uint NumEntries
The number of entries in the function interpretation.
Expr Else
The (symbolic) ‘else’ value of the function interpretation.
Internal base class for interfacing with native Z3 objects. Should not be used externally.