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

void Add ( params BoolExpr[]  constraints )

inline

Alias for Assert.

Definition at line 96 of file Goal.cs.

        {
            Assert(constraints);
        }

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

        {
            Tactic t = Context.MkTactic("simplify");
            ApplyResult res = t.Apply(this, p);

            if (res.NumSubgoals == 0)
                throw new Z3Exception("No subgoals");
            else
                return res.Subgoals[0];
        }

override string ToString ( )

inline

Goal to string conversion.

Returns

A string representation of the Goal.

Definition at line 206 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 180 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 116 of file Goal.cs.

BoolExpr [] Formulas

get

The formulas in the goal.

Definition at line 140 of file Goal.cs.

bool Inconsistent

get

Indicates whether the goal contains `false'.

Definition at line 105 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 165 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 173 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 157 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 132 of file Goal.cs.