Source file options.ml

type _ key =
  | Log_level : int key
  | Produce_models : bool key
  | Produce_unsat_assumptions : bool key
  | Produce_unsat_cores : bool key
  | Seed : int key
  | Verbosity : int key
  | Time_limit_per : int key
  | Memory_limit : int key
  | Bv_solver : bv_solver key
  | Rewrite_level : int key
  | Sat_solver : sat_solver key
  | Prop_const_bits : bool key
  | Prop_ineq_bounds : bool key
  | Prop_nprops : int key
  | Prop_nupdates : int key
  | Prop_opt_lt_concat_sext : bool key
  | Prop_path_sel : prop_path_sel key
  | Prop_prob_pick_rand_input : int key
  | Prop_prob_pick_inv_value : int key
  | Prop_sext : bool key
  | Prop_normalize : bool key
  | Preprocess : bool key
  | Pp_contr_ands : bool key
  | Pp_elim_extracts : bool key
  | Pp_embedded : bool key
  | Pp_flatten_and : bool key
  | Pp_normalize : bool key
  | Pp_normalize_share_aware : bool key
  | Pp_skeleton_preproc : bool key
  | Pp_variable_subst : bool key
  | Pp_variable_subst_norm_eq : bool key
  | Pp_variable_subst_norm_diseq : bool key
  | Pp_variable_subst_norm_bv_ineq : bool key
  | Dbg_rw_node_thresh : int key
  | Dbg_pp_node_thresh : int key
  | Check_model : bool key
  | Check_unsat_core : bool key
and bv_solver =
  | Bitblast
  | Preprop
  | Prop
and sat_solver =
  | Cadical
  | Cms
  | Kissat
and prop_path_sel =
  | Essential
  | Random
let description : type a. a key -> string = function
  | Log_level -> "log level"
  | Produce_models -> "model production"
  | Produce_unsat_assumptions -> "unsat assumptions production"
  | Produce_unsat_cores -> "unsat core production"
  | Seed -> "seed for the random number generator"
  | Verbosity -> "verbosity level"
  | Time_limit_per -> "time limit in milliseconds per satisfiability check"
  | Memory_limit -> "set maximum memory limit in MB"
  | Bv_solver -> "bv solver engine"
  | Rewrite_level -> "rewrite level"
  | Sat_solver -> "backend SAT solver"
  | Prop_const_bits -> "use constant bits propagation"
  | Prop_ineq_bounds -> "infer inequality bounds for invertibility conditions and inverse value computation"
  | Prop_nprops -> "number of propagation steps used as a limit for propagation-based local search engine"
  | Prop_nupdates -> "number of model value updates used as a limit for propagation-based local search engine"
  | Prop_opt_lt_concat_sext -> "optimization for inverse value computation of inequalities over concat and sign extension operands"
  | Prop_path_sel -> "propagation path selection mode for propagation-based local search engine"
  | Prop_prob_pick_rand_input -> "probability for selecting a random input instead of an essential input (interpreted as <n>/1000)"
  | Prop_prob_pick_inv_value -> "probability for producing inverse rather than consistent values (interpreted as <n>/1000)"
  | Prop_sext -> "use sign_extend nodes for concats that represent sign_extend nodes for propagation-based local search engine"
  | Prop_normalize -> "enable normalization for local search"
  | Preprocess -> "enable preprocessing"
  | Pp_contr_ands -> "enable contradicting ands preprocessing pass"
  | Pp_elim_extracts -> "eliminate extract on BV constants"
  | Pp_embedded -> "enable embedded constraint preprocessing pass"
  | Pp_flatten_and -> "enable AND flattening preprocessing pass"
  | Pp_normalize -> "enable normalization pass"
  | Pp_normalize_share_aware -> "disable normalizations in normalization pass that may yield blow-up on the bit-level"
  | Pp_skeleton_preproc -> "enable skeleton preprocessing pass"
  | Pp_variable_subst -> "enable variable substitution preprocessing pass"
  | Pp_variable_subst_norm_eq -> "enable equality normalization via Gaussian elimination if variable substitution preprocessing pass is enabled"
  | Pp_variable_subst_norm_diseq -> "enable disequality normalization if variable substitution preprocessing pass is enabled"
  | Pp_variable_subst_norm_bv_ineq -> "enable bit-vector unsigned inequality normalization if variable substitution preprocessing pass is enabled"
  | Dbg_rw_node_thresh -> "warn threshold [#] for new nodes created through rewriting steps"
  | Dbg_pp_node_thresh -> "warn threshold [%] for new nodes created through preprocessing in total"
  | Check_model -> "check model for each satisfiable query"
  | Check_unsat_core -> "check unsat core model for each unsatisfiable query"
