hasmtlib 1.0.2 → 1.1.0

raw patch · 12 files changed

+471/−248 lines, 12 filesdep +dependent-mapdep +somePVP ok

version bump matches the API change (PVP)

Dependencies added: dependent-map, some

API changes (from Hackage documentation)

Files

• hasmtlib.cabal +4/−1
• src/Language/Hasmtlib.hs +2/−0
• src/Language/Hasmtlib/Codec.hs +43/−56
• src/Language/Hasmtlib/Internal/Expr.hs +214/−126
• src/Language/Hasmtlib/Internal/Parser.hs +108/−50
• src/Language/Hasmtlib/Solver/CVC5.hs +0/−2
• src/Language/Hasmtlib/Solver/Z3.hs +0/−2
• src/Language/Hasmtlib/Type/ArrayMap.hs +44/−0
• src/Language/Hasmtlib/Type/Expr.hs +11/−2
• src/Language/Hasmtlib/Type/Pipe.hs +9/−2
• src/Language/Hasmtlib/Type/SMT.hs +2/−2
• src/Language/Hasmtlib/Type/Solution.hs +34/−5

@@ -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.@@ -47,6 +47,7 @@                      , 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@@ -55,12 +56,14 @@                      , base                         >= 4.17.2 && < 5                      , bytestring                   >= 0.11.5 && < 1                      , containers                   >= 0.6.7  && < 1+                     , dependent-map                >= 0.4    && < 1                      , 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

@@ -7,6 +7,7 @@   , 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.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

@@ -8,17 +8,16 @@ 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-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.@@ -43,57 +42,42 @@ -- | 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 _ (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 (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)@@ -115,8 +99,11 @@   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 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+     encode = Constant . wrapValue  instance Codec () where

@@ -2,12 +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@@ -16,70 +20,129 @@ import GHC.TypeLits  -- | Sorts in SMTLib2 - used as promoted type (data-kind).-data SMTSort = IntSort | RealSort | BoolSort | BvSort Nat+data SMTSort =+    BoolSort                      -- ^ Sort of Bool+  | IntSort                       -- ^ Sort of Int+  | RealSort                      -- ^ Sort of Real+  | BvSort Nat                    -- ^ Sort of BitVec with length n+  | ArraySort SMTSort SMTSort     -- ^ Sort of Array with indices k and values v  -- | An internal SMT variable with a phantom-type which holds an 'Int' as it's identifier. type role SMTVar phantom newtype SMTVar (t :: SMTSort) = SMTVar { _varId :: Int } deriving (Show, Eq, Ord) $(makeLenses ''SMTVar) --- | Injective type-family that computes the Haskell 'Type' of 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) --- | Unwrap a value.+-- | Unwrap a value from 'Value'. unwrapValue :: Value t -> HaskellType t 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.+-- | Wrap a value into 'Value'. wrapValue :: forall t. KnownSMTSort t => HaskellType t -> Value t wrapValue = case sortSing @t of   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) +instance GEq SSMTSort where+  geq SIntSort SIntSort       = Just Refl+  geq SRealSort SRealSort     = Just Refl+  geq SBoolSort SBoolSort     = Just Refl+  geq (SBvSort n) (SBvSort m) = case sameNat n m of+    Just Refl -> Just Refl+    Nothing   -> Nothing+  geq _ _                     = Nothing++instance GCompare SSMTSort where+  gcompare SBoolSort SBoolSort     = GEQ+  gcompare SIntSort SIntSort       = GEQ+  gcompare SRealSort SRealSort     = GEQ+  gcompare (SBvSort n) (SBvSort m) = case cmpNat n m of+    LTI -> GLT+    EQI -> GEQ+    GTI -> GGT+  gcompare (SArraySort k v) (SArraySort k' v') = case gcompare (sortSing' k) (sortSing' k') of+    GLT -> GLT+    GEQ -> case gcompare (sortSing' v) (sortSing' v') of+      GLT -> GLT+      GEQ -> GEQ+      GGT -> GGT+    GGT -> GGT+  gcompare SBoolSort _        = GLT+  gcompare _ SBoolSort        = GGT+  gcompare SIntSort _         = GLT+  gcompare _ SIntSort         = GGT+  gcompare SRealSort _        = GLT+  gcompare _ SRealSort        = GGT+  gcompare (SArraySort _ _) _ = GLT+  gcompare _ (SArraySort _ _) = GGT+ -- | Compute singleton 'SSMTSort' from it's promoted type 'SMTSort'. class    KnownSMTSort (t :: SMTSort)           where sortSing :: SSMTSort t instance KnownSMTSort IntSort                  where sortSing = SIntSort instance KnownSMTSort RealSort                 where sortSing = SRealSort instance KnownSMTSort BoolSort                 where sortSing = SBoolSort instance KnownNat n => KnownSMTSort (BvSort n) where sortSing = SBvSort (Proxy @n)+instance (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => KnownSMTSort (ArraySort k v) where+   sortSing = SArraySort (Proxy @k) (Proxy @v) --- | An existential wrapper that hides some 'SMTSort'.-data SomeKnownSMTSort f where-  SomeKnownSMTSort :: forall (t :: SMTSort) f. KnownSMTSort t => f t -> SomeKnownSMTSort f+-- | Wrapper for 'sortSing' which takes a 'Proxy'+sortSing' :: forall prxy t. KnownSMTSort t => prxy t -> SSMTSort t+sortSing' _ = sortSing @t +-- | AllC ensures that a list of constraints is applied to a poly-kinded 'Type' k+-- +-- @+-- AllC '[]       k = ()+-- AllC (c ': cs) k = (c k, AllC cs k)+-- @ +type AllC :: [k -> Constraint] -> k -> Constraint+type family AllC cs k :: Constraint where+  AllC '[]       k = ()+  AllC (c ': cs) k = (c k, AllC cs k)++-- | An existential wrapper that hides some 'SMTSort' and a list of 'Constraint's holding for it.+data SomeSMTSort cs f where+  SomeSMTSort :: forall cs f (t :: SMTSort). AllC cs t => f t -> SomeSMTSort cs f++-- | An existential wrapper that hides some known 'SMTSort'.+type SomeKnownSMTSort f = SomeSMTSort '[KnownSMTSort] f + -- | A SMT expression. --   For internal use only. --   For building expressions use the corresponding instances (Num, Boolean, ...).@@ -108,47 +171,50 @@   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+  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+  ToReal    :: Expr IntSort  -> Expr RealSort+  ToInt     :: Expr RealSort -> Expr IntSort+  IsInt     :: Expr RealSort -> Expr BoolSort -  Ite      :: Expr BoolSort -> Expr t -> Expr t -> Expr t+  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+  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+  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   {-# INLINE bool #-}@@ -182,22 +248,35 @@   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)+  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 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 (IntValue x))  = render x-  render (Constant (RealValue x)) = render x-  render (Constant (BoolValue x)) = render x-  render (Constant (BvValue   v)) = "#b" <> render v+  render (Var v)      = render v+  render (Constant c) = render c    render (Plus x y)   = renderBinary "+" x y   render (Neg x)      = renderUnary  "-" x@@ -258,6 +337,9 @@   render (BvuGTHE x y)      = renderBinary "bvuge"  (render x) (render y)   render (BvuGT x y)        = renderBinary "bvugt"  (render x) (render y) +  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 @@ -271,65 +353,71 @@     expr = render $ f $ Var qvar renderQuantifier _ Nothing _ = mempty +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+ 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)))) ++ ")"+  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 (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)))) ++ ")"

