Struct ContextBuilder

pub struct ContextBuilder { /* private fields */ }

Implementations

impl ContextBuilder

pub fn new() -> Self

Construct a new builder with the default configuration.

pub fn with_z3_defaults(&mut self) -> &mut Self

Initialize the builder with Z3 defaults.

pub fn with_cvc5_defaults(&mut self) -> &mut Self

Initialize the builder with CVC5 defaults.

pub fn solver<P>(&mut self, program: P) -> &mut Self

where P: Into<OsString>,

Configure the solver that will be used.

You can pass arguments to the underlying solver via the solver_args method.

By default, no solver is configured, and any Context created will only be able to build and display expressions, not assert them or query for their satisfiability.

pub fn solver_args<A>(&mut self, args: A) -> &mut Self

where A: IntoIterator, A::Item: Into<OsString>,

Configure the arguments that will be passed to the solver.

By default, no arguments are passed to the solver.

pub fn without_solver(&mut self) -> &mut Self

Clear the solver configuration, if any.

This returns to the default, no-solver configuration, where any Context created will only be able to build and display expressions, not assert them or query for their satisfiability.

pub fn replay_file<W>(&mut self, replay_file: Option<W>) -> &mut Self

where W: 'static + Write + Send,

An optional file (or anything else that is std::io::Write-able) where all solver queries and commands are tee’d too.

This let’s you replay interactions with the solver offline, without needing to dynamically rebuild your expressions, queries, or commands.

This is unused if no solver is configured.

By default, there is no replay file configured.

pub fn build(&mut self) -> Result<Context>

Finish configuring the context and build it.

Trait Implementations

impl Default for ContextBuilder

fn default() -> ContextBuilder

Returns the “default value” for a type.