package alt-ergo-lib

  1. Overview
  2. Docs

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.

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