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 override void IncRef(
Context ctx, IntPtr obj)
99 public override void DecRef(Context ctx, IntPtr obj)
101 Native.Z3_func_entry_dec_ref(ctx.nCtx, obj);
105 internal override void IncRef(IntPtr o)
107 Context.FuncEntry_DRQ.IncAndClear(Context, o);
111 internal override void DecRef(IntPtr o)
113 Context.FuncEntry_DRQ.Add(o);
122 public uint NumEntries
130 public Entry[] Entries
134 Contract.Ensures(Contract.Result<
Entry[]>() != null);
135 Contract.Ensures(Contract.ForAll(0, Contract.Result<
Entry[]>().Length, j => Contract.Result<
Entry[]>()[j] != null));
139 for (uint i = 0; i < n; i++)
152 Contract.Ensures(Contract.Result<
Expr>() != null);
173 foreach (
Entry e
in Entries)
176 if (n > 1) res +=
"[";
178 for (uint i = 0; i < n; i++)
180 if (i != 0) res +=
", ";
183 if (n > 1) res +=
"]";
184 res +=
" -> " + e.
Value +
", ";
186 res +=
"else -> " + Else;
195 Contract.Requires(ctx != null);
200 public override void IncRef(Context ctx, IntPtr obj)
202 Native.Z3_func_interp_inc_ref(ctx.nCtx, obj);
205 public override void DecRef(Context ctx, IntPtr obj)
207 Native.Z3_func_interp_dec_ref(ctx.nCtx, obj);
211 internal override void IncRef(IntPtr o)
213 Context.FuncInterp_DRQ.IncAndClear(Context, o);
217 internal override void DecRef(IntPtr o)
219 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 void Z3_func_entry_inc_ref(Z3_context a0, Z3_func_entry a1)
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...