00001 00018 package com.microsoft.z3; 00019 00028 public class Probe extends Z3Object 00029 { 00037 public double apply(Goal g) throws Z3Exception 00038 { 00039 getContext().checkContextMatch(g); 00040 return Native.probeApply(getContext().nCtx(), getNativeObject(), 00041 g.getNativeObject()); 00042 } 00043 00044 Probe(Context ctx, long obj) throws Z3Exception 00045 { 00046 super(ctx, obj); 00047 } 00048 00049 Probe(Context ctx, String name) throws Z3Exception 00050 { 00051 super(ctx, Native.mkProbe(ctx.nCtx(), name)); 00052 } 00053 00054 void incRef(long o) throws Z3Exception 00055 { 00056 getContext().probe_DRQ().incAndClear(getContext(), o); 00057 super.incRef(o); 00058 } 00059 00060 void decRef(long o) throws Z3Exception 00061 { 00062 getContext().probe_DRQ().add(o); 00063 super.decRef(o); 00064 } 00065 }