Merge pull request #35 from bruderj15/develop

Develop

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.
@@ -47,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
@@ -55,12 +56,14 @@ library
                      , 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

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

src/Language/Hasmtlib/Codec.hs

@@ -8,17 +8,16 @@ 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
-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 @@ 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 _ (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 @@ 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 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

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

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