Skip to content

Commit

Permalink
Add a little detail to doc comment and bump to 0.2.3
Browse files Browse the repository at this point in the history
  • Loading branch information
fitzgen committed Oct 7, 2024
1 parent 1a4f99c commit 92f6261
Show file tree
Hide file tree
Showing 2 changed files with 27 additions and 9 deletions.
2 changes: 1 addition & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
[package]
name = "easy-smt"
version = "0.2.2"
version = "0.2.3"
authors = [
"Trevor Elliott <[email protected]>",
"Nick Fitzgerald <[email protected]>",
Expand Down
34 changes: 26 additions & 8 deletions src/context.rs
Original file line number Diff line number Diff line change
Expand Up @@ -533,10 +533,19 @@ impl Context {
}

/// Directly send an expression to the solver.
/// This is a low-level API and should be used sparingly, such as
/// for solver-specific commands that this crate does not provide
/// built-in support for. If possible, please use the higher-level
/// interfaces provided by this crate.
///
/// You are responsible for reading the response, if any, from the solver by
/// calling `context.raw_recv()` immediately after sending a message to the
/// solver. Failing to call `context.raw_recv()` afterwards if the solver
/// sends a response to your message, or calling it if the solver doesn't
/// send a response, will lead to general breakage such as dead locks,
/// nonsensical query results, and more.
///
/// This is a low-level API and should be used sparingly, such as for
/// solver-specific commands that this crate does not provide built-in
/// support for. When possible, use the higher-level interfaces provided by
/// this crate, for example by calling `context.assert(foo)` rather than
/// `context.raw_send(context.list([context.atom("assert"), foo]))`.
pub fn raw_send(&mut self, cmd: SExpr) -> io::Result<()> {
let solver = self
.solver
Expand All @@ -546,10 +555,19 @@ impl Context {
}

/// Directly receive a response from the solver.
/// This is a low-level API and should be used sparingly, such as
/// for solver-specific commands that this crate does not provide
/// built-in support for. If possible, please use the higher-level
/// interfaces provided by this crate.
///
/// This method should only be used immediately after calling
/// `context.raw_send(...)`, to receive the solver's response to that sent
/// message. Calling this method at other times, failing to call it when the
/// solver sends a response, or calling it when the solver does not send a
/// response, will lead to general breakage such as dead locks, nonsensical
/// query results, and more.
///
/// This is a low-level API and should be used sparingly, such as for
/// solver-specific commands that this crate does not provide built-in
/// support for. When possible, use the higher-level interfaces provided by
/// this crate, for example by calling `context.assert(foo)` rather than
/// `context.raw_send(context.list([context.atom("assert"), foo]))`.
pub fn raw_recv(&mut self) -> io::Result<SExpr> {
let solver = self
.solver
Expand Down

0 comments on commit 92f6261

Please sign in to comment.