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.