ersatz 0.4.12 → 0.4.13

raw patch · 10 files changed

+270/−31 lines, 10 filesdep ~bytestringPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: bytestring

API changes (from Hackage documentation)

Files

• CHANGELOG.md +6/−0
• ersatz.cabal +1/−1
• examples/regexp-grid/RegexpGrid/Problem.hs +5/−2
• examples/sudoku/Sudoku/Problem.hs +2/−1
• src/Ersatz/Bits.hs +34/−11
• src/Ersatz/Relation.hs +13/−0
• src/Ersatz/Relation/Data.hs +96/−10
• src/Ersatz/Relation/Op.hs +38/−2
• src/Ersatz/Relation/Prop.hs +56/−3
• src/Ersatz/Variable.hs +19/−1

@@ -1,3 +1,9 @@+0.4.13 [2022.11.01]+-------------------+* Make the examples compile with `mtl-2.3.*`.+* Add more documentation to the `Ersatz.Relation.*` modules, the `Variable`+  class, and the data types in `Ersatz.Bits`.+ 0.4.12 [2022.08.11] ------------------- * Add `Equatable` and `Orderable` instances for more base and containers types

@@ -1,5 +1,5 @@ name:           ersatz-version:        0.4.12+version:        0.4.13 license:        BSD3 license-file:   LICENSE author:         Edward A. Kmett, Eric Mertens, Johan Kiviniemi

@@ -10,8 +10,11 @@  import Control.Applicative import qualified Control.Monad.Fail as Fail-import Control.Monad.Reader-import Control.Monad.RWS.Strict hiding ((<>))+import Control.Monad (guard)+import Control.Monad.Reader (MonadReader(..), ReaderT(..))+import Control.Monad.RWS.Strict (RWST, evalRWST)+import Control.Monad.Trans (MonadTrans(..))+import Control.Monad.Writer.Strict (MonadWriter(..)) import Control.Lens import qualified Data.Foldable as F (asum) import Data.Map (Map)

@@ -3,7 +3,8 @@  import Prelude hiding ((&&), (||), not, and, or, all, any) -import Control.Monad.Reader+import Control.Monad (forM_, replicateM, when)+import Control.Monad.Reader (ReaderT(..), asks) import Data.Array (Array, (!)) import qualified Data.Array as Array import Data.Word

