diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -6,6 +6,24 @@
 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/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -41,7 +41,7 @@
 
 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 @@
 
 ## Features
 
-### Supported
 - [x] SMTLib2-Sorts in the Haskell-Type
   ```haskell
     data SMTSort = BoolSort | IntSort | RealSort | BvSort Nat | ArraySort SMTSort SMTSort
@@ -72,7 +71,7 @@
   ```
 - [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
@@ -81,12 +80,12 @@
   ```
 - [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
+- [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 @@
   ```
 - [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 @@
               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/hasmtlib.cabal b/hasmtlib.cabal
--- 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.
@@ -40,12 +40,15 @@
                      , 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
                      , Language.Hasmtlib.Type.MonadSMT
                      , 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
--- a/src/Language/Hasmtlib.hs
+++ b/src/Language/Hasmtlib.hs
@@ -2,10 +2,12 @@
   (
     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
   , module Language.Hasmtlib.Type.Option
+  , module Language.Hasmtlib.Type.SMTSort
   , module Language.Hasmtlib.Type.Solution
   , module Language.Hasmtlib.Type.ArrayMap
   , module Language.Hasmtlib.Integraled
@@ -20,16 +22,19 @@
   , 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
 
 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
 import Language.Hasmtlib.Type.Option
+import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Type.ArrayMap
 import Language.Hasmtlib.Integraled
@@ -44,4 +49,5 @@
 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/Boolean.hs b/src/Language/Hasmtlib/Boolean.hs
--- a/src/Language/Hasmtlib/Boolean.hs
+++ b/src/Language/Hasmtlib/Boolean.hs
@@ -35,12 +35,25 @@
   (==>) :: 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
 
   -- | Exclusive-or
   xor :: b -> b -> b
 
+  infix 4 `xor`
   infixr 3 &&
   infixr 2 ||
   infixr 0 ==>
diff --git a/src/Language/Hasmtlib/Codec.hs b/src/Language/Hasmtlib/Codec.hs
--- a/src/Language/Hasmtlib/Codec.hs
+++ b/src/Language/Hasmtlib/Codec.hs
@@ -10,6 +10,7 @@
 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
--- a/src/Language/Hasmtlib/Counting.hs
+++ b/src/Language/Hasmtlib/Counting.hs
@@ -3,6 +3,7 @@
 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
--- a/src/Language/Hasmtlib/Equatable.hs
+++ b/src/Language/Hasmtlib/Equatable.hs
@@ -6,6 +6,7 @@
 
 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
--- 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 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 @@
   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
 
@@ -250,14 +157,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)
diff --git a/src/Language/Hasmtlib/Internal/Expr/Num.hs b/src/Language/Hasmtlib/Internal/Expr/Num.hs
--- a/src/Language/Hasmtlib/Internal/Expr/Num.hs
+++ b/src/Language/Hasmtlib/Internal/Expr/Num.hs
@@ -3,6 +3,7 @@
 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
--- a/src/Language/Hasmtlib/Internal/Parser.hs
+++ b/src/Language/Hasmtlib/Internal/Parser.hs
@@ -6,12 +6,14 @@
 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 @@
   _   <- char '(' >> skipSpace >> string "to_real" >> skipSpace
   dec <- anyValue decimal
   _   <- skipSpace >> char ')'
-  
+
   return $ fromInteger dec
 {-# INLINEABLE parseToRealDouble #-}
 
diff --git a/src/Language/Hasmtlib/Internal/Render.hs b/src/Language/Hasmtlib/Internal/Render.hs
--- a/src/Language/Hasmtlib/Internal/Render.hs
+++ b/src/Language/Hasmtlib/Internal/Render.hs
@@ -2,9 +2,10 @@
 
 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
 
@@ -28,9 +29,17 @@
     | 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 <> ")"
@@ -49,3 +58,7 @@
   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/Iteable.hs b/src/Language/Hasmtlib/Iteable.hs
--- 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 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')
diff --git a/src/Language/Hasmtlib/Orderable.hs b/src/Language/Hasmtlib/Orderable.hs
--- a/src/Language/Hasmtlib/Orderable.hs
+++ b/src/Language/Hasmtlib/Orderable.hs
@@ -6,6 +6,7 @@
 
 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.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 @@
 
   (>=?) :: a -> a -> Expr BoolSort
   x >=? y = y <=? x
-  
+
   (<?)  :: a -> a -> Expr BoolSort
   x <? y = not $ y <=? x
 
@@ -51,34 +52,34 @@
 
 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
diff --git a/src/Language/Hasmtlib/Solver/CVC5.hs b/src/Language/Hasmtlib/Solver/CVC5.hs
--- a/src/Language/Hasmtlib/Solver/CVC5.hs
+++ b/src/Language/Hasmtlib/Solver/CVC5.hs
@@ -3,5 +3,7 @@
 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/Common.hs b/src/Language/Hasmtlib/Solver/Common.hs
--- a/src/Language/Hasmtlib/Solver/Common.hs
+++ b/src/Language/Hasmtlib/Solver/Common.hs
@@ -1,7 +1,9 @@
 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
 import Data.Default
 import Data.Sequence as Seq hiding ((|>), filter)
@@ -19,11 +21,11 @@
 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'.
@@ -32,44 +34,56 @@
   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
+    }
+
 -- | 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
+--
+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 = renderSMT smt
+    let problem = renderSeq s
     maybe mempty (`debugProblem` problem) debugger
 
     forM_ problem (B.command_ pSolver)
diff --git a/src/Language/Hasmtlib/Solver/MathSAT.hs b/src/Language/Hasmtlib/Solver/MathSAT.hs
--- a/src/Language/Hasmtlib/Solver/MathSAT.hs
+++ b/src/Language/Hasmtlib/Solver/MathSAT.hs
@@ -3,5 +3,12 @@
 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 = [] }
+
+-- | 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
new file mode 100644
--- /dev/null
+++ b/src/Language/Hasmtlib/Solver/OpenSMT.hs
@@ -0,0 +1,9 @@
+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
--- a/src/Language/Hasmtlib/Solver/Yices.hs
+++ b/src/Language/Hasmtlib/Solver/Yices.hs
@@ -3,5 +3,7 @@
 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"] }
diff --git a/src/Language/Hasmtlib/Solver/Z3.hs b/src/Language/Hasmtlib/Solver/Z3.hs
--- a/src/Language/Hasmtlib/Solver/Z3.hs
+++ b/src/Language/Hasmtlib/Solver/Z3.hs
@@ -3,6 +3,7 @@
 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
-
diff --git a/src/Language/Hasmtlib/Type/Expr.hs b/src/Language/Hasmtlib/Type/Expr.hs
--- a/src/Language/Hasmtlib/Type/Expr.hs
+++ b/src/Language/Hasmtlib/Type/Expr.hs
@@ -2,14 +2,12 @@
 {-# 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
+ , toIntSort, toRealSort, isIntSort
  , for_all , exists
  , select, store
  )
@@ -17,6 +15,7 @@
 
 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)
