boogie_options.rs

pub struct BoogieOptions {
    /// Path to the boogie executable.
    pub boogie_exe: String,
    /// Use experimental boogie exe found via env var EXP_BOOGIE_EXE.
    pub use_exp_boogie: bool,
    /// Path to the z3 executable.
    pub z3_exe: String,
    /// Whether to use cvc5.
    pub use_cvc5: bool,
    /// Path to the cvc5 executable.
    pub cvc5_exe: String,
    /// Whether to generate debug trace code.
    pub debug_trace: bool,
    /// List of flags to pass on to boogie.
    pub boogie_flags: Vec<String>,
    /// Whether to use native array theory.
    pub use_array_theory: bool,
    /// Whether to produce an SMT file for each verification problem.
    pub generate_smt: bool,
    /// Whether native instead of stratified equality should be used.
    pub native_equality: bool,
    /// A string determining the type of requires used for parameter type checks. Can be
    /// `"requires"` or `"free requires`".
    pub type_requires: String,
    /// The depth until which stratified functions are expanded.
    pub stratification_depth: usize,
    /// A string to be used to inline a function of medium size. Can be empty or `{:inline}`.
    pub aggressive_func_inline: String,
    /// A string to be used to inline a function of small size. Can be empty or `{:inline}`.
    pub func_inline: String,
    /// A bound to apply to the length of serialization results.
    pub serialize_bound: usize,
    /// How many times to call the prover backend for the verification problem. This is used for
    /// benchmarking.
    pub bench_repeat: usize,
    /// Whether to use the sequence theory as the internal representation for $Vector type.
    pub vector_using_sequences: bool,
    /// A seed for the prover.
    pub random_seed: usize,
    /// The number of cores to use for parallel processing of verification conditions.
    pub proc_cores: usize,
    /// A (soft) timeout for the solver, per verification condition, in seconds.
    pub vc_timeout: usize,
    /// Whether Boogie output and log should be saved.
    pub keep_artifacts: bool,
    /// Eager threshold for quantifier instantiation.
    pub eager_threshold: usize,
    /// Lazy threshold for quantifier instantiation.
    pub lazy_threshold: usize,
    /// Whether to use the new Boogie `{:debug ..}` attribute for tracking debug values.
    pub stable_test_output: bool,
    /// Number of Boogie instances to be run concurrently.
    pub num_instances: usize,
    /// Whether to run Boogie instances sequentially.
    pub sequential_task: bool,
    /// A hard timeout for boogie execution; if the process does not terminate within
    /// this time frame, it will be killed. Zero for no timeout.
    pub hard_timeout_secs: u64,
    /// What vector theory to use.
    pub vector_theory: VectorTheory,
    /// Whether to generate a z3 trace file and where to put it.
    pub z3_trace_file: Option<String>,
    /// Options to define user-custom native funs.
    pub custom_natives: Option<CustomNativeOptions>,
    /// Number of iterations to unroll loops.
    pub loop_unroll: Option<u64>,
    /// Optional aggregate function names for native methods implementing mutable borrow semantics
    pub borrow_aggregates: Vec<BorrowAggregate>,
}

// Default values for boogie options:
impl Default for BoogieOptions {
    fn default() -> Self {
        Self {
            bench_repeat: 1,
            boogie_exe: read_env_var("BOOGIE_EXE"),
            use_exp_boogie: false,
            z3_exe: read_env_var("Z3_EXE"),
            use_cvc5: false,
            cvc5_exe: read_env_var("CVC5_EXE"),
            boogie_flags: vec![],
            debug_trace: false,
            use_array_theory: false,
            generate_smt: false,
            native_equality: false,
            type_requires: "free requires".to_owned(),
            stratification_depth: 6,
            aggressive_func_inline: "".to_owned(),
            func_inline: "{:inline}".to_owned(),
            serialize_bound: 0,
            vector_using_sequences: false,
            random_seed: 1,
            proc_cores: 4,
            vc_timeout: 40,
            keep_artifacts: false,
            eager_threshold: 100,
            lazy_threshold: 100,
            stable_test_output: false,
            num_instances: 1,
            sequential_task: false,
            hard_timeout_secs: 0,
            vector_theory: VectorTheory::BoogieArray,
            z3_trace_file: None,
            custom_natives: None,
            loop_unroll: None,
            borrow_aggregates: vec![],
        }
    }
}