Initial version of theory of array support!

examples/grisette-examples.cabal

@@ -1,11 +1,11 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.38.0.
+-- This file has been generated from package.yaml by hpack version 0.38.1.
 --
 -- see: https://github.com/sol/hpack
 
 name:               grisette-examples
-version:            0.13.0.0
+version:            0.13.0.1
 synopsis:           Examples for Grisette
 description:        More examples are available in the
                     [tutorials](https://github.com/lsrcz/grisette/tree/main/tutorials) of

grisette.cabal

@@ -1,6 +1,6 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.37.0.
+-- This file has been generated from package.yaml by hpack version 0.38.1.
 --
 -- see: https://github.com/sol/hpack
 
@@ -116,6 +116,7 @@ library
       Grisette.Internal.Core.Data.UnionBase
       Grisette.Internal.SymPrim.AlgReal
       Grisette.Internal.SymPrim.AllSyms
+      Grisette.Internal.SymPrim.Array
       Grisette.Internal.SymPrim.BV
       Grisette.Internal.SymPrim.FP
       Grisette.Internal.SymPrim.FunInstanceGen
@@ -147,6 +148,7 @@ library
       Grisette.Internal.SymPrim.Quantifier
       Grisette.Internal.SymPrim.SomeBV
       Grisette.Internal.SymPrim.SymAlgReal
+      Grisette.Internal.SymPrim.SymArray
       Grisette.Internal.SymPrim.SymBool
       Grisette.Internal.SymPrim.SymBV
       Grisette.Internal.SymPrim.SymFP
@@ -329,7 +331,7 @@ library
     , mtl >=2.2.2 && <2.4
     , parallel >=3.2.2 && <3.3
     , prettyprinter >=1.5.0 && <1.8
-    , sbv >=8.17 && <13
+    , sbv >=13.4
     , stm ==2.5.*
     , template-haskell >=2.16 && <2.24
     , text >=1.2.4.1 && <2.2
@@ -378,7 +380,7 @@ test-suite doctest
     , mtl >=2.2.2 && <2.4
     , parallel >=3.2.2 && <3.3
     , prettyprinter >=1.5.0 && <1.8
-    , sbv >=8.17 && <13
+    , sbv >=13.4
     , stm ==2.5.*
     , template-haskell >=2.16 && <2.24
     , text >=1.2.4.1 && <2.2
@@ -499,7 +501,7 @@ test-suite spec
     , mtl >=2.2.2 && <2.4
     , parallel >=3.2.2 && <3.3
     , prettyprinter >=1.5.0 && <1.8
-    , sbv >=8.17 && <13
+    , sbv >=13.4
     , stm ==2.5.*
     , template-haskell >=2.16 && <2.24
     , test-framework >=0.8.2 && <0.9

package.yaml

@@ -36,7 +36,7 @@ dependencies:
   - th-compat >= 0.1.2 && < 0.2
   - th-abstraction >= 0.4 && < 0.8
   - array >= 0.5.4 && < 0.6
-  - sbv >= 8.17 && < 13
+  - sbv >= 13.4
   - parallel >= 3.2.2 && < 3.3
   - text >= 1.2.4.1 && < 2.2
   - QuickCheck >= 2.14 && < 2.17

src/Grisette/Internal/Backend/Solving.hs

@@ -264,6 +264,9 @@ import Grisette.Internal.SymPrim.Prim.Term
     pattern SymTerm,
     pattern ToFPTerm,
     pattern XorBitsTerm,
+    pattern SelectTerm,
+    pattern StoreTerm,
+    pattern ConstArrayTerm,
   )
 import Grisette.Internal.SymPrim.SymBool (SymBool (SymBool))
 
@@ -796,6 +799,18 @@ lowerSinglePrimCached t' m' = do
         mode <- goCached qs mode
         arg <- goCached qs arg
         return $ \qst -> sbvToFPTerm @b (mode qst) (arg qst)
+      goCachedIntermediate qs (SelectTerm (arr :: Term arr) key) = withPrim @arr $ do
+        arr' <- goCached qs arr
+        key' <- goCached qs key
+        pure $ \qst -> SBV.readArray (arr' qst) (key' qst)
+      goCachedIntermediate qs (StoreTerm arr key val) = withPrim @a $ do
+        arr' <- goCached qs arr
+        key' <- goCached qs key
+        val' <- goCached qs val
+        pure $ \qst -> SBV.writeArray (arr' qst) (key' qst) (val' qst)
+      goCachedIntermediate qs (ConstArrayTerm _ val) = withPrim @a $ do
+        val' <- goCached qs val
+        pure $ \qst -> SBV.constArray $ val' qst
       goCachedIntermediate _ ConTerm {} = error "Should not happen"
       goCachedIntermediate _ SymTerm {} = error "Should not happen"
       goCachedIntermediate _ ForallTerm {} = error "Should not happen"

src/Grisette/Internal/Core/Data/Class/ITEOp.hs

@@ -33,10 +33,13 @@ import Grisette.Internal.SymPrim.GeneralFun
 import Grisette.Internal.SymPrim.Prim.SomeTerm (SomeTerm (SomeTerm))
 import Grisette.Internal.SymPrim.Prim.Term
   ( SupportedPrim (pevalITETerm),
+    SupportedNonFuncPrim,
+    LinkedRep,
     TypedConstantSymbol,
     symTerm,
   )
 import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal (SymAlgReal))
