Module Z3.Tactic.ApplyResult

module ApplyResult: sig .. end
Tactic application results

ApplyResult objects represent the result of an application of a tactic to a goal. It contains the subgoals that were produced.


type apply_result 
val get_num_subgoals : apply_result -> int
The number of Subgoals.
val get_subgoals : apply_result -> Goal.goal list
Retrieves the subgoals from the apply_result.
val get_subgoal : apply_result -> int -> Goal.goal
Retrieves a subgoal from the apply_result.
val convert_model : apply_result -> int -> Model.model -> Model.model
Convert a model for a subgoal into a model for the original goal g, that the ApplyResult was obtained from. #return A model for g
val to_string : apply_result -> string
A string representation of the ApplyResult.