Struct easy_smt::ContextBuilder

pub struct ContextBuilder { /* private fields */ }

Implementations

impl ContextBuilder

pub fn new() -> Self

Construct a new builder with the default configuration.

pub fn solver<P, A>(&mut self, program: P, args: A) -> &mut Selfwhere P: Into<OsString>, A: IntoIterator, A::Item: Into<OsString>,

Configure the solver that will be used.

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 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 Selfwhere W: 'static + Write,

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.