From ff8c64490ce3b24ac15dcf6cbb27f23c6a71a604 Mon Sep 17 00:00:00 2001
From: "Julian.Bruder" <julian.bruder@city-concept-leipzig.de>
Date: Thu, 20 Jun 2024 10:09:01 +0200
Subject: [PATCH 01/15] array-sort: partially added ArraySort

---
 src/Language/Hasmtlib/Codec.hs             |  10 +-
 src/Language/Hasmtlib/Internal/ArrayMap.hs |  30 ++
 src/Language/Hasmtlib/Internal/Expr.hs     | 375 ++++++++++++---------
 src/Language/Hasmtlib/Type/Solution.hs     |   2 +-
 4 files changed, 246 insertions(+), 171 deletions(-)
 create mode 100644 src/Language/Hasmtlib/Internal/ArrayMap.hs

diff --git a/src/Language/Hasmtlib/Codec.hs b/src/Language/Hasmtlib/Codec.hs
index 59981cb..acb7326 100644
--- a/src/Language/Hasmtlib/Codec.hs
+++ b/src/Language/Hasmtlib/Codec.hs
@@ -5,6 +5,7 @@
 module Language.Hasmtlib.Codec where
 
 import Prelude hiding (not, (&&), (||))
+import Language.Hasmtlib.Internal.ArrayMap
 import Language.Hasmtlib.Internal.Bitvec
 import Language.Hasmtlib.Internal.Expr
 import Language.Hasmtlib.Type.Solution
@@ -61,6 +62,9 @@ instance KnownSMTSort t => Codec (Expr t) where
         where
           goN :: forall n m. KnownNat n => Proxy n -> Bitvec m -> Maybe (Bitvec n)
           goN _ = coerce . V.toSized @n . V.fromSized . coerce
+      SArraySort k v -> case someSol of
+                    SomeKnownSMTSort (SMTVarSol _ (ArrayValue arr)) -> Just _
+                    _                                               -> Nothing
 
   decode _ (Constant v) = Just $ unwrapValue v
   decode sol (Plus x y) = liftA2 (+)   (decode sol x) (decode sol y)
@@ -115,8 +119,10 @@ instance KnownSMTSort t => Codec (Expr t) where
   decode sol (BvuLTHE x y)      = liftA2 (<=) (decode sol x) (decode sol y)
   decode sol (BvuGTHE x y)      = liftA2 (>=) (decode sol x) (decode sol y)
   decode sol (BvuGT x y)        = liftA2 (>) (decode sol x) (decode sol y)
-  decode _ (ForAll _ _)       = Nothing
-  decode _ (Exists _ _)       = Nothing
+  decode sol (ArrSelect arr i)  = liftA2 select (decode sol arr) (decode sol i)
+  decode sol (ArrStore arr i x) = liftM3 store (decode sol arr) (decode sol i) (decode sol x)
+  decode _ (ForAll _ _)         = Nothing
+  decode _ (Exists _ _)         = Nothing
   encode = Constant . wrapValue
 
 instance Codec () where
diff --git a/src/Language/Hasmtlib/Internal/ArrayMap.hs b/src/Language/Hasmtlib/Internal/ArrayMap.hs
new file mode 100644
index 0000000..7e1d815
--- /dev/null
+++ b/src/Language/Hasmtlib/Internal/ArrayMap.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE TemplateHaskell #-}
+
+module Language.Hasmtlib.Internal.ArrayMap where
+
+import Data.Proxy
+import qualified Data.Map as Map  
+import Control.Lens
+  
+class ArrayMap f k v where
+  asConst'   :: Proxy f -> Proxy k -> v -> f k v 
+  viewConst  :: f k v -> v
+  select     :: f k v -> k -> v
+  store      :: f k v -> k -> v -> f k v
+
+asConst :: forall f k v. ArrayMap f k v => v -> f k v
+asConst = asConst' (Proxy @f) (Proxy @k)
+  
+data ConstArray k v = ConstArray 
+  { _arrConst :: v
+  , _stored :: Map.Map k v
+  } deriving (Show, Eq, Ord, Functor, Foldable, Traversable)
+$(makeLenses ''ConstArray)
+
+instance Ord k => ArrayMap ConstArray k v where
+  asConst' _ _ x = ConstArray x Map.empty
+  viewConst arr = arr^.arrConst
+  select arr i = case Map.lookup i (arr^.stored) of
+    Nothing -> viewConst arr
+    Just x  -> x
+  store arr i x = arr & stored %~ Map.insert i x
\ No newline at end of file
diff --git a/src/Language/Hasmtlib/Internal/Expr.hs b/src/Language/Hasmtlib/Internal/Expr.hs
index 69ae55b..7bbd7a6 100644
--- a/src/Language/Hasmtlib/Internal/Expr.hs
+++ b/src/Language/Hasmtlib/Internal/Expr.hs
@@ -2,12 +2,17 @@
 {-# LANGUAGE NoStarIsType #-}
 {-# LANGUAGE RoleAnnotations #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 
 module Language.Hasmtlib.Internal.Expr where
 
 import Language.Hasmtlib.Internal.Bitvec
 import Language.Hasmtlib.Internal.Render
+import Language.Hasmtlib.Internal.ArrayMap
 import Language.Hasmtlib.Boolean
+import Data.Map
 import Data.Kind
 import Data.Proxy
 import Data.Coerce
@@ -16,65 +21,82 @@ import Control.Lens
 import GHC.TypeLits
 
 -- | Sorts in SMTLib2 - used as promoted type (data-kind).
-data SMTSort = IntSort | RealSort | BoolSort | BvSort Nat
+data SMTSort =
+    IntSort
+  | RealSort
+  | BoolSort
+  | BvSort Nat
+  | ArraySort SMTSort SMTSort
 
 -- | 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 a 'SMTSort'.
+-- | 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 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
-  RealValue :: HaskellType RealSort   -> Value RealSort
-  BoolValue :: HaskellType BoolSort   -> Value BoolSort
-  BvValue   :: HaskellType (BvSort n) -> Value (BvSort n)
+  IntValue   :: HaskellType IntSort         -> Value IntSort
+  RealValue  :: HaskellType RealSort        -> Value RealSort
+  BoolValue  :: HaskellType BoolSort        -> Value BoolSort
+  BvValue    :: HaskellType (BvSort n)      -> Value (BvSort n)
+  ArrayValue :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => HaskellType (ArraySort k v) -> Value (ArraySort k v)
+
+instance Show (Value t) where
+  show (IntValue x)   = "IntValue "   ++ show x
+  show (RealValue x)  = "RealValue "  ++ show x
+  show (BoolValue x)  = "BoolValue "  ++ show x
+  show (BvValue x)    = "BvValue "    ++ show x
+  show (ArrayValue x) = "ArrValue: "  ++ show (render (ArrayValue x)) -- FIXME: This is bad but easy now
 
 -- | Unwrap a value.
 unwrapValue :: Value t -> HaskellType t
-unwrapValue (IntValue  v) = v
-unwrapValue (RealValue v) = v
-unwrapValue (BoolValue v) = v
-unwrapValue (BvValue   v) = v
+unwrapValue (IntValue   v) = v
+unwrapValue (RealValue  v) = v
+unwrapValue (BoolValue  v) = v
+unwrapValue (BvValue    v) = v
+unwrapValue (ArrayValue v) = v
 {-# INLINEABLE unwrapValue #-}
 
 -- | Wrap a value.
 wrapValue :: forall t. KnownSMTSort t => HaskellType t -> Value t
 wrapValue = case sortSing @t of
-  SIntSort  -> IntValue
-  SRealSort -> RealValue
-  SBoolSort -> BoolValue
-  SBvSort _ -> BvValue
+  SIntSort       -> IntValue
+  SRealSort      -> RealValue
+  SBoolSort      -> BoolValue
+  SBvSort _      -> BvValue
+  SArraySort _ _ -> ArrayValue
 {-# INLINEABLE wrapValue #-}
 
-deriving instance Show (Value t)
-deriving instance Eq   (Value t)
-deriving instance Ord  (Value t)
-
 -- | 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)
+  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)
 
 -- | 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)
+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)
+
+sortSing' :: forall proxy t. KnownSMTSort t => proxy t -> SSMTSort t
+sortSing' _ = sortSing @t
 
 -- | An existential wrapper that hides some 'SMTSort'.
 data SomeKnownSMTSort f where
@@ -84,70 +106,73 @@ data SomeKnownSMTSort f where
 --   For internal use only.
 --   For building expressions use the corresponding instances (Num, Boolean, ...).
 data Expr (t :: SMTSort) where
-  Var       :: SMTVar t -> Expr t
-  Constant  :: Value  t -> Expr t
-
-  Plus      :: Num (HaskellType t) => Expr t -> Expr t -> Expr t
-  Neg       :: Num (HaskellType t) => Expr t -> Expr t
-  Mul       :: Num (HaskellType t) => Expr t -> Expr t -> Expr t
-  Abs       :: Num (HaskellType t) => Expr t -> Expr t
-  Mod       :: Expr IntSort  -> Expr IntSort  -> Expr IntSort
-  IDiv      :: Expr IntSort  -> Expr IntSort  -> Expr IntSort
-  Div       :: Expr RealSort -> Expr RealSort -> Expr RealSort
-
-  LTH       :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
-  LTHE      :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
-  EQU       :: (Eq  (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
-  Distinct  :: (Eq  (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
-  GTHE      :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
-  GTH       :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
-
-  Not       :: Boolean (HaskellType t) => Expr t -> Expr t
-  And       :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t
-  Or        :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t
-  Impl      :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t
-  Xor       :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t
-
-  Pi       :: Expr RealSort
-  Sqrt     :: Expr RealSort -> Expr RealSort
-  Exp      :: Expr RealSort -> Expr RealSort
-  Sin      :: Expr RealSort -> Expr RealSort
-  Cos      :: Expr RealSort -> Expr RealSort
-  Tan      :: Expr RealSort -> Expr RealSort
-  Asin     :: Expr RealSort -> Expr RealSort
-  Acos     :: Expr RealSort -> Expr RealSort
-  Atan     :: Expr RealSort -> Expr RealSort
-
-  ToReal   :: Expr IntSort  -> Expr RealSort
-  ToInt    :: Expr RealSort -> Expr IntSort
-  IsInt    :: Expr RealSort -> Expr BoolSort
-
-  Ite      :: Expr BoolSort -> Expr t -> Expr t -> Expr t
-
-  BvNot    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n)
-  BvAnd    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
-  BvOr     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
-  BvXor    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
-  BvNand   :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
-  BvNor    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
-  BvNeg    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n)
-  BvAdd    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
-  BvSub    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
-  BvMul    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
-  BvuDiv   :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
-  BvuRem   :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
-  BvShL    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
-  BvLShR   :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
-  BvConcat :: (KnownNat n, KnownNat m) => Expr (BvSort n) -> Expr (BvSort m) -> Expr (BvSort (n + m))
-  BvRotL   :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)
-  BvRotR   :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)
-  BvuLT    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort
-  BvuLTHE  :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort
-  BvuGTHE  :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort
-  BvuGT    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort
-
-  ForAll   :: KnownSMTSort t => Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Expr BoolSort
-  Exists   :: KnownSMTSort t => Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Expr BoolSort
+  Var        :: SMTVar t -> Expr t
+  Constant   :: Value  t -> Expr t
+
+  Plus       :: Num (HaskellType t) => Expr t -> Expr t -> Expr t
+  Neg        :: Num (HaskellType t) => Expr t -> Expr t
+  Mul        :: Num (HaskellType t) => Expr t -> Expr t -> Expr t
+  Abs        :: Num (HaskellType t) => Expr t -> Expr t
+  Mod        :: Expr IntSort  -> Expr IntSort  -> Expr IntSort
+  IDiv       :: Expr IntSort  -> Expr IntSort  -> Expr IntSort
+  Div        :: Expr RealSort -> Expr RealSort -> Expr RealSort
+
+  LTH        :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
+  LTHE       :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
+  EQU        :: (Eq  (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
+  Distinct   :: (Eq  (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
+  GTHE       :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
+  GTH        :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
+
+  Not        :: Boolean (HaskellType t) => Expr t -> Expr t
+  And        :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t
+  Or         :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t
+  Impl       :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t
+  Xor        :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t
+
+  Pi         :: Expr RealSort
+  Sqrt       :: Expr RealSort -> Expr RealSort
+  Exp        :: Expr RealSort -> Expr RealSort
+  Sin        :: Expr RealSort -> Expr RealSort
+  Cos        :: Expr RealSort -> Expr RealSort
+  Tan        :: Expr RealSort -> Expr RealSort
+  Asin       :: Expr RealSort -> Expr RealSort
+  Acos       :: Expr RealSort -> Expr RealSort
+  Atan       :: Expr RealSort -> Expr RealSort
+
+  ToReal     :: Expr IntSort  -> Expr RealSort
+  ToInt      :: Expr RealSort -> Expr IntSort
+  IsInt      :: Expr RealSort -> Expr BoolSort
+
+  Ite        :: Expr BoolSort -> Expr t -> Expr t -> Expr t
+
+  BvNot      :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n)
+  BvAnd      :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
+  BvOr       :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
+  BvXor      :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
+  BvNand     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
+  BvNor      :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
+  BvNeg      :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n)
+  BvAdd      :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
+  BvSub      :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
+  BvMul      :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
+  BvuDiv     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
+  BvuRem     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
+  BvShL      :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
+  BvLShR     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)
+  BvConcat   :: (KnownNat n, KnownNat m) => Expr (BvSort n) -> Expr (BvSort m) -> Expr (BvSort (n + m))
+  BvRotL     :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)
+  BvRotR     :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)
+  BvuLT      :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort
+  BvuLTHE    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort
+  BvuGTHE    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort
+  BvuGT      :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort
+
+  ArrSelect  :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v
+  ArrStore   :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v -> Expr (ArraySort k v)
+
+  ForAll     :: KnownSMTSort t => Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Expr BoolSort
+  Exists     :: KnownSMTSort t => Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Expr BoolSort
 
 instance Boolean (Expr BoolSort) where
   bool = Constant . BoolValue
@@ -182,23 +207,35 @@ instance KnownNat n => Bounded (Expr (BvSort n)) where
   maxBound = Constant $ BvValue maxBound
 
 instance Render (SSMTSort t) where
-  render SIntSort    = "Int"
-  render SRealSort   = "Real"
-  render SBoolSort   = "Bool"
-  render (SBvSort p) = renderBinary "_" ("BitVec" :: Builder) (natVal p)
+  render SIntSort         = "Int"
+  render SRealSort        = "Real"
+  render SBoolSort        = "Bool"
+  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 #-}
 
