Module AltErgoLib.Util

exception Timeout
exception Unsolvable
exception Cmp of int
module MI : Stdlib.Map.S with type key = int
module SS : Stdlib.Set.S with type elt = string
type case_split_policy =
| AfterTheoryAssume
| BeforeMatching
| 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 =
| Normal
| Forward
| Backward
type sat_solver =
| Tableaux
| Tableaux_CDCL
| CDCL
| CDCL_Tableaux
type theories_extensions =
| Sum
| Adt
| Arrays
| Records
| Bitv
| LIA
| LRA
| NRA
| NIA
| FPA
type axiom_kind =
| Default
| 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

  • Pervasives.compare a b is used if
val cmp_lists : 'a list -> 'a list -> ( 'a -> 'a -> int ) -> int
type matching_env = {
nb_triggers : int;
triggers_var : bool;
no_ematching : bool;
greedy : bool;
use_cs : bool;
backward : inst_kind;
}
val print_list : sep:string -> pp:( Stdlib.Format.formatter -> 'a -> unit ) -> Stdlib.Format.formatter -> 'a list -> unit
val print_list_pp : sep:( Stdlib.Format.formatter -> unit -> unit ) -> pp:( Stdlib.Format.formatter -> 'a -> unit ) -> Stdlib.Format.formatter -> 'a list -> unit