+import Grisette.Internal.SymPrim.SymArray (SymArray (SymArray))
 import Grisette.Internal.SymPrim.SymBV
   ( SymIntN (SymIntN),
     SymWordN (SymWordN),
@@ -93,6 +96,15 @@ ITEOP_FUN((=->), (=~>), SymTabularFun)
 ITEOP_FUN((-->), (-~>), SymGeneralFun)
 #endif
 
+instance
+  ( SupportedNonFuncPrim ck,
+    SupportedNonFuncPrim cv,
+    LinkedRep ck sk,
+    LinkedRep cv sv
+  ) =>
+  ITEOp (SymArray sk sv) where
+  symIte (SymBool c) (SymArray t) (SymArray f) = SymArray $ pevalITETerm c t f
+
 instance ITEOp (a --> b) where
   symIte
     (SymBool c)

src/Grisette/Internal/Internal/Impl/Core/Data/Class/EvalSym.hs

@@ -75,6 +75,7 @@ import Grisette.Internal.Internal.Decl.Core.Data.Class.EvalSym
     evalSym1,
   )
 import Grisette.Internal.SymPrim.AlgReal (AlgReal)
+import Grisette.Internal.SymPrim.Array (Array)
 import Grisette.Internal.SymPrim.BV (IntN, WordN)
 import Grisette.Internal.SymPrim.FP
   ( FP,
@@ -86,9 +87,12 @@ import Grisette.Internal.SymPrim.GeneralFun (type (-->) (GeneralFun))
 import Grisette.Internal.SymPrim.Prim.Model (evalTerm)
 import Grisette.Internal.SymPrim.Prim.Term
   ( SymRep (SymType),
+    SupportedNonFuncPrim,
+    LinkedRep,
     someTypedSymbol,
   )
 import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal (SymAlgReal))
+import Grisette.Internal.SymPrim.SymArray (SymArray (SymArray))
 import Grisette.Internal.SymPrim.SymBV
   ( SymIntN (SymIntN),
     SymWordN (SymWordN),
@@ -137,6 +141,7 @@ CONCRETE_EVALUATESYM(Ordering)
 CONCRETE_EVALUATESYM_BV(IntN)
 CONCRETE_EVALUATESYM_BV(WordN)
 CONCRETE_EVALUATESYM(AlgReal)
+CONCRETE_EVALUATESYM((Array k v))
 #endif
 
 instance EvalSym (Proxy a) where
@@ -186,6 +191,15 @@ instance (ValidFP eb sb) => EvalSym (SymFP eb sb) where
   evalSym fillDefault model (SymFP t) =
     SymFP $ evalTerm fillDefault model HS.empty t
 
+instance
+  ( SupportedNonFuncPrim ck,
+    SupportedNonFuncPrim cv,
+    LinkedRep ck sk,
+    LinkedRep cv sv
+  ) =>
+  EvalSym (SymArray sk sv) where
+  evalSym fill model (SymArray t) = SymArray $ evalTerm fill model HS.empty t
+
 derive
   [ ''(),
     ''AssertionError,

src/Grisette/Internal/Internal/Impl/Core/Data/Class/Mergeable.hs

@@ -90,6 +90,7 @@ import Grisette.Internal.Internal.Decl.Core.Data.Class.Mergeable
     wrapStrategy,
   )
 import Grisette.Internal.SymPrim.AlgReal (AlgReal, AlgRealPoly, RealPoint)
+import Grisette.Internal.SymPrim.Array (Array)
 import Grisette.Internal.SymPrim.BV
   ( IntN,
     WordN,
@@ -103,6 +104,7 @@ import Grisette.Internal.SymPrim.FP
   )
 import Grisette.Internal.SymPrim.GeneralFun (type (-->))
 import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal)
+import Grisette.Internal.SymPrim.SymArray (SymArray)
 import Grisette.Internal.SymPrim.SymBV (SymIntN, SymWordN)
 import Grisette.Internal.SymPrim.SymFP (SymFP, SymFPRoundingMode)
 import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>))