@@ -1,4 +1,5 @@-{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE ImpredicativeTypes #-}+{-# LANGUAGE LiberalTypeSynonyms #-}  module Language.Hasmtlib.Internal.Parser where @@ -12,6 +13,7 @@ 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@@ -20,7 +22,6 @@ 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 +48,7 @@   varSols <- many $ parseSomeSol <* skipSpace   _       <- (skipSpace >> char ')' >> skipSpace) <|> skipSpace -  return $ fromSomeList varSols+  return $ fromSomeVarSols varSols  smt2ModelParser :: Parser Solution smt2ModelParser = do@@ -55,46 +56,64 @@   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))--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)+  return $ fromSomeVarSols varSols -parseSol :: forall t. KnownSMTSort t => Parser (SMTVarSol t)-parseSol = do+parseSomeSol :: Parser (SomeKnownOrdSMTSort SMTVarSol)+parseSomeSol = do   _     <- char '(' >> skipSpace   _     <- string "define-fun" >> skipSpace   _     <- string "var_"   vId   <- decimal @Int   _     <- skipSpace >> string "()" >> skipSpace-  _     <- string $ toStrict $ toLazyByteString $ render (sortSing @t)+  (SomeSMTSort 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 $ SomeSMTSort $ SMTVarSol (coerce vId) (wrapValue value)+{-# INLINEABLE parseSomeSol #-} +parseSomeSort :: Parser (SomeKnownOrdSMTSort SSMTSort)+parseSomeSort = (string "Bool" *> pure (SomeSMTSort SBoolSort))+        <|> (string "Int"  *> pure (SomeSMTSort SIntSort))+        <|> (string "Real" *> pure (SomeSMTSort SRealSort))+        <|> parseSomeBitVecSort+        <|> 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 $ SomeSMTSort $ SBvSort pn+{-# INLINEABLE parseSomeBitVecSort #-}++parseSomeArraySort :: Parser (SomeKnownOrdSMTSort SSMTSort)+parseSomeArraySort = do+  _ <- char '(' >> skipSpace+  _ <- string "Array" >> skipSpace+  (SomeSMTSort keySort)   <- parseSomeSort+  _ <- skipSpace+  (SomeSMTSort valueSort) <- parseSomeSort+  _ <- skipSpace >> char ')'+  return $ SomeSMTSort $ 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' #-}++-- TODO: Add parseSelect 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@@ -115,15 +134,15 @@                       <|> 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                       <|> 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@@ -131,21 +150,24 @@   vId <- decimal @Int    return $ Var $ coerce vId-{-# INLINEABLE var #-}+{-# 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+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 #-} -  return $ Constant $ wrapValue cval-{-# INLINEABLE 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+{-# INLINE anyBitvector #-}  binBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n) binBitvector p = do@@ -161,7 +183,7 @@ hexBitvector _ = do   _ <- string "#x" >> skipSpace   fromInteger <$> hexadecimal-{-# INLINEABLE hexBitvector #-}+{-# INLINE hexBitvector #-}  literalBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n) literalBitvector _ = do@@ -172,8 +194,44 @@   _ <- skipWhile (/= ')') >> char ')'    return $ fromInteger x-{-# INLINEABLE literalBitvector #-}+{-# 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+{-# INLINEABLE constArray #-}++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@@ -182,7 +240,7 @@   _ <- 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@@ -193,7 +251,7 @@   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@@ -202,11 +260,11 @@   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@@ -263,7 +321,7 @@   _ <- skipSpace >> char ')'    return $ negate val-{-# INLINEABLE negativeValue #-}+{-# INLINE negativeValue #-}  parseRatioDouble :: Parser Double parseRatioDouble = do

@@ -3,7 +3,5 @@ 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 = [] }

