From 9c2529586dd0ac9f17882b7a94a59ee5977b01fd Mon Sep 17 00:00:00 2001
From: bruderj15 <julian.bruder@outlook.com>
Date: Mon, 22 Jul 2024 15:45:17 +0200
Subject: [PATCH 01/19] api-extension: LIRA added arith funs

---
 src/Language/Hasmtlib/Example/ArithFun.hs | 20 ++++++++++++++++++++
 src/Language/Hasmtlib/Type/Expr.hs        | 10 ++++++++++
 2 files changed, 30 insertions(+)
 create mode 100644 src/Language/Hasmtlib/Example/ArithFun.hs

diff --git a/src/Language/Hasmtlib/Example/ArithFun.hs b/src/Language/Hasmtlib/Example/ArithFun.hs
new file mode 100644
index 0000000..5302840
--- /dev/null
+++ b/src/Language/Hasmtlib/Example/ArithFun.hs
@@ -0,0 +1,20 @@
+module Language.Hasmtlib.Example.ArithFun where
+
+import Prelude hiding (mod, (&&))
+import Language.Hasmtlib
+import Control.Monad
+
+main :: IO ()
+main = do
+  res <- solveWith (solver cvc5) $ do
+    setLogic "QF_LIRA"
+
+    xs <- replicateM 10 $ var @RealSort
+
+    forM_ xs $ \x -> assert $ x >=? 0 && x <? fromIntegral (length xs)
+    forM_ xs $ assert . isInt
+    assert $ distinct xs
+
+    return xs
+
+  print res
diff --git a/src/Language/Hasmtlib/Type/Expr.hs b/src/Language/Hasmtlib/Type/Expr.hs
index b3742cf..d2f20fd 100644
--- a/src/Language/Hasmtlib/Type/Expr.hs
+++ b/src/Language/Hasmtlib/Type/Expr.hs
@@ -10,6 +10,7 @@ module Language.Hasmtlib.Type.Expr
  , Expr
  , equal, distinct
  , bvShL, bvLShR, bvConcat, bvRotL, bvRotR
+ , toInt, toReal, isInt
  , for_all , exists
  , select, store
  )
@@ -107,3 +108,12 @@ bvRotL   = BvRotL
 bvRotR   :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)
 bvRotR   = BvRotR
 {-# INLINE bvRotR #-}
+
+toReal    :: Expr IntSort  -> Expr RealSort
+toReal = ToReal
+
+toInt     :: Expr RealSort -> Expr IntSort
+toInt = ToInt
+
+isInt     :: Expr RealSort -> Expr BoolSort
+isInt = IsInt

From 5c3af27f94033beff878789410c94c4d7f6afd47 Mon Sep 17 00:00:00 2001
From: bruderj15 <julian.bruder@outlook.com>
Date: Mon, 22 Jul 2024 15:55:08 +0200
Subject: [PATCH 02/19] api-extension: added assertMaybe

---
 src/Language/Hasmtlib/Type/MonadSMT.hs | 23 +++++++++++++++--------
 1 file changed, 15 insertions(+), 8 deletions(-)

diff --git a/src/Language/Hasmtlib/Type/MonadSMT.hs b/src/Language/Hasmtlib/Type/MonadSMT.hs
index 9358235..314cd74 100644
--- a/src/Language/Hasmtlib/Type/MonadSMT.hs
+++ b/src/Language/Hasmtlib/Type/MonadSMT.hs
@@ -15,21 +15,21 @@ class MonadState s m => MonadSMT s m where
   -- | Construct a variable.
   --   This is mainly intended for internal use.
   --   In the API use 'var'' instead.
-  --   
+  --
   -- @
   -- x :: SMTVar RealType <- smtvar' (Proxy @RealType)
   -- @
   smtvar' :: forall t. KnownSMTSort t => Proxy t -> m (SMTVar t)
-  
+
   -- | Construct a variable as expression.
-  -- 
+  --
   -- @
   -- x :: Expr RealType <- var' (Proxy @RealType)
   -- @
   var' :: forall t. KnownSMTSort t => Proxy t -> m (Expr t)
 
   -- | Assert a boolean expression.
-  -- 
+  --
   -- @
   -- x :: Expr IntType <- var @IntType
   -- assert $ x + 5 === 42
@@ -37,14 +37,14 @@ class MonadState s m => MonadSMT s m where
   assert :: Expr BoolSort -> m ()
 
   -- | Set an SMT-Solver-Option.
-  -- 
+  --
   -- @
   -- setOption $ Incremental True
   -- @
   setOption :: SMTOption -> m ()
 
   -- | Set the logic for the SMT-Solver to use.
-  -- 
+  --
   -- @
   -- setLogic \"QF_LRA\"
   -- @
@@ -63,7 +63,7 @@ smtvar = smtvar' (Proxy @t)
 {-# INLINE smtvar #-}
 
 -- | Create a constant.
--- 
+--
 --   >>> constant True
 --       Constant (BoolValue True)
 --
@@ -79,6 +79,13 @@ constant :: KnownSMTSort t => HaskellType t -> Expr t
 constant = Constant . wrapValue
 {-# INLINE constant #-}
 
+-- | Maybe assert a boolean expression.
+--   Asserts given expression if 'Maybe' is a 'Just'.
+--   Does nothing otherwise.
+assertMaybe :: MonadSMT s m => Maybe (Expr BoolSort) -> m ()
+assertMaybe Nothing = return ()
+assertMaybe (Just expr) = assert expr
+
 --   We need this separate so we get a pure API for quantifiers
 --   Ideally we would do that when rendering the expression
 --   However renderSMTLib2 is pure but we need a new quantified var which is stateful
@@ -146,4 +153,4 @@ class MonadSMT s m => MonadIncrSMT s m | m -> s where
 
 -- | First run 'checkSat' and then 'getModel' on the current problem.
 solve :: (MonadIncrSMT s m, MonadIO m) => m (Result, Solution)
-solve = liftM2 (,) checkSat getModel
\ No newline at end of file
+solve = liftM2 (,) checkSat getModel

From 6777c15dd9cbfdf445747f38e6794c7ee4d0b376 Mon Sep 17 00:00:00 2001
From: bruderj15 <julian.bruder@outlook.com>
Date: Mon, 22 Jul 2024 15:55:30 +0200
Subject: [PATCH 03/19] api-extension: added logical equivalence reverse
 implication

---
 src/Language/Hasmtlib/Boolean.hs | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/src/Language/Hasmtlib/Boolean.hs b/src/Language/Hasmtlib/Boolean.hs
index 755eb26..b258716 100644
--- a/src/Language/Hasmtlib/Boolean.hs
+++ b/src/Language/Hasmtlib/Boolean.hs
@@ -35,6 +35,18 @@ class Boolean b where
   (==>) :: b -> b -> b
   x ==> y = not x || y
 
+  -- | Logical implication with arrow reversed.
+  --
+  -- @
+  -- forall x y. (x ==> y) === (y <== x)
+  -- @
+  (<==) :: b -> b -> b
+  y <== x = not x || y
+
+  -- | Logical equivalence.
+  (<==>) :: b -> b -> b
+  x <==> y = (x ==> y) && (y ==> x)
+
   -- | Logical negation
   not :: b -> b
 

From 8f3b85addcae9f240d54d2b3f2f1a7a07b8a2832 Mon Sep 17 00:00:00 2001
From: bruderj15 <julian.bruder@outlook.com>
Date: Mon, 22 Jul 2024 15:57:25 +0200
Subject: [PATCH 04/19] api-extension: added solver OpenSMT

---
 hasmtlib.cabal                          | 1 +
 src/Language/Hasmtlib/Solver/OpenSMT.hs | 7 +++++++
 2 files changed, 8 insertions(+)
 create mode 100644 src/Language/Hasmtlib/Solver/OpenSMT.hs

diff --git a/hasmtlib.cabal b/hasmtlib.cabal
index b3bbbe3..75480db 100644
--- a/hasmtlib.cabal
+++ b/hasmtlib.cabal
@@ -40,6 +40,7 @@ library
                      , Language.Hasmtlib.Solver.Common
                      , Language.Hasmtlib.Solver.CVC5
                      , Language.Hasmtlib.Solver.MathSAT
+                     , Language.Hasmtlib.Solver.OpenSMT
                      , Language.Hasmtlib.Solver.Yices
                      , Language.Hasmtlib.Solver.Z3
                      , Language.Hasmtlib.Type.Expr
diff --git a/src/Language/Hasmtlib/Solver/OpenSMT.hs b/src/Language/Hasmtlib/Solver/OpenSMT.hs
new file mode 100644
index 0000000..234d75e
--- /dev/null
+++ b/src/Language/Hasmtlib/Solver/OpenSMT.hs
@@ -0,0 +1,7 @@
+module Language.Hasmtlib.Solver.CVC5 where
+
+import Language.Hasmtlib.Solver.Common
+import qualified SMTLIB.Backends.Process as P
+
+opensmt :: ProcessSolver
+opensmt = ProcessSolver $ P.defaultConfig { P.exe = "opensmt", P.args = [] }

From b00a776ffdad544b3e49fe041e23de520d0a1d0e Mon Sep 17 00:00:00 2001
From: bruderj15 <julian.bruder@outlook.com>
Date: Mon, 22 Jul 2024 16:13:49 +0200
Subject: [PATCH 05/19] api-extension: added OMT minimize/maximize

---
 hasmtlib.cabal                          |  1 +
 src/Language/Hasmtlib.hs                |  4 ++++
 src/Language/Hasmtlib/Optimization.hs   | 30 +++++++++++++++++++++++++
 src/Language/Hasmtlib/Solver/OpenSMT.hs |  2 +-
 src/Language/Hasmtlib/Type/Pipe.hs      | 14 +++++++-----
 5 files changed, 44 insertions(+), 7 deletions(-)
 create mode 100644 src/Language/Hasmtlib/Optimization.hs

diff --git a/hasmtlib.cabal b/hasmtlib.cabal
index 75480db..3ad4837 100644
--- a/hasmtlib.cabal
+++ b/hasmtlib.cabal
@@ -34,6 +34,7 @@ library
                      , Language.Hasmtlib.Equatable
                      , Language.Hasmtlib.Orderable
                      , Language.Hasmtlib.Integraled
+                     , Language.Hasmtlib.Optimization
                      , Language.Hasmtlib.Internal.Parser
                      , Language.Hasmtlib.Internal.Bitvec
                      , Language.Hasmtlib.Internal.Render
diff --git a/src/Language/Hasmtlib.hs b/src/Language/Hasmtlib.hs
index 37dd2ac..0dbf23d 100644
--- a/src/Language/Hasmtlib.hs
+++ b/src/Language/Hasmtlib.hs
@@ -8,6 +8,7 @@ module Language.Hasmtlib
   , module Language.Hasmtlib.Type.Option
   , module Language.Hasmtlib.Type.Solution
   , module Language.Hasmtlib.Type.ArrayMap
+  , module Language.Hasmtlib.Optimization
   , module Language.Hasmtlib.Integraled
   , module Language.Hasmtlib.Iteable
   , module Language.Hasmtlib.Boolean
@@ -20,6 +21,7 @@ module Language.Hasmtlib
   , module Language.Hasmtlib.Solver.CVC5
   , module Language.Hasmtlib.Solver.Z3
   , module Language.Hasmtlib.Solver.Yices
+  , module Language.Hasmtlib.Solver.OpenSMT
   , module Language.Hasmtlib.Solver.MathSAT
   )
   where
@@ -32,6 +34,7 @@ import Language.Hasmtlib.Type.Solver
 import Language.Hasmtlib.Type.Option
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Type.ArrayMap
+import Language.Hasmtlib.Optimization
 import Language.Hasmtlib.Integraled
 import Language.Hasmtlib.Iteable
 import Language.Hasmtlib.Boolean
@@ -44,4 +47,5 @@ import Language.Hasmtlib.Solver.Common
 import Language.Hasmtlib.Solver.CVC5
 import Language.Hasmtlib.Solver.Z3
 import Language.Hasmtlib.Solver.Yices
+import Language.Hasmtlib.Solver.OpenSMT
 import Language.Hasmtlib.Solver.MathSAT
diff --git a/src/Language/Hasmtlib/Optimization.hs b/src/Language/Hasmtlib/Optimization.hs
new file mode 100644
index 0000000..320e437
--- /dev/null
+++ b/src/Language/Hasmtlib/Optimization.hs
@@ -0,0 +1,30 @@
+module Language.Hasmtlib.Optimization where
+
+import Language.Hasmtlib.Type.Pipe
+import Language.Hasmtlib.Type.MonadSMT
+import Language.Hasmtlib.Internal.Expr
+import Language.Hasmtlib.Internal.Render
+import qualified SMTLIB.Backends as B
+import Control.Monad.IO.Class
+import Control.Monad.State
+import Control.Lens
+
+-- | Minimize a numerical expression within the SMT-Problem.
+--   This is a MaxSMT/OMT operation.
+--
+--   __Caution:__ Currently we do not restrict usage of this function to solvers who actually support it.
+--   When using 'minimize', make sure your solver supports MaxSMT/OMT.
+minimize :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Num (Expr t)) => Expr t -> m ()
+minimize expr = do
+  smt <- get
+  liftIO $ B.command_ (smt^.pipe) $ "(minimize " <> render expr <> ")"
+
+-- | Maximize a numerical expression within the SMT-Problem.
+--   This is a MaxSMT/OMT operation.
+--
+--   __Caution:__ Currently we do not restrict usage of this function to solvers who actually support it.
+--   When using 'maximize', make sure your solver supports MaxSMT/OMT.
+maximize :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Num (Expr t)) => Expr t -> m ()
+maximize expr = do
+  smt <- get
+  liftIO $ B.command_ (smt^.pipe) $ "(maximize " <> render expr <> ")"
diff --git a/src/Language/Hasmtlib/Solver/OpenSMT.hs b/src/Language/Hasmtlib/Solver/OpenSMT.hs
index 234d75e..5e80fda 100644
--- a/src/Language/Hasmtlib/Solver/OpenSMT.hs
+++ b/src/Language/Hasmtlib/Solver/OpenSMT.hs
@@ -1,4 +1,4 @@
-module Language.Hasmtlib.Solver.CVC5 where
+module Language.Hasmtlib.Solver.OpenSMT where
 
 import Language.Hasmtlib.Solver.Common
 import qualified SMTLIB.Backends.Process as P
