From 92f62610144fe7b49ed3ce2c2598fdce05c7a6b7 Mon Sep 17 00:00:00 2001 From: Nick Fitzgerald Date: Mon, 7 Oct 2024 15:19:59 -0700 Subject: [PATCH] Add a little detail to doc comment and bump to 0.2.3 --- Cargo.toml | 2 +- src/context.rs | 34 ++++++++++++++++++++++++++-------- 2 files changed, 27 insertions(+), 9 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index f6c1073..a7fc665 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "easy-smt" -version = "0.2.2" +version = "0.2.3" authors = [ "Trevor Elliott ", "Nick Fitzgerald ", diff --git a/src/context.rs b/src/context.rs index 41b53a1..1ed0f1f 100644 --- a/src/context.rs +++ b/src/context.rs @@ -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 @@ -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 { let solver = self .solver