Z3
Goal.cs
Go to the documentation of this file.
1/*++
2Copyright (c) 2012 Microsoft Corporation
3
4Module Name:
5
6 Goal.cs
7
8Abstract:
9
10 Z3 Managed API: Goal
11
12Author:
13
14 Christoph Wintersteiger (cwinter) 2012-03-21
15
16Notes:
17
18--*/
19
20using System;
21using System.Diagnostics;
22using System.Linq;
23
24namespace Microsoft.Z3
25{
31 public class Goal : Z3Object
32 {
42 {
43 get { return (Z3_goal_prec)Native.Z3_goal_precision(Context.nCtx, NativeObject); }
44 }
45
49 public bool IsPrecise
50 {
51 get { return Precision == Z3_goal_prec.Z3_GOAL_PRECISE; }
52 }
57 {
58 get { return Precision == Z3_goal_prec.Z3_GOAL_UNDER; }
59 }
60
65 {
66 get { return Precision == Z3_goal_prec.Z3_GOAL_OVER; }
67 }
68
72 public bool IsGarbage
73 {
74 get { return Precision == Z3_goal_prec.Z3_GOAL_UNDER_OVER; }
75 }
76
80 public void Assert(params BoolExpr[] constraints)
81 {
82 Debug.Assert(constraints != null);
83 Debug.Assert(constraints.All(c => c != null));
84
85 Context.CheckContextMatch<BoolExpr>(constraints);
86 foreach (BoolExpr c in constraints)
87 {
88 Debug.Assert(c != null); // It was an assume, now made an assert just to be sure we do not regress
89 Native.Z3_goal_assert(Context.nCtx, NativeObject, c.NativeObject);
90 }
91 }
92
96 public void Add(params BoolExpr[] constraints)
97 {
98 Assert(constraints);
99 }
100
104 public bool Inconsistent
105 {
106 get { return Native.Z3_goal_inconsistent(Context.nCtx, NativeObject) != 0; }
107 }
108
115 public uint Depth
116 {
117 get { return Native.Z3_goal_depth(Context.nCtx, NativeObject); }
118 }
119
123 public void Reset()
124 {
125 Native.Z3_goal_reset(Context.nCtx, NativeObject);
126 }
127
131 public uint Size
132 {
133 get { return Native.Z3_goal_size(Context.nCtx, NativeObject); }
134 }
135
140 {
141 get
142 {
143
144 uint n = Size;
145 BoolExpr[] res = new BoolExpr[n];
146 for (uint i = 0; i < n; i++)
147 res[i] = (BoolExpr)Expr.Create(Context, Native.Z3_goal_formula(Context.nCtx, NativeObject, i));
148 return res;
149 }
150 }
151
155 public uint NumExprs
156 {
157 get { return Native.Z3_goal_num_exprs(Context.nCtx, NativeObject); }
158 }
159
163 public bool IsDecidedSat
164 {
165 get { return Native.Z3_goal_is_decided_sat(Context.nCtx, NativeObject) != 0; }
166 }
167
171 public bool IsDecidedUnsat
172 {
173 get { return Native.Z3_goal_is_decided_unsat(Context.nCtx, NativeObject) != 0; }
174 }
175
182 {
183 if (m != null)
184 return new Model(Context, Native.Z3_goal_convert_model(Context.nCtx, NativeObject, m.NativeObject));
185 else
186 return new Model(Context, Native.Z3_goal_convert_model(Context.nCtx, NativeObject, IntPtr.Zero));
187 }
188
189
194 {
195 Debug.Assert(ctx != null);
196
197 return new Goal(ctx, Native.Z3_goal_translate(Context.nCtx, NativeObject, ctx.nCtx));
198 }
199
204 public Goal Simplify(Params p = null)
205 {
206 Tactic t = Context.MkTactic("simplify");
207 ApplyResult res = t.Apply(this, p);
208
209 if (res.NumSubgoals == 0)
210 throw new Z3Exception("No subgoals");
211 else
212 return res.Subgoals[0];
213 }
214
219 public override string ToString()
220 {
221 return Native.Z3_goal_to_string(Context.nCtx, NativeObject);
222 }
223
228 public string ToDimacs(bool include_names = true)
229 {
230 return Native.Z3_goal_to_dimacs_string(Context.nCtx, NativeObject, (byte)(include_names ? 1 : 0));
231 }
232
238 uint n = Size;
239 if (n == 0)
240 return Context.MkTrue();
241 else if (n == 1)
242 return Formulas[0];
243 else {
244 return Context.MkAnd(Formulas);
245 }
246 }
247
248 #region Internal
249 internal Goal(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
250
251 internal Goal(Context ctx, bool models, bool unsatCores, bool proofs)
252 : base(ctx, Native.Z3_mk_goal(ctx.nCtx, (byte)(models ? 1 : 0), (byte)(unsatCores ? 1 : 0), (byte)(proofs ? 1 : 0)))
253 {
254 Debug.Assert(ctx != null);
255 }
256
257 internal class DecRefQueue : IDecRefQueue
258 {
259 public DecRefQueue() : base() { }
260 public DecRefQueue(uint move_limit) : base(move_limit) { }
261 internal override void IncRef(Context ctx, IntPtr obj)
262 {
263 Native.Z3_goal_inc_ref(ctx.nCtx, obj);
264 }
265
266 internal override void DecRef(Context ctx, IntPtr obj)
267 {
268 Native.Z3_goal_dec_ref(ctx.nCtx, obj);
269 }
270 };
271
272 internal override void IncRef(IntPtr o)
273 {
274 Context.Goal_DRQ.IncAndClear(Context, o);
275 base.IncRef(o);
276 }
277
278 internal override void DecRef(IntPtr o)
279 {
280 Context.Goal_DRQ.Add(o);
281 base.DecRef(o);
282 }
283
284 #endregion
285 }
286}
ApplyResult objects represent the result of an application of a tactic to a goal. It contains the sub...
Definition: ApplyResult.cs:30
uint NumSubgoals
The number of Subgoals.
Definition: ApplyResult.cs:35
Goal[] Subgoals
Retrieves the subgoals from the ApplyResult.
Definition: ApplyResult.cs:43
Boolean expressions
Definition: BoolExpr.cs:32
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Tactic MkTactic(string name)
Creates a new Tactic.
Definition: Context.cs:3334
BoolExpr MkTrue()
The true Term.
Definition: Context.cs:815
IDecRefQueue Goal_DRQ
Goal DRQ
Definition: Context.cs:4755
BoolExpr MkAnd(params BoolExpr[] t)
Create an expression representing t[0] and t[1] and ....
Definition: Context.cs:956
Expressions are terms.
Definition: Expr.cs:31
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ...
Definition: Goal.cs:32
Model ConvertModel(Model m)
Convert a model for the goal into a model of the original goal from which this goal was derived.
Definition: Goal.cs:181
Goal Simplify(Params p=null)
Simplifies the goal.
Definition: Goal.cs:204
void Reset()
Erases all formulas from the given goal.
Definition: Goal.cs:123
void Assert(params BoolExpr[] constraints)
Adds the constraints to the given goal.
Definition: Goal.cs:80
bool IsGarbage
Indicates whether the goal is garbage (i.e., the product of over- and under-approximations).
Definition: Goal.cs:73
string ToDimacs(bool include_names=true)
Goal to DIMACS formatted string conversion.
Definition: Goal.cs:228
uint Size
The number of formulas in the goal.
Definition: Goal.cs:132
BoolExpr AsBoolExpr()
Goal to BoolExpr conversion.
Definition: Goal.cs:237
uint NumExprs
The number of formulas, subformulas and terms in the goal.
Definition: Goal.cs:156
override string ToString()
Goal to string conversion.
Definition: Goal.cs:219
bool IsUnderApproximation
Indicates whether the goal is an under-approximation.
Definition: Goal.cs:57
bool IsDecidedSat
Indicates whether the goal is empty, and it is precise or the product of an under approximation.
Definition: Goal.cs:164
bool IsPrecise
Indicates whether the goal is precise.
Definition: Goal.cs:50
Z3_goal_prec Precision
The precision of the goal.
Definition: Goal.cs:42
bool IsOverApproximation
Indicates whether the goal is an over-approximation.
Definition: Goal.cs:65
Goal Translate(Context ctx)
Translates (copies) the Goal to the target Context ctx .
Definition: Goal.cs:193
BoolExpr[] Formulas
The formulas in the goal.
Definition: Goal.cs:140
void Add(params BoolExpr[] constraints)
Alias for Assert.
Definition: Goal.cs:96
bool Inconsistent
Indicates whether the goal contains ‘false’.
Definition: Goal.cs:105
bool IsDecidedUnsat
Indicates whether the goal contains ‘false’, and it is precise or the product of an over approximatio...
Definition: Goal.cs:172
uint Depth
The depth of the goal.
Definition: Goal.cs:116
A Model contains interpretations (assignments) of constants and functions.
Definition: Model.cs:30
A Params objects represents a configuration in the form of Symbol/value pairs.
Definition: Params.cs:29
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:58
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:32
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33
def Model(ctx=None)
Definition: z3py.py:6579
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Definition: z3_api.h:1408
Z3_goal Z3_API Z3_mk_goal(Z3_context c, bool models, bool unsat_cores, bool proofs)
Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or trans...