diff --git a/src/Language/Hasmtlib/Type/Pipe.hs b/src/Language/Hasmtlib/Type/Pipe.hs
index e9b5f84..ca45ed3 100644
--- a/src/Language/Hasmtlib/Type/Pipe.hs
+++ b/src/Language/Hasmtlib/Type/Pipe.hs
@@ -1,3 +1,5 @@
+{-# OPTIONS_GHC -Wno-redundant-constraints #-}
+
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE UndecidableInstances #-}
 
@@ -98,12 +100,12 @@ instance (MonadState Pipe m, MonadIO m) => MonadIncrSMT Pipe m where
       Left e    -> liftIO $ do
         print model
         error e
-      Right sol -> 
-        return $ 
-          decode 
-            (DMap.singleton 
-              (sortSing @t) 
-              (IntValueMap $ IMap.singleton (sol^.solVar.varId) (sol^.solVal))) 
+      Right sol ->
+        return $
+          decode
+            (DMap.singleton
+              (sortSing @t)
+              (IntValueMap $ IMap.singleton (sol^.solVar.varId) (sol^.solVal)))
             v
   getValue expr = do
     model <- getModel

From 2b79bc23d2c3a51b10b1f1535d52646a52eec281 Mon Sep 17 00:00:00 2001
From: bruderj15 <julian.bruder@outlook.com>
Date: Mon, 22 Jul 2024 16:43:14 +0200
Subject: [PATCH 06/19] api-extension: added iterative refinement optimizations

---
 src/Language/Hasmtlib/Optimization.hs | 73 ++++++++++++++++++++++++++-
 src/Language/Hasmtlib/Type/Pipe.hs    |  2 -
 2 files changed, 71 insertions(+), 4 deletions(-)

diff --git a/src/Language/Hasmtlib/Optimization.hs b/src/Language/Hasmtlib/Optimization.hs
index 320e437..ebeead1 100644
--- a/src/Language/Hasmtlib/Optimization.hs
+++ b/src/Language/Hasmtlib/Optimization.hs
@@ -1,13 +1,24 @@
-module Language.Hasmtlib.Optimization where
+-- we want to restrict minimize and maximize to numerical expressions, therefore redundant Num (Expr t)
+{-# OPTIONS_GHC -Wno-redundant-constraints #-}
 
+module Language.Hasmtlib.Optimization
+  ( minimize, maximize
+  , solveMinimized, solveMaximized
+  , solveMinimizedDebug, solveMaximizedDebug
+  )
+where
+
+import Language.Hasmtlib.Codec
+import Language.Hasmtlib.Orderable
 import Language.Hasmtlib.Type.Pipe
 import Language.Hasmtlib.Type.MonadSMT
+import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Internal.Expr
 import Language.Hasmtlib.Internal.Render
 import qualified SMTLIB.Backends as B
 import Control.Monad.IO.Class
 import Control.Monad.State
-import Control.Lens
+import Control.Lens hiding (op)
 
 -- | Minimize a numerical expression within the SMT-Problem.
 --   This is a MaxSMT/OMT operation.
@@ -28,3 +39,61 @@ maximize :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Num (Expr t)) => Ex
 maximize expr = do
   smt <- get
   liftIO $ B.command_ (smt^.pipe) $ "(maximize " <> render expr <> ")"
+
+-- | Solves the current problem with respect to a minimal solution for a given numerical expression.
+--
+--   Does not rely on MaxSMT/OMT.
+--   Instead uses iterative refinement.
+--
+--   If you want access to intermediate results, use 'solveMinimizedDebug' instead.
+solveMinimized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t))
+  => Expr t
+  -> m (Result, Solution)
+solveMinimized = solveOptimized Nothing (<?)
+
+-- | Like 'solveMinimized' but with access to intermediate results.
+solveMinimizedDebug :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t))
+  => (Solution -> IO ())
+  -> Expr t
+  -> m (Result, Solution)
+solveMinimizedDebug debug = solveOptimized (Just debug) (<?)
+
+-- | Solves the current problem with respect to a maximal solution for a given numerical expression.
+--
+--   Does not rely on MaxSMT/OMT.
+--   Instead uses iterative refinement.
+--
+--   If you want access to intermediate results, use 'solveMaximizedDebug' instead.
+solveMaximized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t))
+  => Expr t
+  -> m (Result, Solution)
+solveMaximized = solveOptimized Nothing (>?)
+
+-- | Like 'solveMaximized' but with access to intermediate results.
+solveMaximizedDebug :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t))
+  => (Solution -> IO ())
+  -> Expr t
+  -> m (Result, Solution)
+solveMaximizedDebug debug = solveOptimized (Just debug) (<?)
+
+solveOptimized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t)
+  => Maybe (Solution -> IO ())
+  -> (Expr t -> Expr t -> Expr BoolSort)
+  -> Expr t
+  -> m (Result, Solution)
+solveOptimized mDebug op = go Unknown mempty
+  where
+    go oldRes oldSol target = do
+      push
+      (res, sol) <- solve
+      case res of
+        Sat   -> do
+          case decode sol target of
+            Nothing        -> return (Sat, mempty)
+            Just targetSol -> do
+              case mDebug of
+                Nothing    -> pure ()
+                Just debug -> liftIO $ debug sol
+              assert $ target `op` encode targetSol
+              go res sol target
+        _ -> pop >> return (oldRes, oldSol)
diff --git a/src/Language/Hasmtlib/Type/Pipe.hs b/src/Language/Hasmtlib/Type/Pipe.hs
index ca45ed3..5ad8d21 100644
--- a/src/Language/Hasmtlib/Type/Pipe.hs
+++ b/src/Language/Hasmtlib/Type/Pipe.hs
@@ -1,5 +1,3 @@
-{-# OPTIONS_GHC -Wno-redundant-constraints #-}
-
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE UndecidableInstances #-}
 

From 4034ab0475d2407674f0a9455725656a82fe416c Mon Sep 17 00:00:00 2001
From: bruderj15 <julian.bruder@outlook.com>
Date: Mon, 22 Jul 2024 16:45:31 +0200
Subject: [PATCH 07/19] api-extension: added infix xor

---
 src/Language/Hasmtlib/Boolean.hs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Language/Hasmtlib/Boolean.hs b/src/Language/Hasmtlib/Boolean.hs
index b258716..ad7b670 100644
--- a/src/Language/Hasmtlib/Boolean.hs
+++ b/src/Language/Hasmtlib/Boolean.hs
@@ -53,6 +53,7 @@ class Boolean b where
   -- | Exclusive-or
   xor :: b -> b -> b
 
+  infix 4 `xor`
   infixr 3 &&
   infixr 2 ||
   infixr 0 ==>

From 62b02b96c6b313f57650c522660cfe695cb744e0 Mon Sep 17 00:00:00 2001
From: bruderj15 <julian.bruder@outlook.com>
Date: Mon, 22 Jul 2024 21:05:38 +0200
Subject: [PATCH 08/19] api-extension: added custom user options

---
 src/Language/Hasmtlib/Example/Counting.hs |  2 +-
 src/Language/Hasmtlib/Internal/Render.hs  | 10 +++++++++-
 src/Language/Hasmtlib/Type/Option.hs      |  4 +++-
 3 files changed, 13 insertions(+), 3 deletions(-)

diff --git a/src/Language/Hasmtlib/Example/Counting.hs b/src/Language/Hasmtlib/Example/Counting.hs
index 922f51a..18c9575 100644
--- a/src/Language/Hasmtlib/Example/Counting.hs
+++ b/src/Language/Hasmtlib/Example/Counting.hs
@@ -14,7 +14,7 @@ main = do
     assert $ atMost  (2 :: Expr IntSort) xs
     assert $ atLeast @IntSort 1 xs
 
-    assert $ count @IntSort xs === 1 -- eqivalent to: exactly 1
+    assert $ count @IntSort xs === 1 -- equivalent to: exactly 1
 
     return xs
 
diff --git a/src/Language/Hasmtlib/Internal/Render.hs b/src/Language/Hasmtlib/Internal/Render.hs
index 861e363..b35ff2a 100644
--- a/src/Language/Hasmtlib/Internal/Render.hs
+++ b/src/Language/Hasmtlib/Internal/Render.hs
@@ -28,9 +28,17 @@ instance Render Double where
     | otherwise = formatDouble standardDefaultPrecision x
   {-# INLINEABLE render #-}
 
+instance Render Char where
+  render = char8
+  {-# INLINE render #-}
+
+instance Render String where
+  render = string8
+  {-# INLINE render #-}
+
 instance Render Builder where
   render = id
-  {-# INLINEABLE render #-}
+  {-# INLINE render #-}
 
 renderUnary :: Render a => Builder -> a -> Builder
 renderUnary op x = "(" <> op <> " " <> render x <> ")"
diff --git a/src/Language/Hasmtlib/Type/Option.hs b/src/Language/Hasmtlib/Type/Option.hs
index 3dcccfe..a8dbb48 100644
--- a/src/Language/Hasmtlib/Type/Option.hs
+++ b/src/Language/Hasmtlib/Type/Option.hs
@@ -9,9 +9,11 @@ data SMTOption =
     PrintSuccess  Bool              -- ^ Print \"success\" after each operation
   | ProduceModels Bool              -- ^ Produce a satisfying assignment after each successful checkSat
   | Incremental   Bool              -- ^ Incremental solving
+  | Custom String String            -- ^ Custom options. First String is the option, second its value.
   deriving (Show, Eq, Ord, Data)
 
 instance Render SMTOption where
   render (PrintSuccess  b) = renderBinary "set-option" (":print-success"  :: Builder) b
   render (ProduceModels b) = renderBinary "set-option" (":produce-models" :: Builder) b
-  render (Incremental   b) = renderBinary "set-option" (":incremental"    :: Builder) b
\ No newline at end of file
+  render (Incremental   b) = renderBinary "set-option" (":incremental"    :: Builder) b
+  render (Custom k v)      = renderBinary "set-option" (":" <> render k) (render v)

From c057d6ec04bc5207bf7d7626e19e8fae7fee0b92 Mon Sep 17 00:00:00 2001
From: bruderj15 <julian.bruder@outlook.com>
Date: Mon, 22 Jul 2024 21:28:17 +0200
Subject: [PATCH 09/19] api-extension: added OptiMathSAT + example& docu

---
 src/Language/Hasmtlib/Example/Optimization.hs | 23 +++++++++++++++++++
 src/Language/Hasmtlib/Solver/CVC5.hs          |  2 ++
 src/Language/Hasmtlib/Solver/MathSAT.hs       |  9 +++++++-
 src/Language/Hasmtlib/Solver/OpenSMT.hs       |  2 ++
 src/Language/Hasmtlib/Solver/Yices.hs         |  4 +++-
 src/Language/Hasmtlib/Solver/Z3.hs            |  3 ++-
 6 files changed, 40 insertions(+), 3 deletions(-)
 create mode 100644 src/Language/Hasmtlib/Example/Optimization.hs

diff --git a/src/Language/Hasmtlib/Example/Optimization.hs b/src/Language/Hasmtlib/Example/Optimization.hs
new file mode 100644
index 0000000..c6e9956
--- /dev/null
+++ b/src/Language/Hasmtlib/Example/Optimization.hs
@@ -0,0 +1,23 @@
+module Language.Hasmtlib.Example.Bitvector where
+
+import Language.Hasmtlib
+import Control.Monad.IO.Class
+
+main :: IO ()
+main = do
+  iSolver <- interactiveSolver optimathsat
+  interactiveWith iSolver $ do
+    setOption $ Custom "opt.priority" "lex"
+    setOption $ ProduceModels True
+    setLogic "QF_LIA"
+
+    x <- var @IntSort
+
+    assert $ x >? -2
+
+    minimize x
+
+    (_, sol) <- solve
+    liftIO $ print $ decode sol x
+
+    return ()
diff --git a/src/Language/Hasmtlib/Solver/CVC5.hs b/src/Language/Hasmtlib/Solver/CVC5.hs
index fea6cde..3f3c6de 100644
--- a/src/Language/Hasmtlib/Solver/CVC5.hs
+++ b/src/Language/Hasmtlib/Solver/CVC5.hs
@@ -3,5 +3,7 @@ module Language.Hasmtlib.Solver.CVC5 where
 import Language.Hasmtlib.Solver.Common
 import qualified SMTLIB.Backends.Process as P
 
+-- | A 'ProcessSolver' for CVC5.
+--   Requires binary @cvc5@ to be in path.
 cvc5 :: ProcessSolver
 cvc5 = ProcessSolver $ P.defaultConfig { P.exe = "cvc5", P.args = [] }
diff --git a/src/Language/Hasmtlib/Solver/MathSAT.hs b/src/Language/Hasmtlib/Solver/MathSAT.hs
index 4ecfc2a..e8567da 100644
--- a/src/Language/Hasmtlib/Solver/MathSAT.hs
+++ b/src/Language/Hasmtlib/Solver/MathSAT.hs
@@ -3,5 +3,12 @@ module Language.Hasmtlib.Solver.MathSAT where
 import Language.Hasmtlib.Solver.Common
 import qualified SMTLIB.Backends.Process as P
 
+-- | A 'ProcessSolver' for MathSAT.
+--   Requires binary @mathsat@ to be in path.
 mathsat :: ProcessSolver
-mathsat = ProcessSolver $ P.defaultConfig { P.exe = "mathsat", P.args = [] }
\ No newline at end of file
+mathsat = ProcessSolver $ P.defaultConfig { P.exe = "mathsat", P.args = [] }
+
+-- | A 'ProcessSolver' for OptiMathSAT.
+--   Requires binary @optimathsat@ to be in path.
+optimathsat :: ProcessSolver
+optimathsat = ProcessSolver $ P.defaultConfig { P.exe = "optimathsat", P.args = ["-optimization=true"] }
diff --git a/src/Language/Hasmtlib/Solver/OpenSMT.hs b/src/Language/Hasmtlib/Solver/OpenSMT.hs
index 5e80fda..cc71c70 100644
--- a/src/Language/Hasmtlib/Solver/OpenSMT.hs
+++ b/src/Language/Hasmtlib/Solver/OpenSMT.hs
@@ -3,5 +3,7 @@ module Language.Hasmtlib.Solver.OpenSMT where
 import Language.Hasmtlib.Solver.Common
 import qualified SMTLIB.Backends.Process as P
 
+-- | A 'ProcessSolver' for OpenSMT.
+--   Requires binary @opensmt@ to be in path.
 opensmt :: ProcessSolver
 opensmt = ProcessSolver $ P.defaultConfig { P.exe = "opensmt", P.args = [] }
diff --git a/src/Language/Hasmtlib/Solver/Yices.hs b/src/Language/Hasmtlib/Solver/Yices.hs
index ed48ff7..f9b7c7c 100644
--- a/src/Language/Hasmtlib/Solver/Yices.hs
+++ b/src/Language/Hasmtlib/Solver/Yices.hs
@@ -3,5 +3,7 @@ module Language.Hasmtlib.Solver.Yices where
 import Language.Hasmtlib.Solver.Common
 import qualified SMTLIB.Backends.Process as P
 
+-- | A 'ProcessSolver' for Yices.
+--   Requires binary @yices-smt2@ to be in path.
 yices :: ProcessSolver
-yices = ProcessSolver $ P.defaultConfig { P.exe = "yices-smt2", P.args = ["--smt2-model-format"] }
\ No newline at end of file
+yices = ProcessSolver $ P.defaultConfig { P.exe = "yices-smt2", P.args = ["--smt2-model-format"] }
diff --git a/src/Language/Hasmtlib/Solver/Z3.hs b/src/Language/Hasmtlib/Solver/Z3.hs
index 6caa30f..a61f8cb 100644
--- a/src/Language/Hasmtlib/Solver/Z3.hs
+++ b/src/Language/Hasmtlib/Solver/Z3.hs
@@ -3,6 +3,7 @@ module Language.Hasmtlib.Solver.Z3 where
 import Language.Hasmtlib.Solver.Common
 import qualified SMTLIB.Backends.Process as P
 
+-- | A 'ProcessSolver' for Z3.
+--   Requires binary @z3@ to be in path.
 z3 :: ProcessSolver
 z3 = ProcessSolver P.defaultConfig
-

From fe4e5ad4982af55db49f84826b7a85f5e5b8365e Mon Sep 17 00:00:00 2001
From: bruderj15 <julian.bruder@outlook.com>
Date: Tue, 23 Jul 2024 10:15:46 +0200
Subject: [PATCH 10/19] api-extensiom: added MonadOMT

---
 hasmtlib.cabal                                |  1 -
 src/Language/Hasmtlib.hs                      |  2 -
 src/Language/Hasmtlib/Example/Optimization.hs |  4 +-
 src/Language/Hasmtlib/Optimization.hs         | 99 -------------------
 src/Language/Hasmtlib/Type/MonadSMT.hs        | 51 ++++++++++
 src/Language/Hasmtlib/Type/Pipe.hs            | 19 ++++
 src/Language/Hasmtlib/Type/Solver.hs          | 71 ++++++++++++-
 7 files changed, 141 insertions(+), 106 deletions(-)
 delete mode 100644 src/Language/Hasmtlib/Optimization.hs

diff --git a/hasmtlib.cabal b/hasmtlib.cabal
index 3ad4837..75480db 100644
--- a/hasmtlib.cabal
+++ b/hasmtlib.cabal
@@ -34,7 +34,6 @@ library
                      , Language.Hasmtlib.Equatable
                      , Language.Hasmtlib.Orderable
                      , Language.Hasmtlib.Integraled
-                     , Language.Hasmtlib.Optimization
                      , Language.Hasmtlib.Internal.Parser
                      , Language.Hasmtlib.Internal.Bitvec
                      , Language.Hasmtlib.Internal.Render
diff --git a/src/Language/Hasmtlib.hs b/src/Language/Hasmtlib.hs
index 0dbf23d..c8778fe 100644
--- a/src/Language/Hasmtlib.hs
+++ b/src/Language/Hasmtlib.hs
@@ -8,7 +8,6 @@ module Language.Hasmtlib
   , module Language.Hasmtlib.Type.Option
   , module Language.Hasmtlib.Type.Solution
   , module Language.Hasmtlib.Type.ArrayMap
-  , module Language.Hasmtlib.Optimization
   , module Language.Hasmtlib.Integraled
   , module Language.Hasmtlib.Iteable
   , module Language.Hasmtlib.Boolean
@@ -34,7 +33,6 @@ import Language.Hasmtlib.Type.Solver
 import Language.Hasmtlib.Type.Option
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Type.ArrayMap
-import Language.Hasmtlib.Optimization
 import Language.Hasmtlib.Integraled
 import Language.Hasmtlib.Iteable
 import Language.Hasmtlib.Boolean
diff --git a/src/Language/Hasmtlib/Example/Optimization.hs b/src/Language/Hasmtlib/Example/Optimization.hs
index c6e9956..aec833c 100644
--- a/src/Language/Hasmtlib/Example/Optimization.hs
+++ b/src/Language/Hasmtlib/Example/Optimization.hs
@@ -5,15 +5,15 @@ import Control.Monad.IO.Class
 
 main :: IO ()
 main = do
-  iSolver <- interactiveSolver optimathsat
+  iSolver <- interactiveSolver z3
   interactiveWith iSolver $ do
-    setOption $ Custom "opt.priority" "lex"
     setOption $ ProduceModels True
     setLogic "QF_LIA"
 
     x <- var @IntSort
 
     assert $ x >? -2
+    assertSoftWeighted (x >? -1) 5.0
 
     minimize x
 
diff --git a/src/Language/Hasmtlib/Optimization.hs b/src/Language/Hasmtlib/Optimization.hs
deleted file mode 100644
index ebeead1..0000000
--- a/src/Language/Hasmtlib/Optimization.hs
+++ /dev/null
@@ -1,99 +0,0 @@
--- we want to restrict minimize and maximize to numerical expressions, therefore redundant Num (Expr t)
-{-# OPTIONS_GHC -Wno-redundant-constraints #-}
-
-module Language.Hasmtlib.Optimization
-  ( minimize, maximize
-  , solveMinimized, solveMaximized
-  , solveMinimizedDebug, solveMaximizedDebug
-  )
-where
-
-import Language.Hasmtlib.Codec
-import Language.Hasmtlib.Orderable
-import Language.Hasmtlib.Type.Pipe
-import Language.Hasmtlib.Type.MonadSMT
-import Language.Hasmtlib.Type.Solution
-import Language.Hasmtlib.Internal.Expr
-import Language.Hasmtlib.Internal.Render
-import qualified SMTLIB.Backends as B
-import Control.Monad.IO.Class
-import Control.Monad.State
-import Control.Lens hiding (op)
-
--- | Minimize a numerical expression within the SMT-Problem.
---   This is a MaxSMT/OMT operation.
---
---   __Caution:__ Currently we do not restrict usage of this function to solvers who actually support it.
---   When using 'minimize', make sure your solver supports MaxSMT/OMT.
-minimize :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Num (Expr t)) => Expr t -> m ()
-minimize expr = do
-  smt <- get
-  liftIO $ B.command_ (smt^.pipe) $ "(minimize " <> render expr <> ")"
-
--- | Maximize a numerical expression within the SMT-Problem.
---   This is a MaxSMT/OMT operation.
---
---   __Caution:__ Currently we do not restrict usage of this function to solvers who actually support it.
---   When using 'maximize', make sure your solver supports MaxSMT/OMT.
-maximize :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Num (Expr t)) => Expr t -> m ()
-maximize expr = do
-  smt <- get
-  liftIO $ B.command_ (smt^.pipe) $ "(maximize " <> render expr <> ")"
-
--- | Solves the current problem with respect to a minimal solution for a given numerical expression.
---
---   Does not rely on MaxSMT/OMT.
---   Instead uses iterative refinement.
---
---   If you want access to intermediate results, use 'solveMinimizedDebug' instead.
-solveMinimized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t))
-  => Expr t
-  -> m (Result, Solution)
-solveMinimized = solveOptimized Nothing (<?)
-
--- | Like 'solveMinimized' but with access to intermediate results.
-solveMinimizedDebug :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t))
-  => (Solution -> IO ())
-  -> Expr t
-  -> m (Result, Solution)
-solveMinimizedDebug debug = solveOptimized (Just debug) (<?)
-
--- | Solves the current problem with respect to a maximal solution for a given numerical expression.
---
---   Does not rely on MaxSMT/OMT.
---   Instead uses iterative refinement.
---
---   If you want access to intermediate results, use 'solveMaximizedDebug' instead.
-solveMaximized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t))
-  => Expr t
-  -> m (Result, Solution)
-solveMaximized = solveOptimized Nothing (>?)
-
--- | Like 'solveMaximized' but with access to intermediate results.
-solveMaximizedDebug :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t))
-  => (Solution -> IO ())
-  -> Expr t
-  -> m (Result, Solution)
-solveMaximizedDebug debug = solveOptimized (Just debug) (<?)
-
-solveOptimized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t)
-  => Maybe (Solution -> IO ())
-  -> (Expr t -> Expr t -> Expr BoolSort)
-  -> Expr t
-  -> m (Result, Solution)
-solveOptimized mDebug op = go Unknown mempty
-  where
-    go oldRes oldSol target = do
-      push
-      (res, sol) <- solve
-      case res of
-        Sat   -> do
-          case decode sol target of
-            Nothing        -> return (Sat, mempty)
-            Just targetSol -> do
-              case mDebug of
-                Nothing    -> pure ()
-                Just debug -> liftIO $ debug sol
-              assert $ target `op` encode targetSol
-              go res sol target
-        _ -> pop >> return (oldRes, oldSol)
diff --git a/src/Language/Hasmtlib/Type/MonadSMT.hs b/src/Language/Hasmtlib/Type/MonadSMT.hs
index 314cd74..72565f8 100644
--- a/src/Language/Hasmtlib/Type/MonadSMT.hs
+++ b/src/Language/Hasmtlib/Type/MonadSMT.hs
@@ -154,3 +154,54 @@ class MonadSMT s m => MonadIncrSMT s m | m -> s where
 -- | First run 'checkSat' and then 'getModel' on the current problem.
 solve :: (MonadIncrSMT s m, MonadIO m) => m (Result, Solution)
 solve = liftM2 (,) checkSat getModel