let to_string : type a. a key -> string = function
  | Log_level -> "log-level"
  | Produce_models -> "produce-models"
  | Produce_unsat_assumptions -> "produce-unsat-assumptions"
  | Produce_unsat_cores -> "produce-unsat-cores"
  | Seed -> "seed"
  | Verbosity -> "verbosity"
  | Time_limit_per -> "time-limit-per"
  | Memory_limit -> "memory-limit"
  | Bv_solver -> "bv-solver"
  | Rewrite_level -> "rewrite-level"
  | Sat_solver -> "sat-solver"
  | Prop_const_bits -> "prop-const-bits"
  | Prop_ineq_bounds -> "prop-ineq-bounds"
  | Prop_nprops -> "prop-nprops"
  | Prop_nupdates -> "prop-nupdates"
  | Prop_opt_lt_concat_sext -> "prop-opt-lt-concat-sext"
  | Prop_path_sel -> "prop-path-sel"
  | Prop_prob_pick_rand_input -> "prop-prob-pick-rand-input"
  | Prop_prob_pick_inv_value -> "prop-prob-pick-inv-value"
  | Prop_sext -> "prop-sext"
  | Prop_normalize -> "prop-normalize"
  | Preprocess -> "preprocess"
  | Pp_contr_ands -> "pp-contr-ands"
  | Pp_elim_extracts -> "pp-elim-extracts"
  | Pp_embedded -> "pp-embedded"
  | Pp_flatten_and -> "pp-flatten-and"
  | Pp_normalize -> "pp-normalize"
  | Pp_normalize_share_aware -> "pp-normalize-share-aware"
  | Pp_skeleton_preproc -> "pp-skeleton-preproc"
  | Pp_variable_subst -> "pp-variable-subst"
  | Pp_variable_subst_norm_eq -> "pp-variable-subst-norm-eq"
  | Pp_variable_subst_norm_diseq -> "pp-variable-subst-norm-diseq"
  | Pp_variable_subst_norm_bv_ineq -> "pp-variable-subst-norm-bv-ineq"
  | Dbg_rw_node_thresh -> "dbg-rw-node-thresh"
  | Dbg_pp_node_thresh -> "dbg-pp-node-thresh"
  | Check_model -> "check-model"
  | Check_unsat_core -> "check-unsat-core"
let to_cxx : type a. a key -> int = function
  | Log_level -> 0
  | Produce_models -> 1
  | Produce_unsat_assumptions -> 2
  | Produce_unsat_cores -> 3
  | Seed -> 4
  | Verbosity -> 5
  | Time_limit_per -> 6
  | Memory_limit -> 7
  | Bv_solver -> 8
  | Rewrite_level -> 9
  | Sat_solver -> 10
  | Prop_const_bits -> 11
  | Prop_ineq_bounds -> 12
  | Prop_nprops -> 13
  | Prop_nupdates -> 14
  | Prop_opt_lt_concat_sext -> 15
  | Prop_path_sel -> 16
  | Prop_prob_pick_rand_input -> 17
  | Prop_prob_pick_inv_value -> 18
  | Prop_sext -> 19
  | Prop_normalize -> 20
  | Preprocess -> 21
  | Pp_contr_ands -> 22
  | Pp_elim_extracts -> 23
  | Pp_embedded -> 24
  | Pp_flatten_and -> 25
  | Pp_normalize -> 26
  | Pp_normalize_share_aware -> 27
  | Pp_skeleton_preproc -> 28
  | Pp_variable_subst -> 29
  | Pp_variable_subst_norm_eq -> 30
  | Pp_variable_subst_norm_diseq -> 31
  | Pp_variable_subst_norm_bv_ineq -> 32
  | Dbg_rw_node_thresh -> 33
  | Dbg_pp_node_thresh -> 34
  | Check_model -> 35
  | Check_unsat_core -> 36
let bv_solver_to_string = function
  | Bitblast -> "bitblast"
  | Preprop -> "preprop"
  | Prop -> "prop"
let sat_solver_to_string = function
  | Cadical -> "cadical"
  | Cms -> "cms"
  | Kissat -> "kissat"
let prop_path_sel_to_string = function
  | Essential -> "essential"
  | Random -> "random"
