ersatz 0.5 → 0.6

raw patch · 20 files changed

+999/−182 lines, 20 filesdep +optparse-applicativedep +tastydep +tasty-hunitdep −HUnitdep −test-frameworkdep −test-framework-hunitdep ~arraydep ~basedep ~bytestringnew-component:exe:ersatz-circuit-synthesisnew-component:exe:ersatz-graph-coloringPVP ok

version bump matches the API change (PVP)

Dependencies added: optparse-applicative, tasty, tasty-hunit

Dependencies removed: HUnit, test-framework, test-framework-hunit

Dependency ranges changed: array, base, bytestring, mtl

API changes (from Hackage documentation)

Files

• .hlint.yaml +7/−2
• CHANGELOG.md +14/−0
• ersatz.cabal +48/−10
• examples/qbf/Coloring.hs +115/−0
• examples/qbf/Synthesis.hs +91/−0
• src/Ersatz/Bits.hs +3/−3
• src/Ersatz/Problem.hs +52/−0
• src/Ersatz/Relation.hs +5/−0
• src/Ersatz/Relation/ARS.hs +223/−0
• src/Ersatz/Relation/Data.hs +90/−39
• src/Ersatz/Relation/Op.hs +82/−48
• src/Ersatz/Relation/Prop.hs +28/−33
• src/Ersatz/Solver.hs +4/−0
• src/Ersatz/Solver/DepQBF.hs +82/−8
• src/Ersatz/Solver/Kissat.hs +50/−0
• src/Ersatz/Solver/Lingeling.hs +84/−0
• src/Ersatz/Solver/Minisat.hs +6/−9
• src/Ersatz/Solver/Z3.hs +2/−5
• tests/HUnit.hs +6/−8
• tests/Moore.hs +7/−17

@@ -6,6 +6,11 @@ - ignore:     name: Use lambda-case +- ignore:+    name: Use || # We define a different `or`++- ignore:+    name: Use && # We define a different `and`+ - ignore: {name: Hoist not, within: [Ersatz.Bit]} # This is how we define `any`, ya dingus-- ignore: {name: Use ||, within: [Ersatz.Relation.Prop]} # This is a different `or`-- ignore: {name: Use &&, within: [Ersatz.Relation.Prop]} # This is a different `and`+- ignore: {name: Use infix, within: [Ersatz.Relation.Op]} # We define a different `union` function in this module

@@ -1,3 +1,17 @@+0.6 [2025.06.17]+----------------+* Add the `Ersatz.Relation.ARS` module+* Change the type of `buildFrom`:++  ```diff+  -buildFrom :: (Ix a, Ix b) => (a -> b -> Bit) -> ((a,b),(a,b))  -> Relation a b+  +buildFrom :: (Ix a, Ix b) => ((a,b),(a,b))   -> ((a,b) -> Bit) -> Relation a b+  ```+* Add support for `kissat` and the `lingeling` trio (`lingeling`, `plingeling`,+  `treengeling`) of SAT solvers.+* Add QBF examples (requires DepQBF solver)+* Replace `test-framework` with `tasty` in the test suite.+ 0.5 [2023.09.08] ---------------- * The `forall` function in `Ersatz.Variable` has been renamed to

@@ -1,5 +1,5 @@ name:           ersatz-version:        0.5+version:        0.6 license:        BSD3 license-file:   LICENSE author:         Edward A. Kmett, Eric Mertens, Johan Kiviniemi@@ -82,9 +82,12 @@               , GHC == 8.8.4               , GHC == 8.10.7               , GHC == 9.0.2-              , GHC == 9.2.7-              , GHC == 9.4.5-              , GHC == 9.6.2+              , GHC == 9.2.8+              , GHC == 9.4.8+              , GHC == 9.6.6+              , GHC == 9.8.4+              , GHC == 9.10.1+              , GHC == 9.12.1 extra-source-files:   .gitignore   .hlint.yaml@@ -155,7 +158,7 @@  source-repository head   type: git-  location: git://github.com/ekmett/ersatz.git+  location: https://github.com/ekmett/ersatz.git  flag examples   description: Build examples@@ -171,8 +174,8 @@     array                >= 0.2      && < 0.6,     base                 >= 4.9      && < 5,     bytestring           >= 0.10.4.0 && < 0.13,-    containers           >= 0.2.0.1  && < 0.7,-    data-default         >= 0.5      && < 0.8,+    containers           >= 0.2.0.1  && < 0.9,+    data-default         >= 0.5      && < 0.9,     lens                 >= 4        && < 6,     mtl                  >= 1.1      && < 2.4,     process              >= 1.1      && < 1.7,@@ -197,6 +200,8 @@     Ersatz.Solution     Ersatz.Solver     Ersatz.Solver.DepQBF+    Ersatz.Solver.Kissat+    Ersatz.Solver.Lingeling     Ersatz.Solver.Minisat     Ersatz.Solver.Z3     Ersatz.Variable@@ -210,6 +215,7 @@     Ersatz.Relation.Data     Ersatz.Relation.Prop     Ersatz.Relation.Op+    Ersatz.Relation.ARS  executable ersatz-regexp-grid   -- description: An example program that solves the regular expression crossword problem <http://www.coinheist.com/rubik/a_regular_crossword/> using Ersatz.@@ -252,6 +258,39 @@   ghc-options: -Wall   hs-source-dirs: examples/sudoku +executable ersatz-graph-coloring+  -- description: An example program that solves a graph coloring problem using Ersatz.+  if flag(examples)+    build-depends:+      array,+      base < 5,+      bytestring,+      ersatz,+      mtl,+      optparse-applicative+  else+    buildable: False+  default-language: Haskell2010+  main-is: Coloring.hs+  ghc-options: -Wall+  hs-source-dirs: examples/qbf++executable ersatz-circuit-synthesis+  -- description: An example program that solves a circuit synthesis problem using Ersatz.+  if flag(examples)+    build-depends:+      array,+      base < 5,+      bytestring,+      ersatz,+      mtl+  else+    buildable: False+  default-language: Haskell2010+  main-is: Synthesis.hs+  ghc-options: -Wall -Wno-type-defaults+  hs-source-dirs: examples/qbf+ -- test-suite properties --   type: exitcode-stdio-1.0 --   ghc-options: -Wall@@ -282,9 +321,8 @@     containers,     data-default,     ersatz,-    HUnit >= 1.2,-    test-framework >= 0.6,-    test-framework-hunit >= 0.2+    tasty >= 1.4 && < 1.6,+    tasty-hunit >= 0.10 && < 0.11   default-language: Haskell2010   ghc-options: -Wall 

