pub struct ContextBuilder { /* private fields */ }
Implementations§
Source§impl ContextBuilder
impl ContextBuilder
Sourcepub fn solver<P>(&mut self, program: P) -> &mut Self
pub fn solver<P>(&mut self, program: P) -> &mut Self
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.
Sourcepub fn solver_args<A>(&mut self, args: A) -> &mut Self
pub fn solver_args<A>(&mut self, args: A) -> &mut Self
Configure the arguments that will be passed to the solver.
By default, no arguments are passed to the solver.
Sourcepub fn without_solver(&mut self) -> &mut Self
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.
Sourcepub fn replay_file<W>(&mut self, replay_file: Option<W>) -> &mut Self
pub fn replay_file<W>(&mut self, replay_file: Option<W>) -> &mut Self
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.