90-relation: stole some Ersatz.Relation

hasmtlib.cabal

@@ -56,8 +56,10 @@ library
                      , Language.Hasmtlib.Type.Option
                      , Language.Hasmtlib.Type.ArrayMap
                      , Language.Hasmtlib.Type.Bitvec
+                     , Language.Hasmtlib.Type.Relation
 
-  build-depends:       attoparsec                   >= 0.14.4 && < 1
+  build-depends:       array                        >= 0.5    && < 1
+                     , attoparsec                   >= 0.14.4 && < 1
                      , base                         >= 4.17.2 && < 5
                      , bytestring                   >= 0.11.5 && < 1
                      , containers                   >= 0.6.7  && < 1

src/Language/Hasmtlib.hs

@@ -12,6 +12,7 @@ module Language.Hasmtlib
   , module Language.Hasmtlib.Type.Solution
   , module Language.Hasmtlib.Type.ArrayMap
   , module Language.Hasmtlib.Type.Bitvec
+  , module Language.Hasmtlib.Type.Relation
   , module Language.Hasmtlib.Boolean
   , module Language.Hasmtlib.Codec
   , module Language.Hasmtlib.Counting
@@ -39,6 +40,7 @@ import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Type.ArrayMap
 import Language.Hasmtlib.Type.Bitvec
+import Language.Hasmtlib.Type.Relation
 import Language.Hasmtlib.Boolean
 import Language.Hasmtlib.Codec
 import Language.Hasmtlib.Counting

src/Language/Hasmtlib/Codec.hs

@@ -23,6 +23,7 @@ import Data.Sequence (Seq)
 import Data.IntMap as IM hiding (foldl)
 import Data.Dependent.Map as DMap
 import Data.Tree (Tree)
+import Data.Array (Array, Ix)
 import qualified Data.Text as Text
 import Data.Monoid (Sum, Product, First, Last, Dual)
 import qualified Data.Vector.Sized as V
@@ -182,16 +183,21 @@ instance Codec a => Codec (Dual a)
 instance Codec a => Codec (Identity a)
 
 instance Codec a => Codec (IntMap a) where
-  decode sol = traverse (decode sol)
+  decode = traverse . decode
   encode = fmap encode
 
 instance Codec a => Codec (Seq a) where
-  decode sol = traverse (decode sol)
+  decode = traverse . decode
   encode = fmap encode
 
 instance Codec a => Codec (Map k a) where
   type Decoded (Map k a) = Map k (Decoded a)
-  decode sol = traverse (decode sol)
+  decode = traverse . decode
+  encode = fmap encode
+
+instance (Ix i, Codec e) => Codec (Array i e) where
+  type Decoded (Array i e) = Array i (Decoded e)
+  decode = traverse . decode
   encode = fmap encode
 
 class GCodec f where

src/Language/Hasmtlib/Example/Relation.hs

