Module Z3.Goal

module Goal: sig .. end

Goals

A goal (aka problem). A goal is essentially a of formulas, that can be solved and/or transformed using tactics and solvers.

type goal

val get_precision : goal -> Z3enums.goal_prec

The precision of the goal.

Goals can be transformed using over and under approximations. An under approximation is applied when the objective is to find a model for a given goal. An over approximation is applied when the objective is to find a proof for a given goal.

val is_precise : goal -> bool

Indicates whether the goal is precise.

val is_underapproximation : goal -> bool

Indicates whether the goal is an under-approximation.

val is_overapproximation : goal -> bool

Indicates whether the goal is an over-approximation.

val is_garbage : goal -> bool

Indicates whether the goal is garbage (i.e., the product of over- and under-approximations).

val add : goal -> Expr.expr list -> unit

Adds the constraints to the given goal.

val is_inconsistent : goal -> bool

Indicates whether the goal contains `false'.

val get_depth : goal -> int

The depth of the goal. This tracks how many transformations were applied to it.

val reset : goal -> unit

Erases all formulas from the given goal.

val get_size : goal -> int

The number of formulas in the goal.

val get_formulas : goal -> Expr.expr list

The formulas in the goal.

val get_num_exprs : goal -> int

The number of formulas, subformulas and terms in the goal.

val is_decided_sat : goal -> bool

Indicates whether the goal is empty, and it is precise or the product of an under approximation.

val is_decided_unsat : goal -> bool

Indicates whether the goal contains `false', and it is precise or the product of an over approximation.

val translate : goal -> context -> goal

Translates (copies) the Goal to another context..

val simplify : goal -> Params.params option -> goal

Simplifies the goal. Essentially invokes the `simplify' tactic on the goal.

val mk_goal : context -> bool -> bool -> bool -> goal

Creates a new Goal.

Note that the Context must have been created with proof generation support if the fourth argument is set to true here.

val to_string : goal -> string

A string representation of the Goal.

val as_expr : goal -> Expr.expr

Goal to BoolExpr conversion.