AltErgoLib.Util
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 *
val th_ext_of_string : string -> theories_extensions option
val string_of_th_ext : theories_extensions -> string
generic function for comparing algebraic data types. compare_algebraic a b f
type matching_env = {
nb_triggers : int; |
triggers_var : bool; |
no_ematching : bool; |
greedy : bool; |
use_cs : bool; |
backward : inst_kind; |
}