Z3 |

Goal.cs
Go to the documentation of this file.
1/*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 Goal.cs
7
8 Abstract:
9
10 Z3 Managed API: Goal
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 using System.Linq;
23
24 namespace Microsoft.Z3
25{
31 public class Goal : Z3Object
32 {
41 public Z3_goal_prec Precision
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 }
56 public bool IsUnderApproximation
57 {
58 get { return Precision == Z3_goal_prec.Z3_GOAL_UNDER; }
59 }
60
64 public bool IsOverApproximation
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
139 public BoolExpr[] Formulas
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
181 public Model ConvertModel(Model m)
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
193 public Goal Translate(Context ctx)
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
237 public BoolExpr AsBoolExpr() {
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}
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.ApplyResult.NumSubgoals
uint NumSubgoals
The number of Subgoals.
Definition: ApplyResult.cs:35
Microsoft.Z3.ApplyResult.Subgoals
Goal[] Subgoals
Retrieves the subgoals from the ApplyResult.
Definition: ApplyResult.cs:43
Microsoft.Z3.BoolExpr
Boolean expressions
Definition: BoolExpr.cs:32
Microsoft.Z3.Context
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Microsoft.Z3.Context.MkTactic
Tactic MkTactic(string name)
Creates a new Tactic.
Definition: Context.cs:3334
Microsoft.Z3.Context.MkTrue
BoolExpr MkTrue()
The true Term.
Definition: Context.cs:815
Microsoft.Z3.Context.Goal_DRQ
IDecRefQueue Goal_DRQ
Goal DRQ
Definition: Context.cs:4755
Microsoft.Z3.Context.MkAnd
BoolExpr MkAnd(params BoolExpr[] t)
Create an expression representing t[0] and t[1] and ....
Definition: Context.cs:956
Microsoft.Z3.Expr
Expressions are terms.
Definition: Expr.cs:31
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.Goal.ConvertModel
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
Microsoft.Z3.Goal.Simplify
Goal Simplify(Params p=null)
Simplifies the goal.
Definition: Goal.cs:204
Microsoft.Z3.Goal.Reset
void Reset()
Erases all formulas from the given goal.
Definition: Goal.cs:123
Microsoft.Z3.Goal.Assert
void Assert(params BoolExpr[] constraints)
Adds the constraints to the given goal.
Definition: Goal.cs:80
Microsoft.Z3.Goal.IsGarbage
bool IsGarbage
Indicates whether the goal is garbage (i.e., the product of over- and under-approximations).
Definition: Goal.cs:73
Microsoft.Z3.Goal.ToDimacs
string ToDimacs(bool include_names=true)
Goal to DIMACS formatted string conversion.
Definition: Goal.cs:228
Microsoft.Z3.Goal.Size
uint Size
The number of formulas in the goal.
Definition: Goal.cs:132
Microsoft.Z3.Goal.AsBoolExpr
BoolExpr AsBoolExpr()
Goal to BoolExpr conversion.
Definition: Goal.cs:237
Microsoft.Z3.Goal.NumExprs
uint NumExprs
The number of formulas, subformulas and terms in the goal.
Definition: Goal.cs:156
Microsoft.Z3.Goal.ToString
override string ToString()
Goal to string conversion.
Definition: Goal.cs:219
Microsoft.Z3.Goal.IsUnderApproximation
bool IsUnderApproximation
Indicates whether the goal is an under-approximation.
Definition: Goal.cs:57
Microsoft.Z3.Goal.IsDecidedSat
bool IsDecidedSat
Indicates whether the goal is empty, and it is precise or the product of an under approximation.
Definition: Goal.cs:164
Microsoft.Z3.Goal.IsPrecise
bool IsPrecise
Indicates whether the goal is precise.
Definition: Goal.cs:50
Microsoft.Z3.Goal.Precision
Z3_goal_prec Precision
The precision of the goal.
Definition: Goal.cs:42
Microsoft.Z3.Goal.IsOverApproximation
bool IsOverApproximation
Indicates whether the goal is an over-approximation.
Definition: Goal.cs:65
Microsoft.Z3.Goal.Translate
Goal Translate(Context ctx)
Translates (copies) the Goal to the target Context ctx .
Definition: Goal.cs:193
Microsoft.Z3.Goal.Formulas
BoolExpr[] Formulas
The formulas in the goal.
Definition: Goal.cs:140
Microsoft.Z3.Goal.Add
void Add(params BoolExpr[] constraints)
Alias for Assert.
Definition: Goal.cs:96
Microsoft.Z3.Goal.Inconsistent
bool Inconsistent
Indicates whether the goal contains ‘false’.
Definition: Goal.cs:105
Microsoft.Z3.Goal.IsDecidedUnsat
bool IsDecidedUnsat
Indicates whether the goal contains ‘false’, and it is precise or the product of an over approximatio...
Definition: Goal.cs:172
Microsoft.Z3.Goal.Depth
uint Depth
The depth of the goal.
Definition: Goal.cs:116
Microsoft.Z3.Model
A Model contains interpretations (assignments) of constants and functions.
Definition: Model.cs:30
Microsoft.Z3.Params
A Params objects represents a configuration in the form of Symbol/value pairs.
Definition: Params.cs:29
Microsoft.Z3.Tactic
Tactics are the basic building block for creating custom solvers for specific problem domains....
Definition: Tactic.cs:32
Microsoft.Z3.Tactic.Apply
ApplyResult Apply(Goal g, Params p=null)
Execute the tactic over the goal.
Definition: Tactic.cs:58
Microsoft.Z3.Z3Exception
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:32
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
z3py.Model
def Model(ctx=None)
Definition: z3py.py:6579
Z3_goal_prec
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_mk_goal
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...