@@ -0,0 +1,115 @@+{-# LANGUAGE CPP #-}
+module Main where
+
+import Prelude hiding (not, (&&), and, or)
+
+import Ersatz
+import Ersatz.Relation
+import Ersatz.Counting
+
+import qualified Data.Array as A
+import Data.Array (Array, Ix)
+
+import Control.Monad.State.Lazy (StateT)
+
+import Data.List (tails)
+
+import qualified Data.ByteString.Lazy as B
+import qualified Data.ByteString.Lazy.Char8 as C
+import Data.Functor.Identity
+#if !(MIN_VERSION_base(4,11,0))
+import Data.Semigroup (Semigroup(..))
+#endif
+
+import Options.Applicative
+import Text.Printf (printf)
+
+
+data Coloring = Coloring Int Int Int
+
+coloring :: Parser Coloring
+coloring = Coloring
+  <$> argument auto ( metavar "n" <> showDefault <> value 11 <> help "Number of nodes of graph G" )
+  <*> argument auto ( metavar "c" <> showDefault <> value 3 <> help "G is not c-colorable" )
+  <*> argument auto ( metavar "k" <> showDefault <> value 3 <> help "G has no complete subgraph with k nodes" )
+
+-- | default: Grötzsch graph: not 3-colorable and K3-free (11 nodes)
+main :: IO ()
+main = execParser options >>= run
+  where options = info (coloring <**> helper) fullDesc
+
+run :: Coloring -> IO ()
+run (Coloring n c k) = do
+  printf "n = %d, c = %d, k = %d\n" n c k
+  formulaSize $ problem n c k
+  solve $ problem n c k
+
+
+solve :: StateT QSAT IO (Relation Int Int) -> IO ()
+solve p = do
+  result <- solveWith depqbf p
+  case result of
+    (Satisfied, Just r) -> mapM_ putStrLn [table r, show $ edgesA r]
+    _                   -> putStrLn "unsat"
+
+-- | @problem n c k@ generates a QBF problem that encodes a graph with @n@ nodes,
+-- which is not @c@-colorable and does not contain a complete subgraph with @k@ nodes.
+problem :: Monad a => Int -> Int -> Int -> StateT QSAT a (Relation Int Int)
+problem n c k = do
+  r <- symmetric_relation ((0,0),(n-1,n-1))
+  col <- universally_quantified_relation ((0,0),(n-1,c-1))
+  assert $ and [
+      irreflexive r
+    , not $ has_k k r
+    , is_coloring col ==> not $ proper col r
+    ]
+  return r
+
+
+universally_quantified_relation :: (Ix a, Ix b, MonadQSAT s m)
+  => ((a,b),(a,b)) -> m (Relation a b)
+universally_quantified_relation bnd = do
+  pairs <- sequence $ do
+    p <- A.range bnd
+    return $ do
+      x <- forall_
+      return (p,x)
+  return $ build bnd pairs
+
+-- | @has_k n r@ encodes the constraint that @r@ has a complete subgraph with @n@ nodes.
+has_k :: Ix a => Int -> Relation a a -> Bit
+has_k n r = or $ do
+  xss <- select n $ universe r
+  return $ and $ do
+    (x:xs) <- tails xss
+    y <- xs
+    return $ r!(x,y)
+
+-- | select 2 [1..4] = [[1,2],[1,3],[1,4],[2,3],[2,4],[3,4]]
+select :: Int -> [a] -> [[a]]
+select 0 _ = [[]]
+select _ [] = []
+select k (x:xs) = map (x:) (select (k-1) xs) ++ select k xs
+
+-- | Given a relation r with domain a and codomain b, check if r matches every element in a
+-- to exactly one element in b.
+is_coloring :: Ix a => Relation a a -> Bit
+is_coloring c = and $ do
+  i <- domain c
+  return $ exactly 1 $ do
+    j <- codomain c
+    return $ c!(i,j)
+
+-- | @proper c r@ encodes the constraint that @c@ is a proper coloring for @r@.
+proper :: Ix a => Relation a a -> Relation a a -> Bit
+proper col r = and $ do
+  (p,q) <- indices r
+  j <- codomain col
+  return $ r!(p,q) ==> not $ col!(p,j) && col!(q,j)
+
+
+edgesA :: (Ix a, Ix b) => Array (a,b) Bool -> [(a,b)]
+edgesA a = [ i | (i, b) <- A.assocs a, b == True]
+
+formulaSize :: StateT QSAT Identity a -> IO ()
+formulaSize p = mapM_ C.putStrLn $ take 2 $ B.split 10 $ qdimacsQSAT p

@@ -0,0 +1,91 @@+-- | An example program that solves a circuit synthesis problem with the Boolean Chain approach,
+-- as cited in "Circuit Minimization with QBF-Based Exact Synthesis" by Reichl et al. 2023
+-- <https://doi.org/10.1609/aaai.v37i4.25524/>.
+
+module Main where
+
+import Prelude hiding (not, (&&), and, or, product)
+
+import Ersatz
+import Ersatz.Relation
+import Ersatz.Counting
+
+import qualified Data.Array as A
+import Data.Array (Array, Ix)
+
+import Control.Monad.State.Lazy (StateT)
+import Control.Monad (guard)
+
+import Text.Printf (printf)
+import Data.List (sortOn)
+
+import qualified Data.ByteString.Lazy as B
+import qualified Data.ByteString.Lazy.Char8 as C
+import Data.Functor.Identity
+
+
+-- | AIG where @atmost 2 [1,2,3,4]@ is equivalent to @10@
+--
+-- Another problem that can be quickly solved is, for example:
+-- n = 3, l = 5, m = 1, f xs = [exactly 2 xs]
+-- (AIG where @exactly 2 [1,2,3]@ is equivalent to @8@)
+main :: IO ()
+main = do
+  let n = 4 -- number of inputs
+      l = 6 -- number of steps (gates)
+      m = 1 -- number of outputs
+      f :: [Bit] -> [Bit]
+      f xs = [atmost 2 xs]
+  formulaSize $ problem f n l m
+  solve $ problem f n l m
+
+
+solve :: StateT QSAT IO (Relation Int Int, Relation Int Int) -> IO ()
+solve p = do
+  result <- solveWith depqbf p
+  case result of
+    (Satisfied, Just (s,o)) -> printf "output: %s\nAIG:\n%s%s\n" (show $ map fst $ sortOn snd $ edgesA o) (table s) (show $ edgesA s)
+    _                       -> putStrLn "unsat"
+
+-- | @problem f n l m@ generates a QBF problem that encodes an AIG graph with @n@ inputs,
+-- @l@ gates and @m@ outputs which is equivalent to the boolean function @f@.
+problem :: Monad a => ([Bit] -> [Bit]) -> Int -> Int -> Int -> StateT QSAT a (Relation Int Int, Relation Int Int)
+problem f n l m = do
+  s <- relation ((n+1,1),(n+l,n+l)) -- selection variables: (x,y) is in s iff gate x takes gate/input y as an input
+  assert $ and $ do -- ensure that s is acyclic (DAG)
+    (i,j) <- indices s
+    guard (i <= j)
+    return $ s!(i,j) === false
+  o <- relation ((1,1),(n+l,m)) -- output variables: (x,y) is in o iff output y is gate/input x
+  assert $ regular_in_degree 1 o
+  v <- universally_quantified_relation ((1,1),(1,n)) -- input variables: (1,y) is in v iff input y is true
+  g <- relation ((1,1),(1,n+l)) -- gate value variables: (1,y) is in g iff gate/input y is true
+  assert $ and $ do
+    i <- [1..n]
+    return $ g!(1,i) === v!(1,i)
+  assert $ and $ do -- g!(1,y) = nand xs where xs is the list of inputs of y
+    i <- [n+1..n+l]
+    let val = not $ and $ do
+          p <- [1..i-1]
+          return $ s!(i,p) ==> g!(1,p)
+    return $ g!(1,i) === val
+  assert $ f (elems v) === elems (product g o)
+  return (s,o)
+
+
+universally_quantified_relation :: (Ix a, Ix b, MonadQSAT s m)
+  => ((a,b),(a,b)) -> m (Relation a b)
+universally_quantified_relation bnd = do
+  pairs <- sequence $ do
+    p <- A.range bnd
+    return $ do
+      x <- forall_
+      return (p,x)
+  return $ build bnd pairs
+
+
+edgesA :: (Ix a, Ix b) => Array (a,b) Bool -> [(a,b)]
+edgesA a = [ i | (i, True) <- A.assocs a]
+
+formulaSize :: StateT QSAT Identity a -> IO ()
+formulaSize p = mapM_ C.putStrLn $ take 2 $ B.split 10 $ qdimacsQSAT p

@@ -40,7 +40,7 @@ import Data.Bits ((.&.), (.|.), shiftL, shiftR) import qualified Data.Bits as Data import Data.Foldable (toList)-import Data.List (unfoldr, foldl')+import qualified Data.List as List (unfoldr, foldl') import Data.Stream.Infinite (Stream(..)) import Data.Word (Word8) import Ersatz.Bit@@ -178,7 +178,7 @@ {-# INLINE numToBool #-}  boolsToNum :: (Num a, Data.Bits a) => [Bool] -> a-boolsToNum = foldl' (\n a -> (n `shiftL` 1) .|. boolToNum a) 0+boolsToNum = List.foldl' (\n a -> (n `shiftL` 1) .|. boolToNum a) 0 {-# INLINE boolsToNum #-}  boolToNum :: Num a => Bool -> a@@ -284,7 +284,7 @@        -- Integers to Integer        return (foldr (\x acc -> x + 2 * acc) 0 zs) -  encode = Bits . unfoldr step+  encode = Bits . List.unfoldr step     where     step x =       case compare x 0 of

@@ -39,6 +39,8 @@   , QDIMACS(..)   , WDIMACS(..)   , dimacs, qdimacs, wdimacs+  , writeDimacs, writeQdimacs, writeWdimacs+  , writeDimacs', writeQdimacs', writeWdimacs'   ) where  import Data.ByteString.Builder@@ -57,6 +59,7 @@ import Ersatz.Internal.Formula import Ersatz.Internal.Literal import Ersatz.Internal.StableName+import System.IO ( withFile, IOMode(WriteMode) ) import System.IO.Unsafe import Data.Sequence (Seq) import qualified Data.Sequence as Seq@@ -333,3 +336,52 @@ -- Or is this fused away (because of Coercible)? satClauses :: HasSAT s => s -> Seq IntSet satClauses s = fmap clauseSet (formulaSet (s^.formula))+++------------------------------------------------------------------------------+-- Writing SATs+------------------------------------------------------------------------------++writeBuilder :: MonadIO m => FilePath -> Builder -> m ()+writeBuilder path builder = liftIO $ do+  withFile path WriteMode $ \fh ->+    hPutBuilder fh builder++-- | Write a 'DIMACS' problem to a file at a particular path. Useful if you want+-- to experiment with solvers, solver options, or measure effects of different encodings.+--+-- @writeDimacs path m@ can be used in the same contexts you would call+-- @solveWith solverName m@.+writeDimacs :: (MonadIO m, DIMACS s, Default s) => FilePath -> StateT s m a -> m ()+writeDimacs path m = writeDimacs' path . snd =<< runStateT m def++-- | Write a 'QDIMACS' problem to a file at a particular path. Useful if you want+-- to experiment with solvers, solver options, or measure effects of different encodings.+--+-- @writeQDimacs path m@ can be used in the same contexts you would call+-- @solveWith solverName m@.+writeQdimacs :: (MonadIO m, QDIMACS s, Default s) => FilePath -> StateT s m a -> m ()+writeQdimacs path m = writeQdimacs' path . snd =<< runStateT m def++-- | Write a 'WDIMACS' problem to a file at a particular path. Useful if you want+-- to experiment with solvers, solver options, or measure effects of different encodings.+--+-- | @writeWdimacs path m@ can be used in the same contexts you would call+-- @solveWith solverName m@+writeWdimacs :: (MonadIO m, WDIMACS s, Default s) => FilePath -> StateT s m a -> m ()+writeWdimacs path m = writeWdimacs' path . snd =<< runStateT m def++-- | Write a 'DIMACS' problem to a file at a particular path. Useful if you want+-- to experiment with solvers, solver options, or measure effects of different encodings.+writeDimacs' :: (MonadIO m, DIMACS t) => FilePath -> t -> m ()+writeDimacs' path = writeBuilder path . dimacs++-- | Write a 'QDIMACS' problem to a file at a particular path. Useful if you want+-- to experiment with solvers, solver options, or measure effects of different encodings.+writeQdimacs' :: (MonadIO m, QDIMACS t) => FilePath -> t -> m ()+writeQdimacs' path = writeBuilder path . qdimacs++-- | Write a 'WDIMACS' problem to a file at a particular path. Useful if you want+-- to experiment with solvers, solver options, or measure effects of different encodings.+writeWdimacs' :: (MonadIO m, WDIMACS t) => FilePath -> t -> m ()+writeWdimacs' path = writeBuilder path . wdimacs

@@ -9,15 +9,20 @@ -- -- These are rarely needed, because we provide operations and properties -- in a point-free style, that is, without reference to individual indices and elements.+--+-- Unless otherwise specified, the size of the generated formulas is linear in \( |A| \cdot |B| \),+-- where \(A\) and \(B\) represent the domain and codomain of the involved relation(s).   module Ersatz.Relation ( module Ersatz.Relation.Data , module Ersatz.Relation.Op , module Ersatz.Relation.Prop+, module Ersatz.Relation.ARS ) where  import Ersatz.Relation.Data import Ersatz.Relation.Op import Ersatz.Relation.Prop+import Ersatz.Relation.ARS 

@@ -0,0 +1,223 @@+module Ersatz.Relation.ARS (+-- * Abstract rewriting+  terminating, assert_terminating+, peak, valley+, locally_confluent+, confluent, semiconfluent+, convergent, assert_convergent+, point_symmetric+, relative_to+, connected+, is_nf+, nf_property+, unique_nfs, unique_nfs_reduction+)++where++import Prelude hiding ( (&&), not, or, and, all, product )++import Ersatz.Bit+import Ersatz.Equatable+import Ersatz.Problem ( MonadSAT )++import Ersatz.Relation.Data+import Ersatz.Relation.Op+import Ersatz.Relation.Prop++import Data.Ix+import Control.Monad ( guard )+++-- | Tests if a relation \( R \subseteq A \times A \) is terminating, i.e.,+-- there is no infinite sequence \( x_1, x_2, ... \) with \( x_i \in A \)+-- such that \( (x_i, x_{i+1}) \in R \) holds.+--+-- Formula size: linear in \( |A|^3 \)+terminating :: Ix a => Relation a a -> Bit+terminating r = irreflexive $ transitive_closure r++-- | Monadic version of 'terminating'.+--+-- Note that @assert_terminating@ cannot be used for expressing non-termination of a relation,+-- only for expressing termination.+--+-- Formula size: linear in \( |A|^3 \)+--+-- ==== __Example__+--+-- @+-- example = do+--   result <- 'Ersatz.Solver.solveWith' 'Ersatz.Solver.Minisat.minisat' $ do+--     r <- 'relation' ((0,0),(2,2))+--     'Ersatz.Bit.assert' $ 'Ersatz.Counting.atleast' 3 $ 'elems' r+--     'assert_terminating' r+--     return r+--   case result of+--     (Satisfied, Just r) -> do putStrLn $ 'table' r; return True+--     _                   -> return False+-- @+assert_terminating :: (Ix a, MonadSAT s m) => Relation a a -> m ()+assert_terminating r = do+  s <- relation $ bounds r+  assert $ and [+      transitive s+    , irreflexive s+    , implies r s ]++-- | Constructs the peak \( R^{-1} \circ S \) of two relations+-- \( R, S \subseteq A \times A \).+--+-- Formula size: linear in \( |A|^3 \)+peak :: Ix a => Relation a a -> Relation a a -> Relation a a+peak r = product (mirror r)++-- | Constructs the valley \( R \circ S^{-1} \) of two relations+-- \( R, S \subseteq A \times A \).+--+-- Formula size: linear in \( |A|^3 \)+valley :: Ix a => Relation a a -> Relation a a -> Relation a a+valley r s = product r (mirror s)++-- | Tests if a relation \( R \subseteq A \times A \) is locally confluent, i.e.,+-- \( \forall a,b,c \in A: ((a,b) \in R) \land ((a,c) \in R) \rightarrow \exists d \in A: ((b,d) \in R^*) \land ((c,d)\in R^*) \).+--+-- Formula size: linear in \( |A|^3 \)+locally_confluent :: Ix a => Relation a a -> Bit+locally_confluent r =+  let r' = transitive_reflexive_closure r+  in implies (peak r r) (valley r' r')++-- | Tests if a relation \( R \subseteq A \times A \) is confluent, i.e.,+-- \( \forall a,b,c \in A: ((a,b) \in R^*) \land ((a,c) \in R^*) \rightarrow \exists d \in A: ((b,d) \in R^*) \land ((c,d)\in R^*) \).+--+-- Formula size: linear in \( |A|^3 \)+confluent :: Ix a => Relation a a -> Bit+confluent r =+  let r' = transitive_reflexive_closure r+  in implies (peak r' r') (valley r' r')++-- | Tests if a relation \( R \subseteq A \times A \) is semi-confluent, i.e.,+-- \( \forall a,b,c \in A: ((a,b) \in R) \land ((a,c) \in R^*) \rightarrow \exists d \in A: ((b,d) \in R^*) \land ((c,d)\in R^*) \).+--+-- @semiconfluent@ is equivalent to 'confluent'.+--+-- Formula size: linear in \( |A|^3 \)+semiconfluent :: Ix a => Relation a a -> Bit+semiconfluent r =+  let r' = transitive_reflexive_closure r+  in implies (peak r r') (valley r' r')++-- | Tests if a relation \( R \subseteq A \times A \) is convergent, i.e.,+-- \( R \) is 'terminating' and 'confluent'.+--+-- Formula size: linear in \( |A|^3 \)+convergent :: Ix a => Relation a a -> Bit+convergent r = and [terminating r, locally_confluent r]++-- | Monadic version of 'convergent'.+--+-- Note that @assert_convergent@ cannot be used for expressing non-convergence of a relation,+-- only for expressing convergence.+--+-- Formula size: linear in \( |A|^3 \)+--+-- ==== __Example__+--+-- @+-- example = do+--   result <- 'Ersatz.Solver.solveWith' 'Ersatz.Solver.Minisat.minisat' $ do+--     r <- 'relation' ((0,0),(3,3))+--     'Ersatz.Bit.assert' $ 'Ersatz.Counting.exactly' 3 $ 'elems' r+--     'assert_convergent' r+--     'Ersatz.Bit.assert' $ 'Ersatz.Bit.not' $ 'transitive' r+--     return r+--   case result of+--     (Satisfied, Just r) -> do putStrLn $ 'table' r; return True+--     _                   -> return False+-- @+assert_convergent :: (Ix a, MonadSAT s m) => Relation a a -> m ()+assert_convergent r = do+  s <- relation $ bounds r+  t <- relation $ bounds r+  let u = universe r+      i = indices r+  assert $ and [+      transitive s+    , irreflexive s+    , implies r s+    , all (\x -> is_nf x r ==> t ! (x,x)) u+    , all (\(x,y) -> s!(x,y) && t!(y,y) ==> t!(x,y)) i+    , nor $ do+        (x,y) <- i; z <- u; guard $ y /= z+        return $ t ! (x,y) && t ! (x,z) ]++-- | Tests if the matrix representation (i.e. the array) of a relation+-- \( R \subseteq A \times A \) is point symmetric, i.e., for the matrix representation+-- \( \begin{pmatrix} a_{11} & \dots & a_{1n} \\ \vdots & \ddots & \vdots \\ a_{n1} & \dots & a_{nn} \end{pmatrix} \)+-- holds \( a_{ij} = a_{(n-i+1)(n-j+1)} \).+point_symmetric :: Ix a => Relation a a -> Bit+point_symmetric r+  | is_homogeneous r = elems r === reverse (elems r)+  | otherwise = error "The domain must equal the codomain!"++-- | Given two relations \( R, S \subseteq A \times A \),+-- construct \( R \) relative to \( S \) defined by \( R/S = S^* \circ R \circ S^* \).+--+-- Formula size: linear in \( |A|^3 \)+relative_to :: Ix a => Relation a a -> Relation a a -> Relation a a+r `relative_to` s =+  let s' = transitive_reflexive_closure s+  in foldl1 product [ s', r , s' ]++-- | Tests if a relation \( R \subseteq A \times A \) is connected,+-- i.e., \( (R \cup R^{-1})^* = A \times A \).+--+-- Formula size: linear in \( |A|^3 \)+connected :: Ix a => Relation a a -> Bit+connected r = complete $ equivalence_closure r++-- | Given an element \( x \in A \) and a relation \( R \subseteq A \times A \),+-- check if \( x \) is a normal form, i.e., \( \forall y \in A: (x,y) \notin R \).+--+-- Formula size: linear in \( |A| \)+is_nf :: Ix a => a -> Relation a a -> Bit+is_nf x r =+  let ((_,b),(_,d)) = bounds r+  in nor $ map (r !) $ range ((x,b),(x,d))++-- | Tests if a relation \( R \subseteq A \times A \) has the normal form property,+-- i.e., \( \forall a,b \in A \) holds: if \(b\) is a normal form and+-- \( (a,b) \in (R \cup R^{-1})^{*} \), then \( (a,b) \in R^{*} \).+--+-- Formula size: linear in \( |A|^3 \)+nf_property :: Ix a => Relation a a -> Bit+nf_property r = and $ do+  let trc = transitive_reflexive_closure r+      ec = equivalence_closure r+  (x,y) <- indices r+  return $ and [is_nf y r, ec ! (x,y)] ==> trc ! (x,y)++-- | Tests if a relation \( R \subseteq A \times A \) has the unique normal form property,+-- i.e., \( \forall a,b \in A \) with \( a \neq b \) holds: if \(a\) and \(b\) are normal forms,+-- then \( (a,b) \notin (R \cup R^{-1})^{*} \).+--+-- Formula size: linear in \( |A|^3 \)+unique_nfs :: Ix a => Relation a a -> Bit+unique_nfs r = and $ do+  let ec = equivalence_closure r+  (x,y) <- indices r+  guard $ x < y+  return $ and [is_nf x r, is_nf y r] ==> not $ ec ! (x,y)++-- | Tests if a relation \( R \subseteq A \times A \) has the unique normal form property+-- with respect to reduction, i.e., \( \forall a,b \in A \) with \( a \neq b \) holds:+-- if \(a\) and \(b\) are normal forms, then \( (a,b) \notin ((R^{*})^{-1} \circ R^{*}) \).+--+-- Formula size: linear in \( |A|^3 \)+unique_nfs_reduction :: Ix a => Relation a a -> Bit+unique_nfs_reduction r = and $ do+  let trc = transitive_reflexive_closure r+  (x,y) <- indices r+  guard $ x < y+  return $ and [is_nf x r, is_nf y r] ==> not $ peak trc trc ! (x,y)

@@ -1,22 +1,27 @@ {-# language TypeFamilies #-} -module Ersatz.Relation.Data ( --- * The 'Relation' type+module Ersatz.Relation.Data (+-- * The @Relation@ type   Relation -- * Construction , relation, symmetric_relation , build-, buildFrom+, buildFrom, buildFromM , identity -- * Components , bounds, (!), indices, assocs, elems--- *+, domain, codomain, universe+, universeSize+, is_homogeneous+, card+-- * Pretty printing , table )  where -import Prelude hiding ( and )+import Prelude hiding ( and, (&&), any )  import Ersatz.Bit+import Ersatz.Bits ( Bits, sumBit ) import Ersatz.Codec import Ersatz.Variable (exists) import Ersatz.Problem (MonadSAT)@@ -34,18 +39,18 @@ -- 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)+newtype Relation a b = Relation (Array (a, b) Bit)  instance (Ix a, Ix b) => Codec (Relation a b) where-  type Decoded (Relation a b) = A.Array (a, b) Bool+  type Decoded (Relation a b) = Array (a, b) Bool   decode s (Relation a) = decode s a   encode a = Relation $ encode a   -- | @relation ((amin,bmin),(amax,mbax))@ constructs an indeterminate relation \( R \subseteq A \times B \)--- where \(A\) is @{amin .. amax}@ and \(B\) is @{bmin .. bmax}$.+-- where \(A\) is @{amin .. amax}@ and \(B\) is @{bmin .. bmax}@. relation :: ( Ix a, Ix b, MonadSAT s m ) =>-  ((a,b),(a,b)) +  ((a,b),(a,b))   -> m ( Relation a b ) relation bnd = do     pairs <- sequence $ do@@ -56,12 +61,10 @@     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.+-- that is symmetric, i.e., \( \forall x, y \in B: ((x,y) \in R) \rightarrow ((y,x) \in R) \). symmetric_relation ::   (MonadSAT s m, Ix b) =>-  ((b, b), (b, b)) -- ^ Since a symmetric relation must be homogeneous, the domain must equal the codomain. +  ((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@@ -75,12 +78,12 @@     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))]+-- 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))@@ -92,48 +95,63 @@  -- | Constructs a relation \(R \subseteq A \times B \) from a function. buildFrom :: (Ix a, Ix b)-          => (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))+          => ((a,b),(a,b))+          -> ((a,b) -> Bit) -- ^ A function that assigns a 'Bit'-value+                            -- to each element \( (x,y) \in A \times B \).           -> Relation a b-buildFrom p bnd = build bnd $ flip map (A.range bnd) $ \ (i,j) -> ((i, j), p i j)+buildFrom bnd p = build bnd $ flip map (A.range bnd) $ \ i -> (i, p i) --- | Constructs the identity relation \(I \subseteq A \times A, I = \{ (x,x) ~|~ x \in A \} \).+-- | Constructs an indeterminate relation \(R \subseteq A \times B\) from a function.+buildFromM :: (Ix a, Ix b, MonadSAT s m)+          => ((a,b),(a,b))+          -> ((a,b) -> m Bit)+          -> 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. +         => ((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)+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. -- -- ==== __Example__ ----- >>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false))]+-- >>> 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 \) +-- | 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))]+-- >>> 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 \) +-- | 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))]+-- >>> 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)]@@ -150,10 +168,10 @@ 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 \) +-- | 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))]@@ -164,17 +182,50 @@ (!) :: (Ix a, Ix b) => Relation a b -> (a, b) -> Bit Relation r ! p = r A.! p +-- | The domain \(A\) of a relation \(R \subseteq A \times B\).+domain :: (Ix a, Ix b) => 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 a, Ix b) => Relation a b -> [b]+codomain r =+  let ((_,y),(_,y')) = bounds r+  in A.range (y,y')++-- | The universe \(A\) of a relation \(R \subseteq A \times A\).+universe :: Ix a => Relation a a -> [a]+universe r+  | is_homogeneous r = domain r+  | otherwise = error "Relation is not homogeneous!"++-- | The size of the universe \(A\) of a relation \(R \subseteq A \times A\).+universeSize :: Ix a => Relation a a -> Int+universeSize r+  | is_homogeneous r =+      let ((a,_),(c,_)) = bounds r+      in A.rangeSize (a,c)+  | otherwise = error "Relation is not homogeneous!"++-- | Tests if a relation is homogeneous, i.e., if the domain is equal to the codomain.+is_homogeneous :: Ix a => Relation a a -> Bool+is_homogeneous r =+  let ((a,b),(c,d)) = bounds r+  in (a == b) && (c == d)++-- | The number of pairs \( (x,y) \in R \) for the given relation+-- \( R \subseteq A \times B \).+card :: (Ix a, Ix b) => Relation a b -> Bits+card = sumBit . elems+ -- | 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)+table :: (Ix a, Ix b)       => Array (a,b) Bool -> String table r = unlines $ do     let ((a,b),(c,d)) = A.bounds r-    x <- [ a .. c ]+    x <- A.range (a,c)     return $ unwords $ do-        y <- [ b .. d ]+        y <- A.range (b,d)         return $ if r A.! (x,y) then "*" else "."----

@@ -2,7 +2,7 @@  module Ersatz.Relation.Op -( +( -- * Operations   mirror , union@@ -12,76 +12,79 @@ , intersection , reflexive_closure , symmetric_closure+, transitive_closure+, transitive_reflexive_closure+, equivalence_closure )  where  import Ersatz.Relation.Data -import Prelude hiding ( and, or, not, product )-import Ersatz.Bit (and, or, not)+import Prelude hiding ( (&&), (||), and, or, not, product )+import Ersatz.Bit +import qualified Data.Array as A 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 \} \).+-- | Constructs the converse relation \( R^{-1} \) of a relation+-- \( R \subseteq A \times B \), which is defined by \( R^{-1} = \{ (y,x) ~|~ (x,y) \in R \} \subseteq B \times A \). 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 +-- | 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.,+-- | Constructs the difference \( R \setminus S \) of the relations+-- \(R, S \subseteq A \times B \), 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 \).+-- | Constructs the union \( R \cup S \) of the relations \( R, S \subseteq A \times B \). 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 ] )+        => Relation a b -> Relation a b -> Relation a b+union r s+    | bounds r == bounds s = build ( bounds r ) $ do+        i <- indices r+        return (i, r!i || s!i)+    | otherwise = error "Relations don't have the same bounds!" --- | 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) \} \).+-- | Constructs the composition \( R \circ S \) of the relations+-- \( R \subseteq A \times B \) and \( S \subseteq B \times C \), which is+-- defined by \( R \circ S = \{ (a,c) ~|~ (a,b) \in R \land (b,c) \in S \} \).+--+-- Formula size: linear in \(|A|\cdot|B|\cdot|C|\) product :: ( Ix a , Ix b, Ix c )-        => Relation a b -> Relation b c ->  Relation a c+        => Relation a b -> Relation b c -> Relation a c product a b =     let ((ao,al),(au,ar)) = bounds a-        ((_ ,bl),(_ ,br)) = bounds b+        ((bo,bl),(bu,br)) = bounds b         bnd = ((ao,bl),(au,br))-    in  build bnd $ do-          i@(x,z) <- range bnd-          return (i, or $ do-                y <- range ( al, ar )-                return $ and [ a!(x,y), b!(y,z) ]-                )+    in  if (al,ar) == (bo,bu)+            then build bnd $ do+                i@(x,z) <- range bnd+                return (i, or $ do+                        y <- range ( al, ar )+                        return $ and [ a!(x,y), b!(y,z) ]+                        )+            else error "Codomain of first relation must equal domain of second relation!"  -- | 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 -- ^ \(n\)-        -> Relation a a -> Relation a a+-- \( R^{0} \) is the identity relation \( I = \{ (x,x) ~|~ x \in A \} \).+--+-- Formula size: linear in \( |A|^3 \cdot  \log n \)+power  :: ( Ix a ) => Int -> Relation a a -> Relation a a power 0 r = identity ( bounds r ) power 1 r = r power e r =@@ -92,27 +95,58 @@         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)+-- | Constructs the intersection \( R \cap S \) of the relations \( R, S \subseteq A \times B \).+intersection :: ( Ix a , Ix b )       => Relation a b -> Relation a b       -> Relation a b-intersection r s = build ( bounds r ) $ do+intersection r s+    | bounds r == bounds s = build ( bounds r ) $ do         i <- indices r         return (i, and [ r!i, s!i ] )+    | otherwise = error "Relations don't have the same bounds!" --- | 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\).+-- | Constructs the reflexive closure \( R \cup R^{0} \) of the relation+-- \( R \subseteq A \times A \). 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\).+-- | Constructs the symmetric closure \( R \cup R^{-1} \) of the relation+-- \( R \subseteq A \times A \). symmetric_closure :: Ix a => Relation a a -> Relation a a symmetric_closure r =     union r $ mirror r++-- | Constructs the transitive closure \( R^{+} \) of the relation+-- \( R \subseteq A \times A \), which is defined by+-- \( R^{+} = \bigcup^{\infty}_{i = 1} R^{i} \).+--+-- Formula size: linear in \( |A|^3 \)+transitive_closure :: Ix a => Relation a a -> Relation a a+transitive_closure r =+  let n = universeSize r+      -- @a' ! (0,p,q)@ is true if and only if @r ! (p,q)@ is true+      a' = A.listArray ((0,1,1),(n,n,n)) (elems r)+      -- @a ! (0,p,q)@ is true if and only if @a' ! (0,p,q)@ is true+      a = a' A.// do+        -- If x > 0, then @a ! (p,x,q)@ is true if and only if there is a path from p to q via nodes {1,...,x} in r+        i@(x,p,q) <- A.range ((1,1,1),(n,n,n))+        return (i, a A.! (x-1,p,q) || a A.! (x-1,p,x) && a A.! (x-1,x,q))+  in build (bounds r) $ zip (indices r) [a A.! i | i <- A.range ((n,1,1),(n,n,n))]++-- | Constructs the transitive reflexive closure \( R^{*} \) of the relation+-- \( R \subseteq A \times A \), which is defined by+-- \( R^{*} = \bigcup^{\infty}_{i = 0} R^{i} \).+--+-- Formula size: linear in \( |A|^3 \)+transitive_reflexive_closure :: Ix a => Relation a a -> Relation a a+transitive_reflexive_closure r =+    union (transitive_closure r) (identity $ bounds r)++-- | Constructs the equivalence closure \( (R \cup R^{-1})^* \) of the relation+-- \( R \subseteq A \times A \).+--+-- Formula size: linear in \( |A|^3 \)+equivalence_closure :: Ix a => Relation a a -> Relation a a+equivalence_closure r =+  transitive_reflexive_closure $ symmetric_closure r

