Module 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

| Th_assumed of int

Increment the counter for each term assumed in the theories environment

Define the type of increment

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. Errors.run_error.Steps_limit if the number of steps is reached

val reset_steps : unit -> unit

Reset the global steps counter

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

Incrementality

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