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);
71 Contract.Requires(ctx != null);
76 public DecRefQueue() : base() { }
77 public DecRefQueue(uint move_limit) : base(move_limit) { }
78 internal override void IncRef(
Context ctx, IntPtr obj)
83 internal override void DecRef(
Context ctx, IntPtr obj)
89 internal override void IncRef(IntPtr o)
95 internal override void DecRef(IntPtr o)
Probes are used to inspect a goal (aka problem) and collect information that may be used to decide wh...
static void Z3_probe_dec_ref(Z3_context a0, Z3_probe a1)
static void Z3_probe_inc_ref(Z3_context a0, Z3_probe a1)
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.
IDecRefQueue Probe_DRQ
Probe DRQ
Internal base class for interfacing with native Z3 objects. Should not be used externally.
static Z3_probe Z3_mk_probe(Z3_context a0, string a1)
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ...