21 using System.Diagnostics.Contracts;
29 [ContractVerification(
true)]
45 Contract.Ensures(Contract.Result<
Expr>() != null);
65 Contract.Ensures(Contract.Result<
Expr[]>() != null);
66 Contract.Ensures(Contract.Result<
Expr[]>().Length ==
this.
NumArgs);
70 for (uint i = 0; i < n; i++)
84 for (uint i = 0; i < n; i++)
85 res += args[i] +
", ";
86 return res + Value +
"]";
90 internal Entry(
Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
94 public DecRefQueue() : base() { }
95 public DecRefQueue(uint move_limit) : base(move_limit) { }
96 internal override void IncRef(Context ctx, IntPtr obj)
98 Native.Z3_func_entry_inc_ref(ctx.nCtx, obj);
101 internal override void DecRef(Context ctx, IntPtr obj)
103 Native.Z3_func_entry_dec_ref(ctx.nCtx, obj);
107 internal override void IncRef(IntPtr o)
109 Context.FuncEntry_DRQ.IncAndClear(Context, o);
113 internal override void DecRef(IntPtr o)
115 Context.FuncEntry_DRQ.Add(o);
124 public uint NumEntries
132 public Entry[] Entries
136 Contract.Ensures(Contract.Result<
Entry[]>() != null);
137 Contract.Ensures(Contract.ForAll(0, Contract.Result<
Entry[]>().Length, j => Contract.Result<
Entry[]>()[j] != null));
141 for (uint i = 0; i < n; i++)
154 Contract.Ensures(Contract.Result<
Expr>() != null);
175 foreach (
Entry e
in Entries)
178 if (n > 1) res +=
"[";
180 for (uint i = 0; i < n; i++)
182 if (i != 0) res +=
", ";
185 if (n > 1) res +=
"]";
186 res +=
" -> " + e.
Value +
", ";
188 res +=
"else -> " + Else;
197 Contract.Requires(ctx != null);
200 internal class DecRefQueue : IDecRefQueue
202 public DecRefQueue() : base() { }
203 public DecRefQueue(uint move_limit) : base(move_limit) { }
204 internal override void IncRef(Context ctx, IntPtr obj)
206 Native.Z3_func_interp_inc_ref(ctx.nCtx, obj);
209 internal override void DecRef(Context ctx, IntPtr obj)
211 Native.Z3_func_interp_dec_ref(ctx.nCtx, obj);
215 internal override void IncRef(IntPtr o)
217 Context.FuncInterp_DRQ.IncAndClear(Context, o);
221 internal override void DecRef(IntPtr o)
223 Context.FuncInterp_DRQ.Add(o);
override string ToString()
A string representation of the function entry.
Expr Value
Return the (symbolic) value of this entry.
override string ToString()
A string representation of the function interpretation.
uint NumArgs
The number of arguments of the expression.
static uint Z3_func_entry_get_num_args(Z3_context a0, Z3_func_entry a1)
static uint Z3_func_interp_get_arity(Z3_context a0, Z3_func_interp a1)
static Z3_ast Z3_func_entry_get_arg(Z3_context a0, Z3_func_entry a1, uint a2)
static uint Z3_func_interp_get_num_entries(Z3_context a0, Z3_func_interp a1)
static Z3_ast Z3_func_interp_get_else(Z3_context a0, Z3_func_interp a1)
The main interaction with Z3 happens via the Context.
static Z3_ast Z3_func_entry_get_value(Z3_context a0, Z3_func_entry a1)
Expr[] Args
The arguments of the function entry.
Internal base class for interfacing with native Z3 objects. Should not be used externally.
uint NumArgs
The number of arguments of the entry.
An Entry object represents an element in the finite map used to encode a function interpretation...
static Z3_func_entry Z3_func_interp_get_entry(Z3_context a0, Z3_func_interp a1, uint a2)
A function interpretation is represented as a finite map and an 'else' value. Each entry in the finit...