From f48f8fb28d2bc677ead5e4bf67d4d8de3f2b2046 Mon Sep 17 00:00:00 2001
From: Michael McLoughlin <mmcloughlin@gmail.com>
Date: Thu, 21 Nov 2024 14:26:52 -0500
Subject: [PATCH] Implement `(exit)` command (#32)

Implement the `(exit)` command.

This helps to support graceful solver exit, which is especially
important for clients which create many `easy-smt` contexts.

The `(exit)` command is specified in SMT-LIB 2.6 section 4.2.1
"(Re)starting and terminating".
---
 src/context.rs     | 13 +++++++++++++
 src/known_atoms.rs |  1 +
 2 files changed, 14 insertions(+)

diff --git a/src/context.rs b/src/context.rs
index 1ed0f1f..00890cc 100644
--- a/src/context.rs
+++ b/src/context.rs
@@ -483,6 +483,19 @@ impl Context {
         )
     }
 
+    /// Instruct the solver to exit.
+    pub fn exit(&mut self) -> io::Result<()> {
+        let solver = self
+            .solver
+            .as_mut()
+            .expect("exit requires a running solver");
+        solver.ack_command(
+            &self.arena,
+            self.atoms.success,
+            self.arena.list(vec![self.atoms.exit]),
+        )
+    }
+
     /// Push a new context frame in the solver. Same as SMTLIB's `push` command.
     pub fn push(&mut self) -> io::Result<()> {
         let solver = self
diff --git a/src/known_atoms.rs b/src/known_atoms.rs
index 45de1c6..771449e 100644
--- a/src/known_atoms.rs
+++ b/src/known_atoms.rs
@@ -21,6 +21,7 @@ macro_rules! for_each_known_atom {
             get_unsat_core: "get-unsat-core";
             set_logic: "set-logic";
             set_option: "set-option";
+            exit: "exit";
             push: "push";
             pop: "pop";
             bool: "Bool";