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 }
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 }
BoolExpr MkTrue()
The true Term.
Definition: Context.cs:815
BoolExpr MkAnd(params BoolExpr[] t)
Create an expression representing t[0] and t[1] and ....
Definition: Context.cs:956
uint Size
The number of formulas in the goal.
Definition: Goal.cs:132
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 }
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 }
Tactic MkTactic(string name)
Creates a new Tactic.
Definition: Context.cs:3334
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 }
Z3_goal_prec Precision
The precision of the goal.
Definition: Goal.cs:42
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().