Module AltErgoLib.Util

exception Timeout
exception Step_limit_reached of int
exception Unsolvable
exception Cmp of int
exception Not_implemented of string
module MI : Map.S with type key = int
module SI : Set.S with type elt = int
module MS : Map.S with type key = string
module SS : Set.S with type elt = string
type case_split_policy =
  1. | AfterTheoryAssume
  2. | BeforeMatching
  3. | AfterMatching

Different values for -case-split-policy option: -after-theory-assume (default value): after assuming facts in theory by the SAT -before-matching: just before performing a matching round -after-matching: just after performing a matching round *

type inst_kind =
  1. | Normal
  2. | Forward
  3. | Backward
type sat_solver =
  1. | Tableaux
  2. | Tableaux_CDCL
  3. | CDCL
  4. | CDCL_Tableaux
val pp_sat_solver : Format.formatter -> sat_solver -> unit
type theories_extensions =
  1. | Sum
  2. | Adt
  3. | Arrays
  4. | Records
  5. | Bitv
  6. | LIA
  7. | LRA
  8. | NRA
  9. | NIA
  10. | FPA
  11. | RIA
type axiom_kind =
  1. | Default
  2. | Propagator
type mode =
  1. | Start
  2. | Assert
  3. | Sat
  4. | Unsat

The different modes alt-ergo can be in. https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf#52

val equal_mode : mode -> mode -> bool
val pp_mode : Format.formatter -> mode -> unit
val th_ext_of_string : string -> theories_extensions option
val string_of_th_ext : theories_extensions -> string
val compare_algebraic : 'a -> 'a -> (('a * 'a) -> int) -> int

generic function for comparing algebraic data types. compare_algebraic a b f

  • Stdlib.compare a b is used if
val cmp_lists : 'a list -> 'a list -> ('a -> 'a -> int) -> int
type matching_env = {
  1. nb_triggers : int;
    (*

    Limit the number of trigger generated per axiom.

    *)
  2. triggers_var : bool;
    (*

    If true, we allow trigger variables during the trigger generation.

    *)
  3. no_ematching : bool;
  4. greedy : bool;
  5. use_cs : bool;
  6. backward : inst_kind;
}
val loop : f:(int -> 'a -> 'b -> 'b) -> max:int -> elt:'a -> init:'b -> 'b

Loops from 0 to max and returns (f max elt ... (f 1 elt (f 0 elt init)))...). Returns init if max < 0

val print_list : sep:string -> pp:(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
val print_list_pp : sep:(Format.formatter -> unit -> unit) -> pp:(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
val internal_error : ('a, Format.formatter, unit, 'b) format4 -> 'a