Module Pconfig.State

type mode =
| Logic
| Program
type t = private {
timeout : int;
mode : mode;
redef : bool;
last_timer : float;
load_path : string list;
unroll_depth : int;
unroll_pick_given : int;
random_testing : bool;
sat_seed : int;
sat_random_freq : float;
smt_seed : int;
solver_seed : int;
gc_on_verify : bool;
undo_mode : bool;
console_tags : Console_tag.tag list;

which console tags to print on stdout

console_color : bool;

print tags on stdout

push_top_results : bool;

produce + store Top_result.t objects

lnoise_hints : bool;

enable hints in Linenoise

lockdown : int option;

lockdown with given user

coredump_dir : string option;

coredump dir to write to on error?

validate : bool;

validate definitions

skip_proofs : bool;

skip proofs

dparsetree : bool;

print parsetree

print_banner : bool;

print banner at boot

open_dot : bool;

automatically open graphviz graphs

max_induct : int option;

max induction depth

induct_unroll : int;

how much unrolling to do in the waterfall?

backchain_limit : int;

global back-chaining limit, for rewriting

max_splitter : int option;

max ite-based subgoal splitting in the waterfall

check_models : bool;

check counter models?

enable_all : bool;

should all definitions be enabled (ignoring their f_enabled flags)?

spec_max_depth : int;

maximum depth for specialization

unroll_factor : bool;

factor subcalls in unroll?

unroll_enable_all : bool;

enable all functions for unrolling queries

prelude_loaded : bool;

has the prelude already been loaded?

algnum_print_precision : int;

decimal precision for printing algebraic number approximations

reflect_approx_models : bool;

should approximate models be reflected into CX modules?

chash : Chash.t lazy_t;

hash of some of the parameters

use_ciml : bool;

use ciml certificates

callgraph_size : int;

max size for callgraphs

callgraph_include_expansions : bool;

whether callgraph includes expansion steps

store_proofs : bool;

whether to store proofs in history

}
val copy : unit -> t
val with_ : ?⁠upd:(unit -> unit) -> ('a -> 'b) -> 'a -> 'b
val with1 : ?⁠upd:(unit -> unit) -> (unit -> 'a) -> 'a
val chash : t -> Chash.t
val state : t Stdlib.ref
module Set : sig ... end
val config_rubric : unit -> (string * string * string list) list
val print_config : string option -> unit