Struct z3::Config

pub struct Config { /* private fields */ }

Configuration used to initialize logical contexts.

See also:

• Context::new()

Implementations

impl Config

pub fn new() -> Config

Create a configuration object for the Z3 context object.

Configurations are created in order to assign parameters prior to creating contexts for Z3 interaction. For example, if the users wishes to use proof generation, then call:

use z3::Config;

let mut cfg = Config::new();
cfg.set_proof_generation(true);

See also

• Context::new()

pub fn set_param_value(&mut self, k: &str, v: &str)

Set a configuration parameter.

See also

• Config::set_bool_param_value()

pub fn set_bool_param_value(&mut self, k: &str, v: bool)

Set a configuration parameter.

This is a helper function.

See also

• Config::set_param_value()

pub fn set_proof_generation(&mut self, b: bool)

Enable or disable proof generation.

See also

• Solver::check()
• Solver::get_proof()

pub fn set_model_generation(&mut self, b: bool)

Enable or disable model generation.

See also

• Solver::check()
• Solver::get_model()

pub fn set_debug_ref_count(&mut self, b: bool)

pub fn set_timeout_msec(&mut self, ms: u64)

Trait Implementations

impl Debug for Config

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for Config

fn default() -> Self

Returns the “default value” for a type.

impl Drop for Config

fn drop(&mut self)

Executes the destructor for this type.