20using System.Diagnostics;
22using System.Runtime.InteropServices;
42 Debug.Assert(g !=
null);
45 return Native.Z3_probe_apply(
Context.nCtx, NativeObject, g.NativeObject);
55 Debug.Assert(g !=
null);
65 Debug.Assert(ctx !=
null);
67 internal Probe(Context ctx,
string name)
70 Debug.Assert(ctx !=
null);
73 internal class DecRefQueue : IDecRefQueue
75 public DecRefQueue() : base() { }
76 public DecRefQueue(uint move_limit) : base(move_limit) { }
77 internal override void IncRef(Context ctx, IntPtr obj)
79 Native.Z3_probe_inc_ref(ctx.nCtx, obj);
82 internal override void DecRef(Context ctx, IntPtr obj)
84 Native.Z3_probe_dec_ref(ctx.nCtx, obj);
88 internal override void IncRef(IntPtr o)
90 Context.
Probe_DRQ.IncAndClear(Context, o);
94 internal override void DecRef(IntPtr o)
The main interaction with Z3 happens via the Context.
IDecRefQueue Probe_DRQ
Probe DRQ
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ...
Probes are used to inspect a goal (aka problem) and collect information that may be used to decide wh...
double Apply(Goal g)
Execute the probe over the goal.
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Z3_probe Z3_API Z3_mk_probe(Z3_context c, Z3_string name)
Return a probe associated with the given name. The complete list of probes may be obtained using the ...