package alt-ergo-lib

You can search for identifiers within the package.

in-package search v0.2.0

The Alt-Ergo SMT prover library

Install

Dune Dependency

alt-ergo.ocamlpro.com Readme Changelog LicenseRef-OCamlpro-Non-Commercial; Apache-2.0 License Edit opam file Versions (15)

Authors

A

Alt-Ergo developers

Maintainers

A

Alt-Ergo developers

Sources

alt-ergo-2.5.2.tbz

sha256=f460c17011f8f6c85e3b9023983b339cc11bc34252ae748e708211378d3f6895

sha512=cc4707f22596838dd242dc2e42b5d744dd0c44f5283c0a36074761d5b8c91e6f46fed2aebb5f6a96d50f94e5da2b74cd18447574668db255a19a6fb0cda9bbb7

doc/alt-ergo-lib/AltErgoLib/Steps/index.html

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 =

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

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

On This Page

Steps counters
1. Incrementality