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)
101 internal override void DecRef(
Context ctx, IntPtr obj)
107 internal override void IncRef(IntPtr o)
113 internal override void DecRef(IntPtr 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);
202 public DecRefQueue() : base() { }
203 public DecRefQueue(uint move_limit) : base(move_limit) { }
204 internal override void IncRef(
Context ctx, IntPtr obj)
209 internal override void DecRef(
Context ctx, IntPtr obj)
215 internal override void IncRef(IntPtr o)
221 internal override void DecRef(IntPtr 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)
IDecRefQueue FuncEntry_DRQ
FuncEntry DRQ
static uint Z3_func_entry_get_num_args(Z3_context a0, Z3_func_entry a1)
IDecRefQueue FuncInterp_DRQ
FuncInterp DRQ
static uint Z3_func_interp_get_arity(Z3_context a0, Z3_func_interp a1)
static void Z3_func_entry_dec_ref(Z3_context a0, Z3_func_entry a1)
static Z3_ast Z3_func_entry_get_arg(Z3_context a0, Z3_func_entry a1, uint a2)
static void Z3_func_interp_inc_ref(Z3_context a0, Z3_func_interp a1)
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 void Z3_func_interp_dec_ref(Z3_context a0, Z3_func_interp a1)
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...