Steps (alt-ergo-lib.AltErgoLib.Steps)

Steps counters

type incr_kind =

| Matching
(*
Matching step increment
*)
| Interval_Calculus
(*
Arith : Interval Calculus increment
*)
| Fourier
(*
Arith : FourierMotzkin step increment
*)
| Omega
(*
Arith : number of omega procedure on Real and Int
*)
| Uf
(*
UF step increment
*)
| Ac
(*
AC step reasoning
*)
| CP
(*
Constraint propagation
*)
| Th_assumed of int
(*
Increment the counter for each term assumed in the theories environment
*)

Define the type of increment

val get_steps_bound : unit -> int

Returns the max number of bounds

val set_steps_bound : int -> unit

Sets the max number of bounds

val incr : incr_kind -> unit

Increment the number of steps depending of the incr_kind

raises Errors.Error.Invalid_steps_count
if the number of steps is inbound by the --steps-bound option.

raises Run_error
Errors.run_error.Invalid_steps_count if the number of steps sent to the theories is invalid.

val reset_steps : unit -> unit

Reset the global steps counter

val save_steps : unit -> unit

Saves the step counters

val reinit_steps : unit -> unit

Reinitializes the step counters

val get_steps : unit -> int

Return the number of steps

val cs_steps : unit -> int

Return the number of case-split steps

val incr_cs_steps : unit -> unit

Increase the number of case-split steps

val apply_without_step_limit : (unit -> 'a) -> 'a

Disables the step limit during the execution of the continuation.

val push_steps : unit -> unit

Save all the steps value in an internal stack for each push command

val pop_steps : unit -> unit

Pop the last steps value when a pop command is processed