@@ -111,6 +113,7 @@ import Grisette.Internal.SymPrim.SymTabularFun (type (=~>))
 import Grisette.Internal.SymPrim.TabularFun (type (=->))
 import Grisette.Internal.TH.Derivation.Derive (derive)
 import Unsafe.Coerce (unsafeCoerce)
+import Grisette.Internal.SymPrim.Prim.Internal.Term (SupportedNonFuncPrim, LinkedRep)
 
 #define CONCRETE_ORD_MERGEABLE(type) \
 instance Mergeable type where \
@@ -175,6 +178,9 @@ instance Mergeable (a =-> b) where
 instance Mergeable (a --> b) where
   rootStrategy = SimpleStrategy symIte
 
+instance Mergeable (Array k v) where
+  rootStrategy = NoStrategy
+
 #define MERGEABLE_SIMPLE(symtype) \
 instance Mergeable symtype where \
   rootStrategy = SimpleStrategy symIte
@@ -197,6 +203,15 @@ MERGEABLE_FUN((=->), (=~>), SymTabularFun)
 MERGEABLE_FUN((-->), (-~>), SymGeneralFun)
 #endif
 
+instance
+  ( SupportedNonFuncPrim ck,
+    SupportedNonFuncPrim cv,
+    LinkedRep ck sk,
+    LinkedRep cv sv
+  ) =>
+  Mergeable (SymArray sk sv) where
+  rootStrategy = SimpleStrategy $ symIte
+
 instance (ValidFP eb sb) => Mergeable (SymFP eb sb) where
   rootStrategy = SimpleStrategy symIte
 

src/Grisette/Internal/Internal/Impl/Core/Data/Class/SimpleMergeable.hs

@@ -78,10 +78,11 @@ import Grisette.Internal.Internal.Decl.Core.Data.Class.SimpleMergeable
 import Grisette.Internal.Internal.Impl.Core.Data.Class.TryMerge ()
 import Grisette.Internal.SymPrim.FP (ValidFP)
 import Grisette.Internal.SymPrim.GeneralFun (freshArgSymbol, substTerm, type (-->) (GeneralFun))
-import Grisette.Internal.SymPrim.Prim.Internal.Term (SupportedPrim (pevalITETerm), symTerm)
+import Grisette.Internal.SymPrim.Prim.Internal.Term (SupportedPrim (pevalITETerm), LinkedRep, symTerm)
 import Grisette.Internal.SymPrim.Prim.SomeTerm (SomeTerm (SomeTerm))
-import Grisette.Internal.SymPrim.Prim.Term (TypedConstantSymbol)
+import Grisette.Internal.SymPrim.Prim.Term (TypedConstantSymbol, SupportedNonFuncPrim)
 import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal (SymAlgReal))
+import Grisette.Internal.SymPrim.SymArray (SymArray (SymArray))
 import Grisette.Internal.SymPrim.SymBV
   ( SymIntN (SymIntN),
     SymWordN (SymWordN),
@@ -559,6 +560,15 @@ SIMPLE_MERGEABLE_FUN((=->), (=~>), SymTabularFun)
 SIMPLE_MERGEABLE_FUN((-->), (-~>), SymGeneralFun)
 #endif
 
+instance
+  ( SupportedNonFuncPrim ck,
+    SupportedNonFuncPrim cv,
+    LinkedRep ck sk,
+    LinkedRep cv sv
+  ) =>
+  SimpleMergeable (SymArray sk sv) where
+  mrgIte (SymBool c) (SymArray t) (SymArray f) = SymArray $ pevalITETerm c t f
+
 instance SimpleMergeable (a --> b) where
   mrgIte
     (SymBool c)

src/Grisette/Internal/Internal/Impl/Core/Data/Class/SymEq.hs

@@ -80,8 +80,9 @@ import Grisette.Internal.SymPrim.FP
   )
 import Grisette.Internal.SymPrim.Prim.Term
   ( SupportedPrim (pevalDistinctTerm),
+    LinkedRep (underlyingTerm, wrapTerm),
+    SupportedNonFuncPrim,
     pevalEqTerm,
-    underlyingTerm,
   )
 import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal (SymAlgReal))
 import Grisette.Internal.SymPrim.SymBV
@@ -95,6 +96,7 @@ import Grisette.Internal.SymPrim.SymFP
   )
 import Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger))
 import Grisette.Internal.TH.Derivation.Derive (derive)
+import Grisette.Internal.SymPrim.SymArray (SymArray)
 
 #define CONCRETE_SEQ(type) \
 instance SymEq type where \
