Z3 |

Data Structures | Public Member Functions | Properties
Goal Class Reference

A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers. More...

Inheritance diagram for Goal:

## Data Structures
class | DecRefQueue

## Public Member Functions
void | Assert (params BoolExpr[] constraints)
| Adds the constraints to the given goal. More...
void | Add (params BoolExpr[] constraints)
| Alias for Assert. More...
void | Reset ()
| Erases all formulas from the given goal. More...
Model | ConvertModel (Model m)
| Convert a model for the goal into a model of the original goal from which this goal was derived. More...
Goal | Translate (Context ctx)
| Translates (copies) the Goal to the target Context ctx . More...
Goal | Simplify (Params p=null)
| Simplifies the goal. More...
override string | ToString ()
| Goal to string conversion. More...
string | ToDimacs (bool include_names=true)
| Goal to DIMACS formatted string conversion. More...
BoolExpr | AsBoolExpr ()
| Goal to BoolExpr conversion. More...
Public Member Functions inherited from Z3Object
void | Dispose ()
| Disposes of the underlying native Z3 object. More...

## Properties
Z3_goal_prec | Precision`[get]`
| The precision of the goal. More...
bool | IsPrecise`[get]`
| Indicates whether the goal is precise. More...
bool | IsUnderApproximation`[get]`
| Indicates whether the goal is an under-approximation. More...
bool | IsOverApproximation`[get]`
| Indicates whether the goal is an over-approximation. More...
bool | IsGarbage`[get]`
| Indicates whether the goal is garbage (i.e., the product of over- and under-approximations). More...
bool | Inconsistent`[get]`
| Indicates whether the goal contains ‘false’. More...
uint | Depth`[get]`
| The depth of the goal. More...
uint | Size`[get]`
| The number of formulas in the goal. More...
BoolExpr[] | Formulas`[get]`
| The formulas in the goal. More...
uint | NumExprs`[get]`
| The number of formulas, subformulas and terms in the goal. More...
bool | IsDecidedSat`[get]`
| Indicates whether the goal is empty, and it is precise or the product of an under approximation. More...
bool | IsDecidedUnsat`[get]`
| Indicates whether the goal contains ‘false’, and it is precise or the product of an over approximation. More...

## Detailed Description

A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers.

Definition at line 31 of file Goal.cs.

## Member Function Documentation

## ◆ Add()

void Add | ( | params BoolExpr[] | constraints | ) |
| inline

Alias for Assert.

Definition at line 96 of file Goal.cs.

97 {
98 Assert(constraints);
99 }
Microsoft.Z3.Goal.Assert
void Assert(params BoolExpr[] constraints)
Adds the constraints to the given goal.
Definition: Goal.cs:80

## ◆ AsBoolExpr()

BoolExpr AsBoolExpr | ( |  | ) |
| inline

Goal to BoolExpr conversion.

Returns
  A string representation of the Goal.

Definition at line 237 of file Goal.cs.

237 {
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 }
Microsoft.Z3.Context.MkTrue
BoolExpr MkTrue()
The true Term.
Definition: Context.cs:815
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.Goal.Size
uint Size
The number of formulas in the goal.
Definition: Goal.cs:132
Microsoft.Z3.Goal.Formulas
BoolExpr[] Formulas
The formulas in the goal.
Definition: Goal.cs:140

## ◆ Assert()

void Assert | ( | params BoolExpr[] | constraints | ) |
| inline

Adds the constraints to the given goal.

Definition at line 80 of file Goal.cs.

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 }

Referenced by Goal.Add(), and Goal.Translate().

## ◆ ConvertModel()

Model ConvertModel | ( | Model | m | ) |
| inline

Convert a model for the goal into a model of the original goal from which this goal was derived.

Returns
  A model for `g`

Definition at line 181 of file Goal.cs.

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 }
z3py.Model
def Model(ctx=None)
Definition: z3py.py:6579

## ◆ Reset()

void Reset | ( |  | ) |
| inline

Erases all formulas from the given goal.

Definition at line 123 of file Goal.cs.

124 {
125 Native.Z3_goal_reset(Context.nCtx, NativeObject);
126 }

## ◆ Simplify()

Goal Simplify | ( | Params | p = `null` | ) |
| inline

Simplifies the goal.

Essentially invokes the ‘simplify’ tactic on the goal.

Definition at line 204 of file Goal.cs.

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 }
Microsoft.Z3.Context.MkTactic
Tactic MkTactic(string name)
Creates a new Tactic.
Definition: Context.cs:3334
Microsoft.Z3.Tactic.Apply
ApplyResult Apply(Goal g, Params p=null)
Execute the tactic over the goal.
Definition: Tactic.cs:58