@@ -3,8 +3,6 @@ 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 

@@ -0,0 +1,44 @@+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}++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.+-- +--   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++-- | 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+  } 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+  arrSelect arr i = case Map.lookup i (arr^.stored) of+    Nothing -> viewConst arr+    Just x  -> x+  arrStore arr i x = arr & stored %~ Map.insert i x

@@ -2,12 +2,13 @@  module Language.Hasmtlib.Type.Expr  ( SMTSort(..)- , SMTVar(..)+ , SMTVar(..), varId  , HaskellType  , Value(..), unwrapValue, wrapValue- , SSMTSort(..), KnownSMTSort(..), SomeKnownSMTSort(..)+ , SSMTSort(..), KnownSMTSort(..), sortSing', SomeSMTSort(..), SomeKnownSMTSort  , Expr  , for_all , exists+ , select, store  , module Language.Hasmtlib.Internal.Expr.Num  ) where@@ -49,3 +50,11 @@ --   It will only be scoped for the lambdas body. exists :: forall t. KnownSMTSort t => (Expr t -> Expr BoolSort) -> Expr BoolSort exists = Exists Nothing++-- | Select a value from an array.+select :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v+select = ArrSelect++-- | 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

@@ -12,7 +12,8 @@ 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 @@       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

@@ -35,7 +35,7 @@    var' p = do     newVar <- smtvar' p-    vars %= (|> SomeKnownSMTSort newVar)+    vars %= (|> SomeSMTSort newVar)     return $ Var newVar   {-# INLINEABLE var' #-} @@ -75,5 +75,5 @@ {-# INLINEABLE renderAssert #-}  renderVars :: Seq (SomeKnownSMTSort SMTVar) -> Seq Builder-renderVars = fmap (\(SomeKnownSMTSort v) -> renderDeclareVar v)+renderVars = fmap (\(SomeSMTSort v) -> renderDeclareVar v) {-# INLINEABLE renderVars #-}

@@ -1,9 +1,14 @@+{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE UndecidableInstances #-}  module Language.Hasmtlib.Type.Solution where  import Language.Hasmtlib.Type.Expr-import Data.IntMap+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.@@ -12,12 +17,36 @@ -- | 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 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 (Semigroup, Monoid)+ -- | A solution for a single variable.-data SMTVarSol (t :: SMTSort) = 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)++-- | 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 (SomeSMTSort s) -> let sSort = sortSing' s in+    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+      )+  )+  mempty