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...
 
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...
 
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 215 of file Goal.cs.

215  {
216  uint n = Size;
217  if (n == 0)
218  return Context.MkTrue();
219  else if (n == 1)
220  return Formulas[0];
221  else {
222  return Context.MkAnd(Formulas);
223  }
224  }
BoolExpr MkAnd(params BoolExpr[] t)
Create an expression representing t[0] and t[1] and ....
Definition: Context.cs:967
uint Size
The number of formulas in the goal.
Definition: Goal.cs:132
BoolExpr MkTrue()
The true Term.
Definition: Context.cs:836
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  Contract.Requires(constraints != null);
83  Contract.Requires(Contract.ForAll(constraints, c => c != null));
84 
85  Context.CheckContextMatch<BoolExpr>(constraints);
86  foreach (BoolExpr c in constraints)
87  {
88  Contract.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  }

§ 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 191 of file Goal.cs.

192  {
193  Tactic t = Context.MkTactic("simplify");
194  ApplyResult res = t.Apply(this, p);
195 
196  if (res.NumSubgoals == 0)
197  throw new Z3Exception("No subgoals");
198  else
199  return res.Subgoals[0];
200  }
Tactic MkTactic(string name)
Creates a new Tactic.
Definition: Context.cs:3383
ApplyResult Apply(Goal g, Params p=null)
Execute the tactic over the goal.
Definition: Tactic.cs:60

§ ToString()

override string ToString ( )
inline

Goal to string conversion.

Returns
A string representation of the Goal.

Definition at line 206 of file Goal.cs.

207  {
208  return Native.Z3_goal_to_string(Context.nCtx, NativeObject);
209  }

§ Translate()

Goal Translate ( Context  ctx)
inline

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

Definition at line 180 of file Goal.cs.

181  {
182  Contract.Requires(ctx != null);
183 
184  return new Goal(ctx, Native.Z3_goal_translate(Context.nCtx, NativeObject, ctx.nCtx));
185  }

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.

§ Formulas

BoolExpr [] Formulas
get

The formulas in the goal.

Definition at line 140 of file Goal.cs.

§ Inconsistent

bool Inconsistent
get

Indicates whether the goal contains `false'.

Definition at line 105 of file Goal.cs.

§ IsDecidedSat

bool IsDecidedSat
get

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

Definition at line 165 of file Goal.cs.

§ IsDecidedUnsat

bool IsDecidedUnsat
get

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

Definition at line 173 of file Goal.cs.

§ 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.

§ IsOverApproximation

bool IsOverApproximation
get

Indicates whether the goal is an over-approximation.

Definition at line 65 of file Goal.cs.

§ IsPrecise

bool IsPrecise
get

Indicates whether the goal is precise.

Definition at line 50 of file Goal.cs.

§ IsUnderApproximation

bool IsUnderApproximation
get

Indicates whether the goal is an under-approximation.

Definition at line 57 of file Goal.cs.

§ NumExprs

uint NumExprs
get

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

Definition at line 157 of file Goal.cs.

§ 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.

§ Size

uint Size
get

The number of formulas in the goal.

Definition at line 132 of file Goal.cs.