## ◆ ToDimacs()

string ToDimacs | ( | bool | include_names = `true` | ) |
| inline

Goal to DIMACS formatted string conversion.

Returns
  A string representation of the Goal.

Definition at line 228 of file Goal.cs.

229 {
230 return Native.Z3_goal_to_dimacs_string(Context.nCtx, NativeObject, (byte)(include_names ? 1 : 0));
231 }

## ◆ ToString()

override string ToString | ( |  | ) |
| inline

Goal to string conversion.

Returns
  A string representation of the Goal.

Definition at line 219 of file Goal.cs.

220 {
221 return Native.Z3_goal_to_string(Context.nCtx, NativeObject);
222 }

## ◆ Translate()

Goal Translate | ( | Context | ctx | ) |
| inline

Translates (copies) the Goal to the target Context ctx .

Definition at line 193 of file Goal.cs.

194 {
195 Debug.Assert(ctx != null);
196
197 return new Goal(ctx, Native.Z3_goal_translate(Context.nCtx, NativeObject, ctx.nCtx));
198 }

## Property Documentation

## ◆ Depth

uint Depth
| get

The depth of the goal.

This tracks how many transformations were applied to it.

Definition at line 115 of file Goal.cs.

116 {
117 get { return Native.Z3_goal_depth(Context.nCtx, NativeObject); }
118 }

## ◆ Formulas

BoolExpr [] Formulas
| get

The formulas in the goal.

Definition at line 139 of file Goal.cs.

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 }

Referenced by Goal.AsBoolExpr().

## ◆ Inconsistent

bool Inconsistent
| get

Indicates whether the goal contains ‘false’.

Definition at line 104 of file Goal.cs.

105 {
106 get { return Native.Z3_goal_inconsistent(Context.nCtx, NativeObject) != 0; }
107 }

## ◆ IsDecidedSat

bool IsDecidedSat
| get

Indicates whether the goal is empty, and it is precise or the product of an under approximation.

Definition at line 163 of file Goal.cs.

164 {
165 get { return Native.Z3_goal_is_decided_sat(Context.nCtx, NativeObject) != 0; }
166 }

## ◆ IsDecidedUnsat

bool IsDecidedUnsat
| get

Indicates whether the goal contains ‘false’, and it is precise or the product of an over approximation.

Definition at line 171 of file Goal.cs.

172 {
173 get { return Native.Z3_goal_is_decided_unsat(Context.nCtx, NativeObject) != 0; }
174 }

## ◆ IsGarbage

bool IsGarbage
| get

Indicates whether the goal is garbage (i.e., the product of over- and under-approximations).

Definition at line 72 of file Goal.cs.

73 {
74 get { return Precision == Z3_goal_prec.Z3_GOAL_UNDER_OVER; }
75 }
Microsoft.Z3.Goal.Precision
Z3_goal_prec Precision
The precision of the goal.
Definition: Goal.cs:42
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

## ◆ IsOverApproximation

bool IsOverApproximation
| get

Indicates whether the goal is an over-approximation.

Definition at line 64 of file Goal.cs.

65 {
66 get { return Precision == Z3_goal_prec.Z3_GOAL_OVER; }
67 }

## ◆ IsPrecise

bool IsPrecise
| get

Indicates whether the goal is precise.

Definition at line 49 of file Goal.cs.

50 {
51 get { return Precision == Z3_goal_prec.Z3_GOAL_PRECISE; }
52 }

## ◆ IsUnderApproximation

bool IsUnderApproximation
| get

Indicates whether the goal is an under-approximation.

Definition at line 56 of file Goal.cs.

57 {
58 get { return Precision == Z3_goal_prec.Z3_GOAL_UNDER; }
59 }

## ◆ NumExprs

uint NumExprs
| get

The number of formulas, subformulas and terms in the goal.

Definition at line 155 of file Goal.cs.

156 {
157 get { return Native.Z3_goal_num_exprs(Context.nCtx, NativeObject); }
158 }

## ◆ Precision

Z3_goal_prec Precision
| get

The precision of the goal.

Goals can be transformed using over and under approximations. An under approximation is applied when the objective is to find a model for a given goal. An over approximation is applied when the objective is to find a proof for a given goal.

Definition at line 41 of file Goal.cs.

42 {
43 get { return (Z3_goal_prec)Native.Z3_goal_precision(Context.nCtx, NativeObject); }
44 }

## ◆ Size

uint Size
| get

The number of formulas in the goal.

Definition at line 131 of file Goal.cs.

132 {
133 get { return Native.Z3_goal_size(Context.nCtx, NativeObject); }
134 }

Referenced by Goal.AsBoolExpr().