21 using System.Runtime.InteropServices;
22 using System.Diagnostics.Contracts;
33 [ContractVerification(
true)]
43 Contract.Requires(g != null);
52 public double this[
Goal g]
56 Contract.Requires(g != null);
66 Contract.Requires(ctx != null);
68 internal Probe(Context ctx,
string name)
71 Contract.Requires(ctx != null);
76 public override void IncRef(Context ctx, IntPtr obj)
78 Native.Z3_probe_inc_ref(ctx.nCtx, obj);
81 public override void DecRef(Context ctx, IntPtr obj)
83 Native.Z3_probe_dec_ref(ctx.nCtx, obj);
87 internal override void IncRef(IntPtr o)
89 Context.Probe_DRQ.IncAndClear(Context, o);
93 internal override void DecRef(IntPtr o)
95 Context.Probe_DRQ.Add(o);
Probes are used to inspect a goal (aka problem) and collect information that may be used to decide wh...
static double Z3_probe_apply(Z3_context a0, Z3_probe a1, Z3_goal a2)
double Apply(Goal g)
Execute the probe over the goal.
The main interaction with Z3 happens via the Context.
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Z3_probe Z3_API Z3_mk_probe(__in Z3_context c, __in Z3_string name)
Return a probe associated with the given name. The complete list of probes may be obtained using the ...
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ...