Z3 |

Data Structures | Public Member Functions | Properties
ApplyResult Class Reference

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:

## Data Structures
class | DecRefQueue

## Public Member Functions
override string | ToString ()
| A string representation of the ApplyResult. More...
Public Member Functions inherited from Z3Object
void | Dispose ()
| Disposes of the underlying native Z3 object. More...

## Properties
uint | NumSubgoals`[get]`
| The number of Subgoals. More...
Goal[] | Subgoals`[get]`
| Retrieves the subgoals from the ApplyResult. More...

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

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

## Property Documentation

## ◆ NumSubgoals

uint NumSubgoals
| get

The number of Subgoals.

Definition at line 34 of file ApplyResult.cs.

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

Referenced by Goal.Simplify().

## ◆ Subgoals

Goal [] Subgoals
| get

Retrieves the subgoals from the ApplyResult.

Definition at line 42 of file ApplyResult.cs.

43 {
44 get
45 {
46
47 uint n = NumSubgoals;
48 Goal[] res = new Goal[n];
49 for (uint i = 0; i < n; i++)
50 res[i] = new Goal(Context, Native.Z3_apply_result_get_subgoal(Context.nCtx, NativeObject, i));
51 return res;
52 }
53 }
Microsoft.Z3.ApplyResult.NumSubgoals
uint NumSubgoals
The number of Subgoals.
Definition: ApplyResult.cs:35

Referenced by Goal.Simplify().