Struct z3::Context

pub struct Context { /* private fields */ }

Manager of all other Z3 objects, global configuration options, etc.

An application may use multiple Z3 contexts. Objects created in one context cannot be used in another one. However, several objects may be “translated” from one context to another. It is not safe to access Z3 objects from multiple threads.

Examples:

Creating a context with the default configuration:

use z3::{Config, Context};
let cfg = Config::new();
let ctx = Context::new(&cfg);

See also:

• Config
• Context::new()

Implementations

impl Context

pub fn new(cfg: &Config) -> Context

pub fn interrupt(&self)

Interrupt a solver performing a satisfiability test, a tactic processing a goal, or simplify functions.

pub fn handle(&self) -> ContextHandle<'_>

Obtain a handle that can be used to interrupt computation from another thread.

See also:

• ContextHandle
• ContextHandle::interrupt()

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

Update a global parameter.

See also

• Context::update_bool_param_value()

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

Update a global parameter.

This is a helper function.

See also

• Context::update_param_value()

Trait Implementations

impl Debug for Context

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

Formats the value using the given formatter.

impl Drop for Context

fn drop(&mut self)

Executes the destructor for this type.

impl PartialEq<Context> for Context

fn eq(&self, other: &Context) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

This method tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for Context

impl StructuralEq for Context

impl StructuralPartialEq for Context