ApplyResult objects represent the result of an application of a tactic to a goal. It contains the subgoals that were produced. More...

Inheritance diagram for ApplyResult:

Public Member Functions
override string	ToString ()
	A string representation of the ApplyResult.

Public Member Functions inherited from Z3Object
void	Dispose ()
	Disposes of the underlying native Z3 object.

Properties
uint	NumSubgoals `[get]`
	The number of Subgoals.

Goal[]	Subgoals `[get]`
	Retrieves the subgoals from the ApplyResult.

Properties inherited from Z3Object
Context	Context `[get]`
	Access Context object.

Detailed Description

ApplyResult objects represent the result of an application of a tactic to a goal. It contains the subgoals that were produced.

Definition at line 29 of file ApplyResult.cs.

Member Function Documentation

◆ ToString()

override string ToString ( )

inline

A string representation of the ApplyResult.

Definition at line 58 of file ApplyResult.cs.

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

Property Documentation

◆ NumSubgoals

uint NumSubgoals

get

The number of Subgoals.

Definition at line 34 of file ApplyResult.cs.

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

◆ Subgoals

Goal [] Subgoals

get

Retrieves the subgoals from the ApplyResult.

Definition at line 42 of file ApplyResult.cs.

        {
            get
            {
 
                uint n = NumSubgoals;
                Goal[] res = new Goal[n];
                for (uint i = 0; i < n; i++)
                    res[i] = new Goal(Context, Native.Z3_apply_result_get_subgoal(Context.nCtx, NativeObject, i));
                return res;
            }
        }