Z3
Probe.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  Probe.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Probes
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-03-21
15 
16 Notes:
17 
18 --*/
19 
20 using System;
21 using System.Runtime.InteropServices;
23 
24 namespace Microsoft.Z3
25 {
33  [ContractVerification(true)]
34  public class Probe : Z3Object
35  {
41  public double Apply(Goal g)
42  {
43  Contract.Requires(g != null);
44 
45  Context.CheckContextMatch(g);
46  return Native.Z3_probe_apply(Context.nCtx, NativeObject, g.NativeObject);
47  }
48 
52  public double this[Goal g]
53  {
54  get
55  {
56  Contract.Requires(g != null);
57 
58  return Apply(g);
59  }
60  }
61 
62  #region Internal
63  internal Probe(Context ctx, IntPtr obj)
64  : base(ctx, obj)
65  {
66  Contract.Requires(ctx != null);
67  }
68  internal Probe(Context ctx, string name)
69  : base(ctx, Native.Z3_mk_probe(ctx.nCtx, name))
70  {
71  Contract.Requires(ctx != null);
72  }
73 
74  internal class DecRefQueue : IDecRefQueue
75  {
76  public DecRefQueue() : base() { }
77  public DecRefQueue(uint move_limit) : base(move_limit) { }
78  internal override void IncRef(Context ctx, IntPtr obj)
79  {
80  Native.Z3_probe_inc_ref(ctx.nCtx, obj);
81  }
82 
83  internal override void DecRef(Context ctx, IntPtr obj)
84  {
85  Native.Z3_probe_dec_ref(ctx.nCtx, obj);
86  }
87  };
88 
89  internal override void IncRef(IntPtr o)
90  {
91  Context.Probe_DRQ.IncAndClear(Context, o);
92  base.IncRef(o);
93  }
94 
95  internal override void DecRef(IntPtr o)
96  {
97  Context.Probe_DRQ.Add(o);
98  base.DecRef(o);
99  }
100  #endregion
101  }
102 }
Probes are used to inspect a goal (aka problem) and collect information that may be used to decide wh...
Definition: Probe.cs:34
double Apply(Goal g)
Execute the probe over the goal.
Definition: Probe.cs:41
DecRefQueue interface
Definition: IDecRefQueue.cs:32
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
IDecRefQueue Probe_DRQ
Probe DRQ
Definition: Context.cs:4933
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ...
Definition: Goal.cs:31