From e928466be829eb7410cf07525a058df29a55a31a Mon Sep 17 00:00:00 2001
From: Tim Beurskens <tim.beurskens@simpl.energy>
Date: Thu, 19 Dec 2024 13:28:18 +0100
Subject: [PATCH 1/8] prevent suffix for `Real`

---
 smtlib/src/sorts.rs | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/smtlib/src/sorts.rs b/smtlib/src/sorts.rs
index 1d16b46..a17939b 100644
--- a/smtlib/src/sorts.rs
+++ b/smtlib/src/sorts.rs
@@ -55,7 +55,7 @@ impl Index {
 
 pub(crate) fn is_built_in_sort(name: &str) -> bool {
     match name {
-        "Int" | "Bool" => true,
+        "Int" | "Bool" | "Real" => true,
         _ => false,
     }
 }
@@ -63,10 +63,6 @@ pub(crate) fn is_built_in_sort(name: &str) -> bool {
 impl Sort {
     pub fn new(name: impl Into<String>) -> Self {
         let mut name = name.into();
-        if !is_built_in_sort(&name) {
-            // HACK: how should we handle this? or should we event handle it?
-            name += "_xxx";
-        }
         Self {
             name,
             index: Vec::new(),

From 60ca43afbc47c31e462a755593c0a8ed62a0ab1c Mon Sep 17 00:00:00 2001
From: Tim Beurskens <tim.beurskens@simpl.energy>
Date: Thu, 19 Dec 2024 13:37:36 +0100
Subject: [PATCH 2/8] add commands from maximal satisfaction paper

---
 lowlevel/src/ast.rs | 48 +++++++++++++++++++++++++++++++++++++++++++++
 xtask/src/spec.toml | 13 ++++++++++++
 2 files changed, 61 insertions(+)

diff --git a/lowlevel/src/ast.rs b/lowlevel/src/ast.rs
index 86b353c..4fdfa83 100644
--- a/lowlevel/src/ast.rs
+++ b/lowlevel/src/ast.rs
@@ -1406,6 +1406,12 @@ pub enum Command {
     SetOption(Option),
     /// `(simplify <term>)`
     Simplify(Term),
+    /// `(maximize <term>)`
+    Maximize(Term),
+    /// `(minimize <term>)`
+    Minimize(Term),
+    /// `(assert-soft <term>)`
+    AssertSoft(Term),
 }
 impl std::fmt::Display for Command {
     fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
@@ -1459,6 +1465,9 @@ impl std::fmt::Display for Command {
             Self::SetLogic(m0) => write!(f, "(set-logic {})", m0),
             Self::SetOption(m0) => write!(f, "(set-option {})", m0),
             Self::Simplify(m0) => write!(f, "(simplify {})", m0),
+            Self::Maximize(m0) => write!(f, "(maximize {})", m0),
+            Self::Minimize(m0) => write!(f, "(minimize {})", m0),
+            Self::AssertSoft(m0) => write!(f, "(assert-soft {})", m0),
         }
     }
 }
@@ -1485,6 +1494,12 @@ impl SmtlibParse for Command {
             || (p.nth(offset) == Token::LParen
                 && p.nth_matches(offset + 1, Token::Reserved, "check-sat-assuming")
                 && p.nth(offset + 2) == Token::LParen)
+            || (p.nth(offset) == Token::LParen
+                && p.nth_matches(offset + 1, Token::Symbol, "assert-soft"))
+            || (p.nth(offset) == Token::LParen
+                && p.nth_matches(offset + 1, Token::Symbol, "minimize"))
+            || (p.nth(offset) == Token::LParen
+                && p.nth_matches(offset + 1, Token::Symbol, "maximize"))
             || (p.nth(offset) == Token::LParen
                 && p.nth_matches(offset + 1, Token::Symbol, "simplify"))
             || (p.nth(offset) == Token::LParen
@@ -1633,6 +1648,33 @@ impl SmtlibParse for Command {
             #[allow(clippy::useless_conversion)]
             return Ok(Self::CheckSatAssuming(m0.into()));
         }
+        if p.nth(offset) == Token::LParen
+            && p.nth_matches(offset + 1, Token::Symbol, "assert-soft")
+        {
+            p.expect(Token::LParen)?;
+            p.expect_matches(Token::Symbol, "assert-soft")?;
+            let m0 = <Term as SmtlibParse>::parse(p)?;
+            p.expect(Token::RParen)?;
+            #[allow(clippy::useless_conversion)] return Ok(Self::AssertSoft(m0.into()));
+        }
+        if p.nth(offset) == Token::LParen
+            && p.nth_matches(offset + 1, Token::Symbol, "minimize")
+        {
+            p.expect(Token::LParen)?;
+            p.expect_matches(Token::Symbol, "minimize")?;
+            let m0 = <Term as SmtlibParse>::parse(p)?;
+            p.expect(Token::RParen)?;
+            #[allow(clippy::useless_conversion)] return Ok(Self::Minimize(m0.into()));
+        }
+        if p.nth(offset) == Token::LParen
+            && p.nth_matches(offset + 1, Token::Symbol, "maximize")
+        {
+            p.expect(Token::LParen)?;
+            p.expect_matches(Token::Symbol, "maximize")?;
+            let m0 = <Term as SmtlibParse>::parse(p)?;
+            p.expect(Token::RParen)?;
+            #[allow(clippy::useless_conversion)] return Ok(Self::Maximize(m0.into()));
+        }
         if p.nth(offset) == Token::LParen
             && p.nth_matches(offset + 1, Token::Symbol, "simplify")
         {
@@ -1902,6 +1944,9 @@ impl Command {
             Self::SetLogic(_) => false,
             Self::SetOption(_) => false,
             Self::Simplify(_) => true,
+            Self::Maximize(_) => false,
+            Self::Minimize(_) => false,
+            Self::AssertSoft(_) => false,
         }
     }
     pub fn parse_response(
@@ -2044,6 +2089,9 @@ impl Command {
                     ),
                 )
             }
+            Self::Maximize(_) => Ok(None),
+            Self::Minimize(_) => Ok(None),
+            Self::AssertSoft(_) => Ok(None),
         }
     }
 }
diff --git a/xtask/src/spec.toml b/xtask/src/spec.toml
index 5774fde..a6d1a9a 100644
--- a/xtask/src/spec.toml
+++ b/xtask/src/spec.toml
@@ -263,6 +263,19 @@ syntax = "( set-option <option> )"
 syntax = "( simplify <term> )"
 response = "<simplify_response>"
 
+# Z3 Max-SMT extensions
+
+# https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-scss2014.pdf
+
+[command.maximize]
+syntax = "( maximize <term> )"
+
+[command.minimize]
+syntax = "( minimize <term> )"
+
+[command.assert-soft]
+syntax = "( assert-soft <term> )"
+
 [script]
 syntax = "<command>*"
 separator = "\n"

From 99c45c68f0d2b12d978553ad79a522a816bc34f8 Mon Sep 17 00:00:00 2001
From: Tim Beurskens <tim.beurskens@simpl.energy>
Date: Thu, 19 Dec 2024 13:44:06 +0100
Subject: [PATCH 3/8] add `maximize` and `minimize` to solver

---
 smtlib/src/solver.rs | 33 ++++++++++++++++++++++++++++++++-
 1 file changed, 32 insertions(+), 1 deletion(-)

diff --git a/smtlib/src/solver.rs b/smtlib/src/solver.rs
index 10a2510..9b19d21 100644
--- a/smtlib/src/solver.rs
+++ b/smtlib/src/solver.rs
@@ -9,7 +9,7 @@ use smtlib_lowlevel::{
 use crate::{
     funs, sorts,
     terms::{qual_ident, Dynamic},
-    Bool, Error, Logic, Model, SatResult, SatResultWithModel,
+    Bool, Error, Logic, Model, SatResult, SatResultWithModel, Sorted,
 };
 
 /// The [`Solver`] type is the primary entrypoint to interaction with the
@@ -114,6 +114,37 @@ where
             _ => todo!(),
         }
     }
+
+    /// Adds the optimization goal of `g` as a goal to the solver.
+    pub fn maximize<S>(&mut self, g: S) -> Result<(), Error> where S: Sorted {
+        let term = g.into();
+
+        self.declare_all_consts(&term)?;
+
+        let cmd = ast::Command::Maximize(term);
+
+        match self.driver.exec(&cmd)? {
+            ast::GeneralResponse::Success => Ok(()),
+            ast::GeneralResponse::Error(e) => Err(Error::Smt(e, cmd.to_string())),
+            _ => unimplemented!(),
+        }
+    }
+
+    /// Adds the optimization goal of `g` as a goal to the solver.
+    pub fn minimize<S>(&mut self, g: S) -> Result<(), Error> where S: Sorted {
+        let term = g.into();
+
+        self.declare_all_consts(&term)?;
+
+        let cmd = ast::Command::Minimize(term);
+
+        match self.driver.exec(&cmd)? {
+            ast::GeneralResponse::Success => Ok(()),
+            ast::GeneralResponse::Error(e) => Err(Error::Smt(e, cmd.to_string())),
+            _ => unimplemented!(),
+        }
+    }
+
     /// Checks for satisfiability of the assertions sent to the solver using
     /// [`Solver::assert`].
     ///

From 4ae57d0c566353e23e7af9b97b3427f840b03ffa Mon Sep 17 00:00:00 2001
From: Tim Beurskens <tim.beurskens@simpl.energy>
Date: Thu, 19 Dec 2024 13:45:03 +0100
Subject: [PATCH 4/8] add `assert_soft` to solver

---
 smtlib/src/solver.rs | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/smtlib/src/solver.rs b/smtlib/src/solver.rs
index 9b19d21..b7f45b5 100644
--- a/smtlib/src/solver.rs
+++ b/smtlib/src/solver.rs
@@ -130,6 +130,21 @@ where
         }
     }
 
+    /// Adds soft-constraint `b` to the solver.
+    pub fn assert_soft<S>(&mut self, b: Bool) -> Result<(), Error> where S: Sorted {
+        let term = b.into();
+
+        self.declare_all_consts(&term)?;
+
+        let cmd = ast::Command::AssertSoft(term);
+
+        match self.driver.exec(&cmd)? {
+            ast::GeneralResponse::Success => Ok(()),
+            ast::GeneralResponse::Error(e) => Err(Error::Smt(e, cmd.to_string())),
+            _ => unimplemented!(),
+        }
+    }
+
     /// Adds the optimization goal of `g` as a goal to the solver.
     pub fn minimize<S>(&mut self, g: S) -> Result<(), Error> where S: Sorted {
         let term = g.into();

From 7c842e9e7b2bd4ed14d99fbf7b1d339f84d6f1c7 Mon Sep 17 00:00:00 2001
From: Tim Beurskens <tim.beurskens@simpl.energy>
Date: Thu, 19 Dec 2024 13:48:30 +0100
Subject: [PATCH 5/8] fix function signature for assert-soft

---
 smtlib/src/solver.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/smtlib/src/solver.rs b/smtlib/src/solver.rs
index b7f45b5..a483873 100644
--- a/smtlib/src/solver.rs
+++ b/smtlib/src/solver.rs
@@ -131,7 +131,7 @@ where
     }
 
     /// Adds soft-constraint `b` to the solver.
