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;
21 using System.Diagnostics;
22
23 namespace Microsoft.Z3
24{
31 public class Tactic : Z3Object
32 {
36 public string Help
37 {
38 get
39 {
40
41 return Native.Z3_tactic_get_help(Context.nCtx, NativeObject);
42 }
43 }
44
45
49 public ParamDescrs ParameterDescriptions
50 {
51 get { return new ParamDescrs(Context, Native.Z3_tactic_get_param_descrs(Context.nCtx, NativeObject)); }
52 }
53
54
58 public ApplyResult Apply(Goal g, Params p = null)
59 {
60 Debug.Assert(g != null);
61
62 Context.CheckContextMatch(g);
63 if (p == null)
64 return new ApplyResult(Context, Native.Z3_tactic_apply(Context.nCtx, NativeObject, g.NativeObject));
65 else
66 {
67 Context.CheckContextMatch(p);
68 return new ApplyResult(Context, Native.Z3_tactic_apply_ex(Context.nCtx, NativeObject, g.NativeObject, p.NativeObject));
69 }
70 }
71
75 public ApplyResult this[Goal g]
76 {
77 get
78 {
79 Debug.Assert(g != null);
80
81 return Apply(g);
82 }
83 }
84
89 public Solver Solver
90 {
91 get
92 {
93
94 return Context.MkSolver(this);
95 }
96 }
97
98 #region Internal
99 internal Tactic(Context ctx, IntPtr obj)
100 : base(ctx, obj)
101 {
102 Debug.Assert(ctx != null);
103 }
104 internal Tactic(Context ctx, string name)
105 : base(ctx, Native.Z3_mk_tactic(ctx.nCtx, name))
106 {
107 Debug.Assert(ctx != null);
108 }
109
113 internal class DecRefQueue : IDecRefQueue
114 {
115 public DecRefQueue() : base() { }
116 public DecRefQueue(uint move_limit) : base(move_limit) { }
117 internal override void IncRef(Context ctx, IntPtr obj)
118 {
119 Native.Z3_tactic_inc_ref(ctx.nCtx, obj);
120 }
121
122 internal 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}
Microsoft.Z3.ApplyResult
ApplyResult objects represent the result of an application of a tactic to a goal. It contains the sub...
Definition: ApplyResult.cs:30
Microsoft.Z3.Context
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Microsoft.Z3.Context.Tactic_DRQ
IDecRefQueue Tactic_DRQ
Tactic DRQ
Definition: Context.cs:4790
Microsoft.Z3.Context.MkSolver
Solver MkSolver(Symbol logic=null)
Creates a new (incremental) solver.
Definition: Context.cs:3731
Microsoft.Z3.Goal
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ...
Definition: Goal.cs:32
Microsoft.Z3.ParamDescrs
A ParamDescrs describes a set of parameters.
Definition: ParamDescrs.cs:29
Microsoft.Z3.Params
A Params objects represents a configuration in the form of Symbol/value pairs.
Definition: Params.cs:29
Microsoft.Z3.Solver
Solvers.
Definition: Solver.cs:31
Microsoft.Z3.Tactic
Tactics are the basic building block for creating custom solvers for specific problem domains....
Definition: Tactic.cs:32
Microsoft.Z3.Tactic.Help
string Help
A string containing a description of parameters accepted by the tactic.
Definition: Tactic.cs:37
Microsoft.Z3.Tactic.ParameterDescriptions
ParamDescrs ParameterDescriptions
Retrieves parameter descriptions for Tactics.
Definition: Tactic.cs:50
Microsoft.Z3.Tactic.Apply
ApplyResult Apply(Goal g, Params p=null)
Execute the tactic over the goal.
Definition: Tactic.cs:58
Microsoft.Z3.Z3Object
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33
Microsoft.Z3
Definition: AlgebraicNum.cs:27
Z3_mk_tactic
Z3_tactic Z3_API Z3_mk_tactic(Z3_context c, Z3_string name)
Return a tactic associated with the given name. The complete list of tactics may be obtained using th...