package alt-ergo-lib

  1. Overview
  2. Docs
package alt-ergo-lib
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

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