Struct 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.

While it is not safe to access Z3 objects from multiple threads, this library includes a safe structured abstraction for usage of Z3 objects across threads. See Synchronized.

z3.rs uses an implicit thread-local context by default, which is used in all operations. Most users will not need to create their own contexts or interact with contexts directly.

To use a context with a customized configuration (e.g. setting timeouts), use with_z3_config.

Advanced users (e.g. those performing FFI with other Z3 bindings) can unsafely create their own contexts using Context::from_raw, and then use them with with_z3_context.

See also:

• Config
• with_z3_config
• with_z3_context
• Synchronized
• Translate

Implementations

impl Context

pub fn thread_local() -> Context

Returns a handle to the default thread-local Context.

This Context is used in all z3 operations. Custom Contexts are supported through with_z3_config, which allow for running a closure inside an environment with the provided Context

See also:

• with_z3_config

pub unsafe fn from_raw(z3_ctx: Z3_context) -> Context

Construct a Context from a raw Z3_context pointer. This is mostly useful for consumers who want to interoperate with Z3 contexts created through other means, such as the C API or other bindings such as Python.

Safety

The caller must ensure the pointer is valid and not already managed elsewhere.

Examples

use z3::ast::Bool;
use z3_sys::{Z3_mk_config, Z3_del_config, Z3_mk_context_rc};
use z3::Context;

// Create a raw Z3_config using the low-level API
let cfg = unsafe { Z3_mk_config() }.unwrap();
let raw_ctx = unsafe { Z3_mk_context_rc(cfg) }.unwrap();
let ctx = unsafe { Context::from_raw(raw_ctx) };
// Use `ctx` as usual...
unsafe { Z3_del_config(cfg) };
let b = Bool::from_bool(true);
assert_eq!(b.as_bool(), Some(true));

pub fn get_z3_context(&self) -> Z3_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 Clone for Context

fn clone(&self) -> Context

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Context

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

Formats the value using the given formatter.

impl PartialEq for Context

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

Tests for self and other values to be equal, and is used by ==.

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

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

impl Eq for Context

impl StructuralPartialEq for Context