@@ -107,3 +106,15 @@
 bvRotR   :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)
 bvRotR   = BvRotR
 {-# INLINE bvRotR #-}
+
+-- | Converts an expression of type 'IntSort' to type 'RealSort'.
+toRealSort :: Expr IntSort  -> Expr RealSort
+toRealSort = ToReal
+
+-- | Converts an expression of type 'RealSort' to type 'IntSort'.
+toIntSort :: Expr RealSort -> Expr IntSort
+toIntSort = ToInt
+
+-- | Checks whether an expression of type 'RealSort' may be safely converted to type 'IntSort'.
+isIntSort :: Expr RealSort -> Expr BoolSort
+isIntSort = IsInt
diff --git a/src/Language/Hasmtlib/Type/MonadSMT.hs b/src/Language/Hasmtlib/Type/MonadSMT.hs
--- a/src/Language/Hasmtlib/Type/MonadSMT.hs
+++ b/src/Language/Hasmtlib/Type/MonadSMT.hs
@@ -4,6 +4,7 @@
 
 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
@@ -15,21 +16,21 @@
   -- | 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 +38,14 @@
   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 +64,7 @@
 {-# INLINE smtvar #-}
 
 -- | Create a constant.
--- 
+--
 --   >>> constant True
 --       Constant (BoolValue True)
 --
@@ -79,6 +80,13 @@
 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
@@ -147,3 +155,55 @@
 -- | 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.
+--   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.
+  --
+  --   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/OMT.hs b/src/Language/Hasmtlib/Type/OMT.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Hasmtlib/Type/OMT.hs
@@ -0,0 +1,94 @@
+{-# 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.SMTSort
+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 :: Expr t }
+
+-- | A newtype for numerical expressions that are target of a maximization.
+newtype Maximize t = Maximize { _targetMax :: Expr t }
+
+-- | The state of the OMT-problem.
+data OMT = OMT
+  { _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)
+
+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 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
+      renderGroupId Nothing = mempty
+      renderGroupId (Just groupId) = " :id " <> render groupId
+
+instance KnownSMTSort t => Render (Minimize t) where
+  render (Minimize expr) = "(minimize " <> render expr <> ")"
+
+instance KnownSMTSort t => Render (Maximize t) where
+  render (Maximize 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/Option.hs b/src/Language/Hasmtlib/Type/Option.hs
--- a/src/Language/Hasmtlib/Type/Option.hs
+++ b/src/Language/Hasmtlib/Type/Option.hs
@@ -9,9 +9,11 @@
     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
+  render (Custom k v)      = renderBinary "set-option" (":" <> render k) (render v)
diff --git a/src/Language/Hasmtlib/Type/Pipe.hs b/src/Language/Hasmtlib/Type/Pipe.hs
--- a/src/Language/Hasmtlib/Type/Pipe.hs
+++ b/src/Language/Hasmtlib/Type/Pipe.hs
@@ -4,9 +4,11 @@
 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
+import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Codec
 import Language.Hasmtlib.Internal.Parser hiding (var, constant)
@@ -98,14 +100,29 @@
       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
     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) $ render $ Minimize expr
+  {-# INLINEABLE minimize #-}
+
+  maximize expr = do
+    smt <- get
+    liftIO $ B.command_ (smt^.pipe) $ render $ Maximize expr
+  {-# INLINEABLE maximize #-}
+
+  assertSoft expr w gid = do
+    smt <- get
+    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
--- a/src/Language/Hasmtlib/Type/SMT.hs
+++ b/src/Language/Hasmtlib/Type/SMT.hs
@@ -6,6 +6,7 @@
 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
@@ -54,14 +55,12 @@
 
   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"
diff --git a/src/Language/Hasmtlib/Type/SMTSort.hs b/src/Language/Hasmtlib/Type/SMTSort.hs
new file mode 100644
--- /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
--- 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 @@
 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.
diff --git a/src/Language/Hasmtlib/Type/Solver.hs b/src/Language/Hasmtlib/Type/Solver.hs
--- a/src/Language/Hasmtlib/Type/Solver.hs
+++ b/src/Language/Hasmtlib/Type/Solver.hs
@@ -1,7 +1,17 @@
-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.SMTSort
 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 +104,61 @@
 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)
diff --git a/src/Language/Hasmtlib/Variable.hs b/src/Language/Hasmtlib/Variable.hs
--- a/src/Language/Hasmtlib/Variable.hs
+++ b/src/Language/Hasmtlib/Variable.hs
@@ -4,13 +4,14 @@
 
 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