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  }

◆ 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  }

◆ 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  }

◆ 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  }

◆ 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 116 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 140 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 105 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 164 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 172 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 73 of file Goal.cs.

73  {
74  get { return Precision == Z3_goal_prec.Z3_GOAL_UNDER_OVER; }
75  }

◆ IsOverApproximation

bool IsOverApproximation
get

Indicates whether the goal is an over-approximation.

Definition at line 65 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 50 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 57 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 156 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 42 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 132 of file Goal.cs.

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

Referenced by Goal.AsBoolExpr().

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:1406
Microsoft.Z3.Goal.Assert
void Assert(params BoolExpr[] constraints)
Adds the constraints to the given goal.
Definition: Goal.cs:80
Microsoft.Z3.Tactic.Apply
ApplyResult Apply(Goal g, Params p=null)
Execute the tactic over the goal.
Definition: Tactic.cs:58
z3py.Model
def Model(ctx=None)
Definition: z3py.py:6277
Microsoft.Z3.Context.MkTrue
BoolExpr MkTrue()
The true Term.
Definition: Context.cs:815
Microsoft.Z3.Goal.Formulas
BoolExpr[] Formulas
The formulas in the goal.
Definition: Goal.cs:140
Microsoft.Z3.Goal.Size
uint Size
The number of formulas in the goal.
Definition: Goal.cs:132
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.Context.MkTactic
Tactic MkTactic(string name)
Creates a new Tactic.
Definition: Context.cs:3334