Go to the documentation of this file.00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020 using System;
00021 using System.Runtime.InteropServices;
00022 using System.Diagnostics.Contracts;
00023
00024 namespace Microsoft.Z3
00025 {
00033 [ContractVerification(true)]
00034 public class Probe : Z3Object
00035 {
00041 public double Apply(Goal g)
00042 {
00043 Contract.Requires(g != null);
00044
00045 Context.CheckContextMatch(g);
00046 return Native.Z3_probe_apply(Context.nCtx, NativeObject, g.NativeObject);
00047 }
00048
00052 public double this[Goal g]
00053 {
00054 get
00055 {
00056 Contract.Requires(g != null);
00057
00058 return Apply(g);
00059 }
00060 }
00061
00062 #region Internal
00063 internal Probe(Context ctx, IntPtr obj)
00064 : base(ctx, obj)
00065 {
00066 Contract.Requires(ctx != null);
00067 }
00068 internal Probe(Context ctx, string name)
00069 : base(ctx, Native.Z3_mk_probe(ctx.nCtx, name))
00070 {
00071 Contract.Requires(ctx != null);
00072 }
00073
00074 internal class DecRefQueue : IDecRefQueue
00075 {
00076 public override void IncRef(Context ctx, IntPtr obj)
00077 {
00078 Native.Z3_probe_inc_ref(ctx.nCtx, obj);
00079 }
00080
00081 public override void DecRef(Context ctx, IntPtr obj)
00082 {
00083 Native.Z3_probe_dec_ref(ctx.nCtx, obj);
00084 }
00085 };
00086
00087 internal override void IncRef(IntPtr o)
00088 {
00089 Context.Probe_DRQ.IncAndClear(Context, o);
00090 base.IncRef(o);
00091 }
00092
00093 internal override void DecRef(IntPtr o)
00094 {
00095 Context.Probe_DRQ.Add(o);
00096 base.DecRef(o);
00097 }
00098 #endregion
00099 }
00100 }