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:

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...
Properties inherited from Z3Object
Context	Context [get]
	Access Context object 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.

        {
            Assert(constraints);
        }

AsBoolExpr()

BoolExpr AsBoolExpr ( )

inline

Goal to BoolExpr conversion.

Returns

A string representation of the Goal.

Definition at line 237 of file Goal.cs.

                                     {
            uint n = Size;
            if (n == 0) 
                return Context.MkTrue();
            else if (n == 1)                
                return Formulas[0];
            else {
                return Context.MkAnd(Formulas);
            }
        }

Assert()

void Assert ( params BoolExpr[]  constraints )

inline

Adds the constraints to the given goal.

Definition at line 80 of file Goal.cs.

        {
            Debug.Assert(constraints != null);
            Debug.Assert(constraints.All(c => c != null));
 
            Context.CheckContextMatch<BoolExpr>(constraints);
            foreach (BoolExpr c in constraints)
            {
                Debug.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);
            }
        }

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.

        {
            if (m != null)
               return new Model(Context, Native.Z3_goal_convert_model(Context.nCtx, NativeObject, m.NativeObject));
            else
               return new Model(Context, Native.Z3_goal_convert_model(Context.nCtx, NativeObject, IntPtr.Zero));
        }

Reset()

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);
        }

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.

        {
            using Tactic t = Context.MkTactic("simplify");
            using ApplyResult res = t.Apply(this, p);
 
            if (res.NumSubgoals == 0)
                throw new Z3Exception("No subgoals");
            else
                return res.Subgoals[0];
        }

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.

        {
            return Native.Z3_goal_to_dimacs_string(Context.nCtx, NativeObject, (byte)(include_names ? 1 : 0));
        }

ToString()

override string ToString ( )

inline

Goal to string conversion.

Returns

A string representation of the Goal.

Definition at line 219 of file Goal.cs.

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

Translate()

Goal Translate ( Context  ctx )

inline

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

Definition at line 193 of file Goal.cs.

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

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.

        {
            get { return Native.Z3_goal_depth(Context.nCtx, NativeObject); }
        }

Formulas

BoolExpr [] Formulas

get

The formulas in the goal.

Definition at line 139 of file Goal.cs.

        {
            get
            {
 
                uint n = Size;
                BoolExpr[] res = new BoolExpr[n];
                for (uint i = 0; i < n; i++)
                    res[i] = (BoolExpr)Expr.Create(Context, Native.Z3_goal_formula(Context.nCtx, NativeObject, i));
                return res;
            }
        }

Referenced by Goal.AsBoolExpr().

Inconsistent

bool Inconsistent

get

Indicates whether the goal contains ‘false’.

Definition at line 104 of file Goal.cs.

        {
            get { return Native.Z3_goal_inconsistent(Context.nCtx, NativeObject) != 0; }
        }

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.

        {
            get { return Native.Z3_goal_is_decided_sat(Context.nCtx, NativeObject) != 0; }
        }

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.

        {
            get { return Native.Z3_goal_is_decided_unsat(Context.nCtx, NativeObject) != 0; }
        }

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.

        {
            get { return Precision == Z3_goal_prec.Z3_GOAL_UNDER_OVER; }
        }

IsOverApproximation

bool IsOverApproximation

get

Indicates whether the goal is an over-approximation.

Definition at line 64 of file Goal.cs.

        {
            get { return Precision == Z3_goal_prec.Z3_GOAL_OVER; }
        }

IsPrecise

bool IsPrecise

get

Indicates whether the goal is precise.

Definition at line 49 of file Goal.cs.

        {
            get { return Precision == Z3_goal_prec.Z3_GOAL_PRECISE; }
        }

IsUnderApproximation

bool IsUnderApproximation

get

Indicates whether the goal is an under-approximation.

Definition at line 56 of file Goal.cs.

        {
            get { return Precision == Z3_goal_prec.Z3_GOAL_UNDER; }
        }

NumExprs

uint NumExprs

get

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

Definition at line 155 of file Goal.cs.

        {
            get { return Native.Z3_goal_num_exprs(Context.nCtx, NativeObject); }
        }

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.

        {
            get { return (Z3_goal_prec)Native.Z3_goal_precision(Context.nCtx, NativeObject); }
        }

Size

uint Size

get

The number of formulas in the goal.

Definition at line 131 of file Goal.cs.

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

Referenced by Goal.AsBoolExpr().