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 35 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 43 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  }

Referenced by Goal.Simplify().

Microsoft.Z3.ApplyResult.NumSubgoals
uint NumSubgoals
The number of Subgoals.
Definition: ApplyResult.cs:35