+
+-- | A 'MonadState' that holds an OMT-Problem.
+class MonadSMT s m => MonadOMT s m where
+  -- | Minimizes a numerical expression within the OMT-Problem.
+  --
+  --   For example, below minimization:
+  --
+  -- @
+  -- x <- var @IntSort
+  -- assert $ x >? -2
+  -- minimize x
+  -- @
+  --
+  --   will give @x := -1@ as solution.
+  minimize :: (KnownSMTSort t, Num (Expr t)) => Expr t -> m ()
+
+  -- | Maximizes a numerical expression within the OMT-Problem.
+  --
+  --   For example, below maximization:
+  --
+  -- @
+  -- x <- var @(BvSort 8)
+  -- maximize x
+  -- @
+  --
+  --   will give @x := 11111111@ as solution.
+  maximize :: (KnownSMTSort t, Num (Expr t)) => Expr t -> m ()
+
+  -- | Asserts a soft boolean expression.
+  --   May take a weight and an identifier for grouping.
+  --
+  --   For example, below a soft constraint with weight 2.0 and identifier \"myId\" for grouping:
+  --
+  -- @
+  -- x <- var @BoolSort
+  -- assertSoft x (Just 2.0) (Just "myId")
+  -- @
+  --
+  --   Omitting the weight will default it to 1.0.
+  --
+  -- @
+  -- x <- var @BoolSort
+  -- y <- var @BoolSort
+  -- assertSoft x
+  -- assertSoft y (Just "myId")
+  -- @
+  assertSoft :: Expr BoolSort -> Maybe Double -> Maybe String -> m ()
+
+-- | Like 'assertSoft' but forces a weight and omits the group-id.
+assertSoftWeighted :: MonadOMT s m => Expr BoolSort -> Double -> m ()
+assertSoftWeighted expr w = assertSoft expr (Just w) Nothing
diff --git a/src/Language/Hasmtlib/Type/Pipe.hs b/src/Language/Hasmtlib/Type/Pipe.hs
index 5ad8d21..c255c0f 100644
--- a/src/Language/Hasmtlib/Type/Pipe.hs
+++ b/src/Language/Hasmtlib/Type/Pipe.hs
@@ -109,3 +109,22 @@ instance (MonadState Pipe m, MonadIO m) => MonadIncrSMT Pipe m where
     model <- getModel
     return $ decode model expr
   {-# INLINEABLE getValue #-}
+
+instance (MonadSMT Pipe m, MonadIO m) => MonadOMT Pipe m where
+  minimize expr = do
+    smt <- get
+    liftIO $ B.command_ (smt^.pipe) $ "(minimize " <> render expr <> ")"
+  {-# INLINEABLE minimize #-}
+
+  maximize expr = do
+    smt <- get
+    liftIO $ B.command_ (smt^.pipe) $ "(maximize " <> render expr <> ")"
+  {-# INLINEABLE maximize #-}
+
+  assertSoft expr mWeight mGroupId = do
+    smt <- get
+    liftIO $ B.command_ (smt^.pipe) $
+      "(assert-soft " <> render expr <> " :weight " <> maybe "1" render mWeight <> renderGroupId mGroupId <> ")"
+    where
+      renderGroupId Nothing = mempty
+      renderGroupId (Just groupId) = " :id " <> render groupId
diff --git a/src/Language/Hasmtlib/Type/Solver.hs b/src/Language/Hasmtlib/Type/Solver.hs
index 5e280fa..f1bddeb 100644
--- a/src/Language/Hasmtlib/Type/Solver.hs
+++ b/src/Language/Hasmtlib/Type/Solver.hs
@@ -1,7 +1,16 @@
-module Language.Hasmtlib.Type.Solver where
+module Language.Hasmtlib.Type.Solver
+  ( WithSolver(..)
+  , solveWith, interactiveWith
+  , solveMinimized, solveMinimizedDebug
+  , solveMaximized, solveMaximizedDebug
+  )
+where
 
-import Language.Hasmtlib.Type.Pipe
+import Language.Hasmtlib.Type.MonadSMT
+import Language.Hasmtlib.Internal.Expr
 import Language.Hasmtlib.Type.Solution
+import Language.Hasmtlib.Type.Pipe
+import Language.Hasmtlib.Orderable
 import Language.Hasmtlib.Codec
 import qualified SMTLIB.Backends as B
 import qualified SMTLIB.Backends.Process as P
@@ -94,3 +103,61 @@ interactiveWith :: (MonadIO m, WithSolver s) => (B.Solver, P.Handle) -> StateT s
 interactiveWith (solver, handle) m = do
    _ <- runStateT m $ withSolver solver
    liftIO $ P.close handle
+
+-- | Solves the current problem with respect to a minimal solution for a given numerical expression.
+--
+--   Does not rely on MaxSMT/OMT.
+--   Instead uses iterative refinement.
+--
+--   If you want access to intermediate results, use 'solveMinimizedDebug' instead.
+solveMinimized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t))
+  => Expr t
+  -> m (Result, Solution)
+solveMinimized = solveOptimized Nothing (<?)
+
+-- | Like 'solveMinimized' but with access to intermediate results.
+solveMinimizedDebug :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t))
+  => (Solution -> IO ())
+  -> Expr t
+  -> m (Result, Solution)
+solveMinimizedDebug debug = solveOptimized (Just debug) (<?)
+
+-- | Solves the current problem with respect to a maximal solution for a given numerical expression.
+--
+--   Does not rely on MaxSMT/OMT.
+--   Instead uses iterative refinement.
+--
+--   If you want access to intermediate results, use 'solveMaximizedDebug' instead.
+solveMaximized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t))
+  => Expr t
+  -> m (Result, Solution)
+solveMaximized = solveOptimized Nothing (>?)
+
+-- | Like 'solveMaximized' but with access to intermediate results.
+solveMaximizedDebug :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t, Orderable (Expr t))
+  => (Solution -> IO ())
+  -> Expr t
+  -> m (Result, Solution)
+solveMaximizedDebug debug = solveOptimized (Just debug) (<?)
+
+solveOptimized :: (MonadIncrSMT Pipe m, MonadIO m, KnownSMTSort t)
+  => Maybe (Solution -> IO ())
+  -> (Expr t -> Expr t -> Expr BoolSort)
+  -> Expr t
+  -> m (Result, Solution)
+solveOptimized mDebug op = go Unknown mempty
+  where
+    go oldRes oldSol target = do
+      push
+      (res, sol) <- solve
+      case res of
+        Sat   -> do
+          case decode sol target of
+            Nothing        -> return (Sat, mempty)
+            Just targetSol -> do
+              case mDebug of
+                Nothing    -> pure ()
+                Just debug -> liftIO $ debug sol
+              assert $ target `op` encode targetSol
+              go res sol target
+        _ -> pop >> return (oldRes, oldSol)

From c83c8b40afe10b3ae50bfeb205969435fe8b887a Mon Sep 17 00:00:00 2001
From: bruderj15 <julian.bruder@outlook.com>
Date: Tue, 23 Jul 2024 11:18:02 +0200
Subject: [PATCH 11/19] api-extension: added OMT.hs

---
 hasmtlib.cabal                           |  1 +
 src/Language/Hasmtlib.hs                 |  2 +
 src/Language/Hasmtlib/Internal/Render.hs |  7 +-
 src/Language/Hasmtlib/Solver/Common.hs   | 15 ++--
 src/Language/Hasmtlib/Type/OMT.hs        | 88 ++++++++++++++++++++++++
 src/Language/Hasmtlib/Type/Pipe.hs       | 13 ++--
 src/Language/Hasmtlib/Type/SMT.hs        | 14 ++--
 7 files changed, 116 insertions(+), 24 deletions(-)
 create mode 100644 src/Language/Hasmtlib/Type/OMT.hs

