Module AltErgoLib.StepsSource

Module_Name

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

Steps counters

Sourcetype 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. | Th_assumed of int
    (*

    Increment the counter for each term assumed in the theories environment

    *)

Define the type of increment

Sourceval 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.

Sourceval reset_steps : unit -> unit

Reset the global steps counter

Sourceval get_steps : unit -> int

Return the number of steps

Sourceval cs_steps : unit -> int

Return the number of case-split steps

Sourceval incr_cs_steps : unit -> unit

Increase the number of case-split steps

Incrementality

Sourceval push_steps : unit -> unit

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

Sourceval pop_steps : unit -> unit

Pop the last steps value when a pop command is processed