@@ -0,0 +1,20 @@
+module Language.Hasmtlib.Example.Relation where
+
+import Prelude hiding (not)
+import Language.Hasmtlib
+import Control.Lens
+
+main :: IO ()
+main = do
+  (Sat, Just rel') <- solveWith @SMT (solver opensmt) $ do
+    setLogic "QF_LIA"
+
+    rel <- relation ((0,0), (4,4))
+    assert $ atLeast @IntSort 7 $ elems rel
+    assertMaybe $ do
+      item <- rel^?ix (0,0)
+      return $ item === false
+
+    return rel
+
+  putStrLn $ table rel'

src/Language/Hasmtlib/Type/Relation.hs

@@ -0,0 +1,160 @@
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Language.Hasmtlib.Type.Relation where
+
+import Prelude hiding (and, (&&), any)
+import Language.Hasmtlib.Type.MonadSMT
+import Language.Hasmtlib.Type.SMTSort
+import Language.Hasmtlib.Type.Expr
+import Language.Hasmtlib.Boolean
+import Language.Hasmtlib.Codec
+import Data.Coerce
+import Data.Array (Array, Ix(..))
+import qualified Data.Array as A
+import Control.Monad
+import Control.Lens
+
+-- | @Relation a b@ represents a binary relation \(R \subseteq A \times B \),
+-- where the domain \(A\) is a finite subset of the type @a@,
+-- and the codomain \(B\) is a finite subset of the type @b@.
+--
+-- A relation is stored internally as @Array (a,b) Expr BoolSort@,
+-- so @a@ and @b@ have to be instances of 'Ix',
+-- and both \(A\) and \(B\) are intervals.
+newtype Relation a b = Relation (Array (a, b) (Expr BoolSort))
+  deriving stock Show
+
+instance (Ix a, Ix b) => Codec (Relation a b) where
+  type Decoded (Relation a b) = Array (a, b) Bool
+  decode s (Relation x) = decode s x
+  encode x = Relation $ encode x
+
+instance (Ix a, Ix b, a ~ c, b ~ d) => Each (Relation a b) (Relation c d) (Expr BoolSort) (Expr BoolSort) where
+  each f (Relation arr) = coerce <$> each f arr
+  {-# INLINE each #-}
+
+type instance Index (Relation a b) = (a,b)
+type instance IxValue (Relation a b) = Expr BoolSort
+instance (Ix a, Ix b) => Ixed (Relation a b) where
+  ix i f (Relation arr) = coerce <$> ix i f arr
+  {-# INLINE ix #-}
+
+-- | @relation ((amin,bmin),(amax,mbax))@ constructs an indeterminate relation \(R \subseteq A \times B \)
+-- where \(A\) is @{amin .. amax}@ and \(B\) is @{bmin .. bmax}@.
+relation :: (Ix a, Ix b, MonadSMT s m) =>
+  ((a,b),(a,b))
+  -> m (Relation a b)
+relation bnd = do
+    pairs <- sequence $ do
+        p <- A.range bnd
+        return $ do
+            x <- var
+            return (p, x)
+    return $ build bnd pairs
+
+-- | Constructs an indeterminate relation \(R \subseteq B \times B \)
+-- that is symmetric, i.e., \(\forall x, y \in B: ((x,y) \in R) \rightarrow ((y,x) \in R) \).
+symmetric_relation ::
+  (MonadSMT s m, Ix b) =>
+  ((b, b), (b, b)) -- ^ Since a symmetric relation must be homogeneous, the domain must equal the codomain.
+                   -- Therefore, given bounds @((p,q),(r,s))@, it must hold that @p=q@ and @r=s@.
+  -> m (Relation b b)
+symmetric_relation bnd = do
+    pairs <- sequence $ do
+        (p,q) <- A.range bnd
+        guard $ p <= q
+        return $ do
+            x <- var
+            return $   ((p,q), x)
+                   : [ ((q,p), x) | p /= q ]
+    return $ build bnd $ concat pairs
+
+-- | Constructs a relation \(R \subseteq A \times B \) from a list.
+build :: (Ix a, Ix b)
+      => ((a,b),(a,b))
+      -> [ ((a,b), Expr BoolSort) ] -- ^ A list of tuples, where the first element represents an element
+                           -- \((x,y) \in A \times B \) and the second element is a positive 'Expr' 'BoolSort'
+                           -- if \((x,y) \in R \), or a negative 'Expr' 'BoolSort' if \((x,y) \notin R \).
+      -> Relation a b
+build bnd pairs = Relation $ A.array bnd pairs
+
+-- | Constructs a relation \(R \subseteq A \times B \) from a function.
+buildFrom :: (Ix a, Ix b)
+          => ((a,b),(a,b))
+          -> ((a,b) -> Expr BoolSort) -- ^ A function that assigns a 'Expr' 'BoolSort'-value
+                            -- to each element \((x,y) \in A \times B \).
+          -> Relation a b
+buildFrom bnd p = build bnd $ flip map (A.range bnd) $ \ i -> (i, p i)
+
+-- | Constructs an indeterminate relation \(R \subseteq A \times B\) from a function.
+buildFromM :: (Ix a, Ix b, MonadSMT s m)
+          => ((a,b),(a,b))
+          -> ((a,b) -> m (Expr BoolSort))
+          -> m (Relation a b)
+buildFromM bnd p = do
+    pairs <- sequence $ do
+        i <- A.range bnd
+        return $ do
+            x <- p i
+            return (i, x)
+    return $ build bnd pairs
+
+-- | Constructs the identity relation \(I = \{ (x,x) ~|~ x \in A \} \subseteq A \times A\).
+identity :: (Ix a)
+         => ((a,a),(a,a)) -- ^ Since the identity relation is homogeneous, the domain must equal the codomain.
+                          -- Therefore, given bounds @((p,q),(r,s))@, it must hold that @p=q@ and @r=s@.
+         -> Relation a a
+identity ((a,b),(c,d))
+    | (a,c) == (b,d) = buildFrom ((a,b),(c,d)) (\ (i,j) -> bool $ i == j)
+    | otherwise      = error "The domain must equal the codomain!"
+
+-- | The bounds of the array that correspond to the matrix representation of the given relation.
+bounds :: Relation a b -> ((a,b),(a,b))
+bounds (Relation r) = A.bounds r
+
+-- | The list of indices, where each index represents an element \((x,y) \in A \times B \)
+-- that may be contained in the given relation \(R \subseteq A \times B \).
+indices :: (Ix a, Ix b) => Relation a b -> [(a, b)]
+indices (Relation r) = A.indices r
+
+-- | The list of tuples for the given relation \(R \subseteq A \times B \),
+-- where the first element represents an element \((x,y) \in A \times B \)
+-- and the second element indicates via a 'Expr' 'BoolSort' , if \((x,y) \in R \) or not.
+assocs :: (Ix a, Ix b) => Relation a b -> [((a, b), Expr BoolSort)]
+assocs (Relation r) = A.assocs r
+
+-- | The list of elements of the array
+-- that correspond to the matrix representation of the given relation.
+elems :: Relation a b -> [Expr BoolSort]
+elems (Relation r) = A.elems r
+
+-- | The 'Expr' 'BoolSort'-value for a given element \((x,y) \in A \times B \)
+-- and a given relation \(R \subseteq A \times B \) that indicates
+-- if \((x,y) \in R \) or not.
+(!) :: (Ix a, Ix b) => Relation a b -> (a, b) -> Expr BoolSort
+Relation r ! p = r A.! p
+{-# INLINE (!) #-}
+
+-- | The domain \(A\) of a relation \(R \subseteq A \times B\).
+domain :: Ix a => Relation a b -> [a]
+domain r =
+  let ((x,_),(x',_)) = bounds r
+  in A.range (x,x')
+
+-- | The codomain \(B\) of a relation \(R \subseteq A \times B\).
+codomain :: Ix b => Relation a b -> [b]
+codomain r =
+  let ((_,y),(_,y')) = bounds r
+  in A.range (y,y')
+
+-- | Print a satisfying assignment from an SMT solver, where the assignment is interpreted as a relation.
+-- @putStrLn $ table \</assignment/\>@ corresponds to the matrix representation of this relation.
+table :: (Ix a, Ix b)
+      => Array (a,b) Bool -> String
+table r = unlines $ do
+    let ((a,b),(c,d)) = A.bounds r
+    x <- A.range (a,c)
+    return $ unwords $ do
+        y <- A.range (b,d)
+        return $ if r A.! (x,y) then "*" else "."