Fix up constant array vals

Data/SBV/Control/Utils.hs

@@ -893,7 +893,7 @@ defaultKindedValue k = CV k $ cvt k
         cvt (KTuple ks)      = CTuple $ map cvt ks
         cvt (KMaybe _)       = CMaybe Nothing
         cvt (KEither k1 _)   = CEither . Left $ cvt k1     -- why not?
-        cvt (KArray  _  k2)  = CArray (const (cvt k2))
+        cvt (KArray  _  k2)  = CArray [] (Just (cvt k2))
 
         -- Tricky case of uninterpreted
         uninterp _ (Just (c:_)) = CUserSort (Just 1, c)

Data/SBV/Core/Concrete.hs

@@ -75,21 +75,21 @@ instance HasKind a => HasKind (RCSet a) where
 -- | A constant value.
 -- Note: If you add a new constructor here, make sure you add the
 -- corresponding equality in the instance "Eq CVal" and "Ord CVal"!
-data CVal = CAlgReal  !AlgReal             -- ^ Algebraic real
-          | CInteger  !Integer             -- ^ Bit-vector/unbounded integer
-          | CFloat    !Float               -- ^ Float
-          | CDouble   !Double              -- ^ Double
-          | CFP       !FP                  -- ^ Arbitrary float
-          | CRational Rational             -- ^ Rational
-          | CChar     !Char                -- ^ Character
-          | CString   !String              -- ^ String
-          | CList     ![CVal]              -- ^ List
-          | CSet      !(RCSet CVal)        -- ^ Set. Can be regular or complemented.
-          | CUserSort !(Maybe Int, String) -- ^ Value of an uninterpreted/user kind. The Maybe Int shows index position for enumerations
-          | CTuple    ![CVal]              -- ^ Tuple
-          | CMaybe    !(Maybe CVal)        -- ^ Maybe
-          | CEither   !(Either CVal CVal)  -- ^ Disjoint union
-          | CArray    !(CVal -> CVal)      -- ^ Arrays are backed by functions concretely
+data CVal = CAlgReal  !AlgReal                      -- ^ Algebraic real
+          | CInteger  !Integer                      -- ^ Bit-vector/unbounded integer
+          | CFloat    !Float                        -- ^ Float
+          | CDouble   !Double                       -- ^ Double
+          | CFP       !FP                           -- ^ Arbitrary float
+          | CRational Rational                      -- ^ Rational
+          | CChar     !Char                         -- ^ Character
+          | CString   !String                       -- ^ String
+          | CList     ![CVal]                       -- ^ List
+          | CSet      !(RCSet CVal)                 -- ^ Set. Can be regular or complemented.
+          | CUserSort !(Maybe Int, String)          -- ^ Value of an uninterpreted/user kind. The Maybe Int shows index position for enumerations
+          | CTuple    ![CVal]                       -- ^ Tuple
+          | CMaybe    !(Maybe CVal)                 -- ^ Maybe
+          | CEither   !(Either CVal CVal)           -- ^ Disjoint union
+          | CArray    ![(CVal, CVal)] !(Maybe CVal) -- ^ Arrays are backed by look-up tables concretely
           deriving G.Data
 
 -- | Assign a rank to constant values, this is structural and helps with ordering
@@ -313,7 +313,7 @@ liftCV _ _ _ _ _ _ _ _ _ _ f _ _ _ (CV _ (CSet      v)) = f v
 liftCV _ _ _ _ _ _ _ _ _ _ _ f _ _ (CV _ (CTuple    v)) = f v
 liftCV _ _ _ _ _ _ _ _ _ _ _ _ f _ (CV _ (CMaybe    v)) = f v
 liftCV _ _ _ _ _ _ _ _ _ _ _ _ _ f (CV _ (CEither   v)) = f v
-liftCV _ _ _ _ _ _ _ _ _ _ _ _ _ _ (CV _ (CArray    _)) = error "Data.SBV: liftCV: Unexpected array constant received. Please report!"
+liftCV _ _ _ _ _ _ _ _ _ _ _ _ _ _ (CV _ CArray{}     ) = error "Data.SBV: liftCV: Unexpected array constant received. Please report!"
 
 -- | Lift a binary function through a 'CV'.
 liftCV2 :: (AlgReal             -> AlgReal             -> b)
@@ -524,7 +524,14 @@ randomCVal k =
                              if i
                                 then CEither . Left  <$> randomCVal k1
                                 else CEither . Right <$> randomCVal k2
