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 pp_sat_solver : Stdlib.Format.formatter -> sat_solver -> unit
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;
}
Loops from 0 to max
and returns (f max elt ... (f 1 elt (f 0 elt init)))...)
. Returns init
if max
< 0