Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
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 Add (params BoolExpr[] constraints)
 Alias for Assert.
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.

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

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.

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.

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines