Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules 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 : IDecRefQueue
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 }
Z3_tactic Z3_API Z3_mk_tactic(__in Z3_context c, __in Z3_string name)
Return a tactic associated with the given name. The complete list of tactics may be obtained using th...
static Z3_apply_result Z3_tactic_apply(Z3_context a0, Z3_tactic a1, Z3_goal a2)
Definition: Native.cs:4793
static string Z3_tactic_get_help(Z3_context a0, Z3_tactic a1)
Definition: Native.cs:4753
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
static Z3_apply_result Z3_tactic_apply_ex(Z3_context a0, Z3_tactic a1, Z3_goal a2, Z3_params a3)
Definition: Native.cs:4801
A ParameterSet represents a configuration in the form of Symbol/value pairs.
Definition: Params.cs:29
Solver MkSolver(Symbol logic=null)
Creates a new (incremental) solver.
Definition: Context.cs:3382
The main interaction with Z3 happens via the Context.
Definition: Context.cs:31
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:31
static Z3_param_descrs Z3_tactic_get_param_descrs(Z3_context a0, Z3_tactic a1)
Definition: Native.cs:4761
Solvers.
Definition: Solver.cs:29
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ...
Definition: Goal.cs:31