module Satchmo.Relation.Prop
( implies
, symmetric
, transitive
, irreflexive
, reflexive
, regular
, regular_in_degree
, regular_out_degree
, max_in_degree
, min_in_degree
, max_out_degree
, min_out_degree
, empty
, complete
, disjoint
, equals
, is_function
, is_partial_function
, is_bijection
, is_permutation
)
where
import Prelude hiding ( and, or, not, product )
import qualified Prelude
import Satchmo.Code
import Satchmo.Boolean hiding (implies, equals)
import Satchmo.Counting
import Satchmo.Relation.Data
import Satchmo.Relation.Op
import qualified Satchmo.Counting as C
import Control.Monad ( guard )
import Data.Ix
import Satchmo.SAT
implies :: ( Ix a, Ix b, MonadSAT m )
=> Relation a b -> Relation a b -> m Boolean
{-# specialize inline implies :: ( Ix a, Ix b ) => Relation a b -> Relation a b -> SAT Boolean #-}
implies :: forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Relation a b -> Relation a b -> m Boolean
implies Relation a b
r Relation a b
s = forall (m :: * -> *) a b. Monad m => ([a] -> m b) -> [m a] -> m b
monadic forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and forall a b. (a -> b) -> a -> b
$ do
(a, b)
i <- forall {a} {b}. (Ix a, Ix b) => Relation a b -> [(a, b)]
indices Relation a b
r
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or [ Boolean -> Boolean
not forall a b. (a -> b) -> a -> b
$ Relation a b
r forall {a} {b}. (Ix a, Ix b) => Relation a b -> (a, b) -> Boolean
! (a, b)
i, Relation a b
s forall {a} {b}. (Ix a, Ix b) => Relation a b -> (a, b) -> Boolean
! (a, b)
i ]
empty :: ( Ix a, Ix b, MonadSAT m )
=> Relation a b -> m Boolean
empty :: forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Relation a b -> m Boolean
empty Relation a b
r = forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and forall a b. (a -> b) -> a -> b
$ do
(a, b)
i <- forall {a} {b}. (Ix a, Ix b) => Relation a b -> [(a, b)]
indices Relation a b
r
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Boolean -> Boolean
not forall a b. (a -> b) -> a -> b
$ Relation a b
r forall {a} {b}. (Ix a, Ix b) => Relation a b -> (a, b) -> Boolean
! (a, b)
i
complete :: Relation a b -> m Boolean
complete Relation a b
r = forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Relation a b -> m Boolean
empty forall a b. (a -> b) -> a -> b
$ forall a b. (Ix a, Ix b) => Relation a b -> Relation a b
complement Relation a b
r
disjoint :: Relation a b -> Relation a b -> m Boolean
disjoint Relation a b
r Relation a b
s = do
Relation a b
i <- forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Relation a b -> Relation a b -> m (Relation a b)
intersection Relation a b
r Relation a b
s
forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Relation a b -> m Boolean
empty Relation a b
i
equals :: Relation a b -> Relation a b -> m Boolean
equals Relation a b
r Relation a b
s = do
Boolean
rs <- forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Relation a b -> Relation a b -> m Boolean
implies Relation a b
r Relation a b
s
Boolean
sr <- forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Relation a b -> Relation a b -> m Boolean
implies Relation a b
s Relation a b
r
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ Boolean
rs, Boolean
sr ]
symmetric :: ( Ix a, MonadSAT m) => Relation a a -> m Boolean
{-# specialize inline symmetric :: ( Ix a ) => Relation a a -> SAT Boolean #-}
symmetric :: forall a (m :: * -> *).
(Ix a, MonadSAT m) =>
Relation a a -> m Boolean
symmetric Relation a a
r = forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Relation a b -> Relation a b -> m Boolean
implies Relation a a
r ( forall a b. (Ix a, Ix b) => Relation a b -> Relation b a
mirror Relation a a
r )
irreflexive :: ( Ix a, MonadSAT m) => Relation a a -> m Boolean
{-# specialize inline irreflexive :: ( Ix a ) => Relation a a -> SAT Boolean #-}
irreflexive :: forall a (m :: * -> *).
(Ix a, MonadSAT m) =>
Relation a a -> m Boolean
irreflexive Relation a a
r = forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and forall a b. (a -> b) -> a -> b
$ do
let ((a
a,a
b),(a
c,a
d)) = forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b))
bounds Relation a a
r
a
x <- forall a. Ix a => (a, a) -> [a]
range ( a
a, a
c)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Boolean -> Boolean
Satchmo.Boolean.not forall a b. (a -> b) -> a -> b
$ Relation a a
r forall {a} {b}. (Ix a, Ix b) => Relation a b -> (a, b) -> Boolean
! (a
x,a
x)
reflexive :: ( Ix a, MonadSAT m) => Relation a a -> m Boolean
{-# specialize inline reflexive :: ( Ix a ) => Relation a a -> SAT Boolean #-}
reflexive :: forall a (m :: * -> *).
(Ix a, MonadSAT m) =>
Relation a a -> m Boolean
reflexive Relation a a
r = forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and forall a b. (a -> b) -> a -> b
$ do
let ((a
a,a
b),(a
c,a
d)) = forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b))
bounds Relation a a
r
a
x <- forall a. Ix a => (a, a) -> [a]
range (a
a,a
c)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Relation a a
r forall {a} {b}. (Ix a, Ix b) => Relation a b -> (a, b) -> Boolean
! (a
x,a
x)
regular, regular_in_degree, regular_out_degree, max_in_degree, min_in_degree, max_out_degree, min_out_degree
:: ( Ix a, Ix b, MonadSAT m) => Int -> Relation a b -> m Boolean
regular :: forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Int -> Relation a b -> m Boolean
regular Int
deg Relation a b
r = forall (m :: * -> *) a b. Monad m => ([a] -> m b) -> [m a] -> m b
monadic forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Int -> Relation a b -> m Boolean
regular_in_degree Int
deg Relation a b
r, forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Int -> Relation a b -> m Boolean
regular_out_degree Int
deg Relation a b
r ]
regular_out_degree :: forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Int -> Relation a b -> m Boolean
regular_out_degree = forall {m :: * -> *} {a} {b} {t}.
(MonadSAT m, Ix a, Ix b) =>
(t -> [Boolean] -> m Boolean) -> t -> Relation a b -> m Boolean
out_degree_helper forall (m :: * -> *). MonadSAT m => Int -> [Boolean] -> m Boolean
exactly
max_out_degree :: forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Int -> Relation a b -> m Boolean
max_out_degree = forall {m :: * -> *} {a} {b} {t}.
(MonadSAT m, Ix a, Ix b) =>
(t -> [Boolean] -> m Boolean) -> t -> Relation a b -> m Boolean
out_degree_helper forall (m :: * -> *). MonadSAT m => Int -> [Boolean] -> m Boolean
atmost
min_out_degree :: forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Int -> Relation a b -> m Boolean
min_out_degree = forall {m :: * -> *} {a} {b} {t}.
(MonadSAT m, Ix a, Ix b) =>
(t -> [Boolean] -> m Boolean) -> t -> Relation a b -> m Boolean
out_degree_helper forall (m :: * -> *). MonadSAT m => Int -> [Boolean] -> m Boolean
atleast
regular_in_degree :: forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Int -> Relation a b -> m Boolean
regular_in_degree Int
deg Relation a b
r = forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Int -> Relation a b -> m Boolean
regular_out_degree Int
deg forall a b. (a -> b) -> a -> b
$ forall a b. (Ix a, Ix b) => Relation a b -> Relation b a
mirror Relation a b
r
max_in_degree :: forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Int -> Relation a b -> m Boolean
max_in_degree Int
deg Relation a b
r = forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Int -> Relation a b -> m Boolean
max_out_degree Int
deg forall a b. (a -> b) -> a -> b
$ forall a b. (Ix a, Ix b) => Relation a b -> Relation b a
mirror Relation a b
r
min_in_degree :: forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Int -> Relation a b -> m Boolean
min_in_degree Int
deg Relation a b
r = forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Int -> Relation a b -> m Boolean
min_out_degree Int
deg forall a b. (a -> b) -> a -> b
$ forall a b. (Ix a, Ix b) => Relation a b -> Relation b a
mirror Relation a b
r
out_degree_helper :: (t -> [Boolean] -> m Boolean) -> t -> Relation a b -> m Boolean
out_degree_helper t -> [Boolean] -> m Boolean
f t
deg Relation a b
r = forall (m :: * -> *) a b. Monad m => ([a] -> m b) -> [m a] -> m b
monadic forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and forall a b. (a -> b) -> a -> b
$ do
let ((a
a,b
b),(a
c,b
d)) = forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b))
bounds Relation a b
r
a
x <- forall a. Ix a => (a, a) -> [a]
range ( a
a , a
c )
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ t -> [Boolean] -> m Boolean
f t
deg forall a b. (a -> b) -> a -> b
$ do
b
y <- forall a. Ix a => (a, a) -> [a]
range (b
b,b
d)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Relation a b
r forall {a} {b}. (Ix a, Ix b) => Relation a b -> (a, b) -> Boolean
! (a
x,b
y)
transitive :: ( Ix a, MonadSAT m )
=> Relation a a -> m Boolean
{-# specialize inline transitive :: ( Ix a ) => Relation a a -> SAT Boolean #-}
transitive :: forall a (m :: * -> *).
(Ix a, MonadSAT m) =>
Relation a a -> m Boolean
transitive Relation a a
r = do
Relation a a
r2 <- forall a b c (m :: * -> *).
(Ix a, Ix b, Ix c, MonadSAT m) =>
Relation a b -> Relation b c -> m (Relation a c)
product Relation a a
r Relation a a
r
forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Relation a b -> Relation a b -> m Boolean
implies Relation a a
r2 Relation a a
r
is_function :: (Ix a, Ix b, MonadSAT m)
=> Relation a b -> m Boolean
is_function :: forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Relation a b -> m Boolean
is_function Relation a b
r = forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Int -> Relation a b -> m Boolean
regular_out_degree Int
1 Relation a b
r
is_partial_function :: (Ix a, Ix b, MonadSAT m)
=> Relation a b -> m Boolean
is_partial_function :: forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Relation a b -> m Boolean
is_partial_function Relation a b
r = forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Int -> Relation a b -> m Boolean
max_out_degree Int
1 Relation a b
r
is_bijection :: (Ix a, Ix b, MonadSAT m)
=> Relation a b -> m Boolean
is_bijection :: forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Relation a b -> m Boolean
is_bijection Relation a b
r = forall (m :: * -> *) a b. Monad m => ([a] -> m b) -> [m a] -> m b
monadic forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Relation a b -> m Boolean
is_function Relation a b
r , forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Relation a b -> m Boolean
is_function (forall a b. (Ix a, Ix b) => Relation a b -> Relation b a
mirror Relation a b
r) ]
is_permutation :: (Ix a, MonadSAT m)
=> Relation a a -> m Boolean
is_permutation :: forall a (m :: * -> *).
(Ix a, MonadSAT m) =>
Relation a a -> m Boolean
is_permutation Relation a a
r = forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Relation a b -> m Boolean
is_bijection Relation a a
r