ApplyResult objects represent the result of an application of a tactic to a goal. It contains the subgoals that were produced. More...
Data Structures | |
class | DecRefQueue |
Public Member Functions | |
Model | ConvertModel (uint i, Model m) |
Convert a model for the subgoal i into a model for the original goal g , that the ApplyResult was obtained from. | |
override string | ToString () |
A string representation of the ApplyResult. | |
Properties | |
uint | NumSubgoals [get] |
The number of Subgoals. | |
Goal[] | Subgoals [get] |
Retrieves the subgoals from the ApplyResult. |
ApplyResult objects represent the result of an application of a tactic to a goal. It contains the subgoals that were produced.
Definition at line 30 of file ApplyResult.cs.
Model ConvertModel | ( | uint | i, |
Model | m | ||
) | [inline] |
Convert a model for the subgoal i into a model for the original goal g
, that the ApplyResult was obtained from.
g
Definition at line 63 of file ApplyResult.cs.
{ Contract.Requires(m != null); Contract.Ensures(Contract.Result<Model>() != null); return new Model(Context, Native.Z3_apply_result_convert_model(Context.nCtx, NativeObject, i, m.NativeObject)); }
override string ToString | ( | ) | [inline] |
A string representation of the ApplyResult.
Definition at line 74 of file ApplyResult.cs.
{
return Native.Z3_apply_result_to_string(Context.nCtx, NativeObject);
}
uint NumSubgoals [get] |
The number of Subgoals.
Definition at line 36 of file ApplyResult.cs.
Referenced by Goal.Simplify().
Retrieves the subgoals from the ApplyResult.
Definition at line 44 of file ApplyResult.cs.
Referenced by Goal.Simplify().