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

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

Member Function Documentation

◆ ConvertModel()

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));
         }

◆ ToString()

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

◆ NumSubgoals

uint NumSubgoals

get

The number of Subgoals.

Definition at line 36 of file ApplyResult.cs.

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

Referenced by Goal.Simplify().

◆ Subgoals

Goal [] Subgoals

get

Retrieves the subgoals from the ApplyResult.

Definition at line 44 of file ApplyResult.cs.

         {
             get
             {
                 Contract.Ensures(Contract.Result<Goal[]>() != null);
                 Contract.Ensures(Contract.Result<Goal[]>().Length == this.NumSubgoals);
 
                 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;
             }
         }