-instance KnownSMTSort t => Render (Expr t) where
-  render (Var v)                  = render v
-  render (Constant (IntValue x))  = render x
-  render (Constant (RealValue x)) = render x
-  render (Constant (BoolValue x)) = render x
-  render (Constant (BvValue   v)) = "#b" <> render v
+instance Render (Value t) where
+  render (IntValue x)   = render x
+  render (RealValue x)  = render x
+  render (BoolValue x)  = render x
+  render (BvValue   v)  = "#b" <> render v
+  render (ArrayValue arr) = case minViewWithKey (arr^.stored) of
+    Nothing -> constRender $ arr^.arrConst
+    Just ((k,v), stored')
+      | size (arr^.stored) > 1 -> render $ ArrStore (Constant (wrapValue (arr & stored .~ stored'))) (Constant (wrapValue k)) (Constant (wrapValue v))
+      | otherwise  -> constRender v
+    where
+      constRender v = "((as const " <> render (goSing arr) <> ") " <> render (wrapValue v) <> ")"
+      goSing :: forall k v. (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => ConstArray (HaskellType k) (HaskellType v) -> SSMTSort (ArraySort k v)
+      goSing _ = sortSing @(ArraySort k v)
 
+instance KnownSMTSort t => Render (Expr t) where
+  render (Var v)      = render v
+  render (Constant c) = render c
   render (Plus x y)   = renderBinary "+" x y
   render (Neg x)      = renderUnary  "-" x
   render (Mul x y)    = renderBinary "*" x y
@@ -258,8 +295,11 @@ instance KnownSMTSort t => Render (Expr t) where
   render (BvuGTHE x y)      = renderBinary "bvuge"  (render x) (render y)
   render (BvuGT x y)        = renderBinary "bvugt"  (render x) (render y)
 
-  render (ForAll mQvar f) = renderQuantifier "forall" mQvar f
-  render (Exists mQvar f) = renderQuantifier "exists" mQvar f
+  render (ArrSelect a i)    = renderBinary  "select" (render a) (render i)
+  render (ArrStore a i v)   = renderTernary "store"  (render a) (render i) (render v)
+
+  render (ForAll mQvar f)   = renderQuantifier "forall" mQvar f
+  render (Exists mQvar f)   = renderQuantifier "exists" mQvar f
 
 renderQuantifier :: forall t. KnownSMTSort t => Builder -> Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Builder
 renderQuantifier qname (Just qvar) f =
@@ -272,64 +312,63 @@ renderQuantifier qname (Just qvar) f =
 renderQuantifier _ Nothing _ = mempty
 
 instance Show (Expr t) where
-  show (Var v)                  = show v
-  show (Constant (IntValue x))  = show x
-  show (Constant (RealValue x)) = show x
-  show (Constant (BoolValue x)) = show x
-  show (Constant (BvValue   x)) = show x
-  show (Plus x y)               = "(" ++ show x ++ " + " ++ show y ++ ")"
-  show (Neg x)                  = "(- " ++ show x ++ ")"
-  show (Mul x y)                = "(" ++ show x ++ " * " ++ show y ++ ")"
-  show (Abs x)                  = "(abs " ++ show x ++ ")"
-  show (Mod x y)                = "(" ++ show x ++ " mod " ++ show y ++ ")"
-  show (IDiv x y)               = "(" ++ show x ++ " div " ++ show y ++ ")"
-  show (Div x y)                = "(" ++ show x ++ " / " ++ show y ++ ")"
-  show (LTH x y)                = "(" ++ show x ++ " < " ++ show y ++ ")"
-  show (LTHE x y)               = "(" ++ show x ++ " <= " ++ show y ++ ")"
-  show (EQU x y)                = "(" ++ show x ++ " == " ++ show y ++ ")"
-  show (Distinct x y)           = "(" ++ show x ++ " /= " ++ show y ++ ")"
-  show (GTHE x y)               = "(" ++ show x ++ " >= " ++ show y ++ ")"
-  show (GTH x y)                = "(" ++ show x ++ " > " ++ show y ++ ")"
-  show (Not x)                  = "(not " ++ show x ++ ")"
-  show (And x y)                = "(" ++ show x ++ " && " ++ show y ++ ")"
-  show (Or x y)                 = "(" ++ show x ++ " || " ++ show y ++ ")"
-  show (Impl x y)               = "(" ++ show x ++ " ==> " ++ show y ++ ")"
-  show (Xor x y)                = "(" ++ show x ++ " xor " ++ show y ++ ")"
-  show Pi                       = "pi"
-  show (Sqrt x)                 = "(sqrt "    ++ show x ++ ")"
-  show (Exp x)                  = "(exp "     ++ show x ++ ")"
-  show (Sin x)                  = "(sin "     ++ show x ++ ")"
-  show (Cos x)                  = "(cos "     ++ show x ++ ")"
-  show (Tan x)                  = "(tan "     ++ show x ++ ")"
-  show (Asin x)                 = "(arcsin "  ++ show x ++ ")"
-  show (Acos x)                 = "(arccos "  ++ show x ++ ")"
-  show (Atan x)                 = "(arctan "  ++ show x ++ ")"
-  show (ToReal x)               = "(to_real " ++ show x ++ ")"
-  show (ToInt x)                = "(to_int "  ++ show x ++ ")"
-  show (IsInt x)                = "(is_int "  ++ show x ++ ")"
-  show (Ite p t f)              = "(ite " ++ show p ++ " " ++ show t ++ " " ++ show f ++ ")"
-  show (BvNot x)                = "(not "  ++ show x ++ ")"
-  show (BvAnd x y)              = "(" ++ show x ++ " && " ++ show y ++ ")"
-  show (BvOr x y)               = "(" ++ show x ++ " || " ++ show y ++ ")"
-  show (BvXor x y)              = "(" ++ show x ++ " xor " ++ show y ++ ")"
-  show (BvNand x y)             = "(" ++ show x ++ " nand " ++ show y ++ ")"
-  show (BvNor x y)              = "(" ++ show x ++ " nor " ++ show y ++ ")"
-  show (BvNeg x)                = "(- " ++ show x ++ ")"
-  show (BvAdd x y)              = "(" ++ show x ++ " + " ++ show y ++ ")"
-  show (BvSub x y)              = "(" ++ show x ++ " - " ++ show y ++ ")"
-  show (BvMul x y)              = "(" ++ show x ++ " * " ++ show y ++ ")"
-  show (BvuDiv x y)             = "(" ++ show x ++ " udiv " ++ show y ++ ")"
-  show (BvuRem x y)             = "(" ++ show x ++ " urem " ++ show y ++ ")"
-  show (BvShL x y)              = "(" ++ show x ++ " bvshl " ++ show y ++ ")"
-  show (BvLShR x y)             = "(" ++ show x ++ " bvlshr " ++ show y ++ ")"
-  show (BvConcat x y)           = "(" ++ show x ++ " bvconcat " ++ show y ++ ")"
-  show (BvRotL i x)             = "(" ++ show x ++ " bvrotl " ++ show (natVal i) ++ ")"
-  show (BvRotR i x)             = "(" ++ show x ++ " bvrotr " ++ show (natVal i) ++ ")"
-  show (BvuLT x y)              = "(" ++ show x ++ " bvult " ++ show y ++ ")"
-  show (BvuLTHE x y)            = "(" ++ show x ++ " bvule " ++ show y ++ ")"
-  show (BvuGTHE x y)            = "(" ++ show x ++ " bvuge " ++ show y ++ ")"
-  show (BvuGT x y)              = "(" ++ show x ++ " bvugt " ++ show y ++ ")"
-  show (ForAll (Just qv) f)     = "(forall " ++ show qv ++ ": " ++ show (f (Var qv)) ++ ")"
-  show (ForAll Nothing f)       = "(forall var_-1: " ++ show (f (Var (SMTVar (-1)))) ++ ")"
-  show (Exists (Just qv) f)     = "(exists " ++ show qv ++ ": " ++ show (f (Var qv)) ++ ")"
-  show (Exists Nothing f)       = "(exists var_-1: " ++ show (f (Var (SMTVar (-1)))) ++ ")"
\ No newline at end of file
+  show (Var v)                   = show v
+  show (Constant c)              = show c
+  show (Plus x y)                = "(" ++ show x ++ " + " ++ show y ++ ")"
+  show (Neg x)                   = "(- " ++ show x ++ ")"
+  show (Mul x y)                 = "(" ++ show x ++ " * " ++ show y ++ ")"
+  show (Abs x)                   = "(abs " ++ show x ++ ")"
+  show (Mod x y)                 = "(" ++ show x ++ " mod " ++ show y ++ ")"
+  show (IDiv x y)                = "(" ++ show x ++ " div " ++ show y ++ ")"
+  show (Div x y)                 = "(" ++ show x ++ " / " ++ show y ++ ")"
+  show (LTH x y)                 = "(" ++ show x ++ " < " ++ show y ++ ")"
+  show (LTHE x y)                = "(" ++ show x ++ " <= " ++ show y ++ ")"
+  show (EQU x y)                 = "(" ++ show x ++ " == " ++ show y ++ ")"
+  show (Distinct x y)            = "(" ++ show x ++ " /= " ++ show y ++ ")"
+  show (GTHE x y)                = "(" ++ show x ++ " >= " ++ show y ++ ")"
+  show (GTH x y)                 = "(" ++ show x ++ " > " ++ show y ++ ")"
+  show (Not x)                   = "(not " ++ show x ++ ")"
+  show (And x y)                 = "(" ++ show x ++ " && " ++ show y ++ ")"
+  show (Or x y)                  = "(" ++ show x ++ " || " ++ show y ++ ")"
+  show (Impl x y)                = "(" ++ show x ++ " ==> " ++ show y ++ ")"
+  show (Xor x y)                 = "(" ++ show x ++ " xor " ++ show y ++ ")"
+  show Pi                        = "pi"
+  show (Sqrt x)                  = "(sqrt "    ++ show x ++ ")"
+  show (Exp x)                   = "(exp "     ++ show x ++ ")"
+  show (Sin x)                   = "(sin "     ++ show x ++ ")"
+  show (Cos x)                   = "(cos "     ++ show x ++ ")"
+  show (Tan x)                   = "(tan "     ++ show x ++ ")"
+  show (Asin x)                  = "(arcsin "  ++ show x ++ ")"
+  show (Acos x)                  = "(arccos "  ++ show x ++ ")"
+  show (Atan x)                  = "(arctan "  ++ show x ++ ")"
+  show (ToReal x)                = "(to_real " ++ show x ++ ")"
+  show (ToInt x)                 = "(to_int "  ++ show x ++ ")"
+  show (IsInt x)                 = "(is_int "  ++ show x ++ ")"
+  show (Ite p t f)               = "(ite " ++ show p ++ " " ++ show t ++ " " ++ show f ++ ")"
+  show (BvNot x)                 = "(not "  ++ show x ++ ")"
+  show (BvAnd x y)               = "(" ++ show x ++ " && " ++ show y ++ ")"
+  show (BvOr x y)                = "(" ++ show x ++ " || " ++ show y ++ ")"
+  show (BvXor x y)               = "(" ++ show x ++ " xor " ++ show y ++ ")"
+  show (BvNand x y)              = "(" ++ show x ++ " nand " ++ show y ++ ")"
+  show (BvNor x y)               = "(" ++ show x ++ " nor " ++ show y ++ ")"
+  show (BvNeg x)                 = "(- " ++ show x ++ ")"
+  show (BvAdd x y)               = "(" ++ show x ++ " + " ++ show y ++ ")"
+  show (BvSub x y)               = "(" ++ show x ++ " - " ++ show y ++ ")"
+  show (BvMul x y)               = "(" ++ show x ++ " * " ++ show y ++ ")"
+  show (BvuDiv x y)              = "(" ++ show x ++ " udiv " ++ show y ++ ")"
+  show (BvuRem x y)              = "(" ++ show x ++ " urem " ++ show y ++ ")"
+  show (BvShL x y)               = "(" ++ show x ++ " bvshl " ++ show y ++ ")"
+  show (BvLShR x y)              = "(" ++ show x ++ " bvlshr " ++ show y ++ ")"
+  show (BvConcat x y)            = "(" ++ show x ++ " bvconcat " ++ show y ++ ")"
+  show (BvRotL i x)              = "(" ++ show x ++ " bvrotl " ++ show (natVal i) ++ ")"
+  show (BvRotR i x)              = "(" ++ show x ++ " bvrotr " ++ show (natVal i) ++ ")"
+  show (BvuLT x y)               = "(" ++ show x ++ " bvult " ++ show y ++ ")"
+  show (BvuLTHE x y)             = "(" ++ show x ++ " bvule " ++ show y ++ ")"
+  show (BvuGTHE x y)             = "(" ++ show x ++ " bvuge " ++ show y ++ ")"
+  show (BvuGT x y)               = "(" ++ show x ++ " bvugt " ++ show y ++ ")"
+  show (ArrSelect a i)           = "(select " ++ show a ++ " " ++ show i ++ ")"
+  show (ArrStore a i v)          = "(store "  ++ show a ++ " " ++ show i ++ " " ++ show v ++ ")"
+  show (ForAll (Just qv) f)      = "(forall " ++ show qv ++ ": " ++ show (f (Var qv)) ++ ")"
+  show (ForAll Nothing f)        = "(forall var_-1: " ++ show (f (Var (SMTVar (-1)))) ++ ")"
+  show (Exists (Just qv) f)      = "(exists " ++ show qv ++ ": " ++ show (f (Var qv)) ++ ")"
+  show (Exists Nothing f)        = "(exists var_-1: " ++ show (f (Var (SMTVar (-1)))) ++ ")"
\ No newline at end of file
diff --git a/src/Language/Hasmtlib/Type/Solution.hs b/src/Language/Hasmtlib/Type/Solution.hs
index 6905981..6a656bb 100644
--- a/src/Language/Hasmtlib/Type/Solution.hs
+++ b/src/Language/Hasmtlib/Type/Solution.hs
@@ -19,5 +19,5 @@ type Solution = IntMap (SomeKnownSMTSort SMTVarSol)
 data SMTVarSol (t :: SMTSort) = SMTVarSol 
   { _solVar :: SMTVar t                       -- ^ A variable in the SMT-Problem
   , _solVal :: Value t                        -- ^ An assignment for this variable in a solution
-  } deriving (Show, Eq, Ord)
+  } deriving Show
 $(makeLenses ''SMTVarSol)

From 698976d71adbb05f315e4ab20f0439a7f34fce85 Mon Sep 17 00:00:00 2001
From: "Julian.Bruder" <julian.bruder@city-concept-leipzig.de>
Date: Thu, 20 Jun 2024 11:19:24 +0200
Subject: [PATCH 02/15] dependent-solution: temp commit

---
 hasmtlib.cabal                         |  3 +++
 src/Language/Hasmtlib/Codec.hs         | 23 ++++-------------------
 src/Language/Hasmtlib/Internal/Expr.hs | 25 +++++++++++++++++++++++++
 src/Language/Hasmtlib/Type/Solution.hs | 17 ++++-------------
 4 files changed, 36 insertions(+), 32 deletions(-)

diff --git a/hasmtlib.cabal b/hasmtlib.cabal
index b393472..f8621a6 100644
--- a/hasmtlib.cabal
+++ b/hasmtlib.cabal
@@ -55,12 +55,15 @@ library
                      , base                         >= 4.17.2 && < 5
                      , bytestring                   >= 0.11.5 && < 1
                      , containers                   >= 0.6.7  && < 1
+                     , dependent-map                >= 0.4    && < 0.5
+                     , dependent-sum-template       >= 0.1    && < 0.3
                      , mtl                          >= 2.2.2  && < 3
                      , text                         >= 2.0.2  && < 3
                      , data-default                 >= 0.7.1  && < 1
                      , lens                         >= 5      && < 6
                      , smtlib-backends              >= 0.4    && < 1
                      , smtlib-backends-process      >= 0.3    && < 1
+                     , some                         >= 1.0.6  && < 1.1
                      , utf8-string                  >= 1.0.2  && < 2
                      , bitvec                       >= 1.1.5  && < 2
                      , finite-typelits              >= 0.1.0  && < 1
diff --git a/src/Language/Hasmtlib/Codec.hs b/src/Language/Hasmtlib/Codec.hs
index 59981cb..cdbe458 100644
--- a/src/Language/Hasmtlib/Codec.hs
+++ b/src/Language/Hasmtlib/Codec.hs
@@ -15,6 +15,7 @@ import Data.Proxy
 import Data.Map (Map)
 import Data.Sequence (Seq)
 import Data.IntMap as IM
+import Data.Dependent.Map as DMap
 import Data.Tree (Tree)
 import qualified Data.Vector.Unboxed.Sized as V
 import Control.Monad
@@ -43,25 +44,8 @@ class Codec a where
 -- | Decode and evaluate expressions
 instance KnownSMTSort t => Codec (Expr t) where
   type Decoded (Expr t) = HaskellType t
-  decode sol (Var var)    = do
-    someSol <- IM.lookup (coerce var) sol
-    case sortSing @t of
-      SIntSort   -> case someSol of
-                    SomeKnownSMTSort (SMTVarSol _ (IntValue v))  -> Just v
-                    _                                            -> Nothing
-      SRealSort  -> case someSol of
-                    SomeKnownSMTSort (SMTVarSol _ (RealValue v)) -> Just v
-                    _                                            -> Nothing
-      SBoolSort  -> case someSol of
-                    SomeKnownSMTSort (SMTVarSol _ (BoolValue v)) -> Just v
-                    _                                            -> Nothing
-      SBvSort p  -> case someSol of
-                    SomeKnownSMTSort (SMTVarSol _ (BvValue v))   -> goN p v
-                    _                                            -> Nothing
-        where
-          goN :: forall n m. KnownNat n => Proxy n -> Bitvec m -> Maybe (Bitvec n)
-          goN _ = coerce . V.toSized @n . V.fromSized . coerce
-
+  
+  decode sol (Var var)  = unwrapValue <$> DMap.lookup var sol 
   decode _ (Constant v) = Just $ unwrapValue v
   decode sol (Plus x y) = liftA2 (+)   (decode sol x) (decode sol y)
   decode sol (Neg x)    = fmap negate  (decode sol x)
@@ -117,6 +101,7 @@ instance KnownSMTSort t => Codec (Expr t) where
   decode sol (BvuGT x y)        = liftA2 (>) (decode sol x) (decode sol y)
   decode _ (ForAll _ _)       = Nothing
   decode _ (Exists _ _)       = Nothing
+  
   encode = Constant . wrapValue
 
 instance Codec () where
diff --git a/src/Language/Hasmtlib/Internal/Expr.hs b/src/Language/Hasmtlib/Internal/Expr.hs
index 69ae55b..f1a1fa6 100644
--- a/src/Language/Hasmtlib/Internal/Expr.hs
+++ b/src/Language/Hasmtlib/Internal/Expr.hs
@@ -8,6 +8,7 @@ module Language.Hasmtlib.Internal.Expr where
 import Language.Hasmtlib.Internal.Bitvec
 import Language.Hasmtlib.Internal.Render
 import Language.Hasmtlib.Boolean
+import Data.GADT.Compare
 import Data.Kind
 import Data.Proxy
 import Data.Coerce
@@ -23,6 +24,21 @@ type role SMTVar phantom
 newtype SMTVar (t :: SMTSort) = SMTVar { _varId :: Int } deriving (Show, Eq, Ord)
 $(makeLenses ''SMTVar)
 
+instance GEq SMTVar where
+  geq :: forall a b. (KnownSMTSort a, KnownSMTSort b) => SMTVar a -> SMTVar b -> Maybe (a :~: b)
+  geq x y = case geq (sortSing @a) (sortSing @b) of
+    Nothing -> Nothing
+    Just Refl -> if x == y then Just Refl else Nothing
+
+--instance GCompare SMTVar where
+--  gcompare :: forall a b. (KnownSMTSort a, KnownSMTSort b) => SMTVar a -> SMTVar b -> GOrdering a b
+--  gcompare x y = case sortSing @a of
+--    SIntSort  -> case sortSing @b of SIntSort -> GEQ ; _ -> GLT
+--    SRealSort -> _
+--    SBoolSort -> _
+--    SBvSort _ -> _
+
+
 -- | Injective type-family that computes the Haskell 'Type' of a 'SMTSort'.
 type family HaskellType (t :: SMTSort) = (r :: Type) | r -> t where
   HaskellType IntSort    = Integer
@@ -65,6 +81,15 @@ data SSMTSort (t :: SMTSort) where
   SBoolSort :: SSMTSort BoolSort
   SBvSort   :: KnownNat n => Proxy n -> SSMTSort (BvSort n)
 
+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
+
 deriving instance Show (SSMTSort t)
 deriving instance Eq   (SSMTSort t)
 deriving instance Ord  (SSMTSort t)
diff --git a/src/Language/Hasmtlib/Type/Solution.hs b/src/Language/Hasmtlib/Type/Solution.hs
index 6905981..1020d2c 100644
--- a/src/Language/Hasmtlib/Type/Solution.hs
+++ b/src/Language/Hasmtlib/Type/Solution.hs
@@ -1,10 +1,7 @@
-{-# LANGUAGE TemplateHaskell #-}
-
 module Language.Hasmtlib.Type.Solution where
 
 import Language.Hasmtlib.Type.Expr
-import Data.IntMap
-import Control.Lens
+import Data.Dependent.Map
 
 -- | Function that turns a state into a result and a solution.
 type Solver s m = s -> m (Result, Solution)
@@ -12,12 +9,6 @@ type Solver s m = s -> m (Result, Solution)
 -- | Results of check-sat commands.
 data Result = Unsat | Unknown | Sat deriving (Show, Eq, Ord)
 
--- | A Solution is a Map from the variable-identifier to some solution for it.
-type Solution = IntMap (SomeKnownSMTSort SMTVarSol)
-
--- | A solution for a single variable.
-data SMTVarSol (t :: SMTSort) = SMTVarSol 
-  { _solVar :: SMTVar t                       -- ^ A variable in the SMT-Problem
-  , _solVal :: Value t                        -- ^ An assignment for this variable in a solution
-  } deriving (Show, Eq, Ord)
-$(makeLenses ''SMTVarSol)
+-- TODO
+-- | A Solution is a Map from the variable-identifier to some solution for it. 
+type Solution = DMap SMTVar Value 

From db518d3974e85224e08d55feaff6e954c1a1095a Mon Sep 17 00:00:00 2001
From: "Julian.Bruder" <julian.bruder@city-concept-leipzig.de>
Date: Thu, 20 Jun 2024 17:51:50 +0200
Subject: [PATCH 03/15] dependent-solution: removed dep dependent-sum-template

---
 hasmtlib.cabal | 1 -
 1 file changed, 1 deletion(-)

diff --git a/hasmtlib.cabal b/hasmtlib.cabal
index f8621a6..14167ea 100644
--- a/hasmtlib.cabal
+++ b/hasmtlib.cabal
@@ -56,7 +56,6 @@ library
                      , bytestring                   >= 0.11.5 && < 1
                      , containers                   >= 0.6.7  && < 1
                      , dependent-map                >= 0.4    && < 0.5
-                     , dependent-sum-template       >= 0.1    && < 0.3
                      , mtl                          >= 2.2.2  && < 3
                      , text                         >= 2.0.2  && < 3
                      , data-default                 >= 0.7.1  && < 1

From 4e219d25fa8fe59a2d6a39bcaeea396ef54f8625 Mon Sep 17 00:00:00 2001
From: "Julian.Bruder" <julian.bruder@city-concept-leipzig.de>
Date: Thu, 20 Jun 2024 17:54:52 +0200
Subject: [PATCH 04/15] dependent-solution: parse model existentially & give
 dependent solution

---
 src/Language/Hasmtlib/Codec.hs           | 119 +++++++++++------------
 src/Language/Hasmtlib/Internal/Expr.hs   |  48 ++++-----
 src/Language/Hasmtlib/Internal/Parser.hs |  57 +++++------
 src/Language/Hasmtlib/Type/Expr.hs       |   4 +-
 src/Language/Hasmtlib/Type/Pipe.hs       |  11 ++-
 src/Language/Hasmtlib/Type/Solution.hs   |  38 +++++++-
 6 files changed, 155 insertions(+), 122 deletions(-)

diff --git a/src/Language/Hasmtlib/Codec.hs b/src/Language/Hasmtlib/Codec.hs
index cdbe458..baf534e 100644
--- a/src/Language/Hasmtlib/Codec.hs
+++ b/src/Language/Hasmtlib/Codec.hs
@@ -11,15 +11,12 @@ import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Boolean
 import Data.Kind
 import Data.Coerce
-import Data.Proxy
 import Data.Map (Map)
 import Data.Sequence (Seq)
 import Data.IntMap as IM
 import Data.Dependent.Map as DMap
 import Data.Tree (Tree)
-import qualified Data.Vector.Unboxed.Sized as V
 import Control.Monad
-import GHC.TypeNats
 
 -- | Compute the default 'Decoded' 'Type' for every functor-wrapper.
 --   Useful for instances using default signatures.
@@ -44,63 +41,65 @@ class Codec a where
 -- | Decode and evaluate expressions
 instance KnownSMTSort t => Codec (Expr t) where
   type Decoded (Expr t) = HaskellType t
-  
-  decode sol (Var var)  = unwrapValue <$> DMap.lookup var sol 
-  decode _ (Constant v) = Just $ unwrapValue v
-  decode sol (Plus x y) = liftA2 (+)   (decode sol x) (decode sol y)
-  decode sol (Neg x)    = fmap negate  (decode sol x)
-  decode sol (Mul x y)  = liftA2 (*)   (decode sol x) (decode sol y)
-  decode sol (Abs x)    = fmap abs     (decode sol x)
-  decode sol (Mod x y)  = liftA2 mod   (decode sol x) (decode sol y)
-  decode sol (IDiv x y) = liftA2 div   (decode sol x) (decode sol y)
-  decode sol (Div x y)  = liftA2 (/)   (decode sol x) (decode sol y)
-  decode sol (LTH x y)  = liftA2 (<)   (decode sol x) (decode sol y)
-  decode sol (LTHE x y) = liftA2 (<=)  (decode sol x) (decode sol y)
-  decode sol (EQU x y)  = liftA2 (==)  (decode sol x) (decode sol y)
-  decode sol (Distinct x y)  = liftA2 (/=)  (decode sol x) (decode sol y)
-  decode sol (GTHE x y) = liftA2 (>=)  (decode sol x) (decode sol y)
-  decode sol (GTH x y)  = liftA2 (>)   (decode sol x) (decode sol y)
-  decode sol (Not x)    = fmap   not  (decode sol x)
-  decode sol (And x y)  = liftA2 (&&) (decode sol x) (decode sol y)
-  decode sol (Or x y)   = liftA2 (||) (decode sol x) (decode sol y)
-  decode sol (Impl x y) = liftA2 (==>) (decode sol x) (decode sol y)
-  decode sol (Xor x y)  = liftA2 xor   (decode sol x) (decode sol y)
-  decode _ Pi           = Just pi
-  decode sol (Sqrt x)   = fmap sqrt  (decode sol x)
-  decode sol (Exp x)    = fmap exp   (decode sol x)
-  decode sol (Sin x)    = fmap sin   (decode sol x)
-  decode sol (Cos x)    = fmap cos   (decode sol x)
-  decode sol (Tan x)    = fmap tan   (decode sol x)
-  decode sol (Asin x)   = fmap asin  (decode sol x)
-  decode sol (Acos x)   = fmap acos  (decode sol x)
-  decode sol (Atan x)   = fmap atan  (decode sol x)
-  decode sol (ToReal x) = fmap realToFrac (decode sol x)
-  decode sol (ToInt x)  = fmap truncate   (decode sol x)
-  decode sol (IsInt x)  = fmap ((0 ==) . snd . properFraction) (decode sol x)
-  decode sol (Ite p t f) = liftM3 (\p' t' f' -> if p' then t' else f') (decode sol p) (decode sol t) (decode sol f) 
-  decode sol (BvNot x)          = fmap not (decode sol x)
-  decode sol (BvAnd x y)        = liftA2 (&&) (decode sol x) (decode sol y)
-  decode sol (BvOr x y)         = liftA2 (||) (decode sol x) (decode sol y)
-  decode sol (BvXor x y)        = liftA2 xor (decode sol x) (decode sol y)
-  decode sol (BvNand x y)       = nand <$> sequenceA [decode sol x, decode sol y]
-  decode sol (BvNor x y)        = nor  <$> sequenceA [decode sol x, decode sol y]
-  decode sol (BvNeg x)          = fmap negate (decode sol x)
-  decode sol (BvAdd x y)        = liftA2 (+) (decode sol x) (decode sol y)
-  decode sol (BvSub x y)        = liftA2 (-) (decode sol x) (decode sol y)
-  decode sol (BvMul x y)        = liftA2 (*) (decode sol x) (decode sol y)
-  decode sol (BvuDiv x y)       = liftA2 div (decode sol x) (decode sol y)
-  decode sol (BvuRem x y)       = liftA2 rem (decode sol x) (decode sol y)
-  decode sol (BvShL x y)        = join $ liftA2 bvShL (decode sol x) (decode sol y)
-  decode sol (BvLShR x y)       = join $ liftA2 bvLShR (decode sol x) (decode sol y)
-  decode sol (BvConcat x y)     = liftA2 bvConcat (decode sol x) (decode sol y)
-  decode sol (BvRotL i x)       = bvRotL i <$> decode sol x
-  decode sol (BvRotR i x)       = bvRotR i <$> decode sol x
-  decode sol (BvuLT x y)        = liftA2 (<) (decode sol x) (decode sol y)
-  decode sol (BvuLTHE x y)      = liftA2 (<=) (decode sol x) (decode sol y)
-  decode sol (BvuGTHE x y)      = liftA2 (>=) (decode sol x) (decode sol y)
-  decode sol (BvuGT x y)        = liftA2 (>) (decode sol x) (decode sol y)
-  decode _ (ForAll _ _)       = Nothing
-  decode _ (Exists _ _)       = Nothing
+  decode sol (Var var)  = do
+    (IntValueMap m) <- DMap.lookup (sortSing @t) sol
+    val <- IM.lookup (coerce var) m
+    return $ unwrapValue val
+  decode _ (Constant v)     = Just $ unwrapValue v
+  decode sol (Plus x y)     = liftA2 (+)   (decode sol x) (decode sol y)
+  decode sol (Neg x)        = fmap negate  (decode sol x)
+  decode sol (Mul x y)      = liftA2 (*)   (decode sol x) (decode sol y)
+  decode sol (Abs x)        = fmap abs     (decode sol x)
+  decode sol (Mod x y)      = liftA2 mod   (decode sol x) (decode sol y)
+  decode sol (IDiv x y)     = liftA2 div   (decode sol x) (decode sol y)
+  decode sol (Div x y)      = liftA2 (/)   (decode sol x) (decode sol y)
+  decode sol (LTH x y)      = liftA2 (<)   (decode sol x) (decode sol y)
+  decode sol (LTHE x y)     = liftA2 (<=)  (decode sol x) (decode sol y)
+  decode sol (EQU x y)      = liftA2 (==)  (decode sol x) (decode sol y)
+  decode sol (Distinct x y) = liftA2 (/=)  (decode sol x) (decode sol y)
+  decode sol (GTHE x y)     = liftA2 (>=)  (decode sol x) (decode sol y)
+  decode sol (GTH x y)      = liftA2 (>)   (decode sol x) (decode sol y)
+  decode sol (Not x)        = fmap   not  (decode sol x)
+  decode sol (And x y)      = liftA2 (&&) (decode sol x) (decode sol y)
+  decode sol (Or x y)       = liftA2 (||) (decode sol x) (decode sol y)
+  decode sol (Impl x y)     = liftA2 (==>) (decode sol x) (decode sol y)
+  decode sol (Xor x y)      = liftA2 xor   (decode sol x) (decode sol y)
+  decode _ Pi               = Just pi
+  decode sol (Sqrt x)       = fmap sqrt  (decode sol x)
+  decode sol (Exp x)        = fmap exp   (decode sol x)
+  decode sol (Sin x)        = fmap sin   (decode sol x)
+  decode sol (Cos x)        = fmap cos   (decode sol x)
+  decode sol (Tan x)        = fmap tan   (decode sol x)
+  decode sol (Asin x)       = fmap asin  (decode sol x)
+  decode sol (Acos x)       = fmap acos  (decode sol x)
+  decode sol (Atan x)       = fmap atan  (decode sol x)
+  decode sol (ToReal x)     = fmap realToFrac (decode sol x)
+  decode sol (ToInt x)      = fmap truncate   (decode sol x)
+  decode sol (IsInt x)      = fmap ((0 ==) . snd . properFraction) (decode sol x)
+  decode sol (Ite p t f)    = liftM3 (\p' t' f' -> if p' then t' else f') (decode sol p) (decode sol t) (decode sol f) 
+  decode sol (BvNot x)      = fmap not (decode sol x)
+  decode sol (BvAnd x y)    = liftA2 (&&) (decode sol x) (decode sol y)
+  decode sol (BvOr x y)     = liftA2 (||) (decode sol x) (decode sol y)
+  decode sol (BvXor x y)    = liftA2 xor (decode sol x) (decode sol y)
+  decode sol (BvNand x y)   = nand <$> sequenceA [decode sol x, decode sol y]
+  decode sol (BvNor x y)    = nor  <$> sequenceA [decode sol x, decode sol y]
+  decode sol (BvNeg x)      = fmap negate (decode sol x)
+  decode sol (BvAdd x y)    = liftA2 (+) (decode sol x) (decode sol y)
+  decode sol (BvSub x y)    = liftA2 (-) (decode sol x) (decode sol y)
+  decode sol (BvMul x y)    = liftA2 (*) (decode sol x) (decode sol y)
+  decode sol (BvuDiv x y)   = liftA2 div (decode sol x) (decode sol y)
+  decode sol (BvuRem x y)   = liftA2 rem (decode sol x) (decode sol y)
+  decode sol (BvShL x y)    = join $ liftA2 bvShL (decode sol x) (decode sol y)
+  decode sol (BvLShR x y)   = join $ liftA2 bvLShR (decode sol x) (decode sol y)
+  decode sol (BvConcat x y) = liftA2 bvConcat (decode sol x) (decode sol y)
+  decode sol (BvRotL i x)   = bvRotL i <$> decode sol x
+  decode sol (BvRotR i x)   = bvRotR i <$> decode sol x
+  decode sol (BvuLT x y)    = liftA2 (<) (decode sol x) (decode sol y)
+  decode sol (BvuLTHE x y)  = liftA2 (<=) (decode sol x) (decode sol y)
+  decode sol (BvuGTHE x y)  = liftA2 (>=) (decode sol x) (decode sol y)
+  decode sol (BvuGT x y)    = liftA2 (>) (decode sol x) (decode sol y)
+  decode _ (ForAll _ _)     = Nothing
+  decode _ (Exists _ _)     = Nothing
   
   encode = Constant . wrapValue
 
diff --git a/src/Language/Hasmtlib/Internal/Expr.hs b/src/Language/Hasmtlib/Internal/Expr.hs
index f1a1fa6..91d40b9 100644
--- a/src/Language/Hasmtlib/Internal/Expr.hs
+++ b/src/Language/Hasmtlib/Internal/Expr.hs
@@ -17,28 +17,13 @@ import Control.Lens
 import GHC.TypeLits
 
 -- | Sorts in SMTLib2 - used as promoted type (data-kind).
-data SMTSort = IntSort | RealSort | BoolSort | BvSort Nat
+data SMTSort = BoolSort | IntSort | RealSort | BvSort Nat
 
 -- | 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)
 
-instance GEq SMTVar where
-  geq :: forall a b. (KnownSMTSort a, KnownSMTSort b) => SMTVar a -> SMTVar b -> Maybe (a :~: b)
-  geq x y = case geq (sortSing @a) (sortSing @b) of
-    Nothing -> Nothing
-    Just Refl -> if x == y then Just Refl else Nothing
-
---instance GCompare SMTVar where
---  gcompare :: forall a b. (KnownSMTSort a, KnownSMTSort b) => SMTVar a -> SMTVar b -> GOrdering a b
---  gcompare x y = case sortSing @a of
---    SIntSort  -> case sortSing @b of SIntSort -> GEQ ; _ -> GLT
---    SRealSort -> _
---    SBoolSort -> _
---    SBvSort _ -> _
-
-
 -- | Injective type-family that computes the Haskell 'Type' of a 'SMTSort'.
 type family HaskellType (t :: SMTSort) = (r :: Type) | r -> t where
   HaskellType IntSort    = Integer
@@ -81,6 +66,10 @@ data SSMTSort (t :: SMTSort) where
   SBoolSort :: SSMTSort BoolSort
   SBvSort   :: KnownNat n => Proxy n -> SSMTSort (BvSort n)
 
+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
@@ -90,9 +79,20 @@ instance GEq SSMTSort where
     Nothing   -> Nothing
   geq _ _                     = Nothing
 
-deriving instance Show (SSMTSort t)
-deriving instance Eq   (SSMTSort t)
-deriving instance Ord  (SSMTSort t)
+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 SBoolSort _ = GLT
+  gcompare _ SBoolSort = GGT
+  gcompare SIntSort _  = GLT
+  gcompare _ SIntSort  = GGT
+  gcompare SRealSort _ = GLT
+  gcompare _ SRealSort = GGT
 
 -- | Compute singleton 'SSMTSort' from it's promoted type 'SMTSort'.
 class    KnownSMTSort (t :: SMTSort)           where sortSing :: SSMTSort t
@@ -101,6 +101,10 @@ instance KnownSMTSort RealSort                 where sortSing = SRealSort
 instance KnownSMTSort BoolSort                 where sortSing = SBoolSort
 instance KnownNat n => KnownSMTSort (BvSort n) where sortSing = SBvSort (Proxy @n)
 
+-- | Wrapper for 'sortSing' which takes a 'Proxy'
+sortSing' :: forall prxy t. KnownSMTSort t => prxy t -> SSMTSort t
+sortSing' _ = sortSing @t
+
 -- | An existential wrapper that hides some 'SMTSort'.
 data SomeKnownSMTSort f where
   SomeKnownSMTSort :: forall (t :: SMTSort) f. KnownSMTSort t => f t -> SomeKnownSMTSort f
@@ -207,9 +211,9 @@ instance KnownNat n => Bounded (Expr (BvSort n)) where
   maxBound = Constant $ BvValue maxBound
 
 instance Render (SSMTSort t) where
+  render SBoolSort   = "Bool"
   render SIntSort    = "Int"
   render SRealSort   = "Real"
-  render SBoolSort   = "Bool"
   render (SBvSort p) = renderBinary "_" ("BitVec" :: Builder) (natVal p)
   {-# INLINEABLE render #-}
 
@@ -219,9 +223,9 @@ instance Render (SMTVar t) where
 
 instance KnownSMTSort t => Render (Expr t) where
   render (Var v)                  = render v
+  render (Constant (BoolValue x)) = render x
   render (Constant (IntValue x))  = render x
   render (Constant (RealValue x)) = render x
-  render (Constant (BoolValue x)) = render x
   render (Constant (BvValue   v)) = "#b" <> render v
 
   render (Plus x y)   = renderBinary "+" x y
@@ -298,9 +302,9 @@ renderQuantifier _ Nothing _ = mempty
 
 instance Show (Expr t) where
   show (Var v)                  = show v
+  show (Constant (BoolValue x)) = show x
   show (Constant (IntValue x))  = show x
   show (Constant (RealValue x)) = show x
-  show (Constant (BoolValue x)) = show x
   show (Constant (BvValue   x)) = show x
   show (Plus x y)               = "(" ++ show x ++ " + " ++ show y ++ ")"
   show (Neg x)                  = "(- " ++ show x ++ ")"
diff --git a/src/Language/Hasmtlib/Internal/Parser.hs b/src/Language/Hasmtlib/Internal/Parser.hs
index 428fd14..474e1fe 100644
--- a/src/Language/Hasmtlib/Internal/Parser.hs
+++ b/src/Language/Hasmtlib/Internal/Parser.hs
@@ -1,5 +1,3 @@
-{-# LANGUAGE LambdaCase #-}
-
 module Language.Hasmtlib.Internal.Parser where
 
 import Prelude hiding (not, (&&), (||), and , or)
@@ -20,7 +18,6 @@ import Data.ByteString
 import Data.ByteString.Builder
 import Data.Attoparsec.ByteString hiding (Result, skipWhile)
 import Data.Attoparsec.ByteString.Char8 hiding (Result)
-import qualified Data.IntMap as IM
 import Control.Applicative
 import Control.Lens hiding (op)
 import GHC.TypeNats
@@ -47,7 +44,7 @@ defaultModelParser = do
   varSols <- many $ parseSomeSol <* skipSpace
   _       <- (skipSpace >> char ')' >> skipSpace) <|> skipSpace
 
-  return $ fromSomeList varSols
+  return $ fromSomeVarSols varSols
 
 smt2ModelParser :: Parser Solution
 smt2ModelParser = do
@@ -55,43 +52,41 @@ smt2ModelParser = do
   varSols <- many $ parseSomeSol <* skipSpace
   _       <- (skipSpace >> char ')' >> skipSpace) <|> skipSpace
 
-  return $ fromSomeList varSols
-
-fromSomeList :: [SomeKnownSMTSort SMTVarSol] -> Solution
-fromSomeList = IM.fromList . fmap (\case someVarSol@(SomeKnownSMTSort varSol) -> (coerce (varSol^.solVar), someVarSol))
+  return $ fromSomeVarSols varSols
 
 parseSomeSol :: Parser (SomeKnownSMTSort SMTVarSol)
-parseSomeSol = SomeKnownSMTSort <$> (parseSol @IntSort)
-           <|> SomeKnownSMTSort <$> (parseSol @RealSort)
-           <|> SomeKnownSMTSort <$> (parseSol @BoolSort)
-           <|> parseAnyBvUpToLength 128
-
-parseAnyBvUpToLength :: Natural -> Parser (SomeKnownSMTSort SMTVarSol)
-parseAnyBvUpToLength hi = asum $ fmap ((\case SomeNat p -> goProxy p) . someNatVal) [0..hi]
-  where
-    goProxy :: forall n. KnownNat n => Proxy n -> Parser (SomeKnownSMTSort SMTVarSol)
-    goProxy _ = SomeKnownSMTSort <$> parseSol @(BvSort n)
-
-parseSol :: forall t. KnownSMTSort t => Parser (SMTVarSol t)
-parseSol = do
+parseSomeSol = do
   _     <- char '(' >> skipSpace
   _     <- string "define-fun" >> skipSpace
   _     <- string "var_"
   vId   <- decimal @Int
   _     <- skipSpace >> string "()" >> skipSpace
-  _     <- string $ toStrict $ toLazyByteString $ render (sortSing @t)
+  (SomeKnownSMTSort someSort) <- parseSomeSort
   _     <- skipSpace
-  expr  <- parseExpr @t
+  expr  <- parseExpr' someSort
   _     <- skipSpace >> char ')'
-
-  -- Try to evaluate expression given by solver as solution
-  -- Better: Take into scope already successfully parsed solutions for other vars.
-  -- Is this even required though? Do the solvers ever answer like-wise?
   case decode mempty expr of
     Nothing    -> fail $ "Solver reponded with solution for var_" ++ show vId ++ " but it contains "
                       ++ "another var. This cannot be parsed and evaluated currently."
-    Just value -> return $ SMTVarSol (coerce vId) (wrapValue value)
-{-# INLINEABLE parseSol #-}
+    Just value -> return $ SomeKnownSMTSort $ SMTVarSol (coerce vId) (wrapValue value)
+{-# INLINEABLE parseSomeSol #-}
+
+parseSomeSort :: Parser (SomeKnownSMTSort SSMTSort)
+parseSomeSort = (string "Bool" *> pure (SomeKnownSMTSort SBoolSort))
+        <|> (string "Int"  *> pure (SomeKnownSMTSort SIntSort))
+        <|> (string "Real" *> pure (SomeKnownSMTSort SRealSort))
+        <|> parseSomeBitVecSort
+  where
+    parseSomeBitVecSort = do
+      _ <- char '(' >> skipSpace >> char '_' >> skipSpace
+      _ <- string "BitVec" >> skipSpace
+      n <- decimal
+      _ <- skipSpace >> char ')'
+      case someNatVal $ fromInteger n of
+        SomeNat pn -> return $ SomeKnownSMTSort $ SBvSort pn
+
+parseExpr' :: forall prxy t. KnownSMTSort t => prxy t -> Parser (Expr t)
+parseExpr' _ = parseExpr @t
 
 parseExpr :: forall t. KnownSMTSort t => Parser (Expr t)
 parseExpr = var <|> constant <|> smtIte
@@ -115,9 +110,7 @@ parseExpr = var <|> constant <|> smtIte
                       <|> binary @IntSort ">=" (>=?) <|> binary @IntSort ">" (>?)
                       <|> binary @RealSort "<" (<?) <|> binary @RealSort "<=" (<=?)
                       <|> binary @RealSort ">=" (>=?) <|> binary @RealSort ">" (>?)
-                      -- TODO: All (?) bv lengths - also for '=' and 'distinct'
---                      <|> binary @(BvSort 10) "bvult" (<?) <|> binary @(BvSort 10) "bvule" (<=?)
---                      <|> binary @(BvSort 10) "bvuge" (>=?) <|> binary @(BvSort 10) "bvugt" (>?)
+                      -- TODO: Add compare ops for all (?) bv-sorts
               SBvSort _ -> unary "bvnot" not
                       <|> binary "bvand" (&&)  <|> binary "bvor" (||) <|> binary "bvxor" xor <|> binary "bvnand" BvNand <|> binary "bvnor" BvNor
                       <|> unary  "bvneg" negate
diff --git a/src/Language/Hasmtlib/Type/Expr.hs b/src/Language/Hasmtlib/Type/Expr.hs
index e92b77f..5a5781c 100644
--- a/src/Language/Hasmtlib/Type/Expr.hs
+++ b/src/Language/Hasmtlib/Type/Expr.hs
@@ -2,10 +2,10 @@
 
 module Language.Hasmtlib.Type.Expr
  ( SMTSort(..)
- , SMTVar(..)
+ , SMTVar(..), varId
  , HaskellType
  , Value(..), unwrapValue, wrapValue
- , SSMTSort(..), KnownSMTSort(..), SomeKnownSMTSort(..)
+ , SSMTSort(..), KnownSMTSort(..), sortSing', SomeKnownSMTSort(..)
  , Expr
  , for_all , exists
  , module Language.Hasmtlib.Internal.Expr.Num
diff --git a/src/Language/Hasmtlib/Type/Pipe.hs b/src/Language/Hasmtlib/Type/Pipe.hs
index 4ec2929..e9b5f84 100644
--- a/src/Language/Hasmtlib/Type/Pipe.hs
+++ b/src/Language/Hasmtlib/Type/Pipe.hs
@@ -12,7 +12,8 @@ import Language.Hasmtlib.Codec
 import Language.Hasmtlib.Internal.Parser hiding (var, constant)
 import qualified SMTLIB.Backends as B
 import Data.List (isPrefixOf)
-import Data.IntMap (singleton)
+import Data.IntMap as IMap (singleton)
+import Data.Dependent.Map as DMap
 import Data.Coerce
 import Data.ByteString.Builder
 import Data.ByteString.Lazy hiding (filter, singleton, isPrefixOf)
@@ -97,7 +98,13 @@ instance (MonadState Pipe m, MonadIO m) => MonadIncrSMT Pipe m where
       Left e    -> liftIO $ do
         print model
         error e
-      Right sol -> return $ decode (singleton (sol^.solVar.varId) (SomeKnownSMTSort sol)) v
+      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
diff --git a/src/Language/Hasmtlib/Type/Solution.hs b/src/Language/Hasmtlib/Type/Solution.hs
index 1020d2c..f19d262 100644
--- a/src/Language/Hasmtlib/Type/Solution.hs
+++ b/src/Language/Hasmtlib/Type/Solution.hs
@@ -1,7 +1,14 @@
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE LambdaCase #-}
+
 module Language.Hasmtlib.Type.Solution where
 
 import Language.Hasmtlib.Type.Expr
-import Data.Dependent.Map
+import Data.IntMap as IMap hiding (foldl)
+import Data.Dependent.Map as DMap
+import Data.Dependent.Map.Lens
+import Control.Lens
 
 -- | Function that turns a state into a result and a solution.
 type Solver s m = s -> m (Result, Solution)
@@ -9,6 +16,29 @@ type Solver s m = s -> m (Result, Solution)
 -- | Results of check-sat commands.
 data Result = Unsat | Unknown | Sat deriving (Show, Eq, Ord)
 
--- TODO
--- | A Solution is a Map from the variable-identifier to some solution for it. 
-type Solution = DMap SMTVar Value 
+-- | A Solution is a dependent map 'DMap' from 'SSMTSort's t to 'IntMap' t. 
+type Solution = DMap SSMTSort IntValueMap
+
+-- | Newtype for 'IntMap' 'Value' so we can use it as right-hand-side of 'DMap'.
+newtype IntValueMap t = IntValueMap (IntMap (Value t))
+  deriving stock Show
+  deriving newtype (Eq, Ord, Semigroup, Monoid)
+
+-- | A solution for a single variable.
+data SMTVarSol (t :: SMTSort) = SMTVarSol
+  { _solVar :: SMTVar t                       -- ^ A variable in the SMT-Problem
+  , _solVal :: Value t                        -- ^ An assignment for this variable in a solution
+  } deriving (Show, Eq, Ord)
+$(makeLenses ''SMTVarSol)
+
+-- | Create a 'Solution' from some 'SMTVarSol's.
+fromSomeVarSols :: [SomeKnownSMTSort SMTVarSol] -> Solution
+fromSomeVarSols = foldl
+  (\dsol (SomeKnownSMTSort s) -> let sSort = sortSing' s in
+    dsol & dmat sSort %~   -- TODO: There has got to be lens or map operation for, but which? 
+      (\case
+        Nothing -> Just $ IntValueMap $ IMap.singleton (s^.solVar.varId) (s^.solVal)
+        Just (IntValueMap im) -> Just $ IntValueMap $ IMap.insert (s^.solVar.varId) (s^.solVal) im
+      )
+  )
+  mempty
\ No newline at end of file

From 4b435ef24c448d36a557b6bd724d3546ed0f5428 Mon Sep 17 00:00:00 2001
From: "Julian.Bruder" <julian.bruder@city-concept-leipzig.de>
Date: Thu, 20 Jun 2024 18:06:00 +0200
Subject: [PATCH 05/15] dependent-solution: removed TODO

---
 src/Language/Hasmtlib/Type/Solution.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Language/Hasmtlib/Type/Solution.hs b/src/Language/Hasmtlib/Type/Solution.hs
index f19d262..c70e156 100644
--- a/src/Language/Hasmtlib/Type/Solution.hs
+++ b/src/Language/Hasmtlib/Type/Solution.hs
@@ -16,7 +16,7 @@ type Solver s m = s -> m (Result, Solution)
 -- | Results of check-sat commands.
 data Result = Unsat | Unknown | Sat deriving (Show, Eq, Ord)
 
--- | A Solution is a dependent map 'DMap' from 'SSMTSort's t to 'IntMap' t. 
+-- | A Solution is a dependent map 'DMap' from 'SSMTSort's t to 'IntMap' t.
 type Solution = DMap SSMTSort IntValueMap
 
 -- | Newtype for 'IntMap' 'Value' so we can use it as right-hand-side of 'DMap'.
@@ -35,7 +35,7 @@ $(makeLenses ''SMTVarSol)
 fromSomeVarSols :: [SomeKnownSMTSort SMTVarSol] -> Solution
 fromSomeVarSols = foldl
   (\dsol (SomeKnownSMTSort s) -> let sSort = sortSing' s in
-    dsol & dmat sSort %~   -- TODO: There has got to be lens or map operation for, but which? 
+    dsol & dmat sSort %~
       (\case
         Nothing -> Just $ IntValueMap $ IMap.singleton (s^.solVar.varId) (s^.solVal)
         Just (IntValueMap im) -> Just $ IntValueMap $ IMap.insert (s^.solVar.varId) (s^.solVal) im

From 7a3475e3a940e1d89c7d8742303321adadc8407b Mon Sep 17 00:00:00 2001
From: "Julian.Bruder" <julian.bruder@city-concept-leipzig.de>
Date: Thu, 20 Jun 2024 18:06:27 +0200
Subject: [PATCH 06/15] dependent-solution: removed TODOs

---
 src/Language/Hasmtlib/Solver/CVC5.hs | 2 --
 src/Language/Hasmtlib/Solver/Z3.hs   | 2 --
 2 files changed, 4 deletions(-)

diff --git a/src/Language/Hasmtlib/Solver/CVC5.hs b/src/Language/Hasmtlib/Solver/CVC5.hs
index d6ceb4e..fea6cde 100644
--- a/src/Language/Hasmtlib/Solver/CVC5.hs
+++ b/src/Language/Hasmtlib/Solver/CVC5.hs
@@ -3,7 +3,5 @@ module Language.Hasmtlib.Solver.CVC5 where
 import Language.Hasmtlib.Solver.Common
 import qualified SMTLIB.Backends.Process as P
 
--- TODO: Add support for lib binding: https://github.com/tweag/smtlib-backends/tree/master/smtlib-backends-cvc5
-
 cvc5 :: ProcessSolver
 cvc5 = ProcessSolver $ P.defaultConfig { P.exe = "cvc5", P.args = [] }
diff --git a/src/Language/Hasmtlib/Solver/Z3.hs b/src/Language/Hasmtlib/Solver/Z3.hs
index 7981089..6caa30f 100644
--- a/src/Language/Hasmtlib/Solver/Z3.hs
+++ b/src/Language/Hasmtlib/Solver/Z3.hs
@@ -3,8 +3,6 @@ module Language.Hasmtlib.Solver.Z3 where
 import Language.Hasmtlib.Solver.Common
 import qualified SMTLIB.Backends.Process as P
 
--- TODO: Add support for lib binding: https://github.com/tweag/smtlib-backends/tree/master/smtlib-backends-z3
-
 z3 :: ProcessSolver
 z3 = ProcessSolver P.defaultConfig
 

From 07f725f5e25ef01883fb545264ffeb043f537ff2 Mon Sep 17 00:00:00 2001
From: "Julian.Bruder" <julian.bruder@city-concept-leipzig.de>
Date: Thu, 20 Jun 2024 18:08:12 +0200
Subject: [PATCH 07/15] dependent-solution: more liberal parser inlining

---
 src/Language/Hasmtlib/Internal/Parser.hs | 20 +++++++++++---------
 1 file changed, 11 insertions(+), 9 deletions(-)

diff --git a/src/Language/Hasmtlib/Internal/Parser.hs b/src/Language/Hasmtlib/Internal/Parser.hs
index 474e1fe..16cee7c 100644
--- a/src/Language/Hasmtlib/Internal/Parser.hs
+++ b/src/Language/Hasmtlib/Internal/Parser.hs
@@ -84,9 +84,11 @@ parseSomeSort = (string "Bool" *> pure (SomeKnownSMTSort SBoolSort))
       _ <- skipSpace >> char ')'
       case someNatVal $ fromInteger n of
         SomeNat pn -> return $ SomeKnownSMTSort $ SBvSort pn
+{-# INLINEABLE parseSomeSort #-}
 
 parseExpr' :: forall prxy t. KnownSMTSort t => prxy t -> Parser (Expr t)
 parseExpr' _ = parseExpr @t
+{-# INLINE parseExpr' #-}
 
 parseExpr :: forall t. KnownSMTSort t => Parser (Expr t)
 parseExpr = var <|> constant <|> smtIte
@@ -124,7 +126,7 @@ var = do
   vId <- decimal @Int
 
   return $ Var $ coerce vId
-{-# INLINEABLE var #-}
+{-# INLINE var #-}
 
 constant :: forall t. KnownSMTSort t => Parser (Expr t)
 constant = do
@@ -135,7 +137,7 @@ constant = do
     SBvSort p -> anyBitvector p
 
   return $ Constant $ wrapValue cval
-{-# INLINEABLE constant #-}
+{-# INLINE constant #-}
 
 anyBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n)
 anyBitvector p = binBitvector p <|> hexBitvector p <|> literalBitvector p
@@ -154,7 +156,7 @@ hexBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n)
 hexBitvector _ = do
   _ <- string "#x" >> skipSpace
   fromInteger <$> hexadecimal
-{-# INLINEABLE hexBitvector #-}
+{-# INLINE hexBitvector #-}
 
 literalBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n)
 literalBitvector _ = do
@@ -165,7 +167,7 @@ literalBitvector _ = do
   _ <- skipWhile (/= ')') >> char ')'
 
   return $ fromInteger x
-{-# INLINEABLE literalBitvector #-}
+{-# INLINE literalBitvector #-}
 
 unary :: forall t r. KnownSMTSort t => ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
 unary opStr op = do
@@ -175,7 +177,7 @@ unary opStr op = do
   _ <- skipSpace >> char ')'
 
   return $ op val
-{-# INLINEABLE unary #-}
+{-# INLINE unary #-}
 
 binary :: forall t r. KnownSMTSort t => ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
 binary opStr op = do
@@ -186,7 +188,7 @@ binary opStr op = do
   r <- parseExpr
   _ <- skipSpace >> char ')'
   return $ l `op` r
-{-# INLINEABLE binary #-}
+{-# INLINE binary #-}
 
 nary :: forall t r. KnownSMTSort t => ByteString -> ([Expr t] -> Expr r) -> Parser (Expr r)
 nary opStr op = do
@@ -195,11 +197,11 @@ nary opStr op = do
   args <- parseExpr `sepBy1` skipSpace
   _    <- skipSpace >> char ')'
   return $ op args
-{-# INLINEABLE nary #-}
+{-# INLINE nary #-}
 
 smtPi :: Parser (Expr RealSort)
 smtPi = string "real.pi" *> return pi
-{-# INLINEABLE smtPi #-}
+{-# INLINE smtPi #-}
 
 toRealFun :: Parser (Expr RealSort)
 toRealFun = do
@@ -256,7 +258,7 @@ negativeValue p = do
   _ <- skipSpace >> char ')'
 
   return $ negate val
-{-# INLINEABLE negativeValue #-}
+{-# INLINE negativeValue #-}
 
 parseRatioDouble :: Parser Double
 parseRatioDouble = do

From 2a8b2a26ad185582e4ce7d3c607ea78bb31cf96c Mon Sep 17 00:00:00 2001
From: "Julian.Bruder" <julian.bruder@city-concept-leipzig.de>
Date: Thu, 20 Jun 2024 18:08:59 +0200
Subject: [PATCH 08/15] dependent-solution: more liberal upper-bound for
 dependent-map

---
 hasmtlib.cabal | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/hasmtlib.cabal b/hasmtlib.cabal
index 14167ea..8438219 100644
--- a/hasmtlib.cabal
+++ b/hasmtlib.cabal
@@ -55,7 +55,7 @@ library
                      , base                         >= 4.17.2 && < 5
                      , bytestring                   >= 0.11.5 && < 1
                      , containers                   >= 0.6.7  && < 1
-                     , dependent-map                >= 0.4    && < 0.5
+                     , dependent-map                >= 0.4    && < 1
                      , mtl                          >= 2.2.2  && < 3
                      , text                         >= 2.0.2  && < 3
                      , data-default                 >= 0.7.1  && < 1

From 3e7155a37d8bb3d6201e2430abd8ca9f258baa50 Mon Sep 17 00:00:00 2001
From: "Julian.Bruder" <julian.bruder@city-concept-leipzig.de>
Date: Fri, 21 Jun 2024 13:21:27 +0200
Subject: [PATCH 09/15] array-sort: added ArraySort

---
 hasmtlib.cabal                                |   1 +
 src/Language/Hasmtlib.hs                      |   2 +
 src/Language/Hasmtlib/Codec.hs                | 113 +++++++++---------
 src/Language/Hasmtlib/Internal/Expr.hs        |  37 ++++--
 src/Language/Hasmtlib/Internal/Parser.hs      | 110 +++++++++++++----
 .../Hasmtlib/{Internal => Type}/ArrayMap.hs   |   5 +-
 src/Language/Hasmtlib/Type/Expr.hs            |  11 +-
 src/Language/Hasmtlib/Type/Solution.hs        |   6 +-
 8 files changed, 188 insertions(+), 97 deletions(-)
 rename src/Language/Hasmtlib/{Internal => Type}/ArrayMap.hs (85%)

diff --git a/hasmtlib.cabal b/hasmtlib.cabal
index 8438219..599203d 100644
--- a/hasmtlib.cabal
+++ b/hasmtlib.cabal
@@ -35,6 +35,7 @@ library
                      , Language.Hasmtlib.Internal.Parser
                      , Language.Hasmtlib.Internal.Bitvec
                      , Language.Hasmtlib.Internal.Render
+                     , Language.Hasmtlib.Internal.ArrayMap
                      , Language.Hasmtlib.Solver.Common
                      , Language.Hasmtlib.Solver.CVC5
                      , Language.Hasmtlib.Solver.MathSAT
diff --git a/src/Language/Hasmtlib.hs b/src/Language/Hasmtlib.hs
index 545bd71..f0e5cc6 100644
--- a/src/Language/Hasmtlib.hs
+++ b/src/Language/Hasmtlib.hs
@@ -7,6 +7,7 @@ module Language.Hasmtlib
   , module Language.Hasmtlib.Type.Solver
   , module Language.Hasmtlib.Type.Option
   , module Language.Hasmtlib.Type.Solution
+  , module Language.Hasmtlib.Type.ArrayMap
   , module Language.Hasmtlib.Integraled
   , module Language.Hasmtlib.Iteable
   , module Language.Hasmtlib.Boolean
@@ -29,6 +30,7 @@ import Language.Hasmtlib.Type.Expr
 import Language.Hasmtlib.Type.Solver
 import Language.Hasmtlib.Type.Option
 import Language.Hasmtlib.Type.Solution
+import Language.Hasmtlib.Type.ArrayMap
 import Language.Hasmtlib.Integraled
 import Language.Hasmtlib.Iteable
 import Language.Hasmtlib.Boolean
diff --git a/src/Language/Hasmtlib/Codec.hs b/src/Language/Hasmtlib/Codec.hs
index baf534e..4898580 100644
--- a/src/Language/Hasmtlib/Codec.hs
+++ b/src/Language/Hasmtlib/Codec.hs
@@ -8,6 +8,7 @@ import Prelude hiding (not, (&&), (||))
 import Language.Hasmtlib.Internal.Bitvec
 import Language.Hasmtlib.Internal.Expr
 import Language.Hasmtlib.Type.Solution
+import Language.Hasmtlib.Type.ArrayMap
 import Language.Hasmtlib.Boolean
 import Data.Kind
 import Data.Coerce
@@ -45,61 +46,63 @@ instance KnownSMTSort t => Codec (Expr t) where
     (IntValueMap m) <- DMap.lookup (sortSing @t) sol
     val <- IM.lookup (coerce var) m
     return $ unwrapValue val
-  decode _ (Constant v)     = Just $ unwrapValue v
-  decode sol (Plus x y)     = liftA2 (+)   (decode sol x) (decode sol y)
-  decode sol (Neg x)        = fmap negate  (decode sol x)
-  decode sol (Mul x y)      = liftA2 (*)   (decode sol x) (decode sol y)
-  decode sol (Abs x)        = fmap abs     (decode sol x)
-  decode sol (Mod x y)      = liftA2 mod   (decode sol x) (decode sol y)
-  decode sol (IDiv x y)     = liftA2 div   (decode sol x) (decode sol y)
-  decode sol (Div x y)      = liftA2 (/)   (decode sol x) (decode sol y)
-  decode sol (LTH x y)      = liftA2 (<)   (decode sol x) (decode sol y)
-  decode sol (LTHE x y)     = liftA2 (<=)  (decode sol x) (decode sol y)
-  decode sol (EQU x y)      = liftA2 (==)  (decode sol x) (decode sol y)
-  decode sol (Distinct x y) = liftA2 (/=)  (decode sol x) (decode sol y)
-  decode sol (GTHE x y)     = liftA2 (>=)  (decode sol x) (decode sol y)
-  decode sol (GTH x y)      = liftA2 (>)   (decode sol x) (decode sol y)
-  decode sol (Not x)        = fmap   not  (decode sol x)
-  decode sol (And x y)      = liftA2 (&&) (decode sol x) (decode sol y)
-  decode sol (Or x y)       = liftA2 (||) (decode sol x) (decode sol y)
-  decode sol (Impl x y)     = liftA2 (==>) (decode sol x) (decode sol y)
-  decode sol (Xor x y)      = liftA2 xor   (decode sol x) (decode sol y)
-  decode _ Pi               = Just pi
-  decode sol (Sqrt x)       = fmap sqrt  (decode sol x)
-  decode sol (Exp x)        = fmap exp   (decode sol x)
-  decode sol (Sin x)        = fmap sin   (decode sol x)
-  decode sol (Cos x)        = fmap cos   (decode sol x)
-  decode sol (Tan x)        = fmap tan   (decode sol x)
-  decode sol (Asin x)       = fmap asin  (decode sol x)
-  decode sol (Acos x)       = fmap acos  (decode sol x)
-  decode sol (Atan x)       = fmap atan  (decode sol x)
-  decode sol (ToReal x)     = fmap realToFrac (decode sol x)
-  decode sol (ToInt x)      = fmap truncate   (decode sol x)
-  decode sol (IsInt x)      = fmap ((0 ==) . snd . properFraction) (decode sol x)
-  decode sol (Ite p t f)    = liftM3 (\p' t' f' -> if p' then t' else f') (decode sol p) (decode sol t) (decode sol f) 
-  decode sol (BvNot x)      = fmap not (decode sol x)
-  decode sol (BvAnd x y)    = liftA2 (&&) (decode sol x) (decode sol y)
-  decode sol (BvOr x y)     = liftA2 (||) (decode sol x) (decode sol y)
-  decode sol (BvXor x y)    = liftA2 xor (decode sol x) (decode sol y)
-  decode sol (BvNand x y)   = nand <$> sequenceA [decode sol x, decode sol y]
-  decode sol (BvNor x y)    = nor  <$> sequenceA [decode sol x, decode sol y]
-  decode sol (BvNeg x)      = fmap negate (decode sol x)
-  decode sol (BvAdd x y)    = liftA2 (+) (decode sol x) (decode sol y)
-  decode sol (BvSub x y)    = liftA2 (-) (decode sol x) (decode sol y)
-  decode sol (BvMul x y)    = liftA2 (*) (decode sol x) (decode sol y)
-  decode sol (BvuDiv x y)   = liftA2 div (decode sol x) (decode sol y)
-  decode sol (BvuRem x y)   = liftA2 rem (decode sol x) (decode sol y)
-  decode sol (BvShL x y)    = join $ liftA2 bvShL (decode sol x) (decode sol y)
-  decode sol (BvLShR x y)   = join $ liftA2 bvLShR (decode sol x) (decode sol y)
-  decode sol (BvConcat x y) = liftA2 bvConcat (decode sol x) (decode sol y)
-  decode sol (BvRotL i x)   = bvRotL i <$> decode sol x
-  decode sol (BvRotR i x)   = bvRotR i <$> decode sol x
-  decode sol (BvuLT x y)    = liftA2 (<) (decode sol x) (decode sol y)
-  decode sol (BvuLTHE x y)  = liftA2 (<=) (decode sol x) (decode sol y)
-  decode sol (BvuGTHE x y)  = liftA2 (>=) (decode sol x) (decode sol y)
-  decode sol (BvuGT x y)    = liftA2 (>) (decode sol x) (decode sol y)
-  decode _ (ForAll _ _)     = Nothing
-  decode _ (Exists _ _)     = Nothing
+  decode _ (Constant v)         = Just $ unwrapValue v
+  decode sol (Plus x y)         = liftA2 (+)   (decode sol x) (decode sol y)
+  decode sol (Neg x)            = fmap negate  (decode sol x)
+  decode sol (Mul x y)          = liftA2 (*)   (decode sol x) (decode sol y)
+  decode sol (Abs x)            = fmap abs     (decode sol x)
+  decode sol (Mod x y)          = liftA2 mod   (decode sol x) (decode sol y)
+  decode sol (IDiv x y)         = liftA2 div   (decode sol x) (decode sol y)
+  decode sol (Div x y)          = liftA2 (/)   (decode sol x) (decode sol y)
+  decode sol (LTH x y)          = liftA2 (<)   (decode sol x) (decode sol y)
+  decode sol (LTHE x y)         = liftA2 (<=)  (decode sol x) (decode sol y)
+  decode sol (EQU x y)          = liftA2 (==)  (decode sol x) (decode sol y)
+  decode sol (Distinct x y)     = liftA2 (/=)  (decode sol x) (decode sol y)
+  decode sol (GTHE x y)         = liftA2 (>=)  (decode sol x) (decode sol y)
+  decode sol (GTH x y)          = liftA2 (>)   (decode sol x) (decode sol y)
+  decode sol (Not x)            = fmap   not  (decode sol x)
+  decode sol (And x y)          = liftA2 (&&) (decode sol x) (decode sol y)
+  decode sol (Or x y)           = liftA2 (||) (decode sol x) (decode sol y)
+  decode sol (Impl x y)         = liftA2 (==>) (decode sol x) (decode sol y)
+  decode sol (Xor x y)          = liftA2 xor   (decode sol x) (decode sol y)
+  decode _ Pi                   = Just pi
+  decode sol (Sqrt x)           = fmap sqrt  (decode sol x)
+  decode sol (Exp x)            = fmap exp   (decode sol x)
+  decode sol (Sin x)            = fmap sin   (decode sol x)
+  decode sol (Cos x)            = fmap cos   (decode sol x)
+  decode sol (Tan x)            = fmap tan   (decode sol x)
+  decode sol (Asin x)           = fmap asin  (decode sol x)
+  decode sol (Acos x)           = fmap acos  (decode sol x)
+  decode sol (Atan x)           = fmap atan  (decode sol x)
+  decode sol (ToReal x)         = fmap realToFrac (decode sol x)
+  decode sol (ToInt x)          = fmap truncate   (decode sol x)
+  decode sol (IsInt x)          = fmap ((0 ==) . snd . properFraction) (decode sol x)
+  decode sol (Ite p t f)        = liftM3 (\p' t' f' -> if p' then t' else f') (decode sol p) (decode sol t) (decode sol f) 
+  decode sol (BvNot x)          = fmap not (decode sol x)
+  decode sol (BvAnd x y)        = liftA2 (&&) (decode sol x) (decode sol y)
+  decode sol (BvOr x y)         = liftA2 (||) (decode sol x) (decode sol y)
+  decode sol (BvXor x y)        = liftA2 xor (decode sol x) (decode sol y)
+  decode sol (BvNand x y)       = nand <$> sequenceA [decode sol x, decode sol y]
+  decode sol (BvNor x y)        = nor  <$> sequenceA [decode sol x, decode sol y]
+  decode sol (BvNeg x)          = fmap negate (decode sol x)
+  decode sol (BvAdd x y)        = liftA2 (+) (decode sol x) (decode sol y)
+  decode sol (BvSub x y)        = liftA2 (-) (decode sol x) (decode sol y)
+  decode sol (BvMul x y)        = liftA2 (*) (decode sol x) (decode sol y)
+  decode sol (BvuDiv x y)       = liftA2 div (decode sol x) (decode sol y)
+  decode sol (BvuRem x y)       = liftA2 rem (decode sol x) (decode sol y)
+  decode sol (BvShL x y)        = join $ liftA2 bvShL (decode sol x) (decode sol y)
+  decode sol (BvLShR x y)       = join $ liftA2 bvLShR (decode sol x) (decode sol y)
+  decode sol (BvConcat x y)     = liftA2 bvConcat (decode sol x) (decode sol y)
+  decode sol (BvRotL i x)       = bvRotL i <$> decode sol x
+  decode sol (BvRotR i x)       = bvRotR i <$> decode sol x
+  decode sol (BvuLT x y)        = liftA2 (<) (decode sol x) (decode sol y)
+  decode sol (BvuLTHE x y)      = liftA2 (<=) (decode sol x) (decode sol y)
+  decode sol (BvuGTHE x y)      = liftA2 (>=) (decode sol x) (decode sol y)
+  decode sol (BvuGT x y)        = liftA2 (>) (decode sol x) (decode sol y)
+  decode sol (ArrSelect i arr)  = liftA2 select (decode sol i) (decode sol arr)
+  decode sol (ArrStore i x arr) = liftM3 store (decode sol i) (decode sol x) (decode sol arr)
+  decode _ (ForAll _ _)         = Nothing
+  decode _ (Exists _ _)         = Nothing
   
   encode = Constant . wrapValue
 
diff --git a/src/Language/Hasmtlib/Internal/Expr.hs b/src/Language/Hasmtlib/Internal/Expr.hs
index fd00f24..59b17f5 100644
--- a/src/Language/Hasmtlib/Internal/Expr.hs
+++ b/src/Language/Hasmtlib/Internal/Expr.hs
@@ -2,13 +2,16 @@
 {-# 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.Boolean
 import Data.GADT.Compare
+import Data.Map
 import Data.Kind
 import Data.Proxy
 import Data.Coerce
@@ -64,10 +67,6 @@ wrapValue = case sortSing @t of
   SArraySort _ _ -> ArrayValue
 {-# INLINEABLE wrapValue #-}
 
-deriving instance Show (Value t)
-deriving instance Eq   (Value t)
-deriving instance Ord  (Value t)
-
 -- | Singleton for 'SMTSort'.
 data SSMTSort (t :: SMTSort) where
   SIntSort   :: SSMTSort IntSort
@@ -97,12 +96,21 @@ instance GCompare SSMTSort where
     LTI -> GLT
     EQI -> GEQ
     GTI -> GGT
-  gcompare SBoolSort _ = GLT
-  gcompare _ SBoolSort = GGT
-  gcompare SIntSort _  = GLT
-  gcompare _ SIntSort  = GGT
-  gcompare SRealSort _ = GLT
-  gcompare _ SRealSort = 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
@@ -120,6 +128,13 @@ sortSing' _ = sortSing @t
 data SomeKnownSMTSort f where
   SomeKnownSMTSort :: forall (t :: SMTSort) f. KnownSMTSort t => f t -> SomeKnownSMTSort f
 
+data SomeKnownOrdSMTSort f where
+  -- The Ord (HaskellType t) seems off here
+  -- It is - but we need to to parse ArraySorts existentially where Ord needs to hold for the HaskellType of Key-SMTSort
+  -- Composing constraints bloats the code too much
+  -- The Ord (HaskellType t) is not a problem though as long as all rhs of the type-family hold it, which is trivial
+  SomeKnownOrdSMTSort :: forall (t :: SMTSort) f. (KnownSMTSort t, Ord (HaskellType t)) => f t -> SomeKnownOrdSMTSort f
+
 -- | A SMT expression.
 --   For internal use only.
 --   For building expressions use the corresponding instances (Num, Boolean, ...).
@@ -394,5 +409,7 @@ instance Show (Expr t) where
   show (BvuGT x y)          = "(" ++ show x ++ " bvugt " ++ show y ++ ")"
   show (ForAll (Just qv) f) = "(forall " ++ show qv ++ ": " ++ show (f (Var qv)) ++ ")"
   show (ForAll Nothing f)   = "(forall var_-1: " ++ show (f (Var (SMTVar (-1)))) ++ ")"
+  show (ArrSelect i arr)    = "(select " ++ show i ++ " " ++ show arr ++ ")"
+  show (ArrStore i x arr)   = "(select " ++ show i ++ " " ++ show x ++ " " ++ show arr ++ ")"
   show (Exists (Just qv) f) = "(exists " ++ show qv ++ ": " ++ show (f (Var qv)) ++ ")"
   show (Exists Nothing f)   = "(exists var_-1: " ++ show (f (Var (SMTVar (-1)))) ++ ")"
\ No newline at end of file
diff --git a/src/Language/Hasmtlib/Internal/Parser.hs b/src/Language/Hasmtlib/Internal/Parser.hs
index 16cee7c..ea97aa6 100644
--- a/src/Language/Hasmtlib/Internal/Parser.hs
+++ b/src/Language/Hasmtlib/Internal/Parser.hs
@@ -1,3 +1,6 @@
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE LiberalTypeSynonyms #-}
+
 module Language.Hasmtlib.Internal.Parser where
 
 import Prelude hiding (not, (&&), (||), and , or)
@@ -10,6 +13,7 @@ import Language.Hasmtlib.Boolean
 import Language.Hasmtlib.Iteable
 import Language.Hasmtlib.Codec
 import Language.Hasmtlib.Type.Solution
+import Language.Hasmtlib.Type.ArrayMap
 import Data.Bit
 import Data.Coerce
 import Data.Proxy
@@ -54,44 +58,61 @@ smt2ModelParser = do
 
   return $ fromSomeVarSols varSols
 
-parseSomeSol :: Parser (SomeKnownSMTSort SMTVarSol)
+parseSomeSol :: Parser (SomeKnownOrdSMTSort SMTVarSol)
 parseSomeSol = do
   _     <- char '(' >> skipSpace
   _     <- string "define-fun" >> skipSpace
   _     <- string "var_"
   vId   <- decimal @Int
   _     <- skipSpace >> string "()" >> skipSpace
-  (SomeKnownSMTSort someSort) <- parseSomeSort
+  (SomeKnownOrdSMTSort someSort) <- parseSomeSort
   _     <- skipSpace
   expr  <- parseExpr' someSort
   _     <- skipSpace >> char ')'
   case decode mempty expr of
     Nothing    -> fail $ "Solver reponded with solution for var_" ++ show vId ++ " but it contains "
                       ++ "another var. This cannot be parsed and evaluated currently."
-    Just value -> return $ SomeKnownSMTSort $ SMTVarSol (coerce vId) (wrapValue value)
+    Just value -> return $ SomeKnownOrdSMTSort $ SMTVarSol (coerce vId) (wrapValue value)
 {-# INLINEABLE parseSomeSol #-}
 
-parseSomeSort :: Parser (SomeKnownSMTSort SSMTSort)
-parseSomeSort = (string "Bool" *> pure (SomeKnownSMTSort SBoolSort))
-        <|> (string "Int"  *> pure (SomeKnownSMTSort SIntSort))
-        <|> (string "Real" *> pure (SomeKnownSMTSort SRealSort))
+parseSomeSort :: Parser (SomeKnownOrdSMTSort SSMTSort)
+parseSomeSort = (string "Bool" *> pure (SomeKnownOrdSMTSort SBoolSort))
+        <|> (string "Int"  *> pure (SomeKnownOrdSMTSort SIntSort))
+        <|> (string "Real" *> pure (SomeKnownOrdSMTSort SRealSort))
         <|> parseSomeBitVecSort
-  where
-    parseSomeBitVecSort = do
-      _ <- char '(' >> skipSpace >> char '_' >> skipSpace
-      _ <- string "BitVec" >> skipSpace
-      n <- decimal
-      _ <- skipSpace >> char ')'
-      case someNatVal $ fromInteger n of
-        SomeNat pn -> return $ SomeKnownSMTSort $ SBvSort pn
+        <|> parseSomeArraySort
 {-# INLINEABLE parseSomeSort #-}
 
+parseSomeBitVecSort :: Parser (SomeKnownOrdSMTSort SSMTSort)
+parseSomeBitVecSort = do
+  _ <- char '(' >> skipSpace >> char '_' >> skipSpace
+  _ <- string "BitVec" >> skipSpace
+  n <- decimal
+  _ <- skipSpace >> char ')'
+  case someNatVal $ fromInteger n of
+    SomeNat pn -> return $ SomeKnownOrdSMTSort $ SBvSort pn
+{-# INLINEABLE parseSomeBitVecSort #-}
+
+parseSomeArraySort :: Parser (SomeKnownOrdSMTSort SSMTSort)
+parseSomeArraySort = do
+  _ <- char '(' >> skipSpace
+  _ <- string "Array" >> skipSpace
+  (SomeKnownOrdSMTSort keySort)   <- parseSomeSort
+  _ <- skipSpace
+  (SomeKnownOrdSMTSort valueSort) <- parseSomeSort
+  _ <- skipSpace >> char ')'
+  return $ SomeKnownOrdSMTSort $ SArraySort (goProxy keySort) (goProxy valueSort)
+    where
+      goProxy :: forall t. SSMTSort t -> Proxy t
+      goProxy _ = Proxy @t
+{-# INLINEABLE parseSomeArraySort #-}
+
 parseExpr' :: forall prxy t. KnownSMTSort t => prxy t -> Parser (Expr t)
 parseExpr' _ = parseExpr @t
 {-# INLINE parseExpr' #-}
 
 parseExpr :: forall t. KnownSMTSort t => Parser (Expr t)
-parseExpr = var <|> constant <|> smtIte
+parseExpr = var <|> constantExpr <|> smtIte
         <|> case sortSing @t of
               SIntSort  -> unary "abs" abs <|> unary  "-" negate
                       <|> nary "+" sum  <|> binary "-" (-) <|> nary "*" product <|> binary "mod" Mod
@@ -119,6 +140,8 @@ parseExpr = var <|> constant <|> smtIte
                       <|> binary "bvadd" (+)  <|> binary "bvsub" (-) <|> binary "bvmul" (*)
                       <|> binary "bvudiv" BvuDiv <|> binary "bvurem" BvuRem
                       <|> binary "bvshl" BvShL <|> binary "bvlshr" BvLShR
+              SArraySort _ _ -> parseStore
+                      -- TODO: Add compare ops for all (?) array-sorts
 
 var :: Parser (Expr t)
 var = do
@@ -128,17 +151,19 @@ var = do
   return $ Var $ coerce vId
 {-# INLINE var #-}
 
-constant :: forall t. KnownSMTSort t => Parser (Expr t)
-constant = do
-  cval <- case sortSing @t of
-    SIntSort  -> anyValue decimal
-    SRealSort -> anyValue parseRatioDouble <|> parseToRealDouble <|> anyValue rational
-    SBoolSort -> parseBool
-    SBvSort p -> anyBitvector p
-
-  return $ Constant $ wrapValue cval
+constant :: forall t. KnownSMTSort t => Parser (HaskellType t)
+constant = case sortSing @t of
+  SIntSort  -> anyValue decimal
+  SRealSort -> anyValue parseRatioDouble <|> parseToRealDouble <|> anyValue rational
+  SBoolSort -> parseBool
+  SBvSort p -> anyBitvector p
+  SArraySort k v -> constArray k v
 {-# INLINE constant #-}
 
+constantExpr :: forall t. KnownSMTSort t => Parser (Expr t)
+constantExpr = Constant . wrapValue <$> constant @t
+{-# INLINE constantExpr #-}
+
 anyBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n)
 anyBitvector p = binBitvector p <|> hexBitvector p <|> literalBitvector p
 
@@ -169,6 +194,41 @@ literalBitvector _ = do
   return $ fromInteger x
 {-# INLINE literalBitvector #-}
 
+constArray :: forall k v. (KnownSMTSort v, Ord (HaskellType k)) => Proxy k -> Proxy v -> Parser (ConstArray (HaskellType k) (HaskellType v))
+constArray _ _ = do
+  _ <- char '(' >> skipSpace >> char '(' >> skipSpace
+  _ <- string "as" >> skipSpace >> string "const" >> skipSpace
+  _ <- char '(' >> skipWhile (/= ')') >> char ')' >> skipSpace
+  _ <- char ')' >> skipSpace
+  constVal <- constant @v
+  _ <- skipSpace >> char ')'
+
+  return $ asConst constVal
+
+parseSelect :: forall k v. (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Proxy k -> Parser (Expr v)
+parseSelect _ = do
+  _ <- char '(' >> skipSpace
+  _ <- string "select" >> skipSpace
+  arr <- parseExpr @(ArraySort k v)
+  _ <- skipSpace
+  i <- parseExpr @k
+  _ <- skipSpace >> char ')'
+
+  return $ ArrSelect arr i
+
+parseStore :: forall k v. (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Parser (Expr (ArraySort k v))
+parseStore = do
+  _ <- char '(' >> skipSpace
+  _ <- string "store" >> skipSpace
+  arr <- parseExpr @(ArraySort k v)
+  _ <- skipSpace
+  i <- parseExpr @k
+  _ <- skipSpace
+  x <- parseExpr @v
+  _ <- skipSpace >> char ')'
+
+  return $ ArrStore arr i x
+
 unary :: forall t r. KnownSMTSort t => ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
 unary opStr op = do
   _ <- char '(' >> skipSpace
diff --git a/src/Language/Hasmtlib/Internal/ArrayMap.hs b/src/Language/Hasmtlib/Type/ArrayMap.hs
similarity index 85%
rename from src/Language/Hasmtlib/Internal/ArrayMap.hs
rename to src/Language/Hasmtlib/Type/ArrayMap.hs
index 7e1d815..ca9c51f 100644
--- a/src/Language/Hasmtlib/Internal/ArrayMap.hs
+++ b/src/Language/Hasmtlib/Type/ArrayMap.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE UndecidableInstances #-}
 
-module Language.Hasmtlib.Internal.ArrayMap where
+module Language.Hasmtlib.Type.ArrayMap where
 
 import Data.Proxy
 import qualified Data.Map as Map  
@@ -27,4 +28,4 @@ instance Ord k => ArrayMap ConstArray k v where
   select arr i = case Map.lookup i (arr^.stored) of
     Nothing -> viewConst arr
     Just x  -> x
-  store arr i x = arr & stored %~ Map.insert i x
\ No newline at end of file
+  store arr i x = arr & stored %~ Map.insert i x
diff --git a/src/Language/Hasmtlib/Type/Expr.hs b/src/Language/Hasmtlib/Type/Expr.hs
index 5a5781c..2a4840e 100644
--- a/src/Language/Hasmtlib/Type/Expr.hs
+++ b/src/Language/Hasmtlib/Type/Expr.hs
@@ -5,9 +5,10 @@ module Language.Hasmtlib.Type.Expr
  , SMTVar(..), varId
  , HaskellType
  , Value(..), unwrapValue, wrapValue
- , SSMTSort(..), KnownSMTSort(..), sortSing', SomeKnownSMTSort(..)
+ , SSMTSort(..), KnownSMTSort(..), sortSing', SomeKnownSMTSort(..), SomeKnownOrdSMTSort(..)
  , Expr
  , for_all , exists
+ , arrSelect, arrStore
  , module Language.Hasmtlib.Internal.Expr.Num
  )
 where
@@ -48,4 +49,10 @@ for_all = ForAll Nothing
 --   The lambdas 'y' is existentially quantified here.
 --   It will only be scoped for the lambdas body.
 exists :: forall t. KnownSMTSort t => (Expr t -> Expr BoolSort) -> Expr BoolSort
-exists = Exists Nothing
\ No newline at end of file
+exists = Exists Nothing
+
+arrSelect :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v
+arrSelect = ArrSelect
+
+arrStore :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v -> Expr (ArraySort k v)
+arrStore = ArrStore
\ No newline at end of file
diff --git a/src/Language/Hasmtlib/Type/Solution.hs b/src/Language/Hasmtlib/Type/Solution.hs
index cd691cf..34d4081 100644
--- a/src/Language/Hasmtlib/Type/Solution.hs
+++ b/src/Language/Hasmtlib/Type/Solution.hs
@@ -22,7 +22,7 @@ type Solution = DMap SSMTSort IntValueMap
 -- | Newtype for 'IntMap' 'Value' so we can use it as right-hand-side of 'DMap'.
 newtype IntValueMap t = IntValueMap (IntMap (Value t))
   deriving stock Show
-  deriving newtype (Eq, Ord, Semigroup, Monoid)
+  deriving newtype (Semigroup, Monoid)
 
 -- | A solution for a single variable.
 data SMTVarSol (t :: SMTSort) = SMTVarSol
@@ -32,9 +32,9 @@ data SMTVarSol (t :: SMTSort) = SMTVarSol
 $(makeLenses ''SMTVarSol)
 
 -- | Create a 'Solution' from some 'SMTVarSol's.
-fromSomeVarSols :: [SomeKnownSMTSort SMTVarSol] -> Solution
+fromSomeVarSols :: [SomeKnownOrdSMTSort SMTVarSol] -> Solution
 fromSomeVarSols = foldl
-  (\dsol (SomeKnownSMTSort s) -> let sSort = sortSing' s in
+  (\dsol (SomeKnownOrdSMTSort s) -> let sSort = sortSing' s in
     dsol & dmat sSort %~
       (\case
         Nothing -> Just $ IntValueMap $ IMap.singleton (s^.solVar.varId) (s^.solVal)

From 7e5acd6f75642a9c549c1e626dd703af6d04b3c3 Mon Sep 17 00:00:00 2001
From: "Julian.Bruder" <julian.bruder@city-concept-leipzig.de>
Date: Fri, 21 Jun 2024 14:41:52 +0200
Subject: [PATCH 10/15] array-sort: cleaned api

---
 src/Language/Hasmtlib/Codec.hs         |  4 ++--
 src/Language/Hasmtlib/Internal/Expr.hs | 17 +++++++++--------
 src/Language/Hasmtlib/Type/ArrayMap.hs | 17 +++++++++++------
 src/Language/Hasmtlib/Type/Expr.hs     | 12 +++++++-----
 4 files changed, 29 insertions(+), 21 deletions(-)

diff --git a/src/Language/Hasmtlib/Codec.hs b/src/Language/Hasmtlib/Codec.hs
index 4898580..fd082a6 100644
--- a/src/Language/Hasmtlib/Codec.hs
+++ b/src/Language/Hasmtlib/Codec.hs
@@ -99,8 +99,8 @@ instance KnownSMTSort t => Codec (Expr t) where
   decode sol (BvuLTHE x y)      = liftA2 (<=) (decode sol x) (decode sol y)
   decode sol (BvuGTHE x y)      = liftA2 (>=) (decode sol x) (decode sol y)
   decode sol (BvuGT x y)        = liftA2 (>) (decode sol x) (decode sol y)
-  decode sol (ArrSelect i arr)  = liftA2 select (decode sol i) (decode sol arr)
-  decode sol (ArrStore i x arr) = liftM3 store (decode sol i) (decode sol x) (decode sol arr)
+  decode sol (ArrSelect i arr)  = liftA2 arrSelect (decode sol i) (decode sol arr)
+  decode sol (ArrStore i x arr) = liftM3 arrStore (decode sol i) (decode sol x) (decode sol arr)
   decode _ (ForAll _ _)         = Nothing
   decode _ (Exists _ _)         = Nothing
   
diff --git a/src/Language/Hasmtlib/Internal/Expr.hs b/src/Language/Hasmtlib/Internal/Expr.hs
index 59b17f5..69977ae 100644
--- a/src/Language/Hasmtlib/Internal/Expr.hs
+++ b/src/Language/Hasmtlib/Internal/Expr.hs
@@ -21,11 +21,11 @@ import GHC.TypeLits
 
 -- | Sorts in SMTLib2 - used as promoted type (data-kind).
 data SMTSort =
-    BoolSort
-  | IntSort
-  | RealSort
-  | BvSort Nat
-  | ArraySort SMTSort 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
@@ -48,7 +48,7 @@ data Value (t :: SMTSort) where
   BvValue    :: HaskellType (BvSort n) -> Value (BvSort n)
   ArrayValue :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => HaskellType (ArraySort k v) -> Value (ArraySort k v)
 
--- | Unwrap a value.
+-- | Unwrap a value from 'Value'.
 unwrapValue :: Value t -> HaskellType t
 unwrapValue (IntValue  v) = v
 unwrapValue (RealValue v) = v
@@ -57,7 +57,7 @@ unwrapValue (BvValue   v) = v
 unwrapValue (ArrayValue v) = v
 {-# INLINEABLE unwrapValue #-}
 
--- | Wrap a value.
+-- | Wrap a value into 'Value'.
 wrapValue :: forall t. KnownSMTSort t => HaskellType t -> Value t
 wrapValue = case sortSing @t of
   SIntSort  -> IntValue
@@ -118,7 +118,8 @@ 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)
+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
diff --git a/src/Language/Hasmtlib/Type/ArrayMap.hs b/src/Language/Hasmtlib/Type/ArrayMap.hs
index ca9c51f..a9f9f59 100644
--- a/src/Language/Hasmtlib/Type/ArrayMap.hs
+++ b/src/Language/Hasmtlib/Type/ArrayMap.hs
@@ -6,16 +6,21 @@ module Language.Hasmtlib.Type.ArrayMap where
 import Data.Proxy
 import qualified Data.Map as Map  
 import Control.Lens
-  
+
+-- | Class that allows access to a map-like array where specific values are is the default value or overwritten values.
+--   Every index has a value by default.
+--   Values at indices can be overwritten manually.   
 class ArrayMap f k v where
   asConst'   :: Proxy f -> Proxy k -> v -> f k v 
   viewConst  :: f k v -> v
-  select     :: f k v -> k -> v
-  store      :: f k v -> k -> v -> f k v
+  arrSelect     :: f k v -> k -> v
+  arrStore      :: f k v -> k -> v -> f k v
 
+-- | Wrapper for 'asConst'' which hides the 'Proxy'
 asConst :: forall f k v. ArrayMap f k v => v -> f k v
 asConst = asConst' (Proxy @f) (Proxy @k)
-  
+
+-- | A map-like array with a default constant value and partially overwritten values.  
 data ConstArray k v = ConstArray 
   { _arrConst :: v
   , _stored :: Map.Map k v
@@ -25,7 +30,7 @@ $(makeLenses ''ConstArray)
 instance Ord k => ArrayMap ConstArray k v where
   asConst' _ _ x = ConstArray x Map.empty
   viewConst arr = arr^.arrConst
-  select arr i = case Map.lookup i (arr^.stored) of
+  arrSelect arr i = case Map.lookup i (arr^.stored) of
     Nothing -> viewConst arr
     Just x  -> x
-  store arr i x = arr & stored %~ Map.insert i x
+  arrStore arr i x = arr & stored %~ Map.insert i x
diff --git a/src/Language/Hasmtlib/Type/Expr.hs b/src/Language/Hasmtlib/Type/Expr.hs
index 2a4840e..82f8ee8 100644
--- a/src/Language/Hasmtlib/Type/Expr.hs
+++ b/src/Language/Hasmtlib/Type/Expr.hs
@@ -8,7 +8,7 @@ module Language.Hasmtlib.Type.Expr
  , SSMTSort(..), KnownSMTSort(..), sortSing', SomeKnownSMTSort(..), SomeKnownOrdSMTSort(..)
  , Expr
  , for_all , exists
- , arrSelect, arrStore
+ , select, store
  , module Language.Hasmtlib.Internal.Expr.Num
  )
 where
@@ -51,8 +51,10 @@ for_all = ForAll Nothing
 exists :: forall t. KnownSMTSort t => (Expr t -> Expr BoolSort) -> Expr BoolSort
 exists = Exists Nothing
 
-arrSelect :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v
-arrSelect = ArrSelect
+-- | Select a value from an array.
+select :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v
+select = ArrSelect
 
-arrStore :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v -> Expr (ArraySort k v)
-arrStore = ArrStore
\ No newline at end of file
+-- | Store a value in an array.
+store :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v -> Expr (ArraySort k v)
+store = ArrStore
\ No newline at end of file

From ff4b22cf5cc729621ae23d6f5f4b8564fe806f2a Mon Sep 17 00:00:00 2001
From: "Julian.Bruder" <julian.bruder@city-concept-leipzig.de>
Date: Fri, 21 Jun 2024 14:41:59 +0200
Subject: [PATCH 11/15] array-sort: added examples

---
 src/Language/Hasmtlib/Example/Array.hs        | 19 +++++++++++++
 .../Hasmtlib/Example/McCarthyArrayAxioms.hs   | 27 +++++++++++++++++++
 2 files changed, 46 insertions(+)
 create mode 100644 src/Language/Hasmtlib/Example/Array.hs
 create mode 100644 src/Language/Hasmtlib/Example/McCarthyArrayAxioms.hs

diff --git a/src/Language/Hasmtlib/Example/Array.hs b/src/Language/Hasmtlib/Example/Array.hs
new file mode 100644
index 0000000..1ea1f3a
--- /dev/null
+++ b/src/Language/Hasmtlib/Example/Array.hs
@@ -0,0 +1,19 @@
+module Language.Hasmtlib.Example.Array where
+
+import Language.Hasmtlib
+
+main :: IO ()
+main = do
+  res <- solveWith (solver cvc5) $ do
+    setLogic "QF_AUFLIA"
+
+    x <- var @(ArraySort IntSort BoolSort)
+    let y = constant $ asConst false
+
+    assert $ store y 1 true === x
+
+    let x1 = select x 1
+
+    return (x, x1, select x 100)
+
+  print res
diff --git a/src/Language/Hasmtlib/Example/McCarthyArrayAxioms.hs b/src/Language/Hasmtlib/Example/McCarthyArrayAxioms.hs
new file mode 100644
index 0000000..6d8ebbb
--- /dev/null
+++ b/src/Language/Hasmtlib/Example/McCarthyArrayAxioms.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE BlockArguments #-}
+
+module Language.Hasmtlib.Example.McCarthyArrayAxioms where
+
+import Language.Hasmtlib
+
+main :: IO ()
+main = do
+  res <- solveWith (solver cvc5) $ do
+    setLogic "AUFLIRA"
+
+    assert $
+      for_all @(ArraySort RealSort RealSort) \arr ->
+         for_all \i ->
+            for_all \x ->
+               select (store arr i x) i === x 
+    
+    assert $
+      for_all @(ArraySort IntSort BoolSort) \arr ->
+         for_all \i ->
+           for_all \j ->
+             for_all \x ->
+               i /== j ==> (select (store arr i x) j === select arr j)
+
+    return ()
+
+  print res

From 6e833c8de558fb1b47cd3d7b4bf120094c2b90c9 Mon Sep 17 00:00:00 2001
From: "Julian.Bruder" <julian.bruder@city-concept-leipzig.de>
Date: Fri, 21 Jun 2024 14:48:40 +0200
Subject: [PATCH 12/15] array-sort: added docu

---
 src/Language/Hasmtlib/Type/ArrayMap.hs | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

diff --git a/src/Language/Hasmtlib/Type/ArrayMap.hs b/src/Language/Hasmtlib/Type/ArrayMap.hs
index a9f9f59..336ba9c 100644
--- a/src/Language/Hasmtlib/Type/ArrayMap.hs
+++ b/src/Language/Hasmtlib/Type/ArrayMap.hs
@@ -9,12 +9,20 @@ import Control.Lens
 
 -- | Class that allows access to a map-like array where specific values are is the default value or overwritten values.
 --   Every index has a value by default.
---   Values at indices can be overwritten manually.   
+--   Values at indices can be overwritten manually.
+-- 
+--   Based on McCarthy`s basic array theory.
+-- 
+--   Therefore the following axioms must hold:
+-- 
+-- 1. forall A i x: arrSelect (store A i x) == x
+-- 
+-- 2. forall A i j x: i /= j ==> (arrSelect (arrStore A i x) j === arrSelect A j)
 class ArrayMap f k v where
   asConst'   :: Proxy f -> Proxy k -> v -> f k v 
   viewConst  :: f k v -> v
-  arrSelect     :: f k v -> k -> v
-  arrStore      :: f k v -> k -> v -> f k v
+  arrSelect  :: f k v -> k -> v
+  arrStore   :: f k v -> k -> v -> f k v
 
 -- | Wrapper for 'asConst'' which hides the 'Proxy'
 asConst :: forall f k v. ArrayMap f k v => v -> f k v

From 0b38defaf9c310ff5dde792500d9c6b43befb08c Mon Sep 17 00:00:00 2001
From: "Julian.Bruder" <julian.bruder@city-concept-leipzig.de>
Date: Fri, 21 Jun 2024 14:55:48 +0200
Subject: [PATCH 13/15] array-sort: moved SomeKnownOrdSMTSort

---
 src/Language/Hasmtlib/Internal/Expr.hs | 7 -------
 src/Language/Hasmtlib/Type/Expr.hs     | 2 +-
 src/Language/Hasmtlib/Type/Solution.hs | 9 +++++++++
 3 files changed, 10 insertions(+), 8 deletions(-)

diff --git a/src/Language/Hasmtlib/Internal/Expr.hs b/src/Language/Hasmtlib/Internal/Expr.hs
index 69977ae..8e641fb 100644
--- a/src/Language/Hasmtlib/Internal/Expr.hs
+++ b/src/Language/Hasmtlib/Internal/Expr.hs
@@ -129,13 +129,6 @@ sortSing' _ = sortSing @t
 data SomeKnownSMTSort f where
   SomeKnownSMTSort :: forall (t :: SMTSort) f. KnownSMTSort t => f t -> SomeKnownSMTSort f
 
-data SomeKnownOrdSMTSort f where
-  -- The Ord (HaskellType t) seems off here
-  -- It is - but we need to to parse ArraySorts existentially where Ord needs to hold for the HaskellType of Key-SMTSort
-  -- Composing constraints bloats the code too much
-  -- The Ord (HaskellType t) is not a problem though as long as all rhs of the type-family hold it, which is trivial
-  SomeKnownOrdSMTSort :: forall (t :: SMTSort) f. (KnownSMTSort t, Ord (HaskellType t)) => f t -> SomeKnownOrdSMTSort f
-
 -- | A SMT expression.
 --   For internal use only.
 --   For building expressions use the corresponding instances (Num, Boolean, ...).
diff --git a/src/Language/Hasmtlib/Type/Expr.hs b/src/Language/Hasmtlib/Type/Expr.hs
index 82f8ee8..cb51a18 100644
--- a/src/Language/Hasmtlib/Type/Expr.hs
+++ b/src/Language/Hasmtlib/Type/Expr.hs
@@ -5,7 +5,7 @@ module Language.Hasmtlib.Type.Expr
  , SMTVar(..), varId
  , HaskellType
  , Value(..), unwrapValue, wrapValue
- , SSMTSort(..), KnownSMTSort(..), sortSing', SomeKnownSMTSort(..), SomeKnownOrdSMTSort(..)
+ , SSMTSort(..), KnownSMTSort(..), sortSing', SomeKnownSMTSort(..)
  , Expr
  , for_all , exists
  , select, store
diff --git a/src/Language/Hasmtlib/Type/Solution.hs b/src/Language/Hasmtlib/Type/Solution.hs
index 34d4081..92b4a6b 100644
--- a/src/Language/Hasmtlib/Type/Solution.hs
+++ b/src/Language/Hasmtlib/Type/Solution.hs
@@ -31,6 +31,15 @@ data SMTVarSol (t :: SMTSort) = SMTVarSol
   } deriving Show
 $(makeLenses ''SMTVarSol)
 
+-- This is very ugly with the SomeKnownSMTSort in ...Internal.Expr already
+-- Surely theres abstraction possible, but not worth the bloat currently
+data SomeKnownOrdSMTSort f where
+  -- The Ord (HaskellType t) seems off here
+  -- It is - but we need to to parse ArraySorts existentially where Ord needs to hold for the HaskellType of Key-SMTSort
+  -- Composing constraints bloats the code too much
+  -- The Ord (HaskellType t) is not a problem though as long as all rhs of the type-family hold it, which is trivial
+  SomeKnownOrdSMTSort :: forall (t :: SMTSort) f. (KnownSMTSort t, Ord (HaskellType t)) => f t -> SomeKnownOrdSMTSort f
+
 -- | Create a 'Solution' from some 'SMTVarSol's.
 fromSomeVarSols :: [SomeKnownOrdSMTSort SMTVarSol] -> Solution
 fromSomeVarSols = foldl

From 885ec83bb12ae368f0e33f82a3b5cba867735cbf Mon Sep 17 00:00:00 2001
From: "Julian.Bruder" <julian.bruder@city-concept-leipzig.de>
Date: Fri, 21 Jun 2024 15:30:10 +0200
Subject: [PATCH 14/15] array-sort: poly-kinded & flexible-constraint
 existential for SMTSort

---
 src/Language/Hasmtlib/Internal/Expr.hs   | 20 +++++++++++++++++---
 src/Language/Hasmtlib/Internal/Parser.hs | 21 ++++++++++++---------
 src/Language/Hasmtlib/Type/Expr.hs       |  2 +-
 src/Language/Hasmtlib/Type/SMT.hs        |  4 ++--
 src/Language/Hasmtlib/Type/Solution.hs   | 17 ++++++++---------
 5 files changed, 40 insertions(+), 24 deletions(-)

diff --git a/src/Language/Hasmtlib/Internal/Expr.hs b/src/Language/Hasmtlib/Internal/Expr.hs
index 8e641fb..7be005a 100644
--- a/src/Language/Hasmtlib/Internal/Expr.hs
+++ b/src/Language/Hasmtlib/Internal/Expr.hs
@@ -125,9 +125,23 @@ instance (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => KnownSMTSort (
 sortSing' :: forall prxy t. KnownSMTSort t => prxy t -> SSMTSort t
 sortSing' _ = sortSing @t
 
--- | An existential wrapper that hides some 'SMTSort'.
-data SomeKnownSMTSort f where
-  SomeKnownSMTSort :: forall (t :: SMTSort) f. KnownSMTSort t => f t -> SomeKnownSMTSort f
+-- | 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 
 
 -- | A SMT expression.
 --   For internal use only.
diff --git a/src/Language/Hasmtlib/Internal/Parser.hs b/src/Language/Hasmtlib/Internal/Parser.hs
index ea97aa6..a8bbe79 100644
--- a/src/Language/Hasmtlib/Internal/Parser.hs
+++ b/src/Language/Hasmtlib/Internal/Parser.hs
@@ -65,20 +65,20 @@ parseSomeSol = do
   _     <- string "var_"
   vId   <- decimal @Int
   _     <- skipSpace >> string "()" >> skipSpace
-  (SomeKnownOrdSMTSort someSort) <- parseSomeSort
+  (SomeSMTSort someSort) <- parseSomeSort
   _     <- skipSpace
   expr  <- parseExpr' someSort
   _     <- skipSpace >> char ')'
   case decode mempty expr of
     Nothing    -> fail $ "Solver reponded with solution for var_" ++ show vId ++ " but it contains "
                       ++ "another var. This cannot be parsed and evaluated currently."
-    Just value -> return $ SomeKnownOrdSMTSort $ SMTVarSol (coerce vId) (wrapValue value)
+    Just value -> return $ SomeSMTSort $ SMTVarSol (coerce vId) (wrapValue value)
 {-# INLINEABLE parseSomeSol #-}
 
 parseSomeSort :: Parser (SomeKnownOrdSMTSort SSMTSort)
-parseSomeSort = (string "Bool" *> pure (SomeKnownOrdSMTSort SBoolSort))
-        <|> (string "Int"  *> pure (SomeKnownOrdSMTSort SIntSort))
-        <|> (string "Real" *> pure (SomeKnownOrdSMTSort SRealSort))
+parseSomeSort = (string "Bool" *> pure (SomeSMTSort SBoolSort))
+        <|> (string "Int"  *> pure (SomeSMTSort SIntSort))
+        <|> (string "Real" *> pure (SomeSMTSort SRealSort))
         <|> parseSomeBitVecSort
         <|> parseSomeArraySort
 {-# INLINEABLE parseSomeSort #-}
@@ -90,18 +90,18 @@ parseSomeBitVecSort = do
   n <- decimal
   _ <- skipSpace >> char ')'
   case someNatVal $ fromInteger n of
-    SomeNat pn -> return $ SomeKnownOrdSMTSort $ SBvSort pn
+    SomeNat pn -> return $ SomeSMTSort $ SBvSort pn
 {-# INLINEABLE parseSomeBitVecSort #-}
 
 parseSomeArraySort :: Parser (SomeKnownOrdSMTSort SSMTSort)
 parseSomeArraySort = do
   _ <- char '(' >> skipSpace
   _ <- string "Array" >> skipSpace
-  (SomeKnownOrdSMTSort keySort)   <- parseSomeSort
+  (SomeSMTSort keySort)   <- parseSomeSort
   _ <- skipSpace
-  (SomeKnownOrdSMTSort valueSort) <- parseSomeSort
+  (SomeSMTSort valueSort) <- parseSomeSort
   _ <- skipSpace >> char ')'
-  return $ SomeKnownOrdSMTSort $ SArraySort (goProxy keySort) (goProxy valueSort)
+  return $ SomeSMTSort $ SArraySort (goProxy keySort) (goProxy valueSort)
     where
       goProxy :: forall t. SSMTSort t -> Proxy t
       goProxy _ = Proxy @t
@@ -111,6 +111,7 @@ parseExpr' :: forall prxy t. KnownSMTSort t => prxy t -> Parser (Expr t)
 parseExpr' _ = parseExpr @t
 {-# INLINE parseExpr' #-}
 
+-- TODO: Add parseSelect
 parseExpr :: forall t. KnownSMTSort t => Parser (Expr t)
 parseExpr = var <|> constantExpr <|> smtIte
         <|> case sortSing @t of
@@ -166,6 +167,7 @@ constantExpr = Constant . wrapValue <$> constant @t
 
 anyBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n)
 anyBitvector p = binBitvector p <|> hexBitvector p <|> literalBitvector p
+{-# INLINE anyBitvector #-}
 
 binBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n)
 binBitvector p = do
@@ -204,6 +206,7 @@ constArray _ _ = do
   _ <- skipSpace >> char ')'
 
   return $ asConst constVal
+{-# INLINEABLE constArray #-}
 
 parseSelect :: forall k v. (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Proxy k -> Parser (Expr v)
 parseSelect _ = do
diff --git a/src/Language/Hasmtlib/Type/Expr.hs b/src/Language/Hasmtlib/Type/Expr.hs
index cb51a18..2545b0a 100644
--- a/src/Language/Hasmtlib/Type/Expr.hs
+++ b/src/Language/Hasmtlib/Type/Expr.hs
@@ -5,7 +5,7 @@ module Language.Hasmtlib.Type.Expr
  , SMTVar(..), varId
  , HaskellType
  , Value(..), unwrapValue, wrapValue
- , SSMTSort(..), KnownSMTSort(..), sortSing', SomeKnownSMTSort(..)
+ , SSMTSort(..), KnownSMTSort(..), sortSing', SomeSMTSort(..), SomeKnownSMTSort
  , Expr
  , for_all , exists
  , select, store
diff --git a/src/Language/Hasmtlib/Type/SMT.hs b/src/Language/Hasmtlib/Type/SMT.hs
index 523855e..fe7c8b4 100644
--- a/src/Language/Hasmtlib/Type/SMT.hs
+++ b/src/Language/Hasmtlib/Type/SMT.hs
@@ -35,7 +35,7 @@ instance MonadState SMT m => MonadSMT SMT m where
 
   var' p = do
     newVar <- smtvar' p
-    vars %= (|> SomeKnownSMTSort newVar)
+    vars %= (|> SomeSMTSort newVar)
     return $ Var newVar
   {-# INLINEABLE var' #-}
 
@@ -75,5 +75,5 @@ renderAssert = renderUnary "assert"
 {-# INLINEABLE renderAssert #-}
 
 renderVars :: Seq (SomeKnownSMTSort SMTVar) -> Seq Builder
-renderVars = fmap (\(SomeKnownSMTSort v) -> renderDeclareVar v)
+renderVars = fmap (\(SomeSMTSort v) -> renderDeclareVar v)
 {-# INLINEABLE renderVars #-}
diff --git a/src/Language/Hasmtlib/Type/Solution.hs b/src/Language/Hasmtlib/Type/Solution.hs
index 92b4a6b..494a954 100644
--- a/src/Language/Hasmtlib/Type/Solution.hs
+++ b/src/Language/Hasmtlib/Type/Solution.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 module Language.Hasmtlib.Type.Solution where
 
@@ -31,19 +32,17 @@ data SMTVarSol (t :: SMTSort) = SMTVarSol
   } deriving Show
 $(makeLenses ''SMTVarSol)
 
--- This is very ugly with the SomeKnownSMTSort in ...Internal.Expr already
--- Surely theres abstraction possible, but not worth the bloat currently
-data SomeKnownOrdSMTSort f where
-  -- The Ord (HaskellType t) seems off here
-  -- It is - but we need to to parse ArraySorts existentially where Ord needs to hold for the HaskellType of Key-SMTSort
-  -- Composing constraints bloats the code too much
-  -- The Ord (HaskellType t) is not a problem though as long as all rhs of the type-family hold it, which is trivial
-  SomeKnownOrdSMTSort :: forall (t :: SMTSort) f. (KnownSMTSort t, Ord (HaskellType t)) => f t -> SomeKnownOrdSMTSort f
+-- | Alias class for constraint 'Ord' ('HaskellType' t)
+class Ord (HaskellType t) => OrdHaskellType t
+instance Ord (HaskellType t) => OrdHaskellType t
+
+-- | 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.
 fromSomeVarSols :: [SomeKnownOrdSMTSort SMTVarSol] -> Solution
 fromSomeVarSols = foldl
-  (\dsol (SomeKnownOrdSMTSort s) -> let sSort = sortSing' s in
+  (\dsol (SomeSMTSort s) -> let sSort = sortSing' s in
     dsol & dmat sSort %~
       (\case
         Nothing -> Just $ IntValueMap $ IMap.singleton (s^.solVar.varId) (s^.solVal)

From d7b540e1889ec05ed9bb30433598101dd02c9d14 Mon Sep 17 00:00:00 2001
From: "Julian.Bruder" <julian.bruder@city-concept-leipzig.de>
Date: Fri, 21 Jun 2024 15:35:17 +0200
Subject: [PATCH 15/15] array-sort: bump version

---
 hasmtlib.cabal | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/hasmtlib.cabal b/hasmtlib.cabal
index 599203d..60528c2 100644
--- a/hasmtlib.cabal
+++ b/hasmtlib.cabal
@@ -1,7 +1,7 @@
 cabal-version:         3.0
 
 name:                  hasmtlib
-version:               1.0.2
+version:               1.1.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.
@@ -35,7 +35,6 @@ library
                      , Language.Hasmtlib.Internal.Parser
                      , Language.Hasmtlib.Internal.Bitvec
                      , Language.Hasmtlib.Internal.Render
-                     , Language.Hasmtlib.Internal.ArrayMap
                      , Language.Hasmtlib.Solver.Common
                      , Language.Hasmtlib.Solver.CVC5
                      , Language.Hasmtlib.Solver.MathSAT
@@ -48,6 +47,7 @@ library
                      , Language.Hasmtlib.Type.Solution
                      , Language.Hasmtlib.Type.Solver
                      , Language.Hasmtlib.Type.Option
+                     , Language.Hasmtlib.Type.ArrayMap
 
   other-modules:       Language.Hasmtlib.Internal.Expr
                      , Language.Hasmtlib.Internal.Expr.Num