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

---

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 30 of file ApplyResult.cs.

---

Member Function Documentation

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.

Returns:

A model for 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);
        }

---

Property Documentation

uint NumSubgoals [get]

The number of Subgoals.

Definition at line 36 of file ApplyResult.cs.

Referenced by Goal.Simplify().

Goal [] Subgoals [get]

Retrieves the subgoals from the ApplyResult.

Definition at line 44 of file ApplyResult.cs.

Referenced by Goal.Simplify().