diff --git a/hasmtlib.cabal b/hasmtlib.cabal
index 75480db..d8c3b3b 100644
--- a/hasmtlib.cabal
+++ b/hasmtlib.cabal
@@ -46,6 +46,7 @@ library
                      , Language.Hasmtlib.Type.Expr
                      , Language.Hasmtlib.Type.MonadSMT
                      , Language.Hasmtlib.Type.SMT
+                     , Language.Hasmtlib.Type.OMT
                      , Language.Hasmtlib.Type.Pipe
                      , Language.Hasmtlib.Type.Solution
                      , Language.Hasmtlib.Type.Solver
diff --git a/src/Language/Hasmtlib.hs b/src/Language/Hasmtlib.hs
index c8778fe..92b145a 100644
--- a/src/Language/Hasmtlib.hs
+++ b/src/Language/Hasmtlib.hs
@@ -2,6 +2,7 @@ module Language.Hasmtlib
   (
     module Language.Hasmtlib.Type.MonadSMT
   , module Language.Hasmtlib.Type.SMT
+  , module Language.Hasmtlib.Type.OMT
   , module Language.Hasmtlib.Type.Pipe
   , module Language.Hasmtlib.Type.Expr
   , module Language.Hasmtlib.Type.Solver
@@ -27,6 +28,7 @@ module Language.Hasmtlib
 
 import Language.Hasmtlib.Type.MonadSMT
 import Language.Hasmtlib.Type.SMT
+import Language.Hasmtlib.Type.OMT
 import Language.Hasmtlib.Type.Pipe
 import Language.Hasmtlib.Type.Expr
 import Language.Hasmtlib.Type.Solver
diff --git a/src/Language/Hasmtlib/Internal/Render.hs b/src/Language/Hasmtlib/Internal/Render.hs
index b35ff2a..c0deb75 100644
--- a/src/Language/Hasmtlib/Internal/Render.hs
+++ b/src/Language/Hasmtlib/Internal/Render.hs
@@ -2,9 +2,10 @@ module Language.Hasmtlib.Internal.Render where
 
 import Data.ByteString.Builder
 import Data.Foldable (foldl')
+import Data.Sequence
 import GHC.TypeNats
 
--- | Render values to their SMTLib2-Lisp form, represented as @Builder@.
+-- | Render values to their SMTLib2-Lisp form, represented as 'Builder'.
 class Render a where
   render :: a -> Builder
 
@@ -57,3 +58,7 @@ renderNary op xs = "(" <> op <> renderedXs <> ")"
   where
     renderedXs = foldl' (\s x -> s <> " " <> render x) mempty xs
 {-# INLINEABLE renderNary #-}
+
+-- | Render values to their sequential SMTLib2-Lisp form, represented as a 'Seq' 'Builder'.
+class RenderSeq a where
+  renderSeq :: a -> Seq Builder
diff --git a/src/Language/Hasmtlib/Solver/Common.hs b/src/Language/Hasmtlib/Solver/Common.hs
index 4bad08b..d7d1fe6 100644
--- a/src/Language/Hasmtlib/Solver/Common.hs
+++ b/src/Language/Hasmtlib/Solver/Common.hs
@@ -2,6 +2,7 @@ module Language.Hasmtlib.Solver.Common where
 
 import Language.Hasmtlib.Type.SMT
 import Language.Hasmtlib.Type.Solution
+import Language.Hasmtlib.Internal.Render
 import Language.Hasmtlib.Internal.Parser
 import Data.Default
 import Data.Sequence as Seq hiding ((|>), filter)
@@ -52,24 +53,24 @@ instance Default Debugger where
 
 -- | A 'Solver' which holds an external process with a SMT-Solver.
 --   This will:
--- 
+--
 -- 1. Encode the 'SMT'-problem,
--- 
+--
 -- 2. Start a new external process for the SMT-Solver,
--- 
+--
 -- 3. Send the problem to the SMT-Solver,
--- 
+--
 -- 4. Wait for an answer and parse it and
--- 
+--
 -- 5. close the process and clean up all resources.
--- 
+--
 processSolver :: MonadIO m => P.Config -> Maybe Debugger -> Solver SMT m
 processSolver cfg debugger smt = do
   liftIO $ P.with cfg $ \handle -> do
     maybe mempty (`debugSMT` smt) debugger
     pSolver <- B.initSolver B.Queuing $ P.toBackend handle
 
-    let problem = renderSMT smt
+    let problem = renderSeq smt
     maybe mempty (`debugProblem` problem) debugger
 
     forM_ problem (B.command_ pSolver)
diff --git a/src/Language/Hasmtlib/Type/OMT.hs b/src/Language/Hasmtlib/Type/OMT.hs
new file mode 100644
index 0000000..b0439cf
--- /dev/null
+++ b/src/Language/Hasmtlib/Type/OMT.hs
@@ -0,0 +1,88 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE LambdaCase #-}
+
+module Language.Hasmtlib.Type.OMT where
+
+import Language.Hasmtlib.Internal.Expr
+import Language.Hasmtlib.Internal.Render
+import Language.Hasmtlib.Type.MonadSMT
+import Language.Hasmtlib.Type.Option
+import Language.Hasmtlib.Type.SMT
+import Data.List (isPrefixOf)
+import Data.Default
+import Data.Coerce
+import Data.Sequence hiding ((|>), filter)
+import Data.Data (toConstr, showConstr)
+import Control.Monad.State
+import Control.Lens hiding (List)
+
+-- | An assertion of a booolean expression in OMT that may be weighted.
+data SoftFormula = SoftFormula
+  { _formula  :: Expr BoolSort
+  , _mWeight  :: Maybe Double
+  , _mGroupId :: Maybe String
+  } deriving Show
+$(makeLenses ''SoftFormula)
+
+-- | A newtype for numerical expressions that are target of a minimization.
+newtype Minimize t = Minimize { _targetMin :: (KnownSMTSort t, Num (Expr t)) => Expr t }
+
+-- | A newtype for numerical expressions that are target of a maximization.
+newtype Maximize t = Maximize { _targetMax :: (KnownSMTSort t, Num (Expr t)) => Expr t }
+
+-- | The state of the SMT-problem.
+data OMT = OMT
+  { _smt            :: SMT
+  , _targetMinimize :: !(Seq (SomeKnownSMTSort Minimize))
+  , _targetMaximize :: !(Seq (SomeKnownSMTSort Minimize))
+  , _softFormulas   :: !(Seq SoftFormula)
+  }
+$(makeLenses ''OMT)
+
+instance Default OMT where
+  def = OMT def mempty mempty mempty
+
+instance MonadState OMT m => MonadSMT OMT m where
+  smtvar' _ = fmap coerce $ (smt.lastVarId) <+= 1
+  {-# INLINE smtvar' #-}
+
+  var' p = do
+    newVar <- smtvar' p
+    smt.vars %= (|> SomeSMTSort newVar)
+    return $ Var newVar
+  {-# INLINE var' #-}
+
+  assert expr = do
+    omt <- get
+    qExpr <- case omt^.smt.mlogic of
+      Nothing    -> return expr
+      Just logic -> if "QF" `isPrefixOf` logic then return expr else quantify expr
+    modify $ \s -> s & (smt.formulas) %~ (|> qExpr)
+  {-# INLINE assert #-}
+
+  setOption opt = smt.options %= ((opt:) . filter (not . eqCon opt))
+    where
+      eqCon :: SMTOption -> SMTOption -> Bool
+      eqCon l r = showConstr (toConstr l) == showConstr (toConstr r)
+
+  setLogic l = smt.mlogic ?= l
+
+instance Render SoftFormula where
+  render sf = "(assert-soft " <> render (sf^.formula) <> " :weight " <> maybe "1" render (sf^.mWeight) <> renderGroupId (sf^.mGroupId) <> ")"
+    where
+      renderGroupId Nothing = mempty
+      renderGroupId (Just groupId) = " :id " <> render groupId
+
+instance KnownSMTSort t => Render (Minimize t) where
+  render expr = "(minimize " <> render expr <> ")"
+
+instance KnownSMTSort t => Render (Maximize t) where
+  render expr = "(maximize " <> render expr <> ")"
+
+instance RenderSeq OMT where
+  renderSeq omt =
+       renderSeq (omt^.smt)
+    <> fmap render (omt^.softFormulas)
+    <> fmap (\case SomeSMTSort minExpr -> render minExpr) (omt^.targetMinimize)
+    <> fmap (\case SomeSMTSort maxExpr -> render maxExpr) (omt^.targetMaximize)
diff --git a/src/Language/Hasmtlib/Type/Pipe.hs b/src/Language/Hasmtlib/Type/Pipe.hs
index c255c0f..f682ec6 100644
--- a/src/Language/Hasmtlib/Type/Pipe.hs
+++ b/src/Language/Hasmtlib/Type/Pipe.hs
@@ -4,6 +4,7 @@
 module Language.Hasmtlib.Type.Pipe where
 
 import Language.Hasmtlib.Type.SMT
+import Language.Hasmtlib.Type.OMT (SoftFormula(..), Minimize(..), Maximize(..))
 import Language.Hasmtlib.Type.MonadSMT
 import Language.Hasmtlib.Internal.Expr
 import Language.Hasmtlib.Internal.Render
@@ -113,18 +114,14 @@ instance (MonadState Pipe m, MonadIO m) => MonadIncrSMT Pipe m where
 instance (MonadSMT Pipe m, MonadIO m) => MonadOMT Pipe m where
   minimize expr = do
     smt <- get
-    liftIO $ B.command_ (smt^.pipe) $ "(minimize " <> render expr <> ")"
+    liftIO $ B.command_ (smt^.pipe) $ render $ Minimize expr
   {-# INLINEABLE minimize #-}
 
   maximize expr = do
     smt <- get
-    liftIO $ B.command_ (smt^.pipe) $ "(maximize " <> render expr <> ")"
+    liftIO $ B.command_ (smt^.pipe) $ render $ Maximize expr
   {-# INLINEABLE maximize #-}
 
-  assertSoft expr mWeight mGroupId = do
+  assertSoft expr w gid = do
     smt <- get
-    liftIO $ B.command_ (smt^.pipe) $
-      "(assert-soft " <> render expr <> " :weight " <> maybe "1" render mWeight <> renderGroupId mGroupId <> ")"
-    where
-      renderGroupId Nothing = mempty
-      renderGroupId (Just groupId) = " :id " <> render groupId
+    liftIO $ B.command_ (smt^.pipe) $ render $ SoftFormula expr w gid
diff --git a/src/Language/Hasmtlib/Type/SMT.hs b/src/Language/Hasmtlib/Type/SMT.hs
index fe7c8b4..7277107 100644
--- a/src/Language/Hasmtlib/Type/SMT.hs
+++ b/src/Language/Hasmtlib/Type/SMT.hs
@@ -54,14 +54,12 @@ instance MonadState SMT m => MonadSMT SMT m where
 
   setLogic l = mlogic ?= l
 
--- | Render a 'SMT'-Problem to SMTLib2-Syntax.
---   Each element of the returned Sequence is a line.
-renderSMT :: SMT -> Seq Builder
-renderSMT smt =
-     fromList (render <$> smt^.options)
-  >< maybe mempty (singleton . renderSetLogic . stringUtf8) (smt^.mlogic)
-  >< renderVars (smt^.vars)
-  >< fmap renderAssert (smt^.formulas)
+instance RenderSeq SMT where
+  renderSeq smt =
+       fromList (render <$> smt^.options)
+       >< maybe mempty (singleton . renderSetLogic . stringUtf8) (smt^.mlogic)
+       >< renderVars (smt^.vars)
+       >< fmap renderAssert (smt^.formulas)
 
 renderSetLogic :: Builder -> Builder
 renderSetLogic = renderUnary "set-logic"

From 56ebfe25b944c0dbe4e910c38b0b57d1b6892530 Mon Sep 17 00:00:00 2001
From: bruderj15 <julian.bruder@outlook.com>
Date: Tue, 23 Jul 2024 11:34:30 +0200
Subject: [PATCH 12/19] api-extension: fixed self loop render-bug

---
 src/Language/Hasmtlib/Type/OMT.hs | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/src/Language/Hasmtlib/Type/OMT.hs b/src/Language/Hasmtlib/Type/OMT.hs
index b0439cf..33abe66 100644
--- a/src/Language/Hasmtlib/Type/OMT.hs
+++ b/src/Language/Hasmtlib/Type/OMT.hs
@@ -26,17 +26,17 @@ data SoftFormula = SoftFormula
 $(makeLenses ''SoftFormula)
 
 -- | A newtype for numerical expressions that are target of a minimization.
-newtype Minimize t = Minimize { _targetMin :: (KnownSMTSort t, Num (Expr t)) => Expr t }
+newtype Minimize t = Minimize { _targetMin :: Expr t }
 
 -- | A newtype for numerical expressions that are target of a maximization.
-newtype Maximize t = Maximize { _targetMax :: (KnownSMTSort t, Num (Expr t)) => Expr t }
+newtype Maximize t = Maximize { _targetMax :: Expr t }
 
--- | The state of the SMT-problem.
+-- | The state of the OMT-problem.
 data OMT = OMT
-  { _smt            :: SMT
-  , _targetMinimize :: !(Seq (SomeKnownSMTSort Minimize))
-  , _targetMaximize :: !(Seq (SomeKnownSMTSort Minimize))
-  , _softFormulas   :: !(Seq SoftFormula)
+  { _smt            :: SMT                                  -- ^ The underlying 'SMT'-Problem
+  , _targetMinimize :: !(Seq (SomeKnownSMTSort Minimize))   -- ^ All expressions to minimize
+  , _targetMaximize :: !(Seq (SomeKnownSMTSort Maximize))   -- ^ All expressions to maximize
+  , _softFormulas   :: !(Seq SoftFormula)                   -- ^ All soft assertions of boolean expressions
   }
 $(makeLenses ''OMT)
 
@@ -75,10 +75,10 @@ instance Render SoftFormula where
       renderGroupId (Just groupId) = " :id " <> render groupId
 
 instance KnownSMTSort t => Render (Minimize t) where
-  render expr = "(minimize " <> render expr <> ")"
+  render (Minimize expr) = "(minimize " <> render expr <> ")"
 
 instance KnownSMTSort t => Render (Maximize t) where
-  render expr = "(maximize " <> render expr <> ")"
+  render (Maximize expr) = "(maximize " <> render expr <> ")"
 
 instance RenderSeq OMT where
   renderSeq omt =

From 304b4e08d4decd29f7b0e13668ff88fb2a5cf1a1 Mon Sep 17 00:00:00 2001
From: bruderj15 <julian.bruder@outlook.com>
Date: Tue, 23 Jul 2024 11:59:12 +0200
Subject: [PATCH 13/19] api-extension: adjusted types for OMT-solvers

---
 src/Language/Hasmtlib/Example/Arith.hs        |  4 +-
 src/Language/Hasmtlib/Example/ArithFun.hs     |  2 +-
 src/Language/Hasmtlib/Example/Array.hs        |  2 +-
 src/Language/Hasmtlib/Example/Bitvector.hs    |  2 +-
 src/Language/Hasmtlib/Example/Codec.hs        |  6 +--
 src/Language/Hasmtlib/Example/Counting.hs     |  2 +-
 ...mization.hs => IncrementalOptimization.hs} |  2 +-
 .../Hasmtlib/Example/McCarthyArrayAxioms.hs   |  6 +--
 src/Language/Hasmtlib/Example/Monad.hs        |  4 +-
 .../Hasmtlib/Example/OMTOptimization.hs       | 20 ++++++++++
 src/Language/Hasmtlib/Example/Quantifier.hs   |  4 +-
 .../Hasmtlib/Example/Transcendental.hs        |  4 +-
 src/Language/Hasmtlib/Solver/Common.hs        | 39 ++++++++++++-------
 src/Language/Hasmtlib/Type/MonadSMT.hs        |  1 +
 src/Language/Hasmtlib/Type/OMT.hs             |  5 +++
 15 files changed, 71 insertions(+), 32 deletions(-)
 rename src/Language/Hasmtlib/Example/{Optimization.hs => IncrementalOptimization.hs} (85%)
 create mode 100644 src/Language/Hasmtlib/Example/OMTOptimization.hs

diff --git a/src/Language/Hasmtlib/Example/Arith.hs b/src/Language/Hasmtlib/Example/Arith.hs
index a1e154b..31e47e7 100644
--- a/src/Language/Hasmtlib/Example/Arith.hs
+++ b/src/Language/Hasmtlib/Example/Arith.hs
@@ -5,7 +5,7 @@ import Language.Hasmtlib
 
 main :: IO ()
 main = do
-  res <- solveWith (solver cvc5) $ do
+  res <- solveWith (solver @SMT cvc5) $ do
     setLogic "QF_LIA"
 
     x <- var @IntSort
@@ -14,7 +14,7 @@ main = do
     assert $ y >? 0 && x /== y
     assert $ x `mod` 42 === y
     assert $ y + x + 1 >=? x + y
-    
+
     return (x,y)
 
   print res
diff --git a/src/Language/Hasmtlib/Example/ArithFun.hs b/src/Language/Hasmtlib/Example/ArithFun.hs
index 5302840..49042e8 100644
--- a/src/Language/Hasmtlib/Example/ArithFun.hs
+++ b/src/Language/Hasmtlib/Example/ArithFun.hs
@@ -6,7 +6,7 @@ import Control.Monad
 
 main :: IO ()
 main = do
-  res <- solveWith (solver cvc5) $ do
+  res <- solveWith (solver @SMT cvc5) $ do
     setLogic "QF_LIRA"
 
     xs <- replicateM 10 $ var @RealSort
diff --git a/src/Language/Hasmtlib/Example/Array.hs b/src/Language/Hasmtlib/Example/Array.hs
index 1ea1f3a..30ad028 100644
--- a/src/Language/Hasmtlib/Example/Array.hs
+++ b/src/Language/Hasmtlib/Example/Array.hs
@@ -4,7 +4,7 @@ import Language.Hasmtlib
 
 main :: IO ()
 main = do
-  res <- solveWith (solver cvc5) $ do
+  res <- solveWith (solver @SMT cvc5) $ do
     setLogic "QF_AUFLIA"
 
     x <- var @(ArraySort IntSort BoolSort)
diff --git a/src/Language/Hasmtlib/Example/Bitvector.hs b/src/Language/Hasmtlib/Example/Bitvector.hs
index b134fae..ca39395 100644
--- a/src/Language/Hasmtlib/Example/Bitvector.hs
+++ b/src/Language/Hasmtlib/Example/Bitvector.hs
@@ -4,7 +4,7 @@ import Language.Hasmtlib
 
 main :: IO ()
 main = do
-  res <- solveWith (debug yices) $ do
+  res <- solveWith (debug @SMT yices) $ do
     setLogic "QF_BV"
 
     xbv8 <- variable
diff --git a/src/Language/Hasmtlib/Example/Codec.hs b/src/Language/Hasmtlib/Example/Codec.hs
index 9ffe353..98fdfbf 100644
--- a/src/Language/Hasmtlib/Example/Codec.hs
+++ b/src/Language/Hasmtlib/Example/Codec.hs
@@ -9,17 +9,17 @@ instance Applicative Foo where
   pure x = Foo x x
   (Foo f g) <*> (Foo x y) = Foo (f x) (g y)
 
-instance Equatable a => Equatable (Foo a) 
+instance Equatable a => Equatable (Foo a)
 -- Leverage Functor, Foldable, Traversable and Applicative and get default instances
 instance Codec a => Codec (Foo a)
 instance Variable a => Variable (Foo a)
 
 main :: IO ()
 main = do
-  res <- solveWith (solver z3) $ do
+  res <- solveWith (solver @SMT z3) $ do
     setLogic "ALL"
 
--- These do all the same:    
+-- These do all the same:
     let (c1,c2) :: (Expr IntSort, Expr RealSort) = (5, 10)
 --  let (c1,c2) :: (Expr IntSort, Expr RealSort) = encode (5, 10)
 --  let (c1,c2) :: (Expr IntSort, Expr RealSort) = (constant 5, constant 10)
diff --git a/src/Language/Hasmtlib/Example/Counting.hs b/src/Language/Hasmtlib/Example/Counting.hs
index 18c9575..7df0475 100644
--- a/src/Language/Hasmtlib/Example/Counting.hs
+++ b/src/Language/Hasmtlib/Example/Counting.hs
@@ -5,7 +5,7 @@ import Control.Monad
 
 main :: IO ()
 main = do
-  res <- solveWith (solver cvc5) $ do
+  res <- solveWith (solver @SMT cvc5) $ do
     setLogic "QF_LIA"
 
     xs <- replicateM 10 $ var @BoolSort
diff --git a/src/Language/Hasmtlib/Example/Optimization.hs b/src/Language/Hasmtlib/Example/IncrementalOptimization.hs
similarity index 85%
rename from src/Language/Hasmtlib/Example/Optimization.hs
rename to src/Language/Hasmtlib/Example/IncrementalOptimization.hs
index aec833c..0539431 100644
--- a/src/Language/Hasmtlib/Example/Optimization.hs
+++ b/src/Language/Hasmtlib/Example/IncrementalOptimization.hs
@@ -1,4 +1,4 @@
-module Language.Hasmtlib.Example.Bitvector where
+module Language.Hasmtlib.Example.IncrementalOptimization where
 
 import Language.Hasmtlib
 import Control.Monad.IO.Class
diff --git a/src/Language/Hasmtlib/Example/McCarthyArrayAxioms.hs b/src/Language/Hasmtlib/Example/McCarthyArrayAxioms.hs
index 6d8ebbb..990a7b4 100644
--- a/src/Language/Hasmtlib/Example/McCarthyArrayAxioms.hs
+++ b/src/Language/Hasmtlib/Example/McCarthyArrayAxioms.hs
@@ -6,15 +6,15 @@ import Language.Hasmtlib
 
 main :: IO ()
 main = do
-  res <- solveWith (solver cvc5) $ do
+  res <- solveWith (solver @SMT cvc5) $ do
     setLogic "AUFLIRA"
 
     assert $
       for_all @(ArraySort RealSort RealSort) \arr ->
          for_all \i ->
             for_all \x ->
-               select (store arr i x) i === x 
-    
+               select (store arr i x) i === x
+
     assert $
       for_all @(ArraySort IntSort BoolSort) \arr ->
          for_all \i ->
diff --git a/src/Language/Hasmtlib/Example/Monad.hs b/src/Language/Hasmtlib/Example/Monad.hs
index e889bf9..f1ba198 100644
--- a/src/Language/Hasmtlib/Example/Monad.hs
+++ b/src/Language/Hasmtlib/Example/Monad.hs
@@ -5,13 +5,13 @@ import Control.Monad
 
 main :: IO ()
 main = do
-  res <- solveWith (solver cvc5) $ do
+  res <- solveWith (solver @SMT cvc5) $ do
     setLogic "QF_LIA"
 
     xs <- replicateM 100 $ var @IntSort
 
     forM_ (zip xs [1 :: Integer .. ]) $ \(x, i) -> assert $ x === fromInteger i
-  
+
     return xs
 
   case res of
diff --git a/src/Language/Hasmtlib/Example/OMTOptimization.hs b/src/Language/Hasmtlib/Example/OMTOptimization.hs
new file mode 100644
index 0000000..8106466
--- /dev/null
+++ b/src/Language/Hasmtlib/Example/OMTOptimization.hs
@@ -0,0 +1,20 @@
+module Language.Hasmtlib.Example.IncrementalOptimization where
+
+import Language.Hasmtlib
+
+main :: IO ()
+main = do
+  res <- solveWith (solver @OMT z3) $ do
+    setOption $ ProduceModels True
+    setLogic "QF_LIA"
+
+    x <- var @IntSort
+
+    assert $ x >? -2
+    assertSoftWeighted (x >? -1) 5.0
+
+    minimize x
+
+    return x
+
+  print res
diff --git a/src/Language/Hasmtlib/Example/Quantifier.hs b/src/Language/Hasmtlib/Example/Quantifier.hs
index fb0c7fb..8a262bd 100644
--- a/src/Language/Hasmtlib/Example/Quantifier.hs
+++ b/src/Language/Hasmtlib/Example/Quantifier.hs
@@ -5,7 +5,7 @@ import Language.Hasmtlib
 
 main :: IO ()
 main = do
-  res <- solveWith (debug cvc5) $ do
+  res <- solveWith (debug @SMT cvc5) $ do
     setLogic "BV"
 
     z <- var @(BvSort 8)
@@ -19,4 +19,4 @@ main = do
 
     return ()
 
-  print res
\ No newline at end of file
+  print res
diff --git a/src/Language/Hasmtlib/Example/Transcendental.hs b/src/Language/Hasmtlib/Example/Transcendental.hs
index e071d07..b98dcb8 100644
--- a/src/Language/Hasmtlib/Example/Transcendental.hs
+++ b/src/Language/Hasmtlib/Example/Transcendental.hs
@@ -4,13 +4,13 @@ import Language.Hasmtlib
 
 main :: IO ()
 main = do
-  res <- solveWith (solver cvc5) $ do
+  res <- solveWith (solver @SMT cvc5) $ do
     setLogic "ALL"
 
     x <- var @RealSort
 
     assert $ x >? sin 3
-  
+
     return x
 
   print res
diff --git a/src/Language/Hasmtlib/Solver/Common.hs b/src/Language/Hasmtlib/Solver/Common.hs
index d7d1fe6..c35ce98 100644
--- a/src/Language/Hasmtlib/Solver/Common.hs
+++ b/src/Language/Hasmtlib/Solver/Common.hs
@@ -1,6 +1,7 @@
 module Language.Hasmtlib.Solver.Common where
 
 import Language.Hasmtlib.Type.SMT
+import Language.Hasmtlib.Type.OMT
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Internal.Render
 import Language.Hasmtlib.Internal.Parser
@@ -20,11 +21,11 @@ import qualified SMTLIB.Backends as B
 newtype ProcessSolver = ProcessSolver { conf :: P.Config }
 
 -- | Creates a 'Solver' from a 'ProcessSolver'
-solver :: MonadIO m => ProcessSolver -> Solver SMT m
+solver :: (RenderSeq s, MonadIO m) => ProcessSolver -> Solver s m
 solver (ProcessSolver cfg) = processSolver cfg Nothing
 
 -- | Creates a debugging 'Solver' from a 'ProcessSolver'
-debug :: MonadIO m => ProcessSolver -> Solver SMT m
+debug :: (RenderSeq s, Default (Debugger s), MonadIO m) => ProcessSolver -> Solver s m
 debug (ProcessSolver cfg) = processSolver cfg $ Just def
 
 -- | Creates an interactive session with a solver by creating and returning an alive process-handle 'P.Handle'.
@@ -33,19 +34,31 @@ interactiveSolver (ProcessSolver cfg) = liftIO $ do
   handle  <- P.new cfg
   liftM2 (,) (B.initSolver B.Queuing $ P.toBackend handle) (return handle)
 
--- | A type holding actions to execute for debugging 'SMT' solving.
-data Debugger = Debugger
-  { debugSMT            :: SMT -> IO ()
+-- | A type holding actions for debugging states.
+data Debugger s = Debugger
+  { debugState          :: s -> IO ()
   , debugProblem        :: Seq Builder -> IO ()
   , debugResultResponse :: ByteString -> IO ()
   , debugModelResponse  :: ByteString -> IO ()
   }
 
-instance Default Debugger where
+instance Default (Debugger SMT) where
   def = Debugger
-    { debugSMT            = \smt -> liftIO $ do
-        putStrLn $ "Vars: "       ++ show (Seq.length (smt^.vars))
-        putStrLn $ "Assertions: " ++ show (Seq.length (smt^.formulas))
+    { debugState            = \s -> liftIO $ do
+        putStrLn $ "Vars: "       ++ show (Seq.length (s^.vars))
+        putStrLn $ "Assertions: " ++ show (Seq.length (s^.formulas))
+    , debugProblem        = liftIO . mapM_ (putStrLn . toString . toLazyByteString)
+    , debugResultResponse = liftIO . putStrLn . (\s -> "\n" ++ s ++ "\n") . toString
+    , debugModelResponse  = liftIO . mapM_ (putStrLn . toString) . split 13
+    }
+
+instance Default (Debugger OMT) where
+  def = Debugger
+    { debugState          = \omt -> liftIO $ do
+        putStrLn $ "Vars: "                 ++ show (Seq.length (omt^.smt.vars))
+        putStrLn $ "Hard assertions: "      ++ show (Seq.length (omt^.smt.formulas))
+        putStrLn $ "Soft assertions: "      ++ show (Seq.length (omt^.softFormulas))
+        putStrLn $ "Optimization targets: " ++ show (Seq.length (omt^.targetMinimize) + Seq.length (omt^.targetMaximize))
     , debugProblem        = liftIO . mapM_ (putStrLn . toString . toLazyByteString)
     , debugResultResponse = liftIO . putStrLn . (\s -> "\n" ++ s ++ "\n") . toString
     , debugModelResponse  = liftIO . mapM_ (putStrLn . toString) . split 13
@@ -64,13 +77,13 @@ instance Default Debugger where
 --
 -- 5. close the process and clean up all resources.
 --
-processSolver :: MonadIO m => P.Config -> Maybe Debugger -> Solver SMT m
-processSolver cfg debugger smt = do
+processSolver :: (RenderSeq s, MonadIO m) => P.Config -> Maybe (Debugger s) -> Solver s m
+processSolver cfg debugger s = do
   liftIO $ P.with cfg $ \handle -> do
-    maybe mempty (`debugSMT` smt) debugger
+    maybe mempty (`debugState` s) debugger
     pSolver <- B.initSolver B.Queuing $ P.toBackend handle
 
-    let problem = renderSeq smt
+    let problem = renderSeq s
     maybe mempty (`debugProblem` problem) debugger
 
     forM_ problem (B.command_ pSolver)
diff --git a/src/Language/Hasmtlib/Type/MonadSMT.hs b/src/Language/Hasmtlib/Type/MonadSMT.hs
index 72565f8..bfc5e83 100644
--- a/src/Language/Hasmtlib/Type/MonadSMT.hs
+++ b/src/Language/Hasmtlib/Type/MonadSMT.hs
@@ -156,6 +156,7 @@ solve :: (MonadIncrSMT s m, MonadIO m) => m (Result, Solution)
 solve = liftM2 (,) checkSat getModel
 
 -- | A 'MonadState' that holds an OMT-Problem.
+--   An OMT-Problem is a 'SMT-Problem' with additional optimization targets.
 class MonadSMT s m => MonadOMT s m where
   -- | Minimizes a numerical expression within the OMT-Problem.
   --
diff --git a/src/Language/Hasmtlib/Type/OMT.hs b/src/Language/Hasmtlib/Type/OMT.hs
index 33abe66..c0a9891 100644
--- a/src/Language/Hasmtlib/Type/OMT.hs
+++ b/src/Language/Hasmtlib/Type/OMT.hs
@@ -68,6 +68,11 @@ instance MonadState OMT m => MonadSMT OMT m where
 
   setLogic l = smt.mlogic ?= l
 
+instance MonadSMT OMT m => MonadOMT OMT m where
+  minimize expr = targetMinimize %= (|> SomeSMTSort (Minimize expr))
+  maximize expr = targetMaximize %= (|> SomeSMTSort (Maximize expr))
+  assertSoft expr w gid = softFormulas %= (|> SoftFormula expr w gid)
+
 instance Render SoftFormula where
   render sf = "(assert-soft " <> render (sf^.formula) <> " :weight " <> maybe "1" render (sf^.mWeight) <> renderGroupId (sf^.mGroupId) <> ")"
     where

From 460ad8b02d5e5dbc0124a9345b4b8fc28f48ae6e Mon Sep 17 00:00:00 2001
From: bruderj15 <julian.bruder@outlook.com>
Date: Tue, 23 Jul 2024 12:04:33 +0200
Subject: [PATCH 14/19] api-extension: updated README

---
 README.md                                     | 26 ++++++++++++-------
 .../Hasmtlib/Example/OMTOptimization.hs       |  1 -
 2 files changed, 16 insertions(+), 11 deletions(-)

diff --git a/README.md b/README.md
index 01b8628..83f743a 100644
--- a/README.md
+++ b/README.md
@@ -41,7 +41,7 @@ instance Variable a => Variable (V3 a)
 
 main :: IO ()
 main = do
-  res <- solveWith (solver cvc5) $ do
+  res <- solveWith (solver @SMT cvc5) $ do
     setLogic "QF_NRA"
 
     u :: V3 (Expr RealSort) <- variable
@@ -57,7 +57,6 @@ May print: `(Sat,Just (V3 (-2.0) (-1.0) 0.0,V3 (-2.0) (-1.0) 0.0))`
 
 ## Features
 
-### Supported
 - [x] SMTLib2-Sorts in the Haskell-Type
   ```haskell
     data SMTSort = BoolSort | IntSort | RealSort | BvSort Nat | ArraySort SMTSort SMTSort
@@ -72,7 +71,7 @@ May print: `(Sat,Just (V3 (-2.0) (-1.0) 0.0,V3 (-2.0) (-1.0) 0.0))`
   ```
 - [x] Pure API with Expression-instances for Num, Floating, Bounded, ...
   ```haskell
-    solveWith (solver yices) $ do
+    solveWith (solver @SMT yices) $ do
       setLogic "QF_BV"
       x <- var @(BvSort 16)
       y <- var
@@ -84,9 +83,9 @@ May print: `(Sat,Just (V3 (-2.0) (-1.0) 0.0,V3 (-2.0) (-1.0) 0.0))`
     -- | Function that turns a state (SMT) into a result and a solution
     type Solver s m = s -> m (Result, Solution)
   ```
-- [x] Solvers via external processes: CVC5, Z3, Yices2-SMT & MathSAT
+- [x] Solvers via external processes: CVC5, Z3, Yices2-SMT, MathSAT, OptiMathSAT & OpenSMT
   ```haskell
-    (result, solution) <- solveWith (solver mathsat) $ do
+    (result, solution) <- solveWith (solver @SMT mathsat) $ do
       setLogic "QF_LIA"
       assert $ ...
   ```
@@ -109,7 +108,7 @@ May print: `(Sat,Just (V3 (-2.0) (-1.0) 0.0,V3 (-2.0) (-1.0) 0.0))`
   ```
 - [x] Pure quantifiers `for_all` and `exists`
   ```haskell
-    solveWith (solver z3) $ do
+    solveWith (solver @SMT z3) $ do
       setLogic "LIA"
       z <- var @IntSort
       assert $ z === 0
@@ -119,11 +118,18 @@ May print: `(Sat,Just (V3 (-2.0) (-1.0) 0.0,V3 (-2.0) (-1.0) 0.0))`
               x + y === z
       return z
   ```
+- [x] Optimization Modulo Theories (OMT) / MaxSMT
+  ```haskell
+    res <- solveWith (solver @OMT z3) $ do
+      setLogic "QF_LIA"
+      x <- var @IntSort
 
-### Coming
-- [ ] Observable sharing & access to the expression-tree (useful for rewriting, ...)
-- [ ] (Maybe) signed BitVec with corresponding encoding on the type-level (unsigned, ones-complement, twos-complement)
-- [ ] ...
+      assert $ x >? -2
+      assertSoftWeighted (x >? -1) 5.0
+      minimize x
+
+      return x
+  ```
 
 ## Examples
 There are some examples in [here](https://github.com/bruderj15/Hasmtlib/tree/master/src/Language/Hasmtlib/Example).
diff --git a/src/Language/Hasmtlib/Example/OMTOptimization.hs b/src/Language/Hasmtlib/Example/OMTOptimization.hs
index 8106466..c65d0ad 100644
--- a/src/Language/Hasmtlib/Example/OMTOptimization.hs
+++ b/src/Language/Hasmtlib/Example/OMTOptimization.hs
@@ -5,7 +5,6 @@ import Language.Hasmtlib
 main :: IO ()
 main = do
   res <- solveWith (solver @OMT z3) $ do
-    setOption $ ProduceModels True
     setLogic "QF_LIA"
 
     x <- var @IntSort

From 895b86b8bd24ea4d7fee0718c1c2eee966c4eca8 Mon Sep 17 00:00:00 2001
From: bruderj15 <julian.bruder@outlook.com>
Date: Tue, 23 Jul 2024 12:14:03 +0200
Subject: [PATCH 15/19] api-extension: fix README

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 83f743a..cfb28d5 100644
--- a/README.md
+++ b/README.md
@@ -80,7 +80,7 @@ May print: `(Sat,Just (V3 (-2.0) (-1.0) 0.0,V3 (-2.0) (-1.0) 0.0))`
   ```
 - [x] Add your own solvers via the [Solver type](https://github.com/bruderj15/Hasmtlib/blob/master/src/Language/Hasmtlib/Type/Solution.hs)
   ```haskell
-    -- | Function that turns a state (SMT) into a result and a solution
+    -- | Function that turns a state (usually SMT or OMT) into a result and a solution
     type Solver s m = s -> m (Result, Solution)
   ```
 - [x] Solvers via external processes: CVC5, Z3, Yices2-SMT, MathSAT, OptiMathSAT & OpenSMT

From aee5469b87cd8d4f02f6f9382749d88791c15ec2 Mon Sep 17 00:00:00 2001
From: bruderj15 <julian.bruder@outlook.com>
Date: Tue, 23 Jul 2024 12:24:42 +0200
Subject: [PATCH 16/19] api-extension: moved added dedicated module for SMTSort

---
 hasmtlib.cabal                             |   1 +
 src/Language/Hasmtlib.hs                   |   2 +
 src/Language/Hasmtlib/Codec.hs             |   1 +
 src/Language/Hasmtlib/Counting.hs          |   1 +
 src/Language/Hasmtlib/Equatable.hs         |   1 +
 src/Language/Hasmtlib/Internal/Expr.hs     | 103 +------------------
 src/Language/Hasmtlib/Internal/Expr/Num.hs |   1 +
 src/Language/Hasmtlib/Internal/Parser.hs   |   6 +-
 src/Language/Hasmtlib/Iteable.hs           |  21 ++--
 src/Language/Hasmtlib/Orderable.hs         |  31 +++---
 src/Language/Hasmtlib/Type/Expr.hs         |   6 +-
 src/Language/Hasmtlib/Type/MonadSMT.hs     |   1 +
 src/Language/Hasmtlib/Type/OMT.hs          |   1 +
 src/Language/Hasmtlib/Type/Pipe.hs         |   1 +
 src/Language/Hasmtlib/Type/SMT.hs          |   1 +
 src/Language/Hasmtlib/Type/SMTSort.hs      | 111 +++++++++++++++++++++
 src/Language/Hasmtlib/Type/Solution.hs     |   7 +-
 src/Language/Hasmtlib/Type/Solver.hs       |   1 +
 src/Language/Hasmtlib/Variable.hs          |   5 +-
 19 files changed, 164 insertions(+), 138 deletions(-)
 create mode 100644 src/Language/Hasmtlib/Type/SMTSort.hs

diff --git a/hasmtlib.cabal b/hasmtlib.cabal
index d8c3b3b..e7b28da 100644
--- a/hasmtlib.cabal
+++ b/hasmtlib.cabal
@@ -48,6 +48,7 @@ library
                      , Language.Hasmtlib.Type.SMT
                      , Language.Hasmtlib.Type.OMT
                      , Language.Hasmtlib.Type.Pipe
+                     , Language.Hasmtlib.Type.SMTSort
                      , Language.Hasmtlib.Type.Solution
                      , Language.Hasmtlib.Type.Solver
                      , Language.Hasmtlib.Type.Option
diff --git a/src/Language/Hasmtlib.hs b/src/Language/Hasmtlib.hs
index 92b145a..36ae95c 100644
--- a/src/Language/Hasmtlib.hs
+++ b/src/Language/Hasmtlib.hs
@@ -7,6 +7,7 @@ module Language.Hasmtlib
   , module Language.Hasmtlib.Type.Expr
   , module Language.Hasmtlib.Type.Solver
   , module Language.Hasmtlib.Type.Option
+  , module Language.Hasmtlib.Type.SMTSort
   , module Language.Hasmtlib.Type.Solution
   , module Language.Hasmtlib.Type.ArrayMap
   , module Language.Hasmtlib.Integraled
@@ -33,6 +34,7 @@ import Language.Hasmtlib.Type.Pipe
 import Language.Hasmtlib.Type.Expr
 import Language.Hasmtlib.Type.Solver
 import Language.Hasmtlib.Type.Option
+import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Type.ArrayMap
 import Language.Hasmtlib.Integraled
diff --git a/src/Language/Hasmtlib/Codec.hs b/src/Language/Hasmtlib/Codec.hs
index 1eca65a..64201ed 100644
--- a/src/Language/Hasmtlib/Codec.hs
+++ b/src/Language/Hasmtlib/Codec.hs
@@ -10,6 +10,7 @@ import Language.Hasmtlib.Internal.Bitvec
 import Language.Hasmtlib.Internal.Expr
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Type.ArrayMap
+import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Boolean
 import Data.Kind
 import Data.Coerce
diff --git a/src/Language/Hasmtlib/Counting.hs b/src/Language/Hasmtlib/Counting.hs
index 8c4c19c..3a7746e 100644
--- a/src/Language/Hasmtlib/Counting.hs
+++ b/src/Language/Hasmtlib/Counting.hs
@@ -3,6 +3,7 @@ module Language.Hasmtlib.Counting where
 import Prelude hiding (not, (&&), (||), or)
 import Language.Hasmtlib.Internal.Expr.Num ()
 import Language.Hasmtlib.Internal.Expr
+import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Equatable
 import Language.Hasmtlib.Orderable
 import Language.Hasmtlib.Iteable
diff --git a/src/Language/Hasmtlib/Equatable.hs b/src/Language/Hasmtlib/Equatable.hs
index 7c95039..37295c8 100644
--- a/src/Language/Hasmtlib/Equatable.hs
+++ b/src/Language/Hasmtlib/Equatable.hs
@@ -6,6 +6,7 @@ module Language.Hasmtlib.Equatable where
 
 import Prelude hiding (not, (&&))
 import Language.Hasmtlib.Internal.Expr
+import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Boolean
 import Data.Int
 import Data.Word
diff --git a/src/Language/Hasmtlib/Internal/Expr.hs b/src/Language/Hasmtlib/Internal/Expr.hs
index 3f3b57b..7d9e6a6 100644
--- a/src/Language/Hasmtlib/Internal/Expr.hs
+++ b/src/Language/Hasmtlib/Internal/Expr.hs
@@ -1,19 +1,15 @@
-{-# LANGUAGE TypeFamilyDependencies #-}
-{-# LANGUAGE NoStarIsType #-}
 {-# LANGUAGE RoleAnnotations #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 module Language.Hasmtlib.Internal.Expr where
 
-import Language.Hasmtlib.Internal.Bitvec
 import Language.Hasmtlib.Internal.Render
 import Language.Hasmtlib.Type.ArrayMap
+import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Boolean
-import Data.GADT.Compare
 import Data.Map hiding (toList)
 import Data.List (intercalate)
-import Data.Kind
 import Data.Proxy
 import Data.Coerce
 import Data.Foldable (toList)
@@ -22,27 +18,11 @@ import qualified Data.Vector.Sized as V
 import Control.Lens
 import GHC.TypeLits
 
--- | Sorts in SMTLib2 - used as promoted type (data-kind).
-data SMTSort =
-    BoolSort                      -- ^ Sort of Bool
-  | IntSort                       -- ^ Sort of Int
-  | RealSort                      -- ^ Sort of Real
-  | BvSort Nat                    -- ^ Sort of BitVec with length n
-  | ArraySort SMTSort SMTSort     -- ^ Sort of Array with indices k and values v
-
 -- | An internal SMT variable with a phantom-type which holds an 'Int' as it's identifier.
 type role SMTVar phantom
 newtype SMTVar (t :: SMTSort) = SMTVar { _varId :: Int } deriving (Show, Eq, Ord)
 $(makeLenses ''SMTVar)
 
--- | Injective type-family that computes the Haskell 'Type' of an 'SMTSort'.
-type family HaskellType (t :: SMTSort) = (r :: Type) | r -> t where
-  HaskellType IntSort         = Integer
-  HaskellType RealSort        = Double
-  HaskellType BoolSort        = Bool
-  HaskellType (BvSort n)      = Bitvec n
-  HaskellType (ArraySort k v) = ConstArray (HaskellType k) (HaskellType v)
-
 -- | A wrapper for values of 'SMTSort's.
 data Value (t :: SMTSort) where
   IntValue   :: HaskellType IntSort    -> Value IntSort
@@ -70,79 +50,6 @@ wrapValue = case sortSing @t of
   SArraySort _ _ -> ArrayValue
 {-# INLINEABLE wrapValue #-}
 
--- | Singleton for 'SMTSort'.
-data SSMTSort (t :: SMTSort) where
-  SIntSort   :: SSMTSort IntSort
-  SRealSort  :: SSMTSort RealSort
-  SBoolSort  :: SSMTSort BoolSort
-  SBvSort    :: KnownNat n => Proxy n -> SSMTSort (BvSort n)
-  SArraySort :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Proxy k -> Proxy v -> SSMTSort (ArraySort k v)
-
-deriving instance Show (SSMTSort t)
-deriving instance Eq   (SSMTSort t)
-deriving instance Ord  (SSMTSort t)
-
-instance GEq SSMTSort where
-  geq SIntSort SIntSort       = Just Refl
-  geq SRealSort SRealSort     = Just Refl
-  geq SBoolSort SBoolSort     = Just Refl
-  geq (SBvSort n) (SBvSort m) = case sameNat n m of
-    Just Refl -> Just Refl
-    Nothing   -> Nothing
-  geq _ _                     = Nothing
-
-instance GCompare SSMTSort where
-  gcompare SBoolSort SBoolSort     = GEQ
-  gcompare SIntSort SIntSort       = GEQ
-  gcompare SRealSort SRealSort     = GEQ
-  gcompare (SBvSort n) (SBvSort m) = case cmpNat n m of
-    LTI -> GLT
-    EQI -> GEQ
-    GTI -> GGT
-  gcompare (SArraySort k v) (SArraySort k' v') = case gcompare (sortSing' k) (sortSing' k') of
-    GLT -> GLT
-    GEQ -> case gcompare (sortSing' v) (sortSing' v') of
-      GLT -> GLT
-      GEQ -> GEQ
-      GGT -> GGT
-    GGT -> GGT
-  gcompare SBoolSort _        = GLT
-  gcompare _ SBoolSort        = GGT
-  gcompare SIntSort _         = GLT
-  gcompare _ SIntSort         = GGT
-  gcompare SRealSort _        = GLT
-  gcompare _ SRealSort        = GGT
-  gcompare (SArraySort _ _) _ = GLT
-  gcompare _ (SArraySort _ _) = GGT
-
--- | Compute singleton 'SSMTSort' from it's promoted type 'SMTSort'.
-class    KnownSMTSort (t :: SMTSort)           where sortSing :: SSMTSort t
-instance KnownSMTSort IntSort                  where sortSing = SIntSort
-instance KnownSMTSort RealSort                 where sortSing = SRealSort
-instance KnownSMTSort BoolSort                 where sortSing = SBoolSort
-instance KnownNat n => KnownSMTSort (BvSort n) where sortSing = SBvSort (Proxy @n)
-instance (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => KnownSMTSort (ArraySort k v) where
-   sortSing = SArraySort (Proxy @k) (Proxy @v)
-
--- | Wrapper for 'sortSing' which takes a 'Proxy'
-sortSing' :: forall prxy t. KnownSMTSort t => prxy t -> SSMTSort t
-sortSing' _ = sortSing @t
-
--- | AllC ensures that a list of constraints is applied to a poly-kinded 'Type' k
---
--- @
--- AllC '[]       k = ()
--- AllC (c ': cs) k = (c k, AllC cs k)
--- @
-type AllC :: [k -> Constraint] -> k -> Constraint
-type family AllC cs k :: Constraint where
-  AllC '[]       k = ()
-  AllC (c ': cs) k = (c k, AllC cs k)
-
--- | An existential wrapper that hides some 'SMTSort' and a list of 'Constraint's holding for it.
-data SomeSMTSort cs f where
-  SomeSMTSort :: forall cs f (t :: SMTSort). AllC cs t => f t -> SomeSMTSort cs f
-
 -- | An existential wrapper that hides some known 'SMTSort'.
 type SomeKnownSMTSort f = SomeSMTSort '[KnownSMTSort] f
 
@@ -251,14 +158,6 @@ instance KnownNat n => Bounded (Expr (BvSort n)) where
   minBound = Constant $ BvValue minBound
   maxBound = Constant $ BvValue maxBound
 
-instance Render (SSMTSort t) where
-  render SBoolSort   = "Bool"
-  render SIntSort    = "Int"
-  render SRealSort   = "Real"
-  render (SBvSort p) = renderBinary "_" ("BitVec" :: Builder) (natVal p)
-  render (SArraySort k v) = renderBinary "Array" (sortSing' k) (sortSing' v)
-  {-# INLINEABLE render #-}
-
 instance Render (SMTVar t) where
   render v = "var_" <> intDec (coerce @(SMTVar t) @Int v)
   {-# INLINEABLE render #-}
diff --git a/src/Language/Hasmtlib/Internal/Expr/Num.hs b/src/Language/Hasmtlib/Internal/Expr/Num.hs
index 7617b73..871f454 100644
--- a/src/Language/Hasmtlib/Internal/Expr/Num.hs
+++ b/src/Language/Hasmtlib/Internal/Expr/Num.hs
@@ -3,6 +3,7 @@ module Language.Hasmtlib.Internal.Expr.Num where
 import Prelude hiding (div, mod, quotRem, rem, quot, divMod)
 import Language.Hasmtlib.Internal.Expr
 import Language.Hasmtlib.Integraled
+import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Iteable
 import Language.Hasmtlib.Equatable
 import Language.Hasmtlib.Orderable
diff --git a/src/Language/Hasmtlib/Internal/Parser.hs b/src/Language/Hasmtlib/Internal/Parser.hs
index a8bbe79..bd7b2f5 100644
--- a/src/Language/Hasmtlib/Internal/Parser.hs
+++ b/src/Language/Hasmtlib/Internal/Parser.hs
@@ -6,12 +6,14 @@ module Language.Hasmtlib.Internal.Parser where
 import Prelude hiding (not, (&&), (||), and , or)
 import Language.Hasmtlib.Internal.Bitvec
 import Language.Hasmtlib.Internal.Render
+import Language.Hasmtlib.Internal.Expr.Num ()
 import Language.Hasmtlib.Internal.Expr
 import Language.Hasmtlib.Equatable
 import Language.Hasmtlib.Orderable
 import Language.Hasmtlib.Boolean
 import Language.Hasmtlib.Iteable
 import Language.Hasmtlib.Codec
+import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Type.ArrayMap
 import Data.Bit
@@ -339,7 +341,7 @@ parseToRealDouble = do
   _   <- char '(' >> skipSpace >> string "to_real" >> skipSpace
   dec <- anyValue decimal
   _   <- skipSpace >> char ')'
-  
+
   return $ fromInteger dec
 {-# INLINEABLE parseToRealDouble #-}
 
@@ -357,4 +359,4 @@ getValueParser v = do
   case decode mempty expr of
     Nothing    -> fail $ "Solver reponded with solution for var_" ++ show (v^.varId) ++ " but it contains "
                       ++ "another var. This cannot be parsed and evaluated currently."
-    Just value -> return $ SMTVarSol v (wrapValue value)
\ No newline at end of file
+    Just value -> return $ SMTVarSol v (wrapValue value)
diff --git a/src/Language/Hasmtlib/Iteable.hs b/src/Language/Hasmtlib/Iteable.hs
index 5001e4f..a040efc 100644
--- a/src/Language/Hasmtlib/Iteable.hs
+++ b/src/Language/Hasmtlib/Iteable.hs
@@ -3,15 +3,16 @@
 module Language.Hasmtlib.Iteable where
 
 import Language.Hasmtlib.Internal.Expr
+import Language.Hasmtlib.Type.SMTSort
 import Data.Sequence (Seq)
 import Data.Tree
-  
+
 -- | If condition (p :: b) then (t :: a) else (f :: a)
---   
+--
 --    >>> ite true "1" "2"
 --        "1"
 --    >>> ite false 100 42
---        42 
+--        42
 class Iteable b a where
   ite :: b -> a -> a -> a
   default ite :: (Iteable b c, Applicative f, f c ~ a) => b -> a -> a -> a
@@ -38,18 +39,18 @@ instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b) => Iteable (Expr
 
 instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c) => Iteable (Expr BoolSort) (a,b,c) where
   ite p (a,b,c) (a',b',c') = (ite p a a', ite p b b', ite p c c')
-  
+
 instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d) => Iteable (Expr BoolSort) (a,b,c,d) where
   ite p (a,b,c,d) (a',b',c',d') = (ite p a a', ite p b b', ite p c c', ite p d d')
-  
+
 instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d, Iteable (Expr BoolSort) e) => Iteable (Expr BoolSort) (a,b,c,d,e) where
   ite p (a,b,c,d,e) (a',b',c',d',e') = (ite p a a', ite p b b', ite p c c', ite p d d', ite p e e')
-  
+
 instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d, Iteable (Expr BoolSort) e, Iteable (Expr BoolSort) f) => Iteable (Expr BoolSort) (a,b,c,d,e,f) where
   ite p (a,b,c,d,e,f) (a',b',c',d',e',f') = (ite p a a', ite p b b', ite p c c', ite p d d', ite p e e', ite p f f')
-  
+
 instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d, Iteable (Expr BoolSort) e, Iteable (Expr BoolSort) f, Iteable (Expr BoolSort) g) => Iteable (Expr BoolSort) (a,b,c,d,e,f,g) where
-  ite p (a,b,c,d,e,f,g) (a',b',c',d',e',f',g') = (ite p a a', ite p b b', ite p c c', ite p d d', ite p e e', ite p f f', ite p g g')  
-  
+  ite p (a,b,c,d,e,f,g) (a',b',c',d',e',f',g') = (ite p a a', ite p b b', ite p c c', ite p d d', ite p e e', ite p f f', ite p g g')
+
 instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d, Iteable (Expr BoolSort) e, Iteable (Expr BoolSort) f, Iteable (Expr BoolSort) g, Iteable (Expr BoolSort) h) => Iteable (Expr BoolSort) (a,b,c,d,e,f,g,h) where
-  ite p (a,b,c,d,e,f,g,h) (a',b',c',d',e',f',g',h') = (ite p a a', ite p b b', ite p c c', ite p d d', ite p e e', ite p f f', ite p g g', ite p h h')
\ No newline at end of file
+  ite p (a,b,c,d,e,f,g,h) (a',b',c',d',e',f',g',h') = (ite p a a', ite p b b', ite p c c', ite p d d', ite p e e', ite p f f', ite p g g', ite p h h')
diff --git a/src/Language/Hasmtlib/Orderable.hs b/src/Language/Hasmtlib/Orderable.hs
index df66064..06288f3 100644
--- a/src/Language/Hasmtlib/Orderable.hs
+++ b/src/Language/Hasmtlib/Orderable.hs
@@ -6,6 +6,7 @@ module Language.Hasmtlib.Orderable where
 
 import Prelude hiding (not, (&&), (||))
 import Language.Hasmtlib.Internal.Expr
+import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Equatable
 import Language.Hasmtlib.Iteable
 import Language.Hasmtlib.Boolean
@@ -17,14 +18,14 @@ import GHC.Generics
 import GHC.TypeNats
 
 -- | Compare two as as SMT-Expression.
--- 
+--
 -- @
 -- x <- var @RealSort
--- y <- var 
+-- y <- var
 -- assert $ x >? y
 -- assert $ x === min' 42 100
 -- @
--- 
+--
 class Equatable a => Orderable a where
   (<=?) :: a -> a -> Expr BoolSort
   default (<=?) :: (Generic a, GOrderable (Rep a)) => a -> a -> Expr BoolSort
@@ -32,7 +33,7 @@ class Equatable a => Orderable a where
 
   (>=?) :: a -> a -> Expr BoolSort
   x >=? y = y <=? x
-  
+
   (<?)  :: a -> a -> Expr BoolSort
   x <? y = not $ y <=? x
 
@@ -51,34 +52,34 @@ max' x y = ite (y <=? x) x y
 
 instance Orderable (Expr IntSort) where
   (<?)     = LTH
-  {-# INLINE (<?) #-}  
+  {-# INLINE (<?) #-}
   (<=?)    = LTHE
-  {-# INLINE (<=?) #-}  
+  {-# INLINE (<=?) #-}
   (>=?)    = GTHE
-  {-# INLINE (>=?) #-}  
+  {-# INLINE (>=?) #-}
   (>?)     = GTH
   {-# INLINE (>?) #-}
 
 instance Orderable (Expr RealSort) where
   (<?)     = LTH
-  {-# INLINE (<?) #-}  
+  {-# INLINE (<?) #-}
   (<=?)    = LTHE
-  {-# INLINE (<=?) #-}  
+  {-# INLINE (<=?) #-}
   (>=?)    = GTHE
-  {-# INLINE (>=?) #-}  
+  {-# INLINE (>=?) #-}
   (>?)     = GTH
   {-# INLINE (>?) #-}
 
 instance KnownNat n => Orderable (Expr (BvSort n)) where
   (<?)     = BvuLT
-  {-# INLINE (<?) #-}  
+  {-# INLINE (<?) #-}
   (<=?)    = BvuLTHE
-  {-# INLINE (<=?) #-}  
+  {-# INLINE (<=?) #-}
   (>=?)    = BvuGTHE
-  {-# INLINE (>=?) #-}  
+  {-# INLINE (>=?) #-}
   (>?)     = BvuGT
   {-# INLINE (>?) #-}
-  
+
 class GEquatable f => GOrderable f where
   (<?#)  :: f a -> f a -> Expr BoolSort
   (<=?#) :: f a -> f a -> Expr BoolSort
@@ -153,4 +154,4 @@ instance Orderable Double   where x <?  y = bool (x <  y)
 instance Orderable Ordering where x <?  y = bool (x <  y)
                                   x <=? y = bool (x <= y)
 instance Orderable Bool     where x <?  y = bool (x <  y)
-                                  x <=? y = bool (x <= y)
\ No newline at end of file
+                                  x <=? y = bool (x <= y)
diff --git a/src/Language/Hasmtlib/Type/Expr.hs b/src/Language/Hasmtlib/Type/Expr.hs
index d2f20fd..3185990 100644
--- a/src/Language/Hasmtlib/Type/Expr.hs
+++ b/src/Language/Hasmtlib/Type/Expr.hs
@@ -2,11 +2,8 @@
 {-# LANGUAGE ViewPatterns #-}
 
 module Language.Hasmtlib.Type.Expr
- ( SMTSort(..)
- , SMTVar(..), varId
- , HaskellType
+ ( SMTVar(..), varId
  , Value(..), unwrapValue, wrapValue
- , SSMTSort(..), KnownSMTSort(..), sortSing', SomeSMTSort(..), SomeKnownSMTSort, AllC
  , Expr
  , equal, distinct
  , bvShL, bvLShR, bvConcat, bvRotL, bvRotR
@@ -18,6 +15,7 @@ where
 
 import Language.Hasmtlib.Internal.Expr
 import Language.Hasmtlib.Internal.Expr.Num ()
+import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Boolean
 import Data.Proxy
 import Data.List (genericLength)
diff --git a/src/Language/Hasmtlib/Type/MonadSMT.hs b/src/Language/Hasmtlib/Type/MonadSMT.hs
index bfc5e83..53d4a6f 100644
--- a/src/Language/Hasmtlib/Type/MonadSMT.hs
+++ b/src/Language/Hasmtlib/Type/MonadSMT.hs
@@ -4,6 +4,7 @@ module Language.Hasmtlib.Type.MonadSMT where
 
 import Language.Hasmtlib.Internal.Expr
 import Language.Hasmtlib.Type.Option
+import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Codec
 import Data.Proxy
diff --git a/src/Language/Hasmtlib/Type/OMT.hs b/src/Language/Hasmtlib/Type/OMT.hs
index c0a9891..c5b39dc 100644
--- a/src/Language/Hasmtlib/Type/OMT.hs
+++ b/src/Language/Hasmtlib/Type/OMT.hs
@@ -7,6 +7,7 @@ module Language.Hasmtlib.Type.OMT where
 import Language.Hasmtlib.Internal.Expr
 import Language.Hasmtlib.Internal.Render
 import Language.Hasmtlib.Type.MonadSMT
+import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Option
 import Language.Hasmtlib.Type.SMT
 import Data.List (isPrefixOf)
diff --git a/src/Language/Hasmtlib/Type/Pipe.hs b/src/Language/Hasmtlib/Type/Pipe.hs
index f682ec6..1718e98 100644
--- a/src/Language/Hasmtlib/Type/Pipe.hs
+++ b/src/Language/Hasmtlib/Type/Pipe.hs
@@ -8,6 +8,7 @@ import Language.Hasmtlib.Type.OMT (SoftFormula(..), Minimize(..), Maximize(..))
 import Language.Hasmtlib.Type.MonadSMT
 import Language.Hasmtlib.Internal.Expr
 import Language.Hasmtlib.Internal.Render
+import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Codec
 import Language.Hasmtlib.Internal.Parser hiding (var, constant)
diff --git a/src/Language/Hasmtlib/Type/SMT.hs b/src/Language/Hasmtlib/Type/SMT.hs
index 7277107..2382adc 100644
--- a/src/Language/Hasmtlib/Type/SMT.hs
+++ b/src/Language/Hasmtlib/Type/SMT.hs
@@ -6,6 +6,7 @@ module Language.Hasmtlib.Type.SMT where
 import Language.Hasmtlib.Internal.Expr
 import Language.Hasmtlib.Internal.Render
 import Language.Hasmtlib.Type.MonadSMT
+import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Option
 import Data.List (isPrefixOf)
 import Data.Default
diff --git a/src/Language/Hasmtlib/Type/SMTSort.hs b/src/Language/Hasmtlib/Type/SMTSort.hs
new file mode 100644
index 0000000..2d7a9d7
--- /dev/null
+++ b/src/Language/Hasmtlib/Type/SMTSort.hs
@@ -0,0 +1,111 @@
+{-# LANGUAGE TypeFamilyDependencies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Language.Hasmtlib.Type.SMTSort where
+
+import Language.Hasmtlib.Internal.Bitvec
+import Language.Hasmtlib.Internal.Render
+import Language.Hasmtlib.Type.ArrayMap
+import Data.GADT.Compare
+import Data.Kind
+import Data.Proxy
+import Data.ByteString.Builder
+import Control.Lens
+import GHC.TypeLits
+
+-- | Sorts in SMTLib2 - used as promoted type (data-kind).
+data SMTSort =
+    BoolSort                      -- ^ Sort of Bool
+  | IntSort                       -- ^ Sort of Int
+  | RealSort                      -- ^ Sort of Real
+  | BvSort Nat                    -- ^ Sort of BitVec with length n
+  | ArraySort SMTSort SMTSort     -- ^ Sort of Array with indices k and values v
+
+-- | Injective type-family that computes the Haskell 'Type' of an 'SMTSort'.
+type family HaskellType (t :: SMTSort) = (r :: Type) | r -> t where
+  HaskellType IntSort         = Integer
+  HaskellType RealSort        = Double
+  HaskellType BoolSort        = Bool
+  HaskellType (BvSort n)      = Bitvec n
+  HaskellType (ArraySort k v) = ConstArray (HaskellType k) (HaskellType v)
+
+-- | Singleton for 'SMTSort'.
+data SSMTSort (t :: SMTSort) where
+  SIntSort   :: SSMTSort IntSort
+  SRealSort  :: SSMTSort RealSort
+  SBoolSort  :: SSMTSort BoolSort
+  SBvSort    :: KnownNat n => Proxy n -> SSMTSort (BvSort n)
+  SArraySort :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Proxy k -> Proxy v -> SSMTSort (ArraySort k v)
+
+deriving instance Show (SSMTSort t)
+deriving instance Eq   (SSMTSort t)
+deriving instance Ord  (SSMTSort t)
+
+instance GEq SSMTSort where
+  geq SIntSort SIntSort       = Just Refl
+  geq SRealSort SRealSort     = Just Refl
+  geq SBoolSort SBoolSort     = Just Refl
+  geq (SBvSort n) (SBvSort m) = case sameNat n m of
+    Just Refl -> Just Refl
+    Nothing   -> Nothing
+  geq _ _                     = Nothing
+
+instance GCompare SSMTSort where
+  gcompare SBoolSort SBoolSort     = GEQ
+  gcompare SIntSort SIntSort       = GEQ
+  gcompare SRealSort SRealSort     = GEQ
+  gcompare (SBvSort n) (SBvSort m) = case cmpNat n m of
+    LTI -> GLT
+    EQI -> GEQ
+    GTI -> GGT
+  gcompare (SArraySort k v) (SArraySort k' v') = case gcompare (sortSing' k) (sortSing' k') of
+    GLT -> GLT
+    GEQ -> case gcompare (sortSing' v) (sortSing' v') of
+      GLT -> GLT
+      GEQ -> GEQ
+      GGT -> GGT
+    GGT -> GGT
+  gcompare SBoolSort _        = GLT
+  gcompare _ SBoolSort        = GGT
+  gcompare SIntSort _         = GLT
+  gcompare _ SIntSort         = GGT
+  gcompare SRealSort _        = GLT
+  gcompare _ SRealSort        = GGT
+  gcompare (SArraySort _ _) _ = GLT
+  gcompare _ (SArraySort _ _) = GGT
+
+-- | Compute singleton 'SSMTSort' from it's promoted type 'SMTSort'.
+class    KnownSMTSort (t :: SMTSort)           where sortSing :: SSMTSort t
+instance KnownSMTSort IntSort                  where sortSing = SIntSort
+instance KnownSMTSort RealSort                 where sortSing = SRealSort
+instance KnownSMTSort BoolSort                 where sortSing = SBoolSort
+instance KnownNat n => KnownSMTSort (BvSort n) where sortSing = SBvSort (Proxy @n)
+instance (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => KnownSMTSort (ArraySort k v) where
+   sortSing = SArraySort (Proxy @k) (Proxy @v)
+
+-- | Wrapper for 'sortSing' which takes a 'Proxy'
+sortSing' :: forall prxy t. KnownSMTSort t => prxy t -> SSMTSort t
+sortSing' _ = sortSing @t
+
+-- | AllC ensures that a list of constraints is applied to a poly-kinded 'Type' k
+--
+-- @
+-- AllC '[]       k = ()
+-- AllC (c ': cs) k = (c k, AllC cs k)
+-- @
+type AllC :: [k -> Constraint] -> k -> Constraint
+type family AllC cs k :: Constraint where
+  AllC '[]       k = ()
+  AllC (c ': cs) k = (c k, AllC cs k)
+
+-- | An existential wrapper that hides some 'SMTSort' and a list of 'Constraint's holding for it.
+data SomeSMTSort cs f where
+  SomeSMTSort :: forall cs f (t :: SMTSort). AllC cs t => f t -> SomeSMTSort cs f
+
+instance Render (SSMTSort t) where
+  render SBoolSort   = "Bool"
+  render SIntSort    = "Int"
+  render SRealSort   = "Real"
+  render (SBvSort p) = renderBinary "_" ("BitVec" :: Builder) (natVal p)
+  render (SArraySort k v) = renderBinary "Array" (sortSing' k) (sortSing' v)
+  {-# INLINEABLE render #-}
diff --git a/src/Language/Hasmtlib/Type/Solution.hs b/src/Language/Hasmtlib/Type/Solution.hs
index 494a954..7c00529 100644
--- a/src/Language/Hasmtlib/Type/Solution.hs
+++ b/src/Language/Hasmtlib/Type/Solution.hs
@@ -5,7 +5,8 @@
 
 module Language.Hasmtlib.Type.Solution where
 
-import Language.Hasmtlib.Type.Expr
+import Language.Hasmtlib.Internal.Expr
+import Language.Hasmtlib.Type.SMTSort
 import Data.IntMap as IMap hiding (foldl)
 import Data.Dependent.Map as DMap
 import Data.Dependent.Map.Lens
@@ -36,7 +37,7 @@ $(makeLenses ''SMTVarSol)
 class Ord (HaskellType t) => OrdHaskellType t
 instance Ord (HaskellType t) => OrdHaskellType t
 
--- | An existential wrapper that hides some known 'SMTSort' with an 'Ord' 'HaskellType' 
+-- | An existential wrapper that hides some known 'SMTSort' with an 'Ord' 'HaskellType'
 type SomeKnownOrdSMTSort f = SomeSMTSort '[KnownSMTSort, OrdHaskellType] f
 
 -- | Create a 'Solution' from some 'SMTVarSol's.
@@ -49,4 +50,4 @@ fromSomeVarSols = foldl
         Just (IntValueMap im) -> Just $ IntValueMap $ IMap.insert (s^.solVar.varId) (s^.solVal) im
       )
   )
-  mempty
\ No newline at end of file
+  mempty
diff --git a/src/Language/Hasmtlib/Type/Solver.hs b/src/Language/Hasmtlib/Type/Solver.hs
index f1bddeb..07a1abf 100644
--- a/src/Language/Hasmtlib/Type/Solver.hs
+++ b/src/Language/Hasmtlib/Type/Solver.hs
@@ -8,6 +8,7 @@ where
 
 import Language.Hasmtlib.Type.MonadSMT
 import Language.Hasmtlib.Internal.Expr
+import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Type.Pipe
 import Language.Hasmtlib.Orderable
diff --git a/src/Language/Hasmtlib/Variable.hs b/src/Language/Hasmtlib/Variable.hs
index 0bbcbe5..6c5635a 100644
--- a/src/Language/Hasmtlib/Variable.hs
+++ b/src/Language/Hasmtlib/Variable.hs
@@ -4,13 +4,14 @@ module Language.Hasmtlib.Variable where
 
 import Language.Hasmtlib.Internal.Expr
 import Language.Hasmtlib.Type.MonadSMT
+import Language.Hasmtlib.Type.SMTSort
 import Data.Proxy
 
 -- | Construct a variable datum of a data-type by creating variables for all its fields.
--- 
+--
 -- @
 --    data V3 a = V3 a a a
---    instance Variable a => V3 a 
+--    instance Variable a => V3 a
 -- @
 --
 --    >>> varV3 <- variable @(V3 (Expr RealType)) ; varV3

From 40f080e4caea5ec2058cd73c6bb078d672c8438b Mon Sep 17 00:00:00 2001
From: bruderj15 <julian.bruder@outlook.com>
Date: Tue, 23 Jul 2024 12:32:04 +0200
Subject: [PATCH 17/19] api-extension: renamed arith-funs & added doc for them

---
 src/Language/Hasmtlib/Example/ArithFun.hs |  2 +-
 src/Language/Hasmtlib/Type/Expr.hs        | 17 ++++++++++-------
 2 files changed, 11 insertions(+), 8 deletions(-)

diff --git a/src/Language/Hasmtlib/Example/ArithFun.hs b/src/Language/Hasmtlib/Example/ArithFun.hs
index 49042e8..f92106e 100644
--- a/src/Language/Hasmtlib/Example/ArithFun.hs
+++ b/src/Language/Hasmtlib/Example/ArithFun.hs
@@ -12,7 +12,7 @@ main = do
     xs <- replicateM 10 $ var @RealSort
 
     forM_ xs $ \x -> assert $ x >=? 0 && x <? fromIntegral (length xs)
-    forM_ xs $ assert . isInt
+    forM_ xs $ assert . isIntSort
     assert $ distinct xs
 
     return xs
diff --git a/src/Language/Hasmtlib/Type/Expr.hs b/src/Language/Hasmtlib/Type/Expr.hs
index 3185990..677939e 100644
--- a/src/Language/Hasmtlib/Type/Expr.hs
+++ b/src/Language/Hasmtlib/Type/Expr.hs
@@ -7,7 +7,7 @@ module Language.Hasmtlib.Type.Expr
  , Expr
  , equal, distinct
  , bvShL, bvLShR, bvConcat, bvRotL, bvRotR
- , toInt, toReal, isInt
+ , toIntSort, toRealSort, isIntSort
  , for_all , exists
  , select, store
  )
@@ -107,11 +107,14 @@ bvRotR   :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvS
 bvRotR   = BvRotR
 {-# INLINE bvRotR #-}
 
-toReal    :: Expr IntSort  -> Expr RealSort
-toReal = ToReal
+-- | Converts an expression of type 'IntSort' to type 'RealSort'.
+toRealSort :: Expr IntSort  -> Expr RealSort
+toRealSort = ToReal
 
-toInt     :: Expr RealSort -> Expr IntSort
-toInt = ToInt
+-- | Converts an expression of type 'RealSort' to type 'IntSort'.
+toIntSort :: Expr RealSort -> Expr IntSort
+toIntSort = ToInt
 
-isInt     :: Expr RealSort -> Expr BoolSort
-isInt = IsInt
+-- | Checks whether an expression of type 'RealSort' may be safely converted to type 'IntSort'.
+isIntSort :: Expr RealSort -> Expr BoolSort
+isIntSort = IsInt

From 14451ab558ba127ba2773c99f37565d58d61a09a Mon Sep 17 00:00:00 2001
From: bruderj15 <julian.bruder@outlook.com>
Date: Tue, 23 Jul 2024 12:46:42 +0200
Subject: [PATCH 18/19] api-extension: Bump version & update CHANGELOG

---
 CHANGELOG.md   | 18 ++++++++++++++++++
 hasmtlib.cabal |  2 +-
 2 files changed, 19 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1a21421..9f9acae 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -6,6 +6,24 @@ file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [PVP versioning](https://pvp.haskell.org/).
 
+## v2.0.0 _(2024-07-23)_
+
+### Added
+- Arithmetic functions: `isIntSort`, `toIntSort` & `toRealSort`
+- Asserting maybe-formulas: `assertMaybe :: MonadSMT s m => Maybe (Expr BoolSort) -> m ()`
+- Logical equivalence `(<==>)` & reverse logical implication
+- Solvers: OpenSMT, OptiMathSAT
+- Iterative refinement optimizations utilizing incremental stack
+- Custom solver options via `Custom String String :: SMTOption`
+- Optimization Modulo Theories (OMT) / MaxSMT support with: `minimize`, `maximize` & `assertSoft`
+
+### Changed
+- *(breaking change)* The functions `solver` and `debug` which create `Solver`s from `ProcessSolver`s are polymorph in the state `s` now.
+This requires you to annotate the mentioned functions with the targetted state.
+These are `SMT` and `OMT`.
+For example, `solverWith (solver cvc5) $ do ...` becomes `solverWith (solver @SMT cvc5) $ do ...`.
+- Prefix `xor` now has an `infix 4`
+
 ## v1.3.1 _(2024-07-12)_
 
 ### Added
diff --git a/hasmtlib.cabal b/hasmtlib.cabal
index e7b28da..e1ee795 100644
--- a/hasmtlib.cabal
+++ b/hasmtlib.cabal
@@ -1,7 +1,7 @@
 cabal-version:         3.0
 
 name:                  hasmtlib
-version:               1.3.1
+version:               2.0.0
 synopsis:              A monad for interfacing with external SMT solvers
 description:           Hasmtlib is a library for generating SMTLib2-problems using a monad.
   It takes care of encoding your problem, marshaling the data to an external solver and parsing and interpreting the result into Haskell types.

From 4afc3589a60563c2868f58706bec1c8787b6ae17 Mon Sep 17 00:00:00 2001
From: bruderj15 <julian.bruder@outlook.com>
Date: Tue, 23 Jul 2024 12:49:25 +0200
Subject: [PATCH 19/19] api-extension: added missing infix fin in changelog

---
 CHANGELOG.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9f9acae..c28118b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -11,7 +11,7 @@ and this project adheres to [PVP versioning](https://pvp.haskell.org/).
 ### Added
 - Arithmetic functions: `isIntSort`, `toIntSort` & `toRealSort`
 - Asserting maybe-formulas: `assertMaybe :: MonadSMT s m => Maybe (Expr BoolSort) -> m ()`
-- Logical equivalence `(<==>)` & reverse logical implication
+- Logical equivalence `(<==>)` & reverse logical implication `(<==)`
 - Solvers: OpenSMT, OptiMathSAT
 - Iterative refinement optimizations utilizing incremental stack
 - Custom solver options via `Custom String String :: SMTOption`