Module AltErgoLib.UtilSource

Sourceexception Timeout
Sourceexception Unsolvable
Sourceexception Cmp of int
Sourcemodule MI : Map.S with type key = int
Sourcemodule SS : Set.S with type elt = string
Sourcetype 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 *

Sourcetype inst_kind =
  1. | Normal
  2. | Forward
  3. | Backward
Sourcetype sat_solver =
  1. | Tableaux
  2. | Tableaux_CDCL
  3. | CDCL
  4. | CDCL_Tableaux
Sourcetype theories_extensions =
  1. | Sum
  2. | Adt
  3. | Arrays
  4. | Records
  5. | Bitv
  6. | LIA
  7. | LRA
  8. | NRA
  9. | NIA
  10. | FPA
Sourcetype axiom_kind =
  1. | Default
  2. | Propagator
Sourceval th_ext_of_string : string -> theories_extensions option
Sourceval string_of_th_ext : theories_extensions -> string
Sourceval compare_algebraic : 'a -> 'a -> (('a * 'a) -> int) -> int

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

  • Pervasives.compare a b is used if
Sourceval cmp_lists : 'a list -> 'a list -> ('a -> 'a -> int) -> int
Sourcetype 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;
}
Sourceval print_list : sep:string -> pp:(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit
Sourceval print_list_pp : sep:(Format.formatter -> unit -> unit) -> pp:(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit