Z3
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;
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 
118  internal class DecRefQueue : IDecRefQueue
119  {
120  public DecRefQueue() : base() { }
121  public DecRefQueue(uint move_limit) : base(move_limit) { }
122  internal override void IncRef(Context ctx, IntPtr obj)
123  {
124  Native.Z3_tactic_inc_ref(ctx.nCtx, obj);
125  }
126 
127  internal override void DecRef(Context ctx, IntPtr obj)
128  {
129  Native.Z3_tactic_dec_ref(ctx.nCtx, obj);
130  }
131  };
132 
133  internal override void IncRef(IntPtr o)
134  {
135  Context.Tactic_DRQ.IncAndClear(Context, o);
136  base.IncRef(o);
137  }
138 
139  internal override void DecRef(IntPtr o)
140  {
141  Context.Tactic_DRQ.Add(o);
142  base.DecRef(o);
143  }
144  #endregion
145  }
146 }
IDecRefQueue Tactic_DRQ
Tactic DRQ
Definition: Context.cs:4948
Tactics are the basic building block for creating custom solvers for specific problem domains...
Definition: Tactic.cs:32
ApplyResult Apply(Goal g, Params p=null)
Execute the tactic over the goal.
Definition: Tactic.cs:60
ApplyResult objects represent the result of an application of a tactic to a goal. It contains the sub...
Definition: ApplyResult.cs:30
A Params objects represents a configuration in the form of Symbol/value pairs.
Definition: Params.cs:29
A ParamDescrs describes a set of parameters.
Definition: ParamDescrs.cs:29
DecRefQueue interface
Definition: IDecRefQueue.cs:32
Solver MkSolver(Symbol logic=null)
Creates a new (incremental) solver.
Definition: Context.cs:3808
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33
Solvers.
Definition: Solver.cs:30
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ...
Definition: Goal.cs:31