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 pp_sat_solver : Format.formatter -> sat_solver -> unitThe different modes alt-ergo can be in. https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf#52
val pp_mode : Format.formatter -> mode -> unitval th_ext_of_string : string -> theories_extensions optionval string_of_th_ext : theories_extensions -> stringgeneric function for comparing algebraic data types. compare_algebraic a b f
type matching_env = {nb_triggers : int;Limit the number of trigger generated per axiom.
*)triggers_var : bool;If true, we allow trigger variables during the trigger generation.
no_ematching : bool;greedy : bool;use_cs : bool;backward : inst_kind;}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 ->
unitval print_list_pp :
sep:(Format.formatter -> unit -> unit) ->
pp:(Format.formatter -> 'a -> unit) ->
Format.formatter ->
'a list ->
unitval internal_error : ('a, Format.formatter, unit, 'b) format4 -> 'a