-    KArray _ k2        -> CArray . const <$> randomCVal k2
+    KArray k1 k2       -> do l  <- randomRIO (0, 100)
+                             ks <- replicateM l (randomCVal k1)
+                             vs <- replicateM l (randomCVal k2)
+                             d  <- randomIO
+                             def <- if d
+                                       then Just <$> randomCVal k2
+                                       else pure Nothing
+                             return $ CArray (zip ks vs) def
   where
     bounds :: Bool -> Int -> (Integer, Integer)
     bounds False w = (0, 2^w - 1)

Data/SBV/Core/Data.hs

@@ -34,7 +34,7 @@ module Data.SBV.Core.Data
  , SWord, SInt, WordN, IntN
  , SRational
  , SChar, SString, SList
- , SEither, SMaybe, SArray
+ , SEither, SMaybe, SArray, ArrayModel(..)
  , STuple, STuple2, STuple3, STuple4, STuple5, STuple6, STuple7, STuple8
  , RCSet(..), SSet
  , nan, infinity, sNaN, sInfinity, RoundingMode(..), SRoundingMode
@@ -205,11 +205,18 @@ type SEither a b = SBV (Either a b)
 -- | Symbolic 'Maybe'
 type SMaybe a = SBV (Maybe a)
 
--- | Symbolic 'Array'. The underlying representation is a list of key-value pairs, with a possible
--- default for unmapped elements. Note that this type matches the typical models returned by SMT-solvers.
+-- | Underlying type for SMTLib arrays, as a list of key-value pairs, with a possible default
+-- for unmapped elements. Note that this type matches the typical models returned by SMT-solvers.
 -- When we store the array, we do not bother removing earlier writes, so there might be duplicates.
 -- That is, we store the history of the writes.
-type SArray a b = SBV ([(a, b)], Maybe b)
+data ArrayModel a b = ArrayModel [(a, b)] (Maybe b)
+
+-- | The kind of an ArrayModel
+instance (HasKind a, HasKind b) => HasKind (ArrayModel a b) where
+   kindOf _ = KArray (kindOf (Proxy @a)) (kindOf (Proxy @b))
+
+-- | Symbolic 'Array'
+type SArray a b = SBV (ArrayModel a b)
 
 -- | Symbolic 'Data.Set'. Note that we use 'RCSet', which supports
 -- both regular sets and complements, i.e., those obtained from the

Data/SBV/Core/Model.hs

@@ -321,6 +321,14 @@ instance SymVal a => SymVal (Maybe a) where
   fromCV (CV (KMaybe k) (CMaybe (Just x))) = Just $ fromCV $ CV k x
   fromCV bad                               = error $ "SymVal.fromCV (Maybe): Malformed sum received: " ++ show bad
 
+instance (HasKind a, HasKind b, SymVal a, SymVal b) => SymVal (ArrayModel a b) where
+  mkSymVal = genMkSymVar (KArray (kindOf (Proxy @a)) (kindOf (Proxy @b)))
+
+  literal (ArrayModel tbl def) = SBV . SVal knd . Left . CV knd $ CArray [(toCV k, toCV v) | (k, v) <- tbl] (toCV <$> def)
+    where knd = kindOf (Proxy @(ArrayModel a b))
+
+  fromCV bad = error $ "SymVal.fromCV (SArray): Malformed array received: " ++ show bad
+
 instance (Ord a, SymVal a) => SymVal (RCSet a) where
   mkSymVal = genMkSymVar (kindOf (Proxy @(RCSet a)))
 
@@ -3233,14 +3241,14 @@ readArray array key
                    newExpr st kb (SBVApp ReadArray [f, k])
 
          -- return the first value, since we don't bother deleting previous writes
-         lkUp :: Eq a => ([(a, b)], Maybe b) -> a -> Maybe b
-         lkUp (xs, def) k = k `lookup` xs `mplus` def
+         lkUp :: Eq a => ArrayModel a b -> a -> Maybe b
+         lkUp (ArrayModel xs def) k = k `lookup` xs `mplus` def
 
 -- | Writing a value to an array. For the concrete case, we don't bother deleting earlier entries, we keep a history.
 writeArray :: forall key val. (HasKind key, SymVal key, SymVal val, HasKind val) => SArray key val -> SBV key -> SBV val -> SArray key val
 writeArray array key value
-   | Just (tbl, def) <- unliteral array, Just keyVal <- unliteral key, Just val <- unliteral value
-   = literal ((keyVal, val) : tbl, def)
+   | Just (ArrayModel tbl def) <- unliteral array, Just keyVal <- unliteral key, Just val <- unliteral value
+   = literal $ ArrayModel ((keyVal, val) : tbl) def
    | True
    = SBV . SVal k . Right $ cache g
    where kb = kindOf (Proxy @val)