let bv_solver_of_string = function
  | "bitblast" -> Bitblast
  | "preprop" -> Preprop
  | "prop" -> Prop
  | _ -> assert false
let sat_solver_of_string = function
  | "cadical" -> Cadical
  | "cms" -> Cms
  | "kissat" -> Kissat
  | _ -> assert false
let prop_path_sel_of_string = function
  | "essential" -> Essential
  | "random" -> Random
  | _ -> assert false
let default_value : type a. a key -> a = function
  | Log_level -> 0
  | Produce_models -> false
  | Produce_unsat_assumptions -> false
  | Produce_unsat_cores -> false
  | Seed -> 42
  | Verbosity -> 0
  | Time_limit_per -> 0
  | Memory_limit -> 0
  | Bv_solver -> Bitblast
  | Rewrite_level -> 2
  | Sat_solver -> Cadical
  | Prop_const_bits -> true
  | Prop_ineq_bounds -> true
  | Prop_nprops -> 0
  | Prop_nupdates -> 0
  | Prop_opt_lt_concat_sext -> true
  | Prop_path_sel -> Essential
  | Prop_prob_pick_rand_input -> 10
  | Prop_prob_pick_inv_value -> 990
  | Prop_sext -> true
  | Prop_normalize -> false
  | Preprocess -> true
  | Pp_contr_ands -> false
  | Pp_elim_extracts -> false
  | Pp_embedded -> true
  | Pp_flatten_and -> true
  | Pp_normalize -> true
  | Pp_normalize_share_aware -> true
  | Pp_skeleton_preproc -> true
  | Pp_variable_subst -> true
  | Pp_variable_subst_norm_eq -> true
  | Pp_variable_subst_norm_diseq -> false
  | Pp_variable_subst_norm_bv_ineq -> false
  | Dbg_rw_node_thresh -> 0
  | Dbg_pp_node_thresh -> 0
  | Check_model -> false
  | Check_unsat_core -> false
let min : int key -> int = function
  | Log_level -> 0
  | Seed -> 0
  | Verbosity -> 0
  | Time_limit_per -> 0
  | Memory_limit -> 0
  | Rewrite_level -> 0
  | Prop_nprops -> 0
  | Prop_nupdates -> 0
  | Prop_prob_pick_rand_input -> 0
  | Prop_prob_pick_inv_value -> 0
  | Dbg_rw_node_thresh -> 0
  | Dbg_pp_node_thresh -> 0
let max : int key -> int = function
  | Log_level -> 3
  | Seed -> 4294967295
  | Verbosity -> 4
  | Time_limit_per -> 4611686018427387903
  | Memory_limit -> 4611686018427387903
  | Rewrite_level -> 2
  | Prop_nprops -> 4611686018427387903
  | Prop_nupdates -> 4611686018427387903
  | Prop_prob_pick_rand_input -> 1000
  | Prop_prob_pick_inv_value -> 1000
  | Dbg_rw_node_thresh -> 4611686018427387903
  | Dbg_pp_node_thresh -> 100
type t
external default : unit -> t = "ocaml_bitwuzla_cxx_options_new"
external set_numeric : t -> (int [@untagged])-> (int [@untagged]) -> unit = "ocaml_bitwuzla_cxx_options_set_numeric" "native_bitwuzla_cxx_options_set_numeric"
external set_mode : t -> (int [@untagged]) -> string -> unit = "ocaml_bitwuzla_cxx_options_set_mode" "native_bitwuzla_cxx_options_set_mode"
let set : type a. t -> a key -> a -> unit = fun t k v ->
  match k with
  | Log_level -> set_numeric t (to_cxx k) v
  | Produce_models -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Produce_unsat_assumptions -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Produce_unsat_cores -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Seed -> set_numeric t (to_cxx k) v
  | Verbosity -> set_numeric t (to_cxx k) v
  | Time_limit_per -> set_numeric t (to_cxx k) v
  | Memory_limit -> set_numeric t (to_cxx k) v
  | Bv_solver -> set_mode t (to_cxx k) (bv_solver_to_string v)
  | Rewrite_level -> set_numeric t (to_cxx k) v
  | Sat_solver -> set_mode t (to_cxx k) (sat_solver_to_string v)
  | Prop_const_bits -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Prop_ineq_bounds -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Prop_nprops -> set_numeric t (to_cxx k) v
  | Prop_nupdates -> set_numeric t (to_cxx k) v
  | Prop_opt_lt_concat_sext -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Prop_path_sel -> set_mode t (to_cxx k) (prop_path_sel_to_string v)
  | Prop_prob_pick_rand_input -> set_numeric t (to_cxx k) v
  | Prop_prob_pick_inv_value -> set_numeric t (to_cxx k) v
  | Prop_sext -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Prop_normalize -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Preprocess -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Pp_contr_ands -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Pp_elim_extracts -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Pp_embedded -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Pp_flatten_and -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Pp_normalize -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Pp_normalize_share_aware -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Pp_skeleton_preproc -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Pp_variable_subst -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Pp_variable_subst_norm_eq -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Pp_variable_subst_norm_diseq -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Pp_variable_subst_norm_bv_ineq -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Dbg_rw_node_thresh -> set_numeric t (to_cxx k) v
  | Dbg_pp_node_thresh -> set_numeric t (to_cxx k) v
  | Check_model -> set_numeric t (to_cxx k) (Bool.to_int v)
  | Check_unsat_core -> set_numeric t (to_cxx k) (Bool.to_int v)