-    pub fn assert_soft<S>(&mut self, b: Bool) -> Result<(), Error> where S: Sorted {
+    pub fn assert_soft(&mut self, b: Bool) -> Result<(), Error> {
         let term = b.into();
 
         self.declare_all_consts(&term)?;

From 6d24e853a14e10c48759ecf50de7202302788ced Mon Sep 17 00:00:00 2001
From: Tim Beurskens <tim.beurskens@simpl.energy>
Date: Thu, 19 Dec 2024 15:17:51 +0100
Subject: [PATCH 6/8] use `Real` division for `impl Div`

---
 smtlib/src/theories/reals.rs | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/smtlib/src/theories/reals.rs b/smtlib/src/theories/reals.rs
index 6bd77db..4a5a966 100644
--- a/smtlib/src/theories/reals.rs
+++ b/smtlib/src/theories/reals.rs
@@ -89,6 +89,11 @@ impl Real {
     pub fn abs(self) -> Real {
         fun("abs", vec![self.into()]).into()
     }
+
+    /// Construct the term expressing floor division of two terms
+    pub fn floor_div<R>(self, rhs: R) -> Self where R: Into<Real> {
+        self.binop("div", rhs.into())
+    }
 }
 
 impl std::ops::Neg for Real {
@@ -101,4 +106,4 @@ impl std::ops::Neg for Real {
 impl_op!(Real, f64, Add, add, "+", AddAssign, add_assign, +);
 impl_op!(Real, f64, Sub, sub, "-", SubAssign, sub_assign, -);
 impl_op!(Real, f64, Mul, mul, "*", MulAssign, mul_assign, *);
-impl_op!(Real, f64, Div, div, "div", DivAssign, div_assign, /);
+impl_op!(Real, f64, Div, div, "/", DivAssign, div_assign, /);

From 16f524c397426ae1fd7ffd40e4b0b4aeb4eac4d0 Mon Sep 17 00:00:00 2001
From: Tim Beurskens <tim.beurskens@simpl.energy>
Date: Thu, 19 Dec 2024 15:51:25 +0100
Subject: [PATCH 7/8] allow custimization of optimization priorities

---
 lowlevel/src/ast.rs  | 123 ++++++++++++++++++++++++++++++++++++++++---
 smtlib/src/solver.rs |  16 +++++-
 xtask/src/spec.toml  |  21 +++++++-
 3 files changed, 150 insertions(+), 10 deletions(-)

diff --git a/lowlevel/src/ast.rs b/lowlevel/src/ast.rs
index 4fdfa83..167c50f 100644
--- a/lowlevel/src/ast.rs
+++ b/lowlevel/src/ast.rs
@@ -1410,8 +1410,8 @@ pub enum Command {
     Maximize(Term),
     /// `(minimize <term>)`
     Minimize(Term),
-    /// `(assert-soft <term>)`
-    AssertSoft(Term),
+    /// `(assert-soft <term> <optimization_attribute>*)`
+    AssertSoft(Term, Vec<OptimizationAttribute>),
 }
 impl std::fmt::Display for Command {
     fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
@@ -1467,7 +1467,9 @@ impl std::fmt::Display for Command {
             Self::Simplify(m0) => write!(f, "(simplify {})", m0),
             Self::Maximize(m0) => write!(f, "(maximize {})", m0),
             Self::Minimize(m0) => write!(f, "(minimize {})", m0),
-            Self::AssertSoft(m0) => write!(f, "(assert-soft {})", m0),
+            Self::AssertSoft(m0, m1) => {
+                write!(f, "(assert-soft {} {})", m0, m1.iter().format(" "))
+            }
         }
     }
 }
@@ -1654,8 +1656,10 @@ impl SmtlibParse for Command {
             p.expect(Token::LParen)?;
             p.expect_matches(Token::Symbol, "assert-soft")?;
             let m0 = <Term as SmtlibParse>::parse(p)?;
+            let m1 = p.any::<OptimizationAttribute>()?;
             p.expect(Token::RParen)?;
-            #[allow(clippy::useless_conversion)] return Ok(Self::AssertSoft(m0.into()));
+            #[allow(clippy::useless_conversion)]
+            return Ok(Self::AssertSoft(m0.into(), m1.into()));
         }
         if p.nth(offset) == Token::LParen
             && p.nth_matches(offset + 1, Token::Symbol, "minimize")
@@ -1946,7 +1950,7 @@ impl Command {
             Self::Simplify(_) => true,
             Self::Maximize(_) => false,
             Self::Minimize(_) => false,
-            Self::AssertSoft(_) => false,
+            Self::AssertSoft(_, _) => false,
         }
     }
     pub fn parse_response(
@@ -2091,10 +2095,59 @@ impl Command {
             }
             Self::Maximize(_) => Ok(None),
             Self::Minimize(_) => Ok(None),
-            Self::AssertSoft(_) => Ok(None),
+            Self::AssertSoft(_, _) => Ok(None),
+        }
+    }
+}
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
+pub enum OptimizationAttribute {
+    /// `:weight <numeral>`
+    Weight(Numeral),
+    /// `:id <symbol>`
+    Id(Symbol),
+    /// `<attribute>`
+    Attribute(Attribute),
+}
+impl std::fmt::Display for OptimizationAttribute {
+    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
+        match self {
+            Self::Weight(m0) => write!(f, ":weight {}", m0),
+            Self::Id(m0) => write!(f, ":id {}", m0),
+            Self::Attribute(m0) => write!(f, "{}", m0),
         }
     }
 }
+impl OptimizationAttribute {
+    pub fn parse(src: &str) -> Result<Self, ParseError> {
+        SmtlibParse::parse(&mut Parser::new(src))
+    }
+}
+impl SmtlibParse for OptimizationAttribute {
+    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
+        (p.nth_matches(offset, Token::Keyword, ":id"))
+            || (p.nth_matches(offset, Token::Keyword, ":weight"))
+            || (Attribute::is_start_of(offset, p))
+    }
+    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
+        let offset = 0;
+        if p.nth_matches(offset, Token::Keyword, ":id") {
+            p.expect_matches(Token::Keyword, ":id")?;
+            let m0 = <Symbol as SmtlibParse>::parse(p)?;
+            #[allow(clippy::useless_conversion)] return Ok(Self::Id(m0.into()));
+        }
+        if p.nth_matches(offset, Token::Keyword, ":weight") {
+            p.expect_matches(Token::Keyword, ":weight")?;
+            let m0 = <Numeral as SmtlibParse>::parse(p)?;
+            #[allow(clippy::useless_conversion)] return Ok(Self::Weight(m0.into()));
+        }
+        if Attribute::is_start_of(offset, p) {
+            let m0 = <Attribute as SmtlibParse>::parse(p)?;
+            #[allow(clippy::useless_conversion)] return Ok(Self::Attribute(m0.into()));
+        }
+        Err(p.stuck("optimization_attribute"))
+    }
+}
 /// `<command>*`
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
 #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
@@ -2149,6 +2202,8 @@ pub enum Option {
     ReproducibleResourceLimit(Numeral),
     /// `:verbosity <numeral>`
     Verbosity(Numeral),
+    /// `:opt.priority <optimization_priority>`
+    OptPriority(OptimizationPriority),
     /// `<attribute>`
     Attribute(Attribute),
 }
@@ -2175,6 +2230,7 @@ impl std::fmt::Display for Option {
                 write!(f, ":reproducible-resource-limit {}", m0)
             }
             Self::Verbosity(m0) => write!(f, ":verbosity {}", m0),
+            Self::OptPriority(m0) => write!(f, ":opt.priority {}", m0),
             Self::Attribute(m0) => write!(f, "{}", m0),
         }
     }
