Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
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.
 
void Reset ()
 Erases all formulas from the given goal.
 
Goal Translate (Context ctx)
 Translates (copies) the Goal to the target Context ctx .
 
Goal Simplify (Params p=null)
 Simplifies the goal.
 
override string ToString ()
 Goal to string conversion.
 
- Public Member Functions inherited from Z3Object
void Dispose ()
 Disposes of the underlying native Z3 object.
 

Properties

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

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

void Assert ( params BoolExpr[]  constraints)
inline

Adds the constraints to the given goal.

Definition at line 80 of file Goal.cs.

{
Contract.Requires(constraints != null);
Contract.Requires(Contract.ForAll(constraints, c => c != null));
Context.CheckContextMatch(constraints);
foreach (BoolExpr c in constraints)
{
Contract.Assert(c != null); // It was an assume, now made an assert just to be sure we do not regress
Native.Z3_goal_assert(Context.nCtx, NativeObject, c.NativeObject);
}
}
void Reset ( )
inline

Erases all formulas from the given goal.

Definition at line 115 of file Goal.cs.

{
Native.Z3_goal_reset(Context.nCtx, NativeObject);
}
Goal Simplify ( Params  p = null)
inline

Simplifies the goal.

Essentially invokes the `simplify' tactic on the goal.

Definition at line 183 of file Goal.cs.

{
Tactic t = Context.MkTactic("simplify");
ApplyResult res = t.Apply(this, p);
if (res.NumSubgoals == 0)
return Context.MkGoal();
else
return res.Subgoals[0];
}
override string ToString ( )
inline

Goal to string conversion.

Returns
A string representation of the Goal.

Definition at line 198 of file Goal.cs.

{
return Native.Z3_goal_to_string(Context.nCtx, NativeObject);
}
Goal Translate ( Context  ctx)
inline

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

Definition at line 172 of file Goal.cs.

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

Property Documentation

uint Depth
get

The depth of the goal.

This tracks how many transformations were applied to it.

Definition at line 108 of file Goal.cs.

BoolExpr [] Formulas
get

The formulas in the goal.

Definition at line 132 of file Goal.cs.

bool Inconsistent
get

Indicates whether the goal contains `false'.

Definition at line 97 of file Goal.cs.

bool IsDecidedSat
get

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

Definition at line 157 of file Goal.cs.

bool IsDecidedUnsat
get

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

Definition at line 165 of file Goal.cs.

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.

bool IsOverApproximation
get

Indicates whether the goal is an over-approximation.

Definition at line 65 of file Goal.cs.

bool IsPrecise
get

Indicates whether the goal is precise.

Definition at line 50 of file Goal.cs.

bool IsUnderApproximation
get

Indicates whether the goal is an under-approximation.

Definition at line 57 of file Goal.cs.

uint NumExprs
get

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

Definition at line 149 of file Goal.cs.

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.

uint Size
get

The number of formulas in the goal.

Definition at line 124 of file Goal.cs.