Module AltErgoLib.Steps

Module_Name

This module aims to count the number of steps in the theories used to solve the problem.

Steps counters

type incr_kind =
  1. | Matching
    (*

    Matching step increment

    *)
  2. | Interval_Calculus
    (*

    Arith : Interval Calculus increment

    *)
  3. | Fourier
    (*

    Arith : FourierMotzkin step increment

    *)
  4. | Omega
    (*

    Arith : number of omega procedure on Real and Int

    *)
  5. | Uf
    (*

    UF step increment

    *)
  6. | Ac
    (*

    AC step reasoning

    *)
  7. | CP
    (*

    Constraint propagation

    *)
  8. | 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 {!Util.Step_limit_reached}

    if the number of steps is reached

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 with_step_limit : int -> scope:(unit -> 'a) -> 'a

with_step_limit limit ~scope calls scope with the provided limit. The limit is local: only steps performed during the call to scope are counted towards the limit (in particular, any steps that have already been recorded are *NOT* counted towards the limit).

with_step_limit is not guaranteed to raise if the limit is reached, as the Util.Step_limit_reached exception might be caught by scope.

with_step_limit respects any current limit enforced by set_steps_bound or another call to with_step_limit higher in the call stack: if a parent limit would be reached, then this limit is also considered as reached.

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