Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
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

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.
 
- Public Member Functions inherited from Z3Object
void Dispose ()
 Disposes of the underlying native Z3 object.
 

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