module Goal:sig
..end
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
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
val is_underapproximation : goal -> bool
val is_overapproximation : goal -> bool
val is_garbage : goal -> bool
val add : goal -> Expr.expr list -> unit
val is_inconsistent : goal -> bool
val get_depth : goal -> int
val reset : goal -> unit
val get_size : goal -> int
val get_formulas : goal -> Expr.expr list
val get_num_exprs : goal -> int
val is_decided_sat : goal -> bool
val is_decided_unsat : goal -> bool
val translate : goal -> context -> goal
val simplify : goal -> Params.params option -> goal
val mk_goal : context -> bool -> bool -> bool -> 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
val as_expr : goal -> Expr.expr