Module AltErgoLib.Util

exception Timeout
exception Unsolvable
exception Cmp of int
module MI : Map.S with type key = int
module SI : Set.S with type elt = int
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
type theories_extensions =
  1. | Sum
  2. | Adt
  3. | Arrays
  4. | Records
  5. | Bitv
  6. | LIA
  7. | LRA
  8. | NRA
  9. | NIA
  10. | FPA
type axiom_kind =
  1. | Default
  2. | Propagator
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;
  2. triggers_var : bool;
  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