@@ -8,7 +8,17 @@ -- Stability :  experimental -- Portability: non-portable ----- 'Bits' is an arbitrary length natural number type+-- 'Bit1' .. 'Bit8' represent fixed length bit vectors.+-- The most significant bit comes first.+-- 'Bit1' and 'Bit2' have modular arithmetic+-- (the result has the same width as the arguments, overflow is ignored).+--+-- 'Bits' is an arbitrary length natural number type.+-- The least significant bit comes first.+-- 'Bits' has full arithmetic+-- (the result has large enough width so that there is no overflow).++ -------------------------------------------------------------------- module Ersatz.Bits   (@@ -41,21 +51,21 @@ import GHC.Generics import Prelude hiding (and, or, not, (&&), (||)) --- | A container of 1 'Bit' that 'encode's from and 'decode's to 'Word8'+-- | A container of 1 'Bit' that 'encode's from and 'decode's to 'Word8'. newtype Bit1 = Bit1 Bit deriving (Show,Generic)--- | A container of 2 'Bit's that 'encode's from and 'decode's to 'Word8'+-- | A container of 2 'Bit's that 'encode's from and 'decode's to 'Word8'. MSB is first. data Bit2 = Bit2 !Bit !Bit deriving (Show,Generic)--- | A container of 3 'Bit's that 'encode's from and 'decode's to 'Word8'+-- | A container of 3 'Bit's that 'encode's from and 'decode's to 'Word8'. MSB is first. data Bit3 = Bit3 !Bit !Bit !Bit deriving (Show,Generic)--- | A container of 4 'Bit's that 'encode's from and 'decode's to 'Word8'+-- | A container of 4 'Bit's that 'encode's from and 'decode's to 'Word8'. MSB is first. data Bit4 = Bit4 !Bit !Bit !Bit !Bit deriving (Show,Generic)--- | A container of 5 'Bit's that 'encode's from and 'decode's to 'Word8'+-- | A container of 5 'Bit's that 'encode's from and 'decode's to 'Word8'. MSB is first. data Bit5 = Bit5 !Bit !Bit !Bit !Bit !Bit deriving (Show,Generic)--- | A container of 6 'Bit's that 'encode's from and 'decode's to 'Word8'+-- | A container of 6 'Bit's that 'encode's from and 'decode's to 'Word8'. MSB is first. data Bit6 = Bit6 !Bit !Bit !Bit !Bit !Bit !Bit deriving (Show,Generic)--- | A container of 7 'Bit's that 'encode's from and 'decode's to 'Word8'+-- | A container of 7 'Bit's that 'encode's from and 'decode's to 'Word8'. MSB is first. data Bit7 = Bit7 !Bit !Bit !Bit !Bit !Bit !Bit !Bit deriving (Show,Generic)--- | A container of 8 'Bit's that 'encode's from and 'decode's to 'Word8'+-- | A container of 8 'Bit's that 'encode's from and 'decode's to 'Word8'. MSB is first. data Bit8 = Bit8 !Bit !Bit !Bit !Bit !Bit !Bit !Bit !Bit deriving (Show,Generic)  instance Boolean Bit1@@ -176,6 +186,8 @@ boolToNum True  = 1 {-# INLINE boolToNum #-} ++-- | This instance provides modular arithmetic (overflow is ignored). instance Num Bit1 where   Bit1 a + Bit1 b = Bit1 (xor a b)   Bit1 a * Bit1 b = Bit1 (a && b)@@ -210,6 +222,7 @@ halfAdder :: Bit -> Bit -> (Bit, Bit) -- ^ (sum, carry) halfAdder a b = (a `xor` b, a && b) +-- | This instance provides modular arithmetic (overflow is ignored). instance Num Bit2 where   Bit2 a2 a1 + Bit2 b2 b1 = Bit2 s2 s1 where     (s1,c2) = halfAdder a1 b1@@ -231,8 +244,8 @@   signum (Bit2 a b) = Bit2 false (a || b)   fromInteger k = Bit2 (bool (k .&. 2 /= 0)) (bool (k .&. 1 /= 0)) --- suitable for comparisons and arithmetic. Bits are stored--- in little-endian order to enable phantom 'false' values+-- | A container of 'Bit's that is suitable for comparisons and arithmetic. Bits are stored+-- with least significant bit first to enable phantom 'false' values -- to be truncated. newtype Bits = Bits { _getBits :: [Bit] } @@ -391,6 +404,16 @@   times2 = (false:)   aux x ys = Bits (map (x &&) ys) +-- | This instance provides full arithmetic.+-- The result has large enough width so that there is no overflow.+--+-- Subtraction is modified: @a - b@ denotes @max 0 (a - b)@.+--+-- Width of @a + b@ is @1 + max (width a) (width b)@,+-- width of @a * b@ is @(width a) + (width b)@,+-- width of @a - b@ is @max (width a) (width b)@.+--+-- @fromInteger@ will raise 'error' for negative arguments. instance Num Bits where   (+) = addBits false   (*) = mulBits

@@ -1,3 +1,16 @@+-- | Copyright: Johannes Waldmann, Antonia Swiridoff+-- License: BSD3+--+-- The type @Relation a b@ represents relations+-- between finite subsets of type @a@ and of type @b@.+--+-- A relation is stored internally as @Array (a,b) Bit@,+-- and some methods of @Data.Array@ are provided for managing indices and elements.+--+-- These are rarely needed, because we provide operations and properties+-- in a point-free style, that is, without reference to individual indices and elements.++ module Ersatz.Relation ( module Ersatz.Relation.Data , module Ersatz.Relation.Op

@@ -1,14 +1,21 @@ {-# language TypeFamilies #-} -module Ersatz.Relation.Data ( Relation+module Ersatz.Relation.Data ( +-- * The 'Relation' type+  Relation+-- * Construction , relation, symmetric_relation , build , buildFrom , identity+-- * Components , bounds, (!), indices, assocs, elems+-- * , table )  where +import Prelude hiding ( and )+ import Ersatz.Bit import Ersatz.Codec import Ersatz.Variable (exists)@@ -18,6 +25,15 @@ import qualified Data.Array as A import Data.Array ( Array, Ix ) ++-- | @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) Bit@,+-- so @a@ and @b@ have to be instances of 'Ix',+-- and both \(A\) and \(B\) are intervals.+ newtype Relation a b = Relation (A.Array (a, b) Bit)  instance (Ix a, Ix b) => Codec (Relation a b) where@@ -25,8 +41,12 @@   decode s (Relation a) = decode s a   encode a = Relation $ encode a -relation :: ( Ix a, Ix b, MonadSAT s m )-         => ((a,b),(a,b)) -> m ( Relation a b )++-- | @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, MonadSAT s m ) =>+  ((a,b),(a,b)) +  -> m ( Relation a b ) relation bnd = do     pairs <- sequence $ do         p <- A.range bnd@@ -35,9 +55,15 @@             return ( p, x )     return $ build bnd pairs +-- | Constructs an indeterminate relation \( R \subseteq B \times B \)+-- that it is symmetric, i.e., \( \forall x, y \in B: ((x,y) \in R) \rightarrow ((y,x) \in R) \).+--+-- A symmetric relation is an undirected graph, possibly with loops. symmetric_relation ::   (MonadSAT s m, Ix b) =>-  ((b, b), (b, b)) -> m (Relation b 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@@ -48,38 +74,98 @@                    : [ ((q,p), x) | p /= q ]     return $ build bnd $ concat pairs +-- | Constructs a relation \(R \subseteq A \times B \) from a list.+-- +-- ==== __Example__+--+-- @+-- r = build ((0,'a'),(1,'b')) [((0,'a'), true), ((0,'b'), false), +--                          ((1,'a'), false), ((1,'b'), true))]+-- @ build :: ( Ix a, Ix b )       => ((a,b),(a,b))-      -> [ ((a,b), Bit ) ]+      -> [ ((a,b), Bit ) ] -- ^ A list of tuples, where the first element represents an element+                           -- \( (x,y) \in A \times B \) and the second element is a positive 'Bit'+                           -- if \( (x,y) \in R \), or a negative 'Bit' 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 -> Bit) -> ((a,b),(a,b)) -> Relation a b-buildFrom p bnd = build bnd $ flip map (A.range bnd) $ \ (i,j) ->-    ((i,j), p i j)+          => (a -> b -> Bit) -- ^ A function with the specified signature, that assigns a 'Bit'-value +                             -- to each element \( (x,y) \in A \times B \).+          -> ((a,b),(a,b))+          -> Relation a b+buildFrom p bnd = build bnd $ flip map (A.range bnd) $ \ (i,j) -> ((i, j), p i j) +-- | Constructs the identity relation \(I \subseteq A \times A, I = \{ (x,x) ~|~ x \in A \} \). identity :: (Ix a)-         => ((a,a),(a,a)) -> Relation a 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 = buildFrom (\ i j -> bool $ i == j)  +-- | The bounds of the array that correspond to the matrix representation of the given relation.+--+-- ==== __Example__+--+-- >>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false))]+-- >>> bounds r+-- ((0,0),(1,1)) bounds :: (Ix a, Ix b) => 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 \).+--+-- ==== __Example__+--+-- >>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false))]+-- >>> indices r+-- [(0,0),(0,1),(1,0),(1,1)] 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 'Bit' , if \( (x,y) \in R \) or not.+-- +-- ==== __Example__+--+-- >>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false))]+-- >>> assocs r+-- [((0,0),Var (-1)),((0,1),Var 1),((1,0),Var 1),((1,1),Var (-1))] assocs :: (Ix a, Ix b) => Relation a b -> [((a, b), Bit)] assocs ( Relation r ) = A.assocs r +-- | The list of elements of the array+-- that correspond to the matrix representation of the given relation.+--+-- ==== __Example__+--+-- >>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false))]+-- >>> elems r+-- [Var (-1),Var 1,Var 1,Var (-1)] elems :: (Ix a, Ix b) => Relation a b -> [Bit] elems ( Relation r ) = A.elems r +-- | The 'Bit'-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.+-- +-- ==== __Example__+--+-- >>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false))]+-- >>> r ! (0,0)+-- Var (-1)+-- >>> r ! (0,1)+-- Var 1 (!) :: (Ix a, Ix b) => Relation a b -> (a, b) -> Bit Relation r ! p = r A.! p -+-- | Print a satisfying assignment from a SAT solver, where the assignment is interpreted as a relation.+-- @putStrLn $ table \</assignment/\>@ corresponds to the matrix representation of this relation. table :: (Enum a, Ix a, Enum b, Ix b)       => Array (a,b) Bool -> String table r = unlines $ do

@@ -2,7 +2,9 @@  module Ersatz.Relation.Op -( mirror+( +-- * Operations+  mirror , union , complement , difference@@ -21,26 +23,45 @@  import Data.Ix +-- | Constructs the converse relation \( R^{-1} \subseteq B \times A \) of a relation +-- \( R \subseteq A \times B \), which is defined by \( R^{-1} = \{ (y,x) ~|~ (x,y) \in R \} \). mirror :: ( Ix a , Ix b ) => Relation a b -> Relation b a mirror r =     let ((a,b),(c,d)) = bounds r     in  build ((b,a),(d,c)) $ do (x,y) <- indices r ; return ((y,x), r!(x,y)) +-- | Constructs the complement relation \( \overline{R} \) +-- of a relation \( R \subseteq A \times B \), which is defined by +-- \( \overline{R}  = \{ (x,y) \in A \times B ~|~ (x,y) \notin R \} \). complement :: ( Ix a , Ix b ) => Relation a b -> Relation a b complement r =     build (bounds r) $ do i <- indices r ; return ( i, not $ r!i ) +-- | Constructs the difference \( R \setminus S \) of the relations +-- \(R\) and \(S\), that contains all elements that are in \(R\) but not in \(S\), i.e.,+-- \( R \setminus S = \{ (x,y) \in R ~|~ (x,y) \notin S \} \).+--+-- Note that if \( R \subseteq A \times B \) and \( S \subseteq C \times D \),+-- then \( A \times B \) must be a subset of \( C \times D \) and+-- \( R \setminus S \subseteq A \times B \). difference :: ( Ix a , Ix b )         => Relation a b -> Relation a b ->  Relation a b difference r s =     intersection r $ complement s +-- | Constructs the union \( R \cup S \) of the relations \( R \) and \( S \).+--+-- Note that for \( R \subseteq A \times B \) and \( S \subseteq C \times D \),+-- it must hold that \( A \times B \subseteq C \times D \). union :: ( Ix a , Ix b )         => Relation a b -> Relation a b ->  Relation a b union r s =  build ( bounds r ) $ do     i <- indices r     return (i, or [ r!i, s!i ] ) +-- | Constructs the composition \( R \cdot S \) of the relations +-- \( R \subseteq A \times B \) and \( S \subseteq B \times C \), which is +-- defined by \( R \cdot S = \{ (a,c) ~|~ ((a,b) \in R) \land ((b,c) \in S) \} \). product :: ( Ix a , Ix b, Ix c )         => Relation a b -> Relation b c ->  Relation a c product a b =@@ -54,8 +75,13 @@                 return $ and [ a!(x,y), b!(y,z) ]                 ) +-- | Constructs the relation \( R^{n} \) that results if a relation+-- \( R \subseteq A \times A \) is composed \(n\) times with itself.+--+-- \( R^{0} \) is the identity relation \( I_{R} = \{ (x,x) ~|~ x \in A \} \) of \(R\). power  :: ( Ix a  )-        => Int -> Relation a a -> Relation a a+        => Int -- ^ \(n\)+        -> Relation a a -> Relation a a power 0 r = identity ( bounds r ) power 1 r = r power e r =@@ -66,6 +92,10 @@         0 -> s2         _ -> product s2 r +-- | Constructs the intersection \( R \cap S \) of the relations \( R \) and \( S \).+--+-- Note that for \( R \subseteq A \times B \) and \( S \subseteq C \times D \),+-- it must hold that \( A \times B \subseteq C \times D \). intersection :: ( Ix a , Ix b)       => Relation a b -> Relation a b       -> Relation a b@@ -73,10 +103,16 @@         i <- indices r         return (i, and [ r!i, s!i ] ) +-- | Constructs the reflexive closure \( R \cup I_{R} \) of the relation +-- \( R \subseteq A \times A \), where \( I_{R} = \{ (x,x) ~|~ x \in A \} \) +-- is the identity relation of \(R\). reflexive_closure :: Ix a => Relation a a -> Relation a a reflexive_closure t =     union t $ identity $ bounds t +-- | Constructs the symmetric closure \( R \cup R^{-1} \) of the relation +-- \( R \subseteq A \times A \), where \( R^{-1} = \{ (y,x) ~|~ (x,y) \in R \} \)+-- is converse relation of \(R\). symmetric_closure :: Ix a => Relation a a -> Relation a a symmetric_closure r =     union r $ mirror r

@@ -1,7 +1,8 @@- module Ersatz.Relation.Prop -( implies+( +-- * Properties+  implies , symmetric , anti_symmetric , transitive@@ -31,50 +32,100 @@  import Data.Ix +-- | Tests if the first relation \(R\) is a subset of the second relation \(S\), +-- i.e., every element that is contained in \(R\) is also contained in \(S\).+--+-- Note that if \( R \subseteq A \times B \) and \( S \subseteq C \times D \),+-- then \( A \times B \) must be a subset of \( C \times D \). implies :: ( Ix a, Ix b )         => Relation a b -> Relation a b -> Bit implies r s = and $ do     i <- indices r     return $ or [ not $ r ! i, s ! i ] +-- | Tests if a relation is empty, i.e., the relation doesn't contain any elements. empty ::  ( Ix a, Ix b )         => Relation a b -> Bit empty r = and $ do     i <- indices r     return $ not $ r ! i +-- | Tests if a relation \( R \subseteq A \times B \) is complete,+-- i.e., \(R = A \times B \). complete :: (Ix a, Ix b) => Relation a b -> Bit complete r = empty $ complement r +-- | Tests if a relation \( R \subseteq A \times A \) is strongly connected, i.e.,+-- \( \forall x, y \in A: ((x,y) \in R) \lor ((y,x) \in R) \). total :: ( Ix a) => Relation a a -> Bit total r = complete $ symmetric_closure r +-- | Tests if two relations are disjoint, i.e., +-- there is no element that is contained in both relations. disjoint :: (Ix a, Ix b) => Relation a b -> Relation a b -> Bit disjoint r s = empty $ intersection r s +-- | Tests if two relations \( R, S \subseteq A \times B \) are equal, +-- i.e., they contain the same elements. equals :: (Ix a, Ix b) => Relation a b -> Relation a b -> Bit equals r s = and [implies r s, implies s r] +-- | Tests if a relation \( R \subseteq A \times A \) is symmetric,+-- i.e., \( \forall x, y \in A: ((x,y) \in R) \rightarrow ((y,x) \in R) \). symmetric :: ( Ix a) => Relation a a -> Bit symmetric r = implies r ( mirror r ) ++-- | Tests if a relation \( R \subseteq A \times A \) is antisymmetric,+-- i.e., \( \forall x, y \in A: ((x,y) \in R) \land ((y,x) \in R)) \rightarrow (x = y) \). anti_symmetric :: ( Ix a) => Relation a a -> Bit anti_symmetric r = implies (intersection r (mirror r)) (identity (bounds r)) +-- | Tests if a relation \( R \subseteq A \times A \) is irreflexive, i.e.,+-- \( \forall x \in A: (x,x) \notin R \). irreflexive :: ( Ix a ) => Relation a a -> Bit irreflexive r = and $ do     let ((a,_),(c,_)) = bounds r     x <- range (a, c)     return $ not $ r ! (x,x) +-- | Tests if a relation \( R \subseteq A \times A \) is reflexive, i.e.,+-- \( \forall x \in A: (x,x) \in R \). reflexive :: ( Ix a ) => Relation a a -> Bit reflexive r = and $ do     let ((a,_),(c,_)) = bounds r     x <- range (a,c)     return $ r ! (x,x) -regular, regular_in_degree, regular_out_degree, max_in_degree, min_in_degree, max_out_degree, min_out_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit+-- | Given an 'Int' \( n \) and a relation \( R \subseteq A \times B \), check if+-- \( \forall x \in A: | \{ (x,y) \in R \} | = n \) and+-- \( \forall y \in B: | \{ (x,y) \in R \} | = n \) hold.+regular :: (Ix a, Ix b) => Int -> Relation a b -> Bit +-- | Given an 'Int' \( n \) and a relation \( R \subseteq A \times B \), check if+-- \( \forall y \in B: | \{ (x,y) \in R \} | = n \) holds.+regular_in_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit++-- | Given an 'Int' \( n \) and a relation \( R \subseteq A \times B \), check if+-- \( \forall x \in A: | \{ (x,y) \in R \} | = n \) holds.+regular_out_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit++-- | Given an 'Int' \( n \) and a relation \( R \subseteq A \times B \), check if+-- \( \forall y \in B: | \{ (x,y) \in R \} | \leq n \) holds.+max_in_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit++-- | Given an 'Int' \( n \) and a relation \( R \subseteq A \times B \), check if+-- \( \forall y \in B: | \{ (x,y) \in R \} | \geq n \) holds.+min_in_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit++-- | Given an 'Int' \( n \) and a relation \( R \subseteq A \times B \), check if+-- \( \forall x \in A: | \{ (x,y) \in R \} | \leq n \) holds.+max_out_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit++-- | Given an 'Int' \( n \) and a relation \( R \subseteq A \times B \), check if+-- \( \forall x \in A: | \{ (x,y) \in R \} | \geq n \) holds.+min_out_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit+ regular deg r = and [ regular_in_degree deg r, regular_out_degree deg r ]  regular_out_degree = out_degree_helper exactly@@ -94,6 +145,8 @@         y <- range (b,d)         return $ r ! (x,y) +-- | Tests if a relation \( R \subseteq A \times A \) is transitive, i.e.,+-- \( \forall x, y \in A: ((x,y) \in R) \land ((y,z) \in R) \rightarrow ((x,z) \in R) \). transitive :: ( Ix a )            => Relation a a -> Bit transitive r = implies (product r r) r

@@ -51,8 +51,26 @@ instance GVariable f => GVariable (M1 i c f) where   gliterally = fmap M1 . gliterally --- | Instances for this class for product-like types can be automatically derived+-- | This class describes all types that can be represented+-- by a collection of literals. The class method 'literally'+-- is usually applied to 'literalExists' or 'literalForall',+-- see implementations of 'exists' and 'forall'.+--+-- Instances for this class for product-like types can be automatically derived -- for any type that is an instance of 'Generic'.+--+-- === __Example usage__+--+-- @+-- {-# language DeriveGeneric, TypeApplications #-}+-- import GHC.Generics+--+-- data T = C Bit Bit deriving Generic+-- instance Variable T+--+-- constraint = do t <- exists @T ; ...+-- @+ class Variable t where   literally :: MonadSAT s m => m Literal -> m t   default literally ::