Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Tactic.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  Tactic.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Tactics
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-03-21
15 
16 Notes:
17 
18 --*/
19 
20 using System;
21 using System.Diagnostics.Contracts;
22 
23 namespace Microsoft.Z3
24 {
31  [ContractVerification(true)]
32  public class Tactic : Z3Object
33  {
37  public string Help
38  {
39  get
40  {
41  Contract.Ensures(Contract.Result<string>() != null);
42 
43  return Native.Z3_tactic_get_help(Context.nCtx, NativeObject);
44  }
45  }
46 
47 
51  public ParamDescrs ParameterDescriptions
52  {
53  get { return new ParamDescrs(Context, Native.Z3_tactic_get_param_descrs(Context.nCtx, NativeObject)); }
54  }
55 
56 
60  public ApplyResult Apply(Goal g, Params p = null)
61  {
62  Contract.Requires(g != null);
63  Contract.Ensures(Contract.Result<ApplyResult>() != null);
64 
65  Context.CheckContextMatch(g);
66  if (p == null)
67  return new ApplyResult(Context, Native.Z3_tactic_apply(Context.nCtx, NativeObject, g.NativeObject));
68  else
69  {
70  Context.CheckContextMatch(p);
71  return new ApplyResult(Context, Native.Z3_tactic_apply_ex(Context.nCtx, NativeObject, g.NativeObject, p.NativeObject));
72  }
73  }
74 
78  public ApplyResult this[Goal g]
79  {
80  get
81  {
82  Contract.Requires(g != null);
83  Contract.Ensures(Contract.Result<ApplyResult>() != null);
84 
85  return Apply(g);
86  }
87  }
88 
93  public Solver Solver
94  {
95  get
96  {
97  Contract.Ensures(Contract.Result<Solver>() != null);
98 
99  return Context.MkSolver(this);
100  }
101  }
102 
103  #region Internal
104  internal Tactic(Context ctx, IntPtr obj)
105  : base(ctx, obj)
106  {
107  Contract.Requires(ctx != null);
108  }
109  internal Tactic(Context ctx, string name)
110  : base(ctx, Native.Z3_mk_tactic(ctx.nCtx, name))
111  {
112  Contract.Requires(ctx != null);
113  }
114 
115  internal class DecRefQueue : Z3.DecRefQueue
116  {
117  public override void IncRef(Context ctx, IntPtr obj)
118  {
119  Native.Z3_tactic_inc_ref(ctx.nCtx, obj);
120  }
121 
122  public override void DecRef(Context ctx, IntPtr obj)
123  {
124  Native.Z3_tactic_dec_ref(ctx.nCtx, obj);
125  }
126  };
127 
128  internal override void IncRef(IntPtr o)
129  {
130  Context.Tactic_DRQ.IncAndClear(Context, o);
131  base.IncRef(o);
132  }
133 
134  internal override void DecRef(IntPtr o)
135  {
136  Context.Tactic_DRQ.Add(o);
137  base.DecRef(o);
138  }
139  #endregion
140  }
141 }