@@ -2186,7 +2242,8 @@ impl Option {
 }
 impl SmtlibParse for Option {
     fn is_start_of(offset: usize, p: &mut Parser) -> bool {
-        (p.nth_matches(offset, Token::Keyword, ":verbosity"))
+        (p.nth_matches(offset, Token::Keyword, ":opt.priority"))
+            || (p.nth_matches(offset, Token::Keyword, ":verbosity"))
             || (p.nth_matches(offset, Token::Keyword, ":reproducible-resource-limit"))
             || (p.nth_matches(offset, Token::Keyword, ":regular-output-channel"))
             || (p.nth_matches(offset, Token::Keyword, ":random-seed"))
@@ -2204,6 +2261,11 @@ impl SmtlibParse for Option {
     }
     fn parse(p: &mut Parser) -> Result<Self, ParseError> {
         let offset = 0;
+        if p.nth_matches(offset, Token::Keyword, ":opt.priority") {
+            p.expect_matches(Token::Keyword, ":opt.priority")?;
+            let m0 = <OptimizationPriority as SmtlibParse>::parse(p)?;
+            #[allow(clippy::useless_conversion)] return Ok(Self::OptPriority(m0.into()));
+        }
         if p.nth_matches(offset, Token::Keyword, ":verbosity") {
             p.expect_matches(Token::Keyword, ":verbosity")?;
             let m0 = <Numeral as SmtlibParse>::parse(p)?;
@@ -2295,6 +2357,53 @@ impl SmtlibParse for Option {
 }
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
 #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
+pub enum OptimizationPriority {
+    /// `pareto`
+    Pareto,
+    /// `lex`
+    Lex,
+    /// `box`
+    Box,
+}
+impl std::fmt::Display for OptimizationPriority {
+    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
+        match self {
+            Self::Pareto => write!(f, "pareto"),
+            Self::Lex => write!(f, "lex"),
+            Self::Box => write!(f, "box"),
+        }
+    }
+}
+impl OptimizationPriority {
+    pub fn parse(src: &str) -> Result<Self, ParseError> {
+        SmtlibParse::parse(&mut Parser::new(src))
+    }
+}
+impl SmtlibParse for OptimizationPriority {
+    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
+        (p.nth_matches(offset, Token::Symbol, "box"))
+            || (p.nth_matches(offset, Token::Symbol, "lex"))
+            || (p.nth_matches(offset, Token::Symbol, "pareto"))
+    }
+    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
+        let offset = 0;
+        if p.nth_matches(offset, Token::Symbol, "box") {
+            p.expect_matches(Token::Symbol, "box")?;
+            #[allow(clippy::useless_conversion)] return Ok(Self::Box);
+        }
+        if p.nth_matches(offset, Token::Symbol, "lex") {
+            p.expect_matches(Token::Symbol, "lex")?;
+            #[allow(clippy::useless_conversion)] return Ok(Self::Lex);
+        }
+        if p.nth_matches(offset, Token::Symbol, "pareto") {
+            p.expect_matches(Token::Symbol, "pareto")?;
+            #[allow(clippy::useless_conversion)] return Ok(Self::Pareto);
+        }
+        Err(p.stuck("optimization_priority"))
+    }
+}
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub enum InfoFlag {
     /// `:all-statistics`
     AllStatistics,
diff --git a/smtlib/src/solver.rs b/smtlib/src/solver.rs
index a483873..9ac88cb 100644
--- a/smtlib/src/solver.rs
+++ b/smtlib/src/solver.rs
@@ -1,6 +1,6 @@
 use indexmap::{map::Entry, IndexMap, IndexSet};
 use smtlib_lowlevel::{
-    ast::{self, Identifier, QualIdentifier},
+    ast::{self, Identifier, OptimizationPriority, QualIdentifier},
     backend,
     lexicon::{Numeral, Symbol},
     Driver, Logger,
@@ -82,6 +82,18 @@ where
             _ => todo!(),
         }
     }
+
+    /// sets the :opt.priority option to the given value
+    pub fn set_opt_priority(&mut self, priority: ast::OptimizationPriority) -> Result<(), Error> {
+        let cmd = ast::Command::SetOption(ast::Option::OptPriority(priority));
+
+        match self.driver.exec(&cmd)? {
+            ast::GeneralResponse::Success => Ok(()),
+            ast::GeneralResponse::Error(e) => Err(Error::Smt(e, cmd.to_string())),
+            _ => unimplemented!(),
+        }
+    }
+
     /// Explicitly sets the logic for the solver. For some backends this is not
     /// required, as they will infer what ever logic fits the current program.
     ///
@@ -136,7 +148,7 @@ where
 
         self.declare_all_consts(&term)?;
 
-        let cmd = ast::Command::AssertSoft(term);
+        let cmd = ast::Command::AssertSoft(term, vec![]);
 
         match self.driver.exec(&cmd)? {
             ast::GeneralResponse::Success => Ok(()),
diff --git a/xtask/src/spec.toml b/xtask/src/spec.toml
index a6d1a9a..9053277 100644
--- a/xtask/src/spec.toml
+++ b/xtask/src/spec.toml
@@ -274,7 +274,12 @@ syntax = "( maximize <term> )"
 syntax = "( minimize <term> )"
 
 [command.assert-soft]
-syntax = "( assert-soft <term> )"
+syntax = "( assert-soft <term> <optimization_attribute>* )"
+
+[optimization_attribute]
+weight = { syntax = ":weight <numeral>" }
+id = { syntax = ":id <symbol>"}
+attribute = { syntax = "<attribute>" }
 
 [script]
 syntax = "<command>*"
@@ -303,8 +308,22 @@ random-seed = { syntax = ":random-seed <numeral>" }
 regular-output-channel = { syntax = ":regular-output-channel <string>" }
 reproducible-resource-limit = { syntax = ":reproducible-resource-limit <numeral>" }
 verbosity = { syntax = ":verbosity <numeral>" }
+
+# optimization options
+"opt.priority" = { syntax = ":opt.priority <optimization_priority>"}
+
+# cont'd
 attribute = { syntax = "<attribute>" }
 
+[optimization_priority.pareto]
+syntax = "pareto"
+
+[optimization_priority.lex]
+syntax = "lex"
+
+[optimization_priority.box]
+syntax = "box"
+
 # Info flags.
 
 [info_flag.all-statistics]

From 4d4e0a60f8886d8e5ee1af01d385d7b66c6a810a Mon Sep 17 00:00:00 2001
From: Tim Beurskens <tim.beurskens@simpl.energy>
Date: Fri, 20 Dec 2024 14:23:11 +0100
Subject: [PATCH 8/8] add support for z3 `eval` command

---
 lowlevel/src/ast.rs                           |  58 +++-
 lowlevel/src/backend/mod.rs                   |  47 ++-
 lowlevel/src/lexicon.rs                       |   7 +
 lowlevel/src/lib.rs                           |  35 ++-
 lowlevel/src/parse.rs                         |  25 +-
 lowlevel/src/tests.rs                         |   4 +-
 smtlib/examples/queens.rs                     |  15 +-
 smtlib/examples/queens_bv.rs                  |  15 +-
 smtlib/examples/queens_bv2.rs                 |  15 +-
 smtlib/src/funs.rs                            |   2 +-
 smtlib/src/lib.rs                             |  43 +--
 smtlib/src/solver.rs                          |  66 +++-
 smtlib/src/sorts.rs                           |   2 +
 smtlib/src/terms.rs                           |  26 +-
 smtlib/src/tests.rs                           |   3 +-
 smtlib/src/theories/core.rs                   |  15 +-
 smtlib/src/theories/fixed_size_bit_vectors.rs |  47 ++-
 smtlib/src/theories/ints.rs                   |  13 +-
 smtlib/src/theories/reals.rs                  |  18 +-
 smtlib/src/tokio_solver.rs                    |  48 +--
 xtask/src/ast.rs                              | 286 ++++++++++--------
 xtask/src/logics.rs                           |   1 -
 xtask/src/spec.toml                           |  13 +
 23 files changed, 530 insertions(+), 274 deletions(-)

diff --git a/lowlevel/src/ast.rs b/lowlevel/src/ast.rs
index 167c50f..a87aa2c 100644
--- a/lowlevel/src/ast.rs
+++ b/lowlevel/src/ast.rs
@@ -1406,6 +1406,8 @@ pub enum Command {
     SetOption(Option),
     /// `(simplify <term>)`
     Simplify(Term),
+    /// `(eval <term>)`
+    Eval(Term),
     /// `(maximize <term>)`
     Maximize(Term),
     /// `(minimize <term>)`
@@ -1465,6 +1467,7 @@ impl std::fmt::Display for Command {
             Self::SetLogic(m0) => write!(f, "(set-logic {})", m0),
             Self::SetOption(m0) => write!(f, "(set-option {})", m0),
             Self::Simplify(m0) => write!(f, "(simplify {})", m0),
+            Self::Eval(m0) => write!(f, "(eval {})", m0),
             Self::Maximize(m0) => write!(f, "(maximize {})", m0),
             Self::Minimize(m0) => write!(f, "(minimize {})", m0),
             Self::AssertSoft(m0, m1) => {
@@ -1502,6 +1505,8 @@ impl SmtlibParse for Command {
                 && p.nth_matches(offset + 1, Token::Symbol, "minimize"))
             || (p.nth(offset) == Token::LParen
                 && p.nth_matches(offset + 1, Token::Symbol, "maximize"))
+            || (p.nth(offset) == Token::LParen
+                && p.nth_matches(offset + 1, Token::Symbol, "eval"))
             || (p.nth(offset) == Token::LParen
                 && p.nth_matches(offset + 1, Token::Symbol, "simplify"))
             || (p.nth(offset) == Token::LParen
@@ -1679,6 +1684,15 @@ impl SmtlibParse for Command {
             p.expect(Token::RParen)?;
             #[allow(clippy::useless_conversion)] return Ok(Self::Maximize(m0.into()));
         }
+        if p.nth(offset) == Token::LParen
+            && p.nth_matches(offset + 1, Token::Symbol, "eval")
+        {
+            p.expect(Token::LParen)?;
+            p.expect_matches(Token::Symbol, "eval")?;
+            let m0 = <Term as SmtlibParse>::parse(p)?;
+            p.expect(Token::RParen)?;
+            #[allow(clippy::useless_conversion)] return Ok(Self::Eval(m0.into()));
+        }
         if p.nth(offset) == Token::LParen
             && p.nth_matches(offset + 1, Token::Symbol, "simplify")
         {
@@ -1948,6 +1962,7 @@ impl Command {
             Self::SetLogic(_) => false,
             Self::SetOption(_) => false,
             Self::Simplify(_) => true,
+            Self::Eval(_) => true,
             Self::Maximize(_) => false,
             Self::Minimize(_) => false,
             Self::AssertSoft(_, _) => false,
@@ -2093,6 +2108,15 @@ impl Command {
                     ),
                 )
             }
+            Self::Eval(_) => {
+                Ok(
+                    Some(
+                        SpecificSuccessResponse::EvalResponse(
+                            EvalResponse::parse(response)?,
+                        ),
+                    ),
+                )
+            }
             Self::Maximize(_) => Ok(None),
             Self::Minimize(_) => Ok(None),
             Self::AssertSoft(_, _) => Ok(None),
@@ -3108,6 +3132,29 @@ impl SmtlibParse for SimplifyResponse {
         Ok(Self(m0))
     }
 }
+/// `<term>`
+#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
+pub struct EvalResponse(pub Term);
+impl std::fmt::Display for EvalResponse {
+    fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
+        write!(f, "{}", self.0)
+    }
+}
+impl EvalResponse {
+    pub fn parse(src: &str) -> Result<Self, ParseError> {
+        SmtlibParse::parse(&mut Parser::new(src))
+    }
+}
+impl SmtlibParse for EvalResponse {
+    fn is_start_of(offset: usize, p: &mut Parser) -> bool {
+        Term::is_start_of(offset, p)
+    }
+    fn parse(p: &mut Parser) -> Result<Self, ParseError> {
+        let m0 = <Term as SmtlibParse>::parse(p)?;
+        Ok(Self(m0))
+    }
+}
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
 #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
 pub enum SpecificSuccessResponse {
@@ -3135,6 +3182,8 @@ pub enum SpecificSuccessResponse {
     GetValueResponse(GetValueResponse),
     /// `<simplify_response>`
     SimplifyResponse(SimplifyResponse),
+    /// `<eval_response>`
+    EvalResponse(EvalResponse),
 }
 impl std::fmt::Display for SpecificSuccessResponse {
     fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
@@ -3151,6 +3200,7 @@ impl std::fmt::Display for SpecificSuccessResponse {
             Self::GetUnsatCoreResponse(m0) => write!(f, "{}", m0),
             Self::GetValueResponse(m0) => write!(f, "{}", m0),
             Self::SimplifyResponse(m0) => write!(f, "{}", m0),
+            Self::EvalResponse(m0) => write!(f, "{}", m0),
         }
     }
 }
@@ -3161,7 +3211,8 @@ impl SpecificSuccessResponse {
 }
 impl SmtlibParse for SpecificSuccessResponse {
     fn is_start_of(offset: usize, p: &mut Parser) -> bool {
-        (SimplifyResponse::is_start_of(offset, p))
+        (EvalResponse::is_start_of(offset, p))
+            || (SimplifyResponse::is_start_of(offset, p))
             || (GetValueResponse::is_start_of(offset, p))
             || (GetUnsatCoreResponse::is_start_of(offset, p))
             || (GetProofResponse::is_start_of(offset, p))
@@ -3176,6 +3227,11 @@ impl SmtlibParse for SpecificSuccessResponse {
     }
     fn parse(p: &mut Parser) -> Result<Self, ParseError> {
         let offset = 0;
+        if EvalResponse::is_start_of(offset, p) {
+            let m0 = <EvalResponse as SmtlibParse>::parse(p)?;
+            #[allow(clippy::useless_conversion)]
+            return Ok(Self::EvalResponse(m0.into()));
+        }
         if SimplifyResponse::is_start_of(offset, p) {
             let m0 = <SimplifyResponse as SmtlibParse>::parse(p)?;
             #[allow(clippy::useless_conversion)]
diff --git a/lowlevel/src/backend/mod.rs b/lowlevel/src/backend/mod.rs
index 1121afd..4a2b0aa 100644
--- a/lowlevel/src/backend/mod.rs
+++ b/lowlevel/src/backend/mod.rs
@@ -7,13 +7,18 @@
 //!
 //! ## Backends
 //!
-//! - **[`Z3Binary`](z3_binary::Z3Binary)**: A [Z3](https://github.com/Z3Prover/z3) backend using the binary CLI interface.
-//! - **[`Z3BinaryTokio`](z3_binary::tokio::Z3BinaryTokio)**: An async [Z3](https://github.com/Z3Prover/z3) backend using the binary CLI interface with [`tokio`](::tokio).
+//! - **[`Z3Binary`](z3_binary::Z3Binary)**: A [Z3](https://github.com/Z3Prover/z3)
+//!   backend using the binary CLI interface.
+//! - **[`Z3BinaryTokio`](z3_binary::tokio::Z3BinaryTokio)**: An async [Z3](https://github.com/Z3Prover/z3)
+//!   backend using the binary CLI interface with [`tokio`](::tokio).
 //!     - **Enabled by feature:** `tokio`
-//! - **`Z3Static`**: A [Z3](https://github.com/Z3Prover/z3) backend using the [`z3-sys` crate](https://github.com/prove-rs/z3.rs).
+//! - **`Z3Static`**: A [Z3](https://github.com/Z3Prover/z3) backend using the [`z3-sys`
+//!   crate](https://github.com/prove-rs/z3.rs).
 //!     - **Enabled by feature:** `z3-static`
-//! - **[`Cvc5Binary`](cvc5_binary::Cvc5Binary)**: A [cvc5](https://cvc5.github.io/) backend using the binary CLI interface.
-//! - **[`Cvc5BinaryTokio`](cvc5_binary::tokio::Cvc5BinaryTokio)**: An async [cvc5](https://cvc5.github.io/) backend using the binary CLI interface with [`tokio`](::tokio).
+//! - **[`Cvc5Binary`](cvc5_binary::Cvc5Binary)**: A [cvc5](https://cvc5.github.io/)
+//!   backend using the binary CLI interface.
+//! - **[`Cvc5BinaryTokio`](cvc5_binary::tokio::Cvc5BinaryTokio)**: An async [cvc5](https://cvc5.github.io/)
+//!   backend using the binary CLI interface with [`tokio`](::tokio).
 //!     - **Enabled by feature:** `tokio`
 
 use std::{
@@ -30,7 +35,8 @@ pub mod z3_static;
 
 use crate::parse::Token;
 
-/// The [`Backend`] trait is used to interact with SMT solver using the SMT-LIB language.
+/// The [`Backend`] trait is used to interact with SMT solver using the SMT-LIB
+/// language.
 ///
 /// For more details read the [`backend`](crate::backend) module documentation.
 pub trait Backend {
@@ -65,6 +71,7 @@ impl BinaryBackend {
             buf: String::new(),
         })
     }
+
     pub(crate) fn exec(&mut self, cmd: &crate::Command) -> Result<&str, crate::Error> {
         // println!("> {cmd}");
         writeln!(self.stdin, "{cmd}")?;
@@ -78,10 +85,12 @@ impl BinaryBackend {
             }
             if Lexer::new(self.buf.as_str())
                 .map(|tok| tok.unwrap_or(Token::Error))
-                .fold(0i32, |acc, tok| match tok {
-                    Token::LParen => acc + 1,
-                    Token::RParen => acc - 1,
-                    _ => acc,
+                .fold(0i32, |acc, tok| {
+                    match tok {
+                        Token::LParen => acc + 1,
+                        Token::RParen => acc - 1,
+                        _ => acc,
+                    }
                 })
                 != 0
             {
@@ -101,9 +110,11 @@ pub mod tokio {
 
     use crate::parse::Token;
 
-    /// The [`TokioBackend`] trait is used to interact with SMT solver using the SMT-LIB language.
+    /// The [`TokioBackend`] trait is used to interact with SMT solver using the
+    /// SMT-LIB language.
     ///
-    /// For more details read the [`backend`](crate::backend) module documentation.
+    /// For more details read the [`backend`](crate::backend) module
+    /// documentation.
     pub trait TokioBackend {
         fn exec(
             &mut self,
@@ -126,6 +137,7 @@ pub mod tokio {
             init: impl FnOnce(&mut tokio::process::Command),
         ) -> Result<Self, std::io::Error> {
             use std::process::Stdio;
+
             use tokio::process::Command;
 
             let mut cmd = Command::new(program);
@@ -145,6 +157,7 @@ pub mod tokio {
                 buf: String::new(),
             })
         }
+
         pub(crate) async fn exec(&mut self, cmd: &crate::Command) -> Result<&str, crate::Error> {
             // eprintln!("> {cmd}");
             self.stdin.write_all(cmd.to_string().as_bytes()).await?;
@@ -159,10 +172,12 @@ pub mod tokio {
                 }
                 if Lexer::new(self.buf.as_str())
                     .map(|tok| tok.unwrap_or(Token::Error))
-                    .fold(0i32, |acc, tok| match tok {
-                        Token::LParen => acc + 1,
-                        Token::RParen => acc - 1,
-                        _ => acc,
+                    .fold(0i32, |acc, tok| {
+                        match tok {
+                            Token::LParen => acc + 1,
+                            Token::RParen => acc - 1,
+                            _ => acc,
+                        }
                     })
                     != 0
                 {
diff --git a/lowlevel/src/lexicon.rs b/lowlevel/src/lexicon.rs
index be85971..00a4f14 100644
--- a/lowlevel/src/lexicon.rs
+++ b/lowlevel/src/lexicon.rs
@@ -16,6 +16,7 @@ impl SmtlibParse for Numeral {
     fn is_start_of(offset: usize, tokens: &mut Parser) -> bool {
         tokens.nth(offset) == Token::Numeral
     }
+
     fn parse(tokens: &mut Parser) -> Result<Self, ParseError> {
         Ok(Self(tokens.expect(Token::Numeral)?.into()))
     }
@@ -32,6 +33,7 @@ impl SmtlibParse for Decimal {
     fn is_start_of(offset: usize, tokens: &mut Parser) -> bool {
         tokens.nth(offset) == Token::Decimal
     }
+
     fn parse(tokens: &mut Parser) -> Result<Self, ParseError> {
         Ok(Self(tokens.expect(Token::Decimal)?.into()))
     }
@@ -48,6 +50,7 @@ impl SmtlibParse for Symbol {
     fn is_start_of(offset: usize, tokens: &mut Parser) -> bool {
         tokens.nth(offset) == Token::Symbol
     }
+
     fn parse(tokens: &mut Parser) -> Result<Self, ParseError> {
         Ok(Self(tokens.expect(Token::Symbol)?.into()))
     }
@@ -64,6 +67,7 @@ impl SmtlibParse for Hexadecimal {
     fn is_start_of(offset: usize, tokens: &mut Parser) -> bool {
         tokens.nth(offset) == Token::Hexadecimal
     }
+
     fn parse(tokens: &mut Parser) -> Result<Self, ParseError> {
         Ok(Self(tokens.expect(Token::Hexadecimal)?.into()))
     }
@@ -85,6 +89,7 @@ impl SmtlibParse for Binary {
     fn is_start_of(offset: usize, tokens: &mut Parser) -> bool {
         tokens.nth(offset) == Token::Binary
     }
+
     fn parse(tokens: &mut Parser) -> Result<Self, ParseError> {
         Ok(Self(tokens.expect(Token::Binary)?.into()))
     }
@@ -106,6 +111,7 @@ impl SmtlibParse for Reserved {
     fn is_start_of(offset: usize, tokens: &mut Parser) -> bool {
         tokens.nth(offset) == Token::Reserved
     }
+
     fn parse(tokens: &mut Parser) -> Result<Self, ParseError> {
         Ok(Self(tokens.expect(Token::Reserved)?.into()))
     }
@@ -122,6 +128,7 @@ impl SmtlibParse for Keyword {
     fn is_start_of(offset: usize, tokens: &mut Parser) -> bool {
         tokens.nth(offset) == Token::Keyword
     }
+
     fn parse(tokens: &mut Parser) -> Result<Self, ParseError> {
         Ok(Self(tokens.expect(Token::Keyword)?.into()))
     }
diff --git a/lowlevel/src/lib.rs b/lowlevel/src/lib.rs
index 302f429..59ca236 100644
--- a/lowlevel/src/lib.rs
+++ b/lowlevel/src/lib.rs
@@ -88,9 +88,11 @@ where
 
         Ok(driver)
     }
+
     pub fn set_logger(&mut self, logger: impl Logger) {
         self.logger = Some(Box::new(logger))
     }
+
     pub fn exec(&mut self, cmd: &Command) -> Result<GeneralResponse, Error> {
         if let Some(logger) = &self.logger {
             logger.exec(cmd);
@@ -111,9 +113,9 @@ where
 #[cfg(feature = "tokio")]
 pub mod tokio {
     use crate::{
+        Error, Logger,
         ast::{self, Command, GeneralResponse},
         backend::tokio::TokioBackend,
-        Error, Logger,
     };
 
     pub struct TokioDriver<B> {
@@ -153,9 +155,11 @@ pub mod tokio {
 
             Ok(driver)
         }
+
         pub fn set_logger(&mut self, logger: impl Logger) {
             self.logger = Some(Box::new(logger))
         }
+
         pub async fn exec(&mut self, cmd: &Command) -> Result<GeneralResponse, Error> {
             if let Some(logger) = &self.logger {
                 logger.exec(cmd);
@@ -181,14 +185,15 @@ impl Term {
             Term::SpecConstant(_) => HashSet::new(),
             Term::Identifier(q) => std::iter::once(q).collect(),
             Term::Application(_, args) => args.iter().flat_map(|arg| arg.all_consts()).collect(),
-            Term::Let(_, _) => todo!(),
+            Term::Let(..) => todo!(),
             // TODO
-            Term::Forall(_, _) => HashSet::new(),
-            Term::Exists(_, _) => todo!(),
-            Term::Match(_, _) => todo!(),
-            Term::Annotation(_, _) => todo!(),
+            Term::Forall(..) => HashSet::new(),
+            Term::Exists(..) => todo!(),
+            Term::Match(..) => todo!(),
+            Term::Annotation(..) => todo!(),
         }
     }
+
     pub fn strip_sort(self) -> Term {
         match self {
             Term::SpecConstant(_) => self,
@@ -198,15 +203,17 @@ impl Term {
             Term::Application(
                 QualIdentifier::Identifier(ident) | QualIdentifier::Sorted(ident, _),
                 args,
-            ) => Term::Application(
-                QualIdentifier::Identifier(ident),
-                args.into_iter().map(|arg| arg.strip_sort()).collect(),
-            ),
-            Term::Let(_, _) => todo!(),
+            ) => {
+                Term::Application(
+                    QualIdentifier::Identifier(ident),
+                    args.into_iter().map(|arg| arg.strip_sort()).collect(),
+                )
+            }
+            Term::Let(..) => todo!(),
             Term::Forall(qs, rs) => Term::Forall(qs, rs),
-            Term::Exists(_, _) => todo!(),
-            Term::Match(_, _) => todo!(),
-            Term::Annotation(_, _) => todo!(),
+            Term::Exists(..) => todo!(),
+            Term::Match(..) => todo!(),
+            Term::Annotation(..) => todo!(),
         }
     }
 }
diff --git a/lowlevel/src/parse.rs b/lowlevel/src/parse.rs
index 79084af..9736cdf 100644
--- a/lowlevel/src/parse.rs
+++ b/lowlevel/src/parse.rs
@@ -9,7 +9,8 @@ pub(crate) enum Token {
     #[token(")")]
     RParen,
 
-    /// A ⟨numeral⟩ is the digit 0 or a non-empty sequence of digits not starting with 0 .
+    /// A ⟨numeral⟩ is the digit 0 or a non-empty sequence of digits not
+    /// starting with 0 .
     #[regex("0|([1-9][0-9]*)", priority = 2)]
     Numeral,
 
@@ -132,14 +133,17 @@ impl SourceSpan {
     pub fn offset(&self) -> usize {
         self.offset
     }
+
     #[must_use]
     pub fn len(&self) -> usize {
         self.length
     }
+
     #[must_use]
     pub fn is_empty(&self) -> bool {
         self.len() == 0
     }
+
     #[must_use]
     pub fn join(&self, span: SourceSpan) -> SourceSpan {
         let offset = self.offset.min(span.offset);
@@ -147,10 +151,12 @@ impl SourceSpan {
         let length = end - offset;
         SourceSpan { offset, length }
     }
+
     #[must_use]
     pub fn end(&self) -> usize {
         self.offset + self.length
     }
+
     #[must_use]
     pub fn contains(&self, byte_offset: usize) -> bool {
         self.offset() <= byte_offset && byte_offset < self.end()
@@ -248,27 +254,34 @@ impl<'src> Parser<'src> {
             errors: vec![],
         }
     }
+
     pub(crate) fn current(&self) -> Token {
         self.nth(0)
     }
+
     pub(crate) fn nth_span(&self, n: usize) -> SourceSpan {
         self.nth_raw(n).1
     }
+
     pub(crate) fn current_span(&self) -> SourceSpan {
         self.nth_span(0)
     }
+
     pub(crate) fn nth_str(&self, n: usize) -> &'src str {
         let span = self.nth_span(n);
         &self.src[span.offset()..span.end()]
     }
+
     pub(crate) fn current_str(&self) -> &'src str {
         self.nth_str(0)
     }
+
     #[allow(unused)]
     pub(crate) fn current_src_str(&self) -> Spanned<&'src str> {
         let span = self.current_span();
         Spanned(self.current_str(), span)
     }
+
     pub(crate) fn nth_raw(&self, n: usize) -> (Token, SourceSpan) {
         if self.cursor + n >= self.lexer.len() {
             (Token::Error, SourceSpan::from((self.src.len(), 0)))
@@ -276,24 +289,30 @@ impl<'src> Parser<'src> {
             self.lexer[self.cursor + n]
         }
     }
+
     pub(crate) fn nth(&self, n: usize) -> Token {
         self.nth_raw(n).0
     }
+
     // TODO: Maybe we should assert end of stream when parsing scripts?
     #[allow(unused)]
     pub(crate) fn eoi(&self) -> bool {
         self.cursor >= self.lexer.len()
     }
+
     #[allow(unused)]
     pub(crate) fn pos(&self) -> usize {
         self.cursor
     }
+
     pub(crate) fn bump(&mut self) {
         self.cursor += 1
     }
+
     pub(crate) fn nth_matches(&self, n: usize, t: Token, s: &str) -> bool {
         self.nth(n) == t && self.nth_str(n) == s
     }
+
     pub(crate) fn expect_matches(&mut self, t: Token, s: &str) -> Result<&'src str, ParseError> {
         if self.nth_matches(0, t, s) {
             let s = self.current_str();
@@ -303,6 +322,7 @@ impl<'src> Parser<'src> {
             todo!()
         }
     }
+
     pub(crate) fn expect(&mut self, t: Token) -> Result<&'src str, ParseError> {
         match self.current() {
             found if found == t => {
@@ -324,6 +344,7 @@ impl<'src> Parser<'src> {
             }
         }
     }
+
     pub(crate) fn any<T: SmtlibParse>(&mut self) -> Result<Vec<T>, ParseError> {
         let mut res = vec![];
         while T::is_start_of(0, self) {
@@ -331,6 +352,7 @@ impl<'src> Parser<'src> {
         }
         Ok(res)
     }
+
     pub(crate) fn non_zero<T: SmtlibParse>(&mut self) -> Result<Vec<T>, ParseError> {
         let mut res = vec![T::parse(self)?];
         while T::is_start_of(0, self) {
@@ -338,6 +360,7 @@ impl<'src> Parser<'src> {
         }
         Ok(res)
     }
+
     pub(crate) fn n_plus_one<T: SmtlibParse>(&mut self) -> Result<Vec<T>, ParseError> {
         // TODO
         self.non_zero()
diff --git a/lowlevel/src/tests.rs b/lowlevel/src/tests.rs
index 58146f1..dd79856 100644
--- a/lowlevel/src/tests.rs
+++ b/lowlevel/src/tests.rs
@@ -13,7 +13,7 @@ fn bubble_sort() {
 }
 
 mod z3 {
-    use crate::{ast::Command, backend::z3_binary::Z3Binary, Driver};
+    use crate::{Driver, ast::Command, backend::z3_binary::Z3Binary};
 
     macro_rules! cmd {
         ($d:expr, $cmd:literal) => {
@@ -46,7 +46,7 @@ mod z3 {
 
 #[cfg(feature = "z3-static")]
 mod z3_static {
-    use crate::{ast::Command, backend::Z3Static, Driver};
+    use crate::{Driver, ast::Command, backend::Z3Static};
 
     macro_rules! cmd {
         ($d:expr, $cmd:literal) => {
diff --git a/smtlib/examples/queens.rs b/smtlib/examples/queens.rs
index 9559033..591332a 100644
--- a/smtlib/examples/queens.rs
+++ b/smtlib/examples/queens.rs
@@ -3,11 +3,10 @@ use miette::IntoDiagnostic;
 #[cfg(feature = "z3-static")]
 use smtlib::backend::Z3Static;
 use smtlib::{
-    and,
-    backend::{cvc5_binary::Cvc5Binary, z3_binary::Z3Binary, Backend},
+    Int, Logic, SatResultWithModel, Solver, and,
+    backend::{Backend, cvc5_binary::Cvc5Binary, z3_binary::Z3Binary},
     distinct, or,
     prelude::*,
-    Int, Logic, SatResultWithModel, Solver,
 };
 
 fn queens<B: Backend>(backend: B) -> miette::Result<()> {
@@ -82,10 +81,12 @@ fn main() -> miette::Result<()> {
         #[cfg(feature = "z3-static")]
         "z3-static" => queens(Z3Static::new().into_diagnostic()?)?,
         "cvc5" => queens(Cvc5Binary::new("cvc5").into_diagnostic()?)?,
-        given => miette::bail!(
-            "Invalid backend: '{}'. Available backends are: 'z3', 'z3-static', 'cvc5'",
-            given
-        ),
+        given => {
+            miette::bail!(
+                "Invalid backend: '{}'. Available backends are: 'z3', 'z3-static', 'cvc5'",
+                given
+            )
+        }
     }
 
     Ok(())
diff --git a/smtlib/examples/queens_bv.rs b/smtlib/examples/queens_bv.rs
index 6198856..ff061d6 100644
--- a/smtlib/examples/queens_bv.rs
+++ b/smtlib/examples/queens_bv.rs
@@ -3,11 +3,10 @@
 use itertools::Itertools;
 use miette::IntoDiagnostic;
 use smtlib::{
-    and,
-    backend::{cvc5_binary::Cvc5Binary, z3_binary::Z3Binary, Backend},
+    BitVec, SatResultWithModel, Solver, and,
+    backend::{Backend, cvc5_binary::Cvc5Binary, z3_binary::Z3Binary},
     distinct, or,
     prelude::*,
-    BitVec, SatResultWithModel, Solver,
 };
 
 fn queens<B: Backend>(backend: B) -> miette::Result<()> {
@@ -80,10 +79,12 @@ fn main() -> miette::Result<()> {
     match std::env::args().nth(1).as_deref().unwrap_or("z3") {
         "z3" => queens(Z3Binary::new("z3").into_diagnostic()?)?,
         "cvc5" => queens(Cvc5Binary::new("cvc5").into_diagnostic()?)?,
-        given => miette::bail!(
-            "Invalid backend: '{}'. Available backends are: 'z3', 'cvc5'",
-            given
-        ),
+        given => {
+            miette::bail!(
+                "Invalid backend: '{}'. Available backends are: 'z3', 'cvc5'",
+                given
+            )
+        }
     }
 
     Ok(())
diff --git a/smtlib/examples/queens_bv2.rs b/smtlib/examples/queens_bv2.rs
index 911256f..1aea41d 100644
--- a/smtlib/examples/queens_bv2.rs
+++ b/smtlib/examples/queens_bv2.rs
@@ -3,11 +3,10 @@
 use itertools::Itertools;
 use miette::IntoDiagnostic;
 use smtlib::{
-    and,
-    backend::{cvc5_binary::Cvc5Binary, z3_binary::Z3Binary, Backend},
+    BitVec, Logic, SatResultWithModel, Solver, and,
+    backend::{Backend, cvc5_binary::Cvc5Binary, z3_binary::Z3Binary},
     distinct, or,
     prelude::*,
-    BitVec, Logic, SatResultWithModel, Solver,
 };
 
 fn queens<B: Backend>(backend: B) -> miette::Result<()> {
@@ -94,10 +93,12 @@ fn main() -> miette::Result<()> {
     match std::env::args().nth(1).as_deref().unwrap_or("z3") {
         "z3" => queens(Z3Binary::new("z3").into_diagnostic()?)?,
         "cvc5" => queens(Cvc5Binary::new("cvc5").into_diagnostic()?)?,
-        given => miette::bail!(
-            "Invalid backend: '{}'. Available backends are: 'z3', 'cvc5'",
-            given
-        ),
+        given => {
+            miette::bail!(
+                "Invalid backend: '{}'. Available backends are: 'z3', 'cvc5'",
+                given
+            )
+        }
     }
 
     Ok(())
diff --git a/smtlib/src/funs.rs b/smtlib/src/funs.rs
index 01e6997..5c48951 100644
--- a/smtlib/src/funs.rs
+++ b/smtlib/src/funs.rs
@@ -2,7 +2,7 @@ use smtlib_lowlevel::{ast, lexicon::Symbol};
 
 use crate::{
     sorts::Sort,
-    terms::{qual_ident, Dynamic},
+    terms::{Dynamic, qual_ident},
 };
 
 #[derive(Debug)]
diff --git a/smtlib/src/lib.rs b/smtlib/src/lib.rs
index 135dd7b..0fd3aa4 100644
--- a/smtlib/src/lib.rs
+++ b/smtlib/src/lib.rs
@@ -5,15 +5,14 @@
 
 use std::collections::HashMap;
 
+pub use backend::Backend;
 use itertools::Itertools;
+pub use logics::Logic;
 use smtlib_lowlevel::ast;
+pub use smtlib_lowlevel::{self as lowlevel, Logger, backend};
 use terms::Const;
 pub use terms::Sorted;
 
-pub use backend::Backend;
-pub use logics::Logic;
-pub use smtlib_lowlevel::{self as lowlevel, backend, Logger};
-
 #[cfg(feature = "tokio")]
 mod tokio_solver;
 #[rustfmt::skip]
@@ -56,8 +55,9 @@ impl std::fmt::Display for SatResult {
     }
 }
 
-/// The satisfiability result produced by a solver, where the [`Sat`](SatResultWithModel::Sat) variant
-/// carries the satisfying model as well.
+/// The satisfiability result produced by a solver, where the
+/// [`Sat`](SatResultWithModel::Sat) variant carries the satisfying model as
+/// well.
 #[derive(Debug)]
 pub enum SatResultWithModel {
     /// The solver produced `unsat`
@@ -74,14 +74,18 @@ impl SatResultWithModel {
     pub fn expect_sat(self) -> Result<Model, Error> {
         match self {
             SatResultWithModel::Sat(m) => Ok(m),
-            SatResultWithModel::Unsat => Err(Error::UnexpectedSatResult {
-                expected: SatResult::Sat,
-                actual: SatResult::Unsat,
-            }),
-            SatResultWithModel::Unknown => Err(Error::UnexpectedSatResult {
-                expected: SatResult::Sat,
-                actual: SatResult::Unknown,
-            }),
+            SatResultWithModel::Unsat => {
+                Err(Error::UnexpectedSatResult {
+                    expected: SatResult::Sat,
+                    actual: SatResult::Unsat,
+                })
+            }
+            SatResultWithModel::Unknown => {
+                Err(Error::UnexpectedSatResult {
+                    expected: SatResult::Sat,
+                    actual: SatResult::Unknown,
+                })
+            }
         }
     }
 }
@@ -156,14 +160,17 @@ impl Model {
             values: model
                 .0
                 .into_iter()
-                .map(|res| match res {
-                    ast::ModelResponse::DefineFun(f) => (f.0 .0.trim_matches('|').into(), f.3),
-                    ast::ModelResponse::DefineFunRec(_) => todo!(),
-                    ast::ModelResponse::DefineFunsRec(_, _) => todo!(),
+                .map(|res| {
+                    match res {
+                        ast::ModelResponse::DefineFun(f) => (f.0.0.trim_matches('|').into(), f.3),
+                        ast::ModelResponse::DefineFunRec(_) => todo!(),
+                        ast::ModelResponse::DefineFunsRec(..) => todo!(),
+                    }
                 })
                 .collect(),
         }
     }
+
     /// Extract the value of a constant. Returns `None` if the value was not
     /// part of the model, which occurs if the constant was not part of any
     /// expression asserted.
diff --git a/smtlib/src/solver.rs b/smtlib/src/solver.rs
index 9ac88cb..49ec524 100644
--- a/smtlib/src/solver.rs
+++ b/smtlib/src/solver.rs
@@ -1,15 +1,17 @@
-use indexmap::{map::Entry, IndexMap, IndexSet};
+use indexmap::{IndexMap, IndexSet, map::Entry};
 use smtlib_lowlevel::{
-    ast::{self, Identifier, OptimizationPriority, QualIdentifier},
+    Driver, Logger,
+    ast::{
+        self, EvalResponse, GeneralResponse, Identifier, OptimizationPriority, QualIdentifier,
+        SpecificSuccessResponse, Term,
+    },
     backend,
     lexicon::{Numeral, Symbol},
-    Driver, Logger,
 };
 
 use crate::{
-    funs, sorts,
-    terms::{qual_ident, Dynamic},
-    Bool, Error, Logic, Model, SatResult, SatResultWithModel, Sorted,
+    Bool, Error, Logic, Model, SatResult, SatResultWithModel, Sorted, funs, sorts,
+    terms::{Dynamic, qual_ident},
 };
 
 /// The [`Solver`] type is the primary entrypoint to interaction with the
@@ -68,9 +70,11 @@ where
             declared_sorts: Default::default(),
         })
     }
+
     pub fn set_logger(&mut self, logger: impl Logger) {
         self.driver.set_logger(logger)
     }
+
     pub fn set_timeout(&mut self, ms: usize) -> Result<(), Error> {
         let cmd = ast::Command::SetOption(ast::Option::Attribute(ast::Attribute::WithValue(
             smtlib_lowlevel::lexicon::Keyword(":timeout".to_string()),
@@ -107,10 +111,12 @@ where
             ast::GeneralResponse::Error(_) => todo!(),
         }
     }
+
     /// Runs the given command on the solver, and returns the result.
     pub fn run_command(&mut self, cmd: &ast::Command) -> Result<ast::GeneralResponse, Error> {
         Ok(self.driver.exec(cmd)?)
     }
+
     /// Adds the constraint of `b` as an assertion to the solver. To check for
     /// satisfiability call [`Solver::check_sat`] or
     /// [`Solver::check_sat_with_model`].
@@ -128,7 +134,10 @@ where
     }
 
     /// Adds the optimization goal of `g` as a goal to the solver.
-    pub fn maximize<S>(&mut self, g: S) -> Result<(), Error> where S: Sorted {
+    pub fn maximize<S>(&mut self, g: S) -> Result<(), Error>
+    where
+        S: Sorted,
+    {
         let term = g.into();
 
         self.declare_all_consts(&term)?;
@@ -158,7 +167,10 @@ where
     }
 
     /// Adds the optimization goal of `g` as a goal to the solver.
-    pub fn minimize<S>(&mut self, g: S) -> Result<(), Error> where S: Sorted {
+    pub fn minimize<S>(&mut self, g: S) -> Result<(), Error>
+    where
+        S: Sorted,
+    {
         let term = g.into();
 
         self.declare_all_consts(&term)?;
@@ -182,15 +194,18 @@ where
         match self.driver.exec(&cmd)? {
             ast::GeneralResponse::SpecificSuccessResponse(
                 ast::SpecificSuccessResponse::CheckSatResponse(res),
-            ) => Ok(match res {
-                ast::CheckSatResponse::Sat => SatResult::Sat,
-                ast::CheckSatResponse::Unsat => SatResult::Unsat,
-                ast::CheckSatResponse::Unknown => SatResult::Unknown,
-            }),
+            ) => {
+                Ok(match res {
+                    ast::CheckSatResponse::Sat => SatResult::Sat,
+                    ast::CheckSatResponse::Unsat => SatResult::Unsat,
+                    ast::CheckSatResponse::Unknown => SatResult::Unknown,
+                })
+            }
             ast::GeneralResponse::Error(msg) => Err(Error::Smt(msg, format!("{cmd}"))),
             res => todo!("{res:?}"),
         }
     }
+
     /// Checks for satisfiability of the assertions sent to the solver using
     /// [`Solver::assert`], and produces a [model](Model) in case of `sat`.
     ///
@@ -203,6 +218,7 @@ where
             SatResult::Unknown => Ok(SatResultWithModel::Unknown),
         }
     }
+
     /// Produces the model for satisfying the assertions. If you are looking to
     /// retrieve a model after calling [`Solver::check_sat`], consider using
     /// [`Solver::check_sat_with_model`] instead.
@@ -217,6 +233,7 @@ where
             res => todo!("{res:?}"),
         }
     }
+
     pub fn declare_fun(&mut self, fun: &funs::Fun) -> Result<(), Error> {
         for var in &fun.vars {
             self.declare_sort(&var.ast())?;
@@ -238,6 +255,7 @@ where
             _ => todo!(),
         }
     }
+
     /// Simplifies the given term
     pub fn simplify(&mut self, t: Dynamic) -> Result<smtlib_lowlevel::ast::Term, Error> {
         self.declare_all_consts(&t.into())?;
@@ -252,6 +270,22 @@ where
         }
     }
 
+    pub fn eval<S>(&mut self, term: S) -> Result<S::Inner, Error>
+    where
+        S: Sorted,
+        S::Inner: From<Term>,
+    {
+        let cmd = ast::Command::Eval(term.into());
+
+        match self.driver.exec(&cmd)? {
+            GeneralResponse::SpecificSuccessResponse(SpecificSuccessResponse::EvalResponse(
+                EvalResponse(t),
+            )) => Ok(t.into()),
+            GeneralResponse::Error(e) => Err(Error::Smt(e, cmd.to_string())),
+            _ => unimplemented!(),
+        }
+    }
+
     pub fn scope<T>(
         &mut self,
         f: impl FnOnce(&mut Solver<B>) -> Result<T, Error>,
@@ -312,7 +346,7 @@ where
                                 self.driver
                                     .exec(&ast::Command::DeclareConst(sym.clone(), s.clone()))?;
                             }
-                            Identifier::Indexed(_, _) => todo!(),
+                            Identifier::Indexed(..) => todo!(),
                         }
                     }
                 }
@@ -330,7 +364,7 @@ where
             ast::Sort::Sort(ident) => {
                 let sym = match ident {
                     Identifier::Simple(sym) => sym,
-                    Identifier::Indexed(_, _) => {
+                    Identifier::Indexed(..) => {
                         // TODO: is it correct that only sorts from theores can
                         // be indexed, and thus does not need to be declared?
                         return Ok(());
@@ -344,7 +378,7 @@ where
             ast::Sort::Parametric(ident, params) => {
                 let sym = match ident {
                     Identifier::Simple(sym) => sym,
-                    Identifier::Indexed(_, _) => {
+                    Identifier::Indexed(..) => {
                         // TODO: is it correct that only sorts from theores can
                         // be indexed, and thus does not need to be declared?
                         return Ok(());
diff --git a/smtlib/src/sorts.rs b/smtlib/src/sorts.rs
index a17939b..462b927 100644
--- a/smtlib/src/sorts.rs
+++ b/smtlib/src/sorts.rs
@@ -69,6 +69,7 @@ impl Sort {
             parameters: Vec::new(),
         }
     }
+
     pub fn new_parametric(name: impl Into<String>, parameters: Vec<Sort>) -> Self {
         Self {
             name: name.into(),
@@ -76,6 +77,7 @@ impl Sort {
             parameters,
         }
     }
+
     pub fn new_indexed(name: impl Into<String>, index: Vec<Index>) -> Self {
         Self {
             name: name.into(),
diff --git a/smtlib/src/terms.rs b/smtlib/src/terms.rs
index b67b20a..bec3707 100644
--- a/smtlib/src/terms.rs
+++ b/smtlib/src/terms.rs
@@ -11,7 +11,7 @@ use smtlib_lowlevel::{
     lexicon::{Keyword, Symbol},
 };
 
-use crate::{sorts::Sort, Bool};
+use crate::{Bool, sorts::Sort};
 
 pub(crate) fn fun(name: &str, args: Vec<Term>) -> Term {
     Term::Application(qual_ident(name.to_string(), None), args)
@@ -74,7 +74,8 @@ pub trait StaticSorted: Into<Term> + From<Term> {
 /// low-level primitive that is used to define expressions for the SMT solvers
 /// to evaluate.
 pub trait Sorted: Into<Term> {
-    /// The inner type of the term. This is used for [`Const<T>`](Const) where the inner type is `T`.
+    /// The inner type of the term. This is used for [`Const<T>`](Const) where
+    /// the inner type is `T`.
     type Inner: Sorted;
     /// The sort of the term
     fn sort(&self) -> Sort;
@@ -135,13 +136,10 @@ pub trait Sorted: Into<Term> {
 
         (
             label,
-            Term::Annotation(
-                Box::new(self.into()),
-                vec![Attribute::WithValue(
-                    Keyword("named".to_string()),
-                    AttributeValue::Symbol(Symbol(name)),
-                )],
-            )
+            Term::Annotation(Box::new(self.into()), vec![Attribute::WithValue(
+                Keyword("named".to_string()),
+                AttributeValue::Symbol(Symbol(name)),
+            )])
             .into(),
         )
     }
@@ -153,9 +151,11 @@ impl<T: Into<Term>> From<Const<T>> for Term {
 }
 impl<T: Sorted> Sorted for Const<T> {
     type Inner = T;
+
     fn sort(&self) -> Sort {
         T::sort(self)
     }
+
     fn is_sort(sort: &Sort) -> bool {
         T::is_sort(sort)
     }
@@ -188,6 +188,7 @@ impl<T> Label<T> {
 
         Label(n, PhantomData)
     }
+
     pub(crate) fn name(&self) -> String {
         format!("named-label-{}", self.0)
     }
@@ -240,9 +241,11 @@ impl Dynamic {
 }
 impl Sorted for Dynamic {
     type Inner = Self;
+
     fn sort(&self) -> Sort {
         self.1.clone()
     }
+
     fn is_sort(_sort: &Sort) -> bool {
         true
     }
@@ -293,7 +296,8 @@ macro_rules! impl_op {
     };
 }
 
-/// This trait is implemented for types and sequences which can be used as quantified variables in [`forall`] and [`exists`].
+/// This trait is implemented for types and sequences which can be used as
+/// quantified variables in [`forall`] and [`exists`].
 pub trait QuantifierVars {
     /// The concrete sequence of variable declaration which should be quantified
     /// over.
@@ -340,7 +344,7 @@ impl_quantifiers!(A 0, B 1, C 2, D 3, E 4);
 impl QuantifierVars for Vec<Const<Dynamic>> {
     fn into_vars(self) -> Vec<SortedVar> {
         self.into_iter()
-            .map(|v| SortedVar(Symbol(v.0.into()), v.1 .1.ast()))
+            .map(|v| SortedVar(Symbol(v.0.into()), v.1.1.ast()))
             .collect()
     }
 }
diff --git a/smtlib/src/tests.rs b/smtlib/src/tests.rs
index 94168a7..44dff2f 100644
--- a/smtlib/src/tests.rs
+++ b/smtlib/src/tests.rs
@@ -1,8 +1,7 @@
 use terms::StaticSorted;
 
-use crate::terms::{forall, Sorted};
-
 use super::*;
+use crate::terms::{Sorted, forall};
 
 #[test]
 fn int_math() {
diff --git a/smtlib/src/theories/core.rs b/smtlib/src/theories/core.rs
index 14bfdc5..9409600 100644
--- a/smtlib/src/theories/core.rs
+++ b/smtlib/src/theories/core.rs
@@ -5,7 +5,7 @@ use smtlib_lowlevel::ast::{self, Term};
 use crate::{
     impl_op,
     sorts::Sort,
-    terms::{fun, qual_ident, Const, Dynamic, Sorted, StaticSorted},
+    terms::{Const, Dynamic, Sorted, StaticSorted, fun, qual_ident},
 };
 
 /// A [`Bool`] is a term containing a
@@ -77,9 +77,11 @@ impl From<(Term, Sort)> for Bool {
 }
 impl StaticSorted for Bool {
     type Inner = Self;
+
     fn static_sort() -> Sort {
         Sort::new("Bool")
     }
+
     fn new_const(name: impl Into<String>) -> Const<Self> {
         let name = String::leak(name.into());
         Const(name, Bool(BoolImpl::Const(name)))
@@ -89,9 +91,11 @@ impl Bool {
     pub fn sort() -> Sort {
         Self::static_sort()
     }
+
     fn binop(self, op: &str, other: Bool) -> Self {
         fun(op, vec![self.into(), other.into()]).into()
     }
+
     /// Construct the term expressing `(==> self other)`.
     ///
     /// The value of the returned boolean is true if:
@@ -100,6 +104,7 @@ impl Bool {
     pub fn implies(self, other: Bool) -> Bool {
         self.binop("=>", other)
     }
+
     /// Construct the term expressing `(ite self then otherwise)`.
     ///
     /// This is similar to the [ternary condition
@@ -134,8 +139,8 @@ pub fn and<const N: usize>(terms: [Bool; N]) -> Bool {
     fun("and", terms.map(Into::into).to_vec()).into()
 }
 /// Construct the term expressing `(or ...terms)` representing the disjunction
-/// of all of the terms. That is to say, the result is true iff any of the terms in
-/// `terms` is true.
+/// of all of the terms. That is to say, the result is true iff any of the terms
+/// in `terms` is true.
 pub fn or<const N: usize>(terms: [Bool; N]) -> Bool {
     fun("or", terms.map(Into::into).to_vec()).into()
 }
@@ -152,8 +157,8 @@ where
 {
     fun("=", terms.map(Into::into).to_vec()).into()
 }
-/// Construct the term expressing `(distinct terms)` representing that all of the
-/// terms in `terms` are distinct (or not-equal).
+/// Construct the term expressing `(distinct terms)` representing that all of
+/// the terms in `terms` are distinct (or not-equal).
 pub fn distinct<T, const N: usize>(terms: [T; N]) -> Bool
 where
     T: Into<ast::Term>,
diff --git a/smtlib/src/theories/fixed_size_bit_vectors.rs b/smtlib/src/theories/fixed_size_bit_vectors.rs
index 1c8e6d5..5c829e6 100644
--- a/smtlib/src/theories/fixed_size_bit_vectors.rs
+++ b/smtlib/src/theories/fixed_size_bit_vectors.rs
@@ -4,9 +4,9 @@ use itertools::Itertools;
 use smtlib_lowlevel::ast::{self, Term};
 
 use crate::{
-    sorts::{Index, Sort},
-    terms::{fun, qual_ident, Const, Dynamic, Sorted, StaticSorted},
     Bool,
+    sorts::{Index, Sort},
+    terms::{Const, Dynamic, Sorted, StaticSorted, fun, qual_ident},
 };
 
 /// A bit-vec is a fixed size sequence of boolean values. You can [read more
@@ -57,13 +57,15 @@ impl<const M: usize> TryFrom<BitVec<M>> for i64 {
 
     fn try_from(value: BitVec<M>) -> Result<Self, Self::Error> {
         match value.0 {
-            Term::SpecConstant(c) => match c {
-                ast::SpecConstant::Numeral(_) => todo!(),
-                ast::SpecConstant::Decimal(_) => todo!(),
-                ast::SpecConstant::Hexadecimal(h) => h.parse(),
-                ast::SpecConstant::Binary(b) => b.parse(),
-                ast::SpecConstant::String(_) => todo!(),
-            },
+            Term::SpecConstant(c) => {
+                match c {
+                    ast::SpecConstant::Numeral(_) => todo!(),
+                    ast::SpecConstant::Decimal(_) => todo!(),
+                    ast::SpecConstant::Hexadecimal(h) => h.parse(),
+                    ast::SpecConstant::Binary(b) => b.parse(),
+                    ast::SpecConstant::String(_) => todo!(),
+                }
+            }
             _ => todo!(),
         }
     }
@@ -78,6 +80,7 @@ impl<const M: usize> TryFrom<BitVec<M>> for [bool; M] {
 
 impl<const M: usize> StaticSorted for BitVec<M> {
     type Inner = Self;
+
     fn static_sort() -> Sort {
         Sort::new_indexed("BitVec", vec![Index::Numeral(M)])
     }
@@ -100,6 +103,7 @@ impl<const M: usize> BitVec<M> {
     fn binop<T: From<Term>>(self, op: &str, other: BitVec<M>) -> T {
         fun(op, vec![self.into(), other.into()]).into()
     }
+
     fn unop<T: From<Term>>(self, op: &str) -> T {
         fun(op, vec![self.into()]).into()
     }
@@ -128,14 +132,15 @@ impl<const M: usize> BitVec<M> {
         )
         .into()
     }
+
     #[cfg(feature = "const-bit-vec")]
     /// Concatenates `self` and `other` bit-vecs to a single contiguous bit-vec
     /// with length `N + M`
     pub fn concat<const N: usize>(self, other: impl Into<BitVec<N>>) -> BitVec<{ N + M }> {
-        Term::Application(
-            qual_ident("concat".to_string(), None),
-            vec![self.into(), other.into().into()],
-        )
+        Term::Application(qual_ident("concat".to_string(), None), vec![
+            self.into(),
+            other.into().into(),
+        ])
         .into()
     }
 
@@ -144,6 +149,7 @@ impl<const M: usize> BitVec<M> {
     pub fn bvnot(self) -> Self {
         self.unop("bvnot")
     }
+
     /// Calls `(bvneg self)` i.e. two's complement negation
     pub fn bvneg(self) -> Self {
         self.unop("bvneg")
@@ -154,42 +160,52 @@ impl<const M: usize> BitVec<M> {
     pub fn bvnand(self, other: impl Into<Self>) -> Self {
         self.binop("bvnand", other.into())
     }
+
     /// Calls `(bvnor self other)` i.e. bitwise nor
     pub fn bvnor(self, other: impl Into<Self>) -> Self {
         self.binop("bvnor", other.into())
     }
+
     /// Calls `(bvxnor self other)` i.e. bitwise xnor
     pub fn bvxnor(self, other: impl Into<Self>) -> Self {
         self.binop("bvxnor", other.into())
     }
+
     /// Calls `(bvult self other)`
     pub fn bvult(self, other: impl Into<Self>) -> Bool {
         self.binop("bvult", other.into())
     }
+
     /// Calls `(bvule self other)` i.e. unsigned less or equal
     pub fn bvule(self, other: impl Into<Self>) -> Bool {
         self.binop("bvule", other.into())
     }
+
     /// Calls `(bvugt self other)` i.e. unsigned greater than
     pub fn bvugt(self, other: impl Into<Self>) -> Bool {
         self.binop("bvugt", other.into())
     }
+
     /// Calls `(bvuge self other)` i.e. unsigned greater or equal
     pub fn bvuge(self, other: impl Into<Self>) -> Bool {
         self.binop("bvuge", other.into())
     }
+
     /// Calls `(bvslt self other)` i.e. signed less than
     pub fn bvslt(self, other: impl Into<Self>) -> Bool {
         self.binop("bvslt", other.into())
     }
+
     /// Calls `(bvsle self other)` i.e. signed less or equal
     pub fn bvsle(self, other: impl Into<Self>) -> Bool {
         self.binop("bvsle", other.into())
     }
+
     /// Calls `(bvsgt self other)` i.e. signed greater than
     pub fn bvsgt(self, other: impl Into<Self>) -> Bool {
         self.binop("bvsgt", other.into())
     }
+
     /// Calls `(bvsge self other)` i.e. signed greater or equal
     pub fn bvsge(self, other: impl Into<Self>) -> Bool {
         self.binop("bvsge", other.into())
@@ -198,12 +214,14 @@ impl<const M: usize> BitVec<M> {
 
 impl<const M: usize> std::ops::Not for BitVec<M> {
     type Output = Self;
+
     fn not(self) -> Self::Output {
         self.bvnot()
     }
 }
 impl<const M: usize> std::ops::Neg for BitVec<M> {
     type Output = Self;
+
     fn neg(self) -> Self::Output {
         self.bvneg()
     }
@@ -274,9 +292,8 @@ impl_op!(BitVec<M>, [bool; M], Shl, shl, bvshl, ShlAssign, shl_assign, <<);
 mod tests {
     use smtlib_lowlevel::backend::Z3Binary;
 
-    use crate::{terms::Sorted, Solver};
-
     use super::BitVec;
+    use crate::{Solver, terms::Sorted};
 
     #[test]
     fn bit_vec_extract_concat() -> Result<(), Box<dyn std::error::Error>> {
diff --git a/smtlib/src/theories/ints.rs b/smtlib/src/theories/ints.rs
index 3ff55ce..846b2d2 100644
--- a/smtlib/src/theories/ints.rs
+++ b/smtlib/src/theories/ints.rs
@@ -3,10 +3,9 @@
 use smtlib_lowlevel::{ast::Term, lexicon::Numeral};
 
 use crate::{
-    impl_op,
+    Bool, impl_op,
     sorts::Sort,
-    terms::{fun, qual_ident, Const, Dynamic, Sorted, StaticSorted},
-    Bool,
+    terms::{Const, Dynamic, Sorted, StaticSorted, fun, qual_ident},
 };
 
 /// A [`Int`] is a term containing a
@@ -48,6 +47,7 @@ impl From<(Term, Sort)> for Int {
 }
 impl StaticSorted for Int {
     type Inner = Self;
+
     fn static_sort() -> Sort {
         Sort::new("Int")
     }
@@ -64,25 +64,31 @@ impl Int {
     pub fn sort() -> Sort {
         Self::static_sort()
     }
+
     fn binop<T: From<Term>>(self, op: &str, other: Int) -> T {
         fun(op, vec![self.into(), other.into()]).into()
     }
+
     /// Construct the term expressing `(> self other)`
     pub fn gt(self, other: impl Into<Self>) -> Bool {
         self.binop(">", other.into())
     }
+
     /// Construct the term expressing `(>= self other)`
     pub fn ge(self, other: impl Into<Self>) -> Bool {
         self.binop(">=", other.into())
     }
+
     /// Construct the term expressing `(< self other)`
     pub fn lt(self, other: impl Into<Self>) -> Bool {
         self.binop("<", other.into())
     }
+
     /// Construct the term expressing `(<= self other)`
     pub fn le(self, other: impl Into<Self>) -> Bool {
         self.binop("<=", other.into())
     }
+
     // TODO: This seems to not be supported by z3?
     /// Construct the term expressing `(abs self)`
     pub fn abs(self) -> Int {
@@ -92,6 +98,7 @@ impl Int {
 
 impl std::ops::Neg for Int {
     type Output = Self;
+
     fn neg(self) -> Self::Output {
         fun("-", vec![self.into()]).into()
     }
diff --git a/smtlib/src/theories/reals.rs b/smtlib/src/theories/reals.rs
index 4a5a966..9885acc 100644
--- a/smtlib/src/theories/reals.rs
+++ b/smtlib/src/theories/reals.rs
@@ -3,10 +3,9 @@
 use smtlib_lowlevel::ast::Term;
 
 use crate::{
-    impl_op,
+    Bool, impl_op,
     sorts::Sort,
-    terms::{fun, qual_ident, Const, Dynamic, Sorted, StaticSorted},
-    Bool,
+    terms::{Const, Dynamic, Sorted, StaticSorted, fun, qual_ident},
 };
 
 /// A [`Real`] is a term containing a
@@ -43,6 +42,7 @@ impl From<Term> for Real {
 }
 impl StaticSorted for Real {
     type Inner = Self;
+
     fn static_sort() -> Sort {
         Sort::new("Real")
     }
@@ -66,38 +66,48 @@ impl Real {
     pub fn sort() -> Sort {
         Self::static_sort()
     }
+
     fn binop<T: From<Term>>(self, op: &str, other: Real) -> T {
         fun(op, vec![self.into(), other.into()]).into()
     }
+
     /// Construct the term expressing `(> self other)`
     pub fn gt(self, other: impl Into<Self>) -> Bool {
         self.binop(">", other.into())
     }
+
     /// Construct the term expressing `(>= self other)`
     pub fn ge(self, other: impl Into<Self>) -> Bool {
         self.binop(">=", other.into())
     }
+
     /// Construct the term expressing `(< self other)`
     pub fn lt(self, other: impl Into<Self>) -> Bool {
         self.binop("<", other.into())
     }
+
     /// Construct the term expressing `(<= self other)`
     pub fn le(self, other: impl Into<Self>) -> Bool {
         self.binop("<=", other.into())
     }
+
     /// Construct the term expressing `(abs self)`
     pub fn abs(self) -> Real {
         fun("abs", vec![self.into()]).into()
     }
 
     /// Construct the term expressing floor division of two terms
-    pub fn floor_div<R>(self, rhs: R) -> Self where R: Into<Real> {
+    pub fn floor_div<R>(self, rhs: R) -> Self
+    where
+        R: Into<Real>,
+    {
         self.binop("div", rhs.into())
     }
 }
 
 impl std::ops::Neg for Real {
     type Output = Self;
+
     fn neg(self) -> Self::Output {
         fun("-", vec![self.into()]).into()
     }
diff --git a/smtlib/src/tokio_solver.rs b/smtlib/src/tokio_solver.rs
index c828277..2ca2e10 100644
--- a/smtlib/src/tokio_solver.rs
+++ b/smtlib/src/tokio_solver.rs
@@ -1,4 +1,4 @@
-use std::collections::{hash_map::Entry, HashMap};
+use std::collections::{HashMap, hash_map::Entry};
 
 use smtlib_lowlevel::{
     ast::{self, Identifier, QualIdentifier},
@@ -57,6 +57,7 @@ where
             decls: Default::default(),
         })
     }
+
     /// Explicitly sets the logic for the solver. For some backends this is not
     /// required, as they will infer what ever logic fits the current program.
     ///
@@ -70,10 +71,12 @@ where
             ast::GeneralResponse::Error(_) => todo!(),
         }
     }
+
     /// Runs the given command on the solver, and returns the result.
     pub async fn run_command(&mut self, cmd: &ast::Command) -> Result<ast::GeneralResponse, Error> {
         Ok(self.driver.exec(cmd).await?)
     }
+
     /// Adds the constraint of `b` as an assertion to the solver. To check for
     /// satisfiability call [`TokioSolver::check_sat`] or
     /// [`TokioSolver::check_sat_with_model`].
@@ -82,20 +85,22 @@ where
         for q in term.all_consts() {
             match q {
                 QualIdentifier::Identifier(_) => {}
-                QualIdentifier::Sorted(i, s) => match self.decls.entry(i.clone()) {
-                    Entry::Occupied(stored) => assert_eq!(s, stored.get()),
-                    Entry::Vacant(v) => {
-                        v.insert(s.clone());
-                        match i {
-                            Identifier::Simple(sym) => {
-                                self.driver
-                                    .exec(&ast::Command::DeclareConst(sym.clone(), s.clone()))
-                                    .await?;
+                QualIdentifier::Sorted(i, s) => {
+                    match self.decls.entry(i.clone()) {
+                        Entry::Occupied(stored) => assert_eq!(s, stored.get()),
+                        Entry::Vacant(v) => {
+                            v.insert(s.clone());
+                            match i {
+                                Identifier::Simple(sym) => {
+                                    self.driver
+                                        .exec(&ast::Command::DeclareConst(sym.clone(), s.clone()))
+                                        .await?;
+                                }
+                                Identifier::Indexed(..) => todo!(),
                             }
-                            Identifier::Indexed(_, _) => todo!(),
                         }
                     }
-                },
+                }
             }
         }
         let cmd = ast::Command::Assert(term);
@@ -105,6 +110,7 @@ where
             _ => todo!(),
         }
     }
+
     /// Checks for satisfiability of the assertions sent to the solver using
     /// [`TokioSolver::assert`].
     ///
@@ -115,15 +121,18 @@ where
         match self.driver.exec(&cmd).await? {
             ast::GeneralResponse::SpecificSuccessResponse(
                 ast::SpecificSuccessResponse::CheckSatResponse(res),
-            ) => Ok(match res {
-                ast::CheckSatResponse::Sat => SatResult::Sat,
-                ast::CheckSatResponse::Unsat => SatResult::Unsat,
-                ast::CheckSatResponse::Unknown => SatResult::Unknown,
-            }),
+            ) => {
+                Ok(match res {
+                    ast::CheckSatResponse::Sat => SatResult::Sat,
+                    ast::CheckSatResponse::Unsat => SatResult::Unsat,
+                    ast::CheckSatResponse::Unknown => SatResult::Unknown,
+                })
+            }
             ast::GeneralResponse::Error(msg) => Err(Error::Smt(msg, format!("{cmd}"))),
             res => todo!("{res:?}"),
         }
     }
+
     /// Checks for satisfiability of the assertions sent to the solver using
     /// [`TokioSolver::assert`], and produces a [model](Model) in case of `sat`.
     ///
@@ -136,9 +145,10 @@ where
             SatResult::Unknown => Ok(SatResultWithModel::Unknown),
         }
     }
+
     /// Produces the model for satisfying the assertions. If you are looking to
-    /// retrieve a model after calling [`TokioSolver::check_sat`], consider using
-    /// [`TokioSolver::check_sat_with_model`] instead.
+    /// retrieve a model after calling [`TokioSolver::check_sat`], consider
+    /// using [`TokioSolver::check_sat_with_model`] instead.
     ///
     /// > **NOTE:** This must only be called after having called
     /// > [`TokioSolver::check_sat`] and it returning [`SatResult::Sat`].
diff --git a/xtask/src/ast.rs b/xtask/src/ast.rs
index c0f14ac..c61f3cb 100644
--- a/xtask/src/ast.rs
+++ b/xtask/src/ast.rs
@@ -48,35 +48,40 @@ impl RawSyntax {
                 priority,
                 separator,
                 response,
-            } => Syntax::Rule(Rule {
-                syntax: parse_raw_grammar(syntax),
-                priority: priority.unwrap_or_default(),
-                separator: separator.clone(),
-                response: response.as_ref().map(|s| parse_raw_token(s, 0)),
-            }),
-            RawSyntax::Class { response, cases } => Syntax::Class {
-                response: response.clone(),
-                cases: cases
-                    .iter()
-                    .map(|(n, s)| match s {
-                        RawSyntax::Just {
-                            syntax,
-                            priority,
-                            separator,
-                            response,
-                        } => (
-                            n.clone(),
-                            Rule {
-                                syntax: parse_raw_grammar(syntax),
-                                priority: priority.unwrap_or_default(),
-                                separator: separator.clone(),
-                                response: response.as_ref().map(|r| parse_raw_token(r, 0)),
-                            },
-                        ),
-                        RawSyntax::Class { .. } => todo!(),
-                    })
-                    .collect(),
-            },
+            } => {
+                Syntax::Rule(Rule {
+                    syntax: parse_raw_grammar(syntax),
+                    priority: priority.unwrap_or_default(),
+                    separator: separator.clone(),
+                    response: response.as_ref().map(|s| parse_raw_token(s, 0)),
+                })
+            }
+            RawSyntax::Class { response, cases } => {
+                Syntax::Class {
+                    response: response.clone(),
+                    cases: cases
+                        .iter()
+                        .map(|(n, s)| {
+                            match s {
+                                RawSyntax::Just {
+                                    syntax,
+                                    priority,
+                                    separator,
+                                    response,
+                                } => {
+                                    (n.clone(), Rule {
+                                        syntax: parse_raw_grammar(syntax),
+                                        priority: priority.unwrap_or_default(),
+                                        separator: separator.clone(),
+                                        response: response.as_ref().map(|r| parse_raw_token(r, 0)),
+                                    })
+                                }
+                                RawSyntax::Class { .. } => todo!(),
+                            }
+                        })
+                        .collect(),
+                }
+            }
         }
     }
 }
@@ -128,7 +133,7 @@ impl Token {
             LParen | RParen | Underscore | Annotation | Keyword(_) | Builtin(_) | Reserved(_) => {
                 true
             }
-            Field(_, _) => false,
+            Field(..) => false,
         }
     }
 }
@@ -190,7 +195,7 @@ fn parse_raw_grammar(s: &str) -> Grammar {
         .split(' ')
         .map(|t| {
             let t = parse_raw_token(t, acc);
-            if let Token::Field(_, _) = t {
+            if let Token::Field(..) = t {
                 acc += 1
             }
             t
@@ -198,9 +203,11 @@ fn parse_raw_grammar(s: &str) -> Grammar {
         .collect_vec();
     let fields = p
         .iter()
-        .filter_map(|t| match t {
-            Token::Field(_, f) => Some(f.clone()),
-            _ => None,
+        .filter_map(|t| {
+            match t {
+                Token::Field(_, f) => Some(f.clone()),
+                _ => None,
+            }
         })
         .collect();
     Grammar { tokens: p, fields }
@@ -285,72 +292,86 @@ impl Syntax {
     fn rust_ty_decl_top(&self, name: &str) -> String {
         let derive = r#"#[derive(Debug, Clone, PartialEq, Eq, Hash)] #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]"#;
         match self {
-            Syntax::Rule(r) => format!(
-                "/// `{}`\n{derive}\npub struct {}({});",
-                r.syntax,
-                name.to_pascal_case(),
-                r.syntax
-                    .tuple_fields(&[name.to_string()].into_iter().collect())
-                    .map(|f| format!("pub {f}"))
-                    .format(",")
-            ),
-            Syntax::Class { cases, .. } => format!(
-                "{derive}pub enum {} {{ {} }}",
-                name.to_pascal_case(),
-                cases
-                    .iter()
-                    .map(|(n, c)| c.rust_ty_decl_child(n, [name.to_string()].into_iter().collect()))
-                    .format(", ")
-            ),
+            Syntax::Rule(r) => {
+                format!(
+                    "/// `{}`\n{derive}\npub struct {}({});",
+                    r.syntax,
+                    name.to_pascal_case(),
+                    r.syntax
+                        .tuple_fields(&[name.to_string()].into_iter().collect())
+                        .map(|f| format!("pub {f}"))
+                        .format(",")
+                )
+            }
+            Syntax::Class { cases, .. } => {
+                format!(
+                    "{derive}pub enum {} {{ {} }}",
+                    name.to_pascal_case(),
+                    cases
+                        .iter()
+                        .map(|(n, c)| {
+                            c.rust_ty_decl_child(n, [name.to_string()].into_iter().collect())
+                        })
+                        .format(", ")
+                )
+            }
         }
     }
+
     fn rust_display(&self, name: &str) -> String {
         match self {
-            Syntax::Rule(r) => format!(
-                r#"
+            Syntax::Rule(r) => {
+                format!(
+                    r#"
                 impl std::fmt::Display for {} {{
                     fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {{
                         {}
                     }}
                 }}
                 "#,
-                name.to_pascal_case(),
-                r.rust_display_impl("self.")
-            ),
-            Syntax::Class { cases, .. } => format!(
-                r#"
+                    name.to_pascal_case(),
+                    r.rust_display_impl("self.")
+                )
+            }
+            Syntax::Class { cases, .. } => {
+                format!(
+                    r#"
                 impl std::fmt::Display for {} {{
                     fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {{
                         match self {{ {} }}
                     }}
                 }}
                 "#,
-                name.to_pascal_case(),
-                cases
-                    .iter()
-                    .map(|(n, c)| if c.syntax.fields.is_empty() {
-                        format!(
-                            "Self::{} => {},",
-                            n.to_pascal_case(),
-                            c.rust_display_impl("todo.")
-                        )
-                    } else {
-                        format!(
-                            "Self::{}({}) => {},",
-                            n.to_pascal_case(),
-                            c.syntax
-                                .fields
-                                .iter()
-                                .enumerate()
-                                .map(|(idx, _)| format!("m{idx}"))
-                                .format(","),
-                            c.rust_display_impl("m")
-                        )
-                    })
-                    .format("\n")
-            ),
+                    name.to_pascal_case(),
+                    cases
+                        .iter()
+                        .map(|(n, c)| {
+                            if c.syntax.fields.is_empty() {
+                                format!(
+                                    "Self::{} => {},",
+                                    n.to_pascal_case(),
+                                    c.rust_display_impl("todo.")
+                                )
+                            } else {
+                                format!(
+                                    "Self::{}({}) => {},",
+                                    n.to_pascal_case(),
+                                    c.syntax
+                                        .fields
+                                        .iter()
+                                        .enumerate()
+                                        .map(|(idx, _)| format!("m{idx}"))
+                                        .format(","),
+                                    c.rust_display_impl("m")
+                                )
+                            }
+                        })
+                        .format("\n")
+                )
+            }
         }
     }
+
     fn rust_parse(&self, name: &str) -> String {
         match self {
             Syntax::Rule(r) => {
@@ -440,6 +461,7 @@ impl Syntax {
             }
         }
     }
+
     fn rust_response(&self, name: &str) -> String {
         match self {
             Syntax::Rule(_) | Syntax::Class { response: None, .. } => "".to_string(),
@@ -482,12 +504,14 @@ impl Syntax {
                                     | Token::Builtin(_)
                                     | Token::Reserved(_)
                                     | Token::Keyword(_) => todo!(),
-                                    Token::Field(_, f) => match f {
-                                        Field::One(t)
-                                        | Field::Any(t)
-                                        | Field::NonZero(t)
-                                        | Field::NPlusOne(t) => t.to_string(),
-                                    },
+                                    Token::Field(_, f) => {
+                                        match f {
+                                            Field::One(t)
+                                            | Field::Any(t)
+                                            | Field::NonZero(t)
+                                            | Field::NPlusOne(t) => t.to_string(),
+                                        }
+                                    }
                                 };
                                 format!(
                                     "Ok(Some({}::{}({}::parse(response)?)))",
@@ -550,7 +574,7 @@ impl Rule {
                         Builtin(s) => s,
                         Reserved(s) => s,
                         Keyword(k) => k,
-                        Field(_, _) => "{}",
+                        Field(..) => "{}",
                     };
                     acc
                 }),
@@ -558,20 +582,23 @@ impl Rule {
                 .fields
                 .iter()
                 .enumerate()
-                .map(|(idx, f)| match f {
-                    Field::One(_) => {
-                        format!(", {scope}{idx}")
-                    }
-                    Field::Any(_) | Field::NonZero(_) | Field::NPlusOne(_) => {
-                        format!(
-                            r#", {scope}{idx}.iter().format({:?})"#,
-                            self.separator.as_deref().unwrap_or(" ")
-                        )
+                .map(|(idx, f)| {
+                    match f {
+                        Field::One(_) => {
+                            format!(", {scope}{idx}")
+                        }
+                        Field::Any(_) | Field::NonZero(_) | Field::NPlusOne(_) => {
+                            format!(
+                                r#", {scope}{idx}.iter().format({:?})"#,
+                                self.separator.as_deref().unwrap_or(" ")
+                            )
+                        }
                     }
                 })
                 .format("")
         )
     }
+
     fn rust_ty_decl_child(&self, name: &str, inside_of: HashSet<String>) -> String {
         if self.syntax.fields.is_empty() {
             format!("/// `{}`\n{}", self.syntax, name.to_pascal_case())
@@ -584,6 +611,7 @@ impl Rule {
             )
         }
     }
+
     fn rust_start_of_check(&self) -> String {
         let is_all_variable = !self.syntax.tokens.iter().any(|t| t.is_concrete());
 
@@ -610,9 +638,11 @@ impl Rule {
                 .to_string()
         }
     }
+
     fn rust_start_of_impl(&self) -> String {
         self.rust_start_of_check()
     }
+
     fn rust_parse_impl(&self) -> String {
         let stmts = self.syntax.tokens.iter().map(rust_parse_token);
         stmts.format("\n").to_string()
@@ -649,19 +679,23 @@ fn rust_parse_token(t: &Token) -> String {
         Token::Builtin(b) => format!("p.expect_matches(Token::Symbol, {b:?})?;"),
         Token::Reserved(b) => format!("p.expect_matches(Token::Reserved, {b:?})?;"),
         Token::Keyword(kw) => format!("p.expect_matches(Token::Keyword, {kw:?})?;"),
-        Token::Field(idx, f) => match f {
-            Field::One(t) => format!(
-                "let m{idx} = <{} as SmtlibParse>::parse(p)?;",
-                t.to_pascal_case()
-            ),
-            Field::Any(t) => format!("let m{idx} = p.any::<{}>()?;", t.to_pascal_case()),
-            Field::NonZero(t) => {
-                format!("let m{idx} = p.non_zero::<{}>()?;", t.to_pascal_case())
-            }
-            Field::NPlusOne(t) => {
-                format!("let m{idx} = p.n_plus_one::<{}>()?;", t.to_pascal_case())
+        Token::Field(idx, f) => {
+            match f {
+                Field::One(t) => {
+                    format!(
+                        "let m{idx} = <{} as SmtlibParse>::parse(p)?;",
+                        t.to_pascal_case()
+                    )
+                }
+                Field::Any(t) => format!("let m{idx} = p.any::<{}>()?;", t.to_pascal_case()),
+                Field::NonZero(t) => {
+                    format!("let m{idx} = p.non_zero::<{}>()?;", t.to_pascal_case())
+                }
+                Field::NPlusOne(t) => {
+                    format!("let m{idx} = p.n_plus_one::<{}>()?;", t.to_pascal_case())
+                }
             }
-        },
+        }
     }
 }
 
@@ -676,12 +710,14 @@ fn rust_check_token(idx: usize, t: &Token) -> String {
         Token::Keyword(kw) => {
             format!("p.nth_matches(offset + {idx}, Token::Keyword, {kw:?})")
         }
-        Token::Field(_, f) => match f {
-            Field::One(t) | Field::NonZero(t) | Field::NPlusOne(t) => {
-                format!("{}::is_start_of(offset + {idx}, p)", t.to_pascal_case())
+        Token::Field(_, f) => {
+            match f {
+                Field::One(t) | Field::NonZero(t) | Field::NPlusOne(t) => {
+                    format!("{}::is_start_of(offset + {idx}, p)", t.to_pascal_case())
+                }
+                Field::Any(_) => "todo!(\"{offset:?}, {p:?}\")".to_string(),
             }
-            Field::Any(_) => "todo!(\"{offset:?}, {p:?}\")".to_string(),
-        },
+        }
     }
 }
 
@@ -690,16 +726,18 @@ impl Grammar {
         &'a self,
         inside_of: &'a HashSet<String>,
     ) -> impl Iterator<Item = String> + 'a {
-        self.fields.iter().map(|f| match &f {
-            Field::One(t) => {
-                if inside_of.contains(t) {
-                    format!("Box<{}>", t.to_pascal_case())
-                } else {
-                    t.to_pascal_case()
+        self.fields.iter().map(|f| {
+            match &f {
+                Field::One(t) => {
+                    if inside_of.contains(t) {
+                        format!("Box<{}>", t.to_pascal_case())
+                    } else {
+                        t.to_pascal_case()
+                    }
+                }
+                Field::Any(t) | Field::NonZero(t) | Field::NPlusOne(t) => {
+                    format!("Vec<{}>", t.to_pascal_case())
                 }
-            }
-            Field::Any(t) | Field::NonZero(t) | Field::NPlusOne(t) => {
-                format!("Vec<{}>", t.to_pascal_case())
             }
         })
     }
diff --git a/xtask/src/logics.rs b/xtask/src/logics.rs
index be85e6a..3f2bb28 100644
--- a/xtask/src/logics.rs
+++ b/xtask/src/logics.rs
@@ -1,5 +1,4 @@
 use color_eyre::Result;
-
 use itertools::Itertools;
 use quote::{format_ident, quote};
 use xshell::Shell;
diff --git a/xtask/src/spec.toml b/xtask/src/spec.toml
index 9053277..09a9bde 100644
--- a/xtask/src/spec.toml
+++ b/xtask/src/spec.toml
@@ -263,6 +263,12 @@ syntax = "( set-option <option> )"
 syntax = "( simplify <term> )"
 response = "<simplify_response>"
 
+# Z3 eval extension
+
+[command.eval]
+syntax = "( eval <term> )"
+response = "<eval_response>"
+
 # Z3 Max-SMT extensions
 
 # https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-scss2014.pdf
@@ -412,6 +418,11 @@ syntax = "( <valuation_pair>+ )"
 [simplify_response]
 syntax = "<term>"
 
+# Z3 eval extension
+
+[eval_response]
+syntax = "<term>"
+
 [specific_success_response]
 get_unsat_assumptions_response = { syntax = "<get_unsat_assumptions_response>" }
 check_sat_response = { syntax = "<check_sat_response>" }
@@ -425,6 +436,8 @@ get_proof_response = { syntax = "<get_proof_response>" }
 get_unsat_core_response = { syntax = "<get_unsat_core_response>" }
 get_value_response = { syntax = "<get_value_response>" }
 simplify_response = { syntax = "<simplify_response>" }
+# Z3 eval extension
+eval_response = { syntax = "<eval_response>" }
 
 [general_response]
 success = { syntax = "success" }