@@ -185,6 +187,15 @@ instance (ValidFP eb sb) => SymEq (SymFP eb sb) where
   (SymFP l) .== (SymFP r) = SymBool $ pevalEqTerm l r
   {-# INLINE (.==) #-}
 
+instance
+  ( SupportedNonFuncPrim ck,
+    SupportedNonFuncPrim cv,
+    LinkedRep ck sk,
+    LinkedRep cv sv
+  ) =>
+  SymEq (SymArray sk sv) where
+  lhs .== rhs = wrapTerm $ pevalEqTerm (underlyingTerm lhs) (underlyingTerm rhs)
+
 derive
   [ ''(),
     ''AssertionError,

src/Grisette/Internal/Internal/Impl/Core/Data/Class/SymOrd.hs

@@ -100,10 +100,7 @@ import Grisette.Internal.SymPrim.SymBV
     SymWordN (SymWordN),
   )
 import Grisette.Internal.SymPrim.SymBool (SymBool (SymBool))
-import Grisette.Internal.SymPrim.SymFP
-  ( SymFP (SymFP),
-    SymFPRoundingMode (SymFPRoundingMode),
-  )
+import Grisette.Internal.SymPrim.SymFP (SymFP (SymFP))
 import Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger))
 import Grisette.Internal.TH.Derivation.Derive (derive)
 
@@ -254,7 +251,6 @@ instance SymOrd SymBool where
 #if 1
 SORD_SIMPLE(SymInteger)
 SORD_SIMPLE(SymAlgReal)
-SORD_SIMPLE(SymFPRoundingMode)
 SORD_BV(SymIntN)
 SORD_BV(SymWordN)
 #endif

src/Grisette/Internal/SymPrim/Array.hs

@@ -0,0 +1,73 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveLift #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE ImportQualifiedPost #-}
+
+-- |
+-- Module      :   Grisette.Internal.SymPrim.Array
+-- Copyright   :   (c) Sirui Lu 2021-2023
+-- License     :   BSD-3-Clause (see the LICENSE file)
+--
+-- Maintainer  :   siruilu@cs.washington.edu
+-- Stability   :   Experimental
+-- Portability :   GHC only
+module Grisette.Internal.SymPrim.Array
+  ( Array (..)
+  , const
+  , select
+  , store
+  ) where
+
+import Control.DeepSeq (NFData)
+import Data.Binary qualified as Binary
+import Data.Bytes.Serial (Serial (serialize, deserialize))
+import Data.Hashable (Hashable)
+import Data.HashMap.Strict qualified as HM
+import Data.Serialize qualified as Cereal
+import GHC.Generics (Generic)
+import Language.Haskell.TH.Syntax (Lift)
+import Prelude (Show, Eq, Ord)
+
+-- TODO: The equality of this array model is incorrect. The easy solution is
+-- to disallow it entirely. Alternatively, I already have a version with a
+-- working equality check. It works by canonicalising the array.
+--
+-- Canonicalisation will not happen for keys with an infinite domain and
+-- realistically also not for keys with a sufficiently large domain. In fact,
+-- we avoid tracking information for canonicalisation in these cases altogether!
+-- The main gripe with this is that at that point is that insertions do require
+-- keys for which we know both their cardinality and can enumerate their domain.
+-- The latter we could restrict to only enumerable domains given a finite
+-- cardinality with type-level shenanigans, but still.
+--
+-- Yet another alternative would be to simply accept that we cannot conclude
+-- inequality if one of the arrays would require canonicalisation? Then we don't
+-- need the additional typeclass constraints. This way, we could still perform
+-- normalisation of most terms.
+data Array k v = Array (HM.HashMap k v) v
+  deriving (Show, Eq, Ord, Generic, Lift, Hashable, NFData)
+
+instance (Hashable k, Serial k, Serial v) => Serial (Array k v)
+
+instance (Hashable k, Serial k, Serial v) => Cereal.Serialize (Array k v) where
+  put = serialize
+  get = deserialize
+
+instance (Hashable k, Serial k, Serial v) => Binary.Binary (Array k v) where
+  put = serialize
+  get = deserialize
+
+-- TODO: Perhaps it is nice to make this a typeclass and give it names that do
+-- not require qualified imports? I don't necessarily mind the qualified import,
+-- but we'll see what the library author thinks.
+const :: forall k v. v -> Array k v
+const = Array HM.empty
+
+select :: forall k v. Hashable k => Array k v -> k -> v
+select (Array entries root) key = HM.lookupDefault root key entries
+
+store :: forall k v. Hashable k => Array k v -> k -> v -> Array k v
+store (Array entries root) key value = do
+  let entries' = HM.insert key value entries
+  Array entries' root