external get_numeric : t -> (int [@untagged])-> (int [@untagged]) = "ocaml_bitwuzla_cxx_options_get_numeric" "native_bitwuzla_cxx_options_get_numeric"
external get_mode : t -> (int [@untagged]) -> string = "ocaml_bitwuzla_cxx_options_get_mode" "native_bitwuzla_cxx_options_get_mode"
let get : type a. t -> a key -> a = fun t k ->
  match k with
  | Log_level -> get_numeric t (to_cxx k)
  | Produce_models -> get_numeric t (to_cxx k) <> 0
  | Produce_unsat_assumptions -> get_numeric t (to_cxx k) <> 0
  | Produce_unsat_cores -> get_numeric t (to_cxx k) <> 0
  | Seed -> get_numeric t (to_cxx k)
  | Verbosity -> get_numeric t (to_cxx k)
  | Time_limit_per -> get_numeric t (to_cxx k)
  | Memory_limit -> get_numeric t (to_cxx k)
  | Bv_solver -> bv_solver_of_string (get_mode t (to_cxx k))
  | Rewrite_level -> get_numeric t (to_cxx k)
  | Sat_solver -> sat_solver_of_string (get_mode t (to_cxx k))
  | Prop_const_bits -> get_numeric t (to_cxx k) <> 0
  | Prop_ineq_bounds -> get_numeric t (to_cxx k) <> 0
  | Prop_nprops -> get_numeric t (to_cxx k)
  | Prop_nupdates -> get_numeric t (to_cxx k)
  | Prop_opt_lt_concat_sext -> get_numeric t (to_cxx k) <> 0
  | Prop_path_sel -> prop_path_sel_of_string (get_mode t (to_cxx k))
  | Prop_prob_pick_rand_input -> get_numeric t (to_cxx k)
  | Prop_prob_pick_inv_value -> get_numeric t (to_cxx k)
  | Prop_sext -> get_numeric t (to_cxx k) <> 0
  | Prop_normalize -> get_numeric t (to_cxx k) <> 0
  | Preprocess -> get_numeric t (to_cxx k) <> 0
  | Pp_contr_ands -> get_numeric t (to_cxx k) <> 0
  | Pp_elim_extracts -> get_numeric t (to_cxx k) <> 0
  | Pp_embedded -> get_numeric t (to_cxx k) <> 0
  | Pp_flatten_and -> get_numeric t (to_cxx k) <> 0
  | Pp_normalize -> get_numeric t (to_cxx k) <> 0
  | Pp_normalize_share_aware -> get_numeric t (to_cxx k) <> 0
  | Pp_skeleton_preproc -> get_numeric t (to_cxx k) <> 0
  | Pp_variable_subst -> get_numeric t (to_cxx k) <> 0
  | Pp_variable_subst_norm_eq -> get_numeric t (to_cxx k) <> 0
  | Pp_variable_subst_norm_diseq -> get_numeric t (to_cxx k) <> 0
  | Pp_variable_subst_norm_bv_ineq -> get_numeric t (to_cxx k) <> 0
  | Dbg_rw_node_thresh -> get_numeric t (to_cxx k)
  | Dbg_pp_node_thresh -> get_numeric t (to_cxx k)
  | Check_model -> get_numeric t (to_cxx k) <> 0
  | Check_unsat_core -> get_numeric t (to_cxx k) <> 0