@@ -1,6 +1,7 @@+{-# OPTIONS_GHC -Wno-orphans #-} module Ersatz.Relation.Prop -( +( -- * Properties   implies , symmetric@@ -19,7 +20,6 @@ , complete , total , disjoint-, equals )  where@@ -29,19 +29,23 @@ import Ersatz.Relation.Data import Ersatz.Relation.Op import Ersatz.Counting+import Ersatz.Equatable  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 \).++instance (Ix a, Ix b) => Equatable (Relation a b) where+  r === s = and [implies r s, implies s r]+  r /== s = not $ r === s++-- | Given two relations \( R, S \subseteq A \times B \), check if \(R\) is a subset of \(S\). 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 ]+implies r s+  | bounds r == bounds s = and $ do+      i <- indices r+      return $ (r ! i) ==> (s ! i)+  | otherwise = error "Relations don't have the same bounds!"  -- | Tests if a relation is empty, i.e., the relation doesn't contain any elements. empty ::  ( Ix a, Ix b )@@ -56,46 +60,35 @@ 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+-- \( R \cup R^{-1} = A \times A \).+total :: ( Ix a ) => Relation a a -> Bit total r = complete $ symmetric_closure r --- | Tests if two relations are disjoint, i.e., +-- | 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+-- i.e., \( R \cup R^{-1} = 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+-- i.e., \( R \cap R^{-1} \subseteq R^{0} \).+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 \).+-- \( R \cap R^{0} = \emptyset \). 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)+irreflexive r = empty $ intersection (identity $ bounds r) r  -- | Tests if a relation \( R \subseteq A \times A \) is reflexive, i.e.,--- \( \forall x \in A: (x,x) \in R \).+-- \( R^{0} \subseteq 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)+reflexive r = implies (identity $ bounds r) r  -- | Given an 'Int' \( n \) and a relation \( R \subseteq A \times B \), check if -- \( \forall x \in A: | \{ (x,y) \in R \} | = n \) and@@ -146,7 +139,9 @@         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) \).+-- \( R \circ R = R \).+--+-- Formula size: linear in \( |A|^3 \) transitive :: ( Ix a )            => Relation a a -> Bit transitive r = implies (product r r) r

@@ -9,6 +9,8 @@ -------------------------------------------------------------------- module Ersatz.Solver   ( module Ersatz.Solver.DepQBF+  , module Ersatz.Solver.Kissat+  , module Ersatz.Solver.Lingeling   , module Ersatz.Solver.Minisat   , module Ersatz.Solver.Z3   , solveWith@@ -20,6 +22,8 @@ import Ersatz.Problem import Ersatz.Solution import Ersatz.Solver.DepQBF+import Ersatz.Solver.Kissat+import Ersatz.Solver.Lingeling import Ersatz.Solver.Minisat import Ersatz.Solver.Z3 

@@ -12,16 +12,18 @@ module Ersatz.Solver.DepQBF   ( depqbf   , depqbfPath+  , depqbfPathArgs   ) where -import Data.ByteString.Builder import Control.Monad.IO.Class-import Ersatz.Problem+import Data.Version (Version, makeVersion, parseVersion)+import Ersatz.Problem ( QSAT, writeQdimacs' ) import Ersatz.Solution import Ersatz.Solver.Common import qualified Data.IntMap as I-import System.IO+import System.Exit (ExitCode(..)) import System.Process (readProcessWithExitCode)+import qualified Text.ParserCombinators.ReadP as P  -- | This is a 'Solver' for 'QSAT' problems that runs the @depqbf@ solver using -- the current @PATH@, it tries to run an executable named @depqbf@.@@ -36,10 +38,14 @@ -- http://www.qbflib.org/qdimacs.html#output parseOutput :: String -> [(Int, Bool)] parseOutput out =-  case lines out of+  case filter (not . comment) $ lines out of     (_preamble:certLines) -> map parseCertLine certLines     [] -> error "QDIMACS output without preamble"   where+    comment [] = True+    comment ('c' : _) = True+    comment _ = False+     parseCertLine :: String -> (Int, Bool)     parseCertLine certLine =       case words certLine of@@ -47,14 +53,29 @@         _ -> error $ "Malformed QDIMACS certificate line: " ++ certLine  -- | This is a 'Solver' for 'QSAT' problems that lets you specify the path to the @depqbf@ executable.+-- This passes different arguments to @depqbf@ depending on its version:+--+-- * If using version 6.03 or later, this passes @[\"--qdo\", \"--no-dynamic-nenofex\"]@.+--+-- * Otherwise, this passes @[\"--qdo\"]@. depqbfPath :: MonadIO m => FilePath -> Solver QSAT m-depqbfPath path problem = liftIO $+depqbfPath path problem = do+  ver <- liftIO $ depqbfVersion path+  let args | ver >= makeVersion [6,03]+           = [ "--qdo", "--no-dynamic-nenofex" ]+           | otherwise+           = [ "--qdo" ]+  depqbfPathArgs path args problem++-- | This is a 'Solver' for 'QSAT' problems that lets you specify the path to the @depqbf@ executable+-- as well as a list of command line arguments. They will appear after the problem file name.+depqbfPathArgs :: MonadIO m => FilePath -> [String] -> Solver QSAT m+depqbfPathArgs path args problem = liftIO $   withTempFiles ".cnf" "" $ \problemPath _ -> do-    withFile problemPath WriteMode $ \fh ->-      hPutBuilder fh (qdimacs problem)+    writeQdimacs' problemPath problem      (exit, out, _err) <--      readProcessWithExitCode path [problemPath, "--qdo"] []+      readProcessWithExitCode path (problemPath : args) []      let result = resultOf exit @@ -64,3 +85,56 @@           I.fromList $ parseOutput out         _ ->           I.empty++-- | Query @depqbf@'s 'Version' by invoking @depqbf --version@ and parsing the+-- output. This assumes that the output can be parsed as a valid 'Version' and+-- that @depqbf@ versions increase in a way that is compatible with the+-- 'Ord Version' instance (see 'depqbfPath', which compares 'Version's using+-- ('>=')).+depqbfVersion :: FilePath -> IO Version+depqbfVersion path = do+  (exit, out, err) <-+    readProcessWithExitCode path ["--version"] []++  let parseError reason =+        fail $ unlines+          [ "Could not query depqbf version (" ++ reason ++ ")"+          , "Standard output:"+          , out+          , ""+          , "Standard error:"+          , err+          ]++  case exit of+    ExitSuccess -> do+      -- Should be something like "DepQBF 6.03"+      verStrLine <-+        case lines err of+          line:_ -> pure line+          [] -> parseError "no lines of standard error"+      -- Should be something like "6.03"+      verStr <-+        case words verStrLine of+          _depQBF:ver:_ -> pure ver+          _ -> parseError $ "unexpected version number " ++ verStrLine+      -- Convert the string to a full Version+      case readEitherP parseVersion verStr of+        Left reason -> parseError reason+        Right v -> pure v+    ExitFailure i ->+      parseError $ "exit code " ++ show i ++ ")"++-- | Like @readEither@ from "Text.Read", but accepting an arbitrary 'P.ReadP'+-- argument instead of requiring a 'Read' constraint.+readEitherP :: P.ReadP a -> String -> Either String a+readEitherP rp s =+  case [ x | (x,"") <- P.readP_to_S read' s ] of+    [x] -> Right x+    []  -> Left "no parse"+    _   -> Left "ambiguous parse"+ where+  read' = do+    x <- rp+    P.skipSpaces+    pure x

@@ -0,0 +1,50 @@+{-# LANGUAGE OverloadedStrings #-}++module Ersatz.Solver.Kissat+  ( kissat+  , kissatPath+  ) where++import Control.Monad.IO.Class+  ( MonadIO ( liftIO+            )+  )+import Ersatz.Problem+  ( SAT+  , writeDimacs'+  )+import Ersatz.Solution+  ( Solver+  )+import Ersatz.Solver.Common+  ( resultOf+  , withTempFiles+  , parseSolution5+  )+import System.Process+  ( readProcessWithExitCode+  )+++-- | 'Solver' for 'SAT' problems that tries to invoke the @kissat@ executable+-- from the @PATH@.+kissat :: MonadIO m => Solver SAT m+kissat = kissatPath "kissat"++-- | 'Solver' for 'SAT' problems that tries to invoke a program that takes+-- @kissat@ compatible arguments.+--+-- The 'FilePath' refers to the path to the executable.+kissatPath :: MonadIO m => FilePath -> Solver SAT m+kissatPath path problem = liftIO $+  withTempFiles ".cnf" "" $ \problemPath _ -> do+    writeDimacs' problemPath problem++    (exit, out, _err) <-+      readProcessWithExitCode path+                              [problemPath]+                              []++    let sol = parseSolution5 out++    return (resultOf exit, sol)

@@ -0,0 +1,84 @@+{-# LANGUAGE OverloadedStrings #-}++module Ersatz.Solver.Lingeling+  ( lingeling+  , plingeling+  , treengeling+  , lingelingPath+  , plingelingPath+  , treengelingPath+  ) where++import Control.Monad.IO.Class+  ( MonadIO ( liftIO+            )+  )+import Ersatz.Problem+  ( SAT+  , writeDimacs'+  )+import Ersatz.Solution+  ( Solver+  )+import Ersatz.Solver.Common+  ( resultOf+  , withTempFiles+  , parseSolution5+  )+import System.Process+  ( readProcessWithExitCode+  )++-- | 'Solver' for 'SAT' problems that tries to invoke the @lingeling@ executable+-- from the @PATH@.+lingeling :: MonadIO m => Solver SAT m+lingeling = lingelingPath "lingeling"++-- | 'Solver' for 'SAT' problems that tries to invoke the @plingeling@ executable+-- from the @PATH@.+plingeling :: MonadIO m => Solver SAT m+plingeling = ngelingPath "plingeling"++-- | 'Solver' for 'SAT' problems that tries to invoke the @treengeling@ executable+-- from the @PATH@.+treengeling :: MonadIO m => Solver SAT m+treengeling = ngelingPath "treengeling"++-- | 'Solver' for 'SAT' problems that tries to invoke a program that takes+-- @lingeling@ compatible arguments.+--+-- The 'FilePath' refers to the path to the executable.+lingelingPath :: MonadIO m => FilePath -> Solver SAT m+lingelingPath = ngelingPath++-- | 'Solver' for 'SAT' problems that tries to invoke a program that takes+-- @plingeling@ compatible arguments.+--+-- The 'FilePath' refers to the path to the executable.+plingelingPath :: MonadIO m => FilePath -> Solver SAT m+plingelingPath = ngelingPath++-- | 'Solver' for 'SAT' problems that tries to invoke a program that takes+-- @treengeling@ compatible arguments.+--+-- The 'FilePath' refers to the path to the executable.+treengelingPath :: MonadIO m => FilePath -> Solver SAT m+treengelingPath = ngelingPath++-- | 'Solver' for 'SAT' problems that tries to invoke a program that takes+-- @*ngeling@ compatible arguments.+--+-- The 'FilePath' refers to the path to the executable.+ngelingPath :: MonadIO m => FilePath -> Solver SAT m+ngelingPath path problem = liftIO $+  withTempFiles ".cnf" "" $ \problemPath _ -> do+    writeDimacs' problemPath problem++    (exit, out, _err) <-+      readProcessWithExitCode path+                              [problemPath]+                              []++    let sol = parseSolution5 out++    return (resultOf exit, sol)

@@ -19,19 +19,17 @@   , anyminisat   ) where -import Data.ByteString.Builder import Control.Exception (IOException, handle) import Control.Monad.IO.Class import Data.IntMap (IntMap)-import Ersatz.Problem+import Ersatz.Problem ( SAT, writeDimacs' ) import Ersatz.Solution import Ersatz.Solver.Common import qualified Data.IntMap.Strict as IntMap-import System.IO import System.Process (readProcessWithExitCode)  import qualified Data.ByteString.Char8 as B-import Data.List ( foldl' )+import qualified Data.List as List ( foldl' )  -- | Hybrid 'Solver' that tries to use: 'cryptominisat5', 'cryptominisat', and 'minisat' anyminisat :: Solver SAT IO@@ -51,8 +49,7 @@ minisatPath :: MonadIO m => FilePath -> Solver SAT m minisatPath path problem = liftIO $   withTempFiles ".cnf" "" $ \problemPath solutionPath -> do-    withFile problemPath WriteMode $ \fh ->-      hPutBuilder fh (dimacs problem)+    writeDimacs' problemPath problem      (exit, _out, _err) <-       readProcessWithExitCode path [problemPath, solutionPath] []@@ -71,7 +68,8 @@ parseSolution s =   case B.words s of     x : ys | x == "SAT" ->-          foldl' ( \ m y -> case B.readInt y of+          List.foldl'+                 ( \ m y -> case B.readInt y of                               Just (v,_) -> if 0 == v then m else IntMap.insert (abs v) (v>0) m                               Nothing    -> error $ "parseSolution: Expected an Int, received " ++ show y                  ) IntMap.empty ys@@ -87,8 +85,7 @@ cryptominisat5Path :: MonadIO m => FilePath -> Solver SAT m cryptominisat5Path path problem = liftIO $   withTempFiles ".cnf" "" $ \problemPath _ -> do-    withFile problemPath WriteMode $ \fh ->-      hPutBuilder fh (dimacs problem)+    writeDimacs' problemPath problem      (exit, out, _err) <-       readProcessWithExitCode path [problemPath] []

@@ -12,12 +12,10 @@   , z3Path   ) where -import Data.ByteString.Builder import Control.Monad.IO.Class-import Ersatz.Problem+import Ersatz.Problem ( SAT, writeDimacs' ) import Ersatz.Solution import Ersatz.Solver.Common-import System.IO import System.Process (readProcessWithExitCode)  -- | 'Solver' for 'SAT' problems that tries to invoke the @z3@ executable from the @PATH@@@ -30,8 +28,7 @@ z3Path :: MonadIO m => FilePath -> Solver SAT m z3Path path problem = liftIO $   withTempFiles ".cnf" "" $ \problemPath _ -> do-    withFile problemPath WriteMode $ \fh ->-      hPutBuilder fh (dimacs problem)+    writeDimacs' problemPath problem      (_exit, out, _err) <-       readProcessWithExitCode path ["-dimacs", problemPath] []

@@ -6,9 +6,8 @@ import Data.Default import qualified Data.IntMap.Strict as IntMap -import Test.Framework-import Test.Framework.Providers.HUnit-import Test.HUnit (Assertion, (@?=))+import Test.Tasty (TestTree, defaultMain, testGroup)+import Test.Tasty.HUnit (Assertion, (@?=), testCase)  import Ersatz import Ersatz.Internal.Literal@@ -16,12 +15,11 @@ main :: IO () main = defaultMain tests -tests :: [Test]+tests :: TestTree tests =-  [ testGroup "unit tests"-      [ testCase "unconstrained literals" case_unconstrained_literals-      ]-  ]+  testGroup "unit tests"+    [ testCase "unconstrained literals" case_unconstrained_literals+    ]  -- A regression test for #60 and #76. case_unconstrained_literals :: Assertion

@@ -1,4 +1,4 @@--- | graphs n nodes of degree <= d and diameter <= k +-- | graphs n nodes of degree <= d and diameter <= k -- see http://combinatoricswiki.org/wiki/The_Degree_Diameter_Problem_for_General_Graphs  -- usage: ./Moore d k n [s]@@ -9,7 +9,7 @@ -- s smaller => faster (more symmetries) but may lose solutions  -- test cases:  3 2 10 2  -- petersen graph---              5 2 24    +--              5 2 24   {-# language FlexibleContexts #-}@@ -39,7 +39,7 @@   putStrLn $ unwords [ "degree <=", show d, "diameter <=", show k, "nodes ==", show n, "symmetry ==", show s ]   (s, mg) <- solveWith anyminisat $ moore d k n s   case (s, mg) of-     (Satisfied, Just g) -> do printA g ; return True+     (Satisfied, Just g) -> do putStrLn $ R.table g ; return True      _ -> do return False  moore ::@@ -50,11 +50,11 @@   -- g <- R.symmetric_relation ((0,0),(n-1,n-1))   g <- periodic_relation s ((0,0),(n-1,n-1))   assert $ R.symmetric g-  assert $ R.reflexive g -  assert $ R.max_in_degree (d+1) g -  assert $ R.max_out_degree (d+1) g +  assert $ R.reflexive g+  assert $ R.max_in_degree (d+1) g+  assert $ R.max_out_degree (d+1) g   let p = R.power k g-  assert $ R.complete p +  assert $ R.complete p   return g  periodic_relation s bnd = do@@ -65,14 +65,4 @@   return $ R.build bnd $ do     i <- A.range bnd     return (i, r R.! normal i)-  --- | FIXME: this needs to go into a library-printA :: A.Array (Int,Int) Bool -> IO ()-printA a = putStrLn $ unlines $ do-         let ((u,l),(o,r)) = A.bounds a-         x <- [u .. o]-         return $ unwords $ do -             y <- [ l ..r ]-             return $ case a A.! (x,y) of-                  True -> "* " ; False -> ". "