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 = ([Boolean] -> m Boolean) -> [m Boolean] -> m Boolean
forall (m :: * -> *) a b. Monad m => ([a] -> m b) -> [m a] -> m b
monadic [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and ([m Boolean] -> m Boolean) -> [m Boolean] -> m Boolean
forall a b. (a -> b) -> a -> b
$ do
    (a, b)
i <- Relation a b -> [(a, b)]
forall {a} {b}. (Ix a, Ix b) => Relation a b -> [(a, b)]
indices Relation a b
r
    m Boolean -> [m Boolean]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (m Boolean -> [m Boolean]) -> m Boolean -> [m Boolean]
forall a b. (a -> b) -> a -> b
$ [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or [ Boolean -> Boolean
not (Boolean -> Boolean) -> Boolean -> Boolean
forall a b. (a -> b) -> a -> b
$ Relation a b
r Relation a b -> (a, b) -> Boolean
forall {a} {b}. (Ix a, Ix b) => Relation a b -> (a, b) -> Boolean
! (a, b)
i, Relation a b
s Relation a b -> (a, b) -> Boolean
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 = [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and ([Boolean] -> m Boolean) -> [Boolean] -> m Boolean
forall a b. (a -> b) -> a -> b
$ do
    (a, b)
i <- Relation a b -> [(a, b)]
forall {a} {b}. (Ix a, Ix b) => Relation a b -> [(a, b)]
indices Relation a b
r
    Boolean -> [Boolean]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Boolean -> [Boolean]) -> Boolean -> [Boolean]
forall a b. (a -> b) -> a -> b
$ Boolean -> Boolean
not (Boolean -> Boolean) -> Boolean -> Boolean
forall a b. (a -> b) -> a -> b
$ Relation a b
r Relation a b -> (a, b) -> Boolean
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 = Relation a b -> m Boolean
forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Relation a b -> m Boolean
empty (Relation a b -> m Boolean) -> Relation a b -> m Boolean
forall a b. (a -> b) -> a -> b
$ Relation a b -> Relation 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 <- Relation a b -> Relation a b -> m (Relation a b)
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
    Relation a b -> m Boolean
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 <- Relation a b -> Relation a b -> m Boolean
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 <- Relation a b -> Relation a b -> m Boolean
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
    [Boolean] -> m Boolean
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 = Relation a a -> Relation a a -> m Boolean
forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Relation a b -> Relation a b -> m Boolean
implies Relation a a
r ( Relation a a -> Relation a a
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 = [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and ([Boolean] -> m Boolean) -> [Boolean] -> m Boolean
forall a b. (a -> b) -> a -> b
$ do
    let ((a
a,a
b),(a
c,a
d)) = Relation a a -> ((a, a), (a, a))
forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b))
bounds Relation a a
r
    a
x <- (a, a) -> [a]
forall a. Ix a => (a, a) -> [a]
range ( a
a, a
c)
    Boolean -> [Boolean]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Boolean -> [Boolean]) -> Boolean -> [Boolean]
forall a b. (a -> b) -> a -> b
$ Boolean -> Boolean
Satchmo.Boolean.not (Boolean -> Boolean) -> Boolean -> Boolean
forall a b. (a -> b) -> a -> b
$ Relation a a
r Relation a a -> (a, a) -> Boolean
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 = [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and ([Boolean] -> m Boolean) -> [Boolean] -> m Boolean
forall a b. (a -> b) -> a -> b
$ do
    let ((a
a,a
b),(a
c,a
d)) = Relation a a -> ((a, a), (a, a))
forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b))
bounds Relation a a
r
    a
x <- (a, a) -> [a]
forall a. Ix a => (a, a) -> [a]
range (a
a,a
c)
    Boolean -> [Boolean]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Boolean -> [Boolean]) -> Boolean -> [Boolean]
forall a b. (a -> b) -> a -> b
$ Relation a a
r Relation a a -> (a, a) -> Boolean
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 = ([Boolean] -> m Boolean) -> [m Boolean] -> m Boolean
forall (m :: * -> *) a b. Monad m => ([a] -> m b) -> [m a] -> m b
monadic [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ Int -> Relation a b -> m Boolean
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, Int -> Relation a b -> m Boolean
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 = (Int -> [Boolean] -> m Boolean) -> Int -> Relation a b -> m Boolean
forall {m :: * -> *} {a} {b} {t}.
(MonadSAT m, Ix a, Ix b) =>
(t -> [Boolean] -> m Boolean) -> t -> Relation a b -> m Boolean
out_degree_helper Int -> [Boolean] -> m Boolean
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 = (Int -> [Boolean] -> m Boolean) -> Int -> Relation a b -> m Boolean
forall {m :: * -> *} {a} {b} {t}.
(MonadSAT m, Ix a, Ix b) =>
(t -> [Boolean] -> m Boolean) -> t -> Relation a b -> m Boolean
out_degree_helper Int -> [Boolean] -> m Boolean
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 = (Int -> [Boolean] -> m Boolean) -> Int -> Relation a b -> m Boolean
forall {m :: * -> *} {a} {b} {t}.
(MonadSAT m, Ix a, Ix b) =>
(t -> [Boolean] -> m Boolean) -> t -> Relation a b -> m Boolean
out_degree_helper Int -> [Boolean] -> m Boolean
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 = Int -> Relation b a -> m Boolean
forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Int -> Relation a b -> m Boolean
regular_out_degree Int
deg (Relation b a -> m Boolean) -> Relation b a -> m Boolean
forall a b. (a -> b) -> a -> b
$ Relation a b -> Relation b a
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 = Int -> Relation b a -> m Boolean
forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Int -> Relation a b -> m Boolean
max_out_degree Int
deg (Relation b a -> m Boolean) -> Relation b a -> m Boolean
forall a b. (a -> b) -> a -> b
$ Relation a b -> Relation b a
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 = Int -> Relation b a -> m Boolean
forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Int -> Relation a b -> m Boolean
min_out_degree Int
deg (Relation b a -> m Boolean) -> Relation b a -> m Boolean
forall a b. (a -> b) -> a -> b
$ Relation a b -> Relation b a
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 = ([Boolean] -> m Boolean) -> [m Boolean] -> m Boolean
forall (m :: * -> *) a b. Monad m => ([a] -> m b) -> [m a] -> m b
monadic [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and ([m Boolean] -> m Boolean) -> [m Boolean] -> m Boolean
forall a b. (a -> b) -> a -> b
$ do
    let ((a
a,b
b),(a
c,b
d)) = Relation a b -> ((a, b), (a, b))
forall a b. (Ix a, Ix b) => Relation a b -> ((a, b), (a, b))
bounds Relation a b
r
    a
x <- (a, a) -> [a]
forall a. Ix a => (a, a) -> [a]
range ( a
a , a
c )
    m Boolean -> [m Boolean]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (m Boolean -> [m Boolean]) -> m Boolean -> [m Boolean]
forall a b. (a -> b) -> a -> b
$ t -> [Boolean] -> m Boolean
f t
deg ([Boolean] -> m Boolean) -> [Boolean] -> m Boolean
forall a b. (a -> b) -> a -> b
$ do 
        b
y <- (b, b) -> [b]
forall a. Ix a => (a, a) -> [a]
range (b
b,b
d)
        Boolean -> [Boolean]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Boolean -> [Boolean]) -> Boolean -> [Boolean]
forall a b. (a -> b) -> a -> b
$ Relation a b
r Relation a b -> (a, b) -> Boolean
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 <- Relation a a -> Relation a a -> m (Relation a a)
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
    Relation a a -> Relation a a -> m Boolean
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

-- | relation R is a function iff for each x,
-- there is exactly one y such that R(x,y)
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 = Int -> Relation a b -> m Boolean
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

-- | relation R is a partial function iff for each x,
-- there is at most one y such that R(x,y)
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 = Int -> Relation a b -> m Boolean
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 = ([Boolean] -> m Boolean) -> [m Boolean] -> m Boolean
forall (m :: * -> *) a b. Monad m => ([a] -> m b) -> [m a] -> m b
monadic [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ Relation a b -> m Boolean
forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Relation a b -> m Boolean
is_function Relation a b
r , Relation b a -> m Boolean
forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Relation a b -> m Boolean
is_function (Relation a b -> Relation b a
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 = Relation a a -> m Boolean
forall a b (m :: * -> *).
(Ix a, Ix b, MonadSAT m) =>
Relation a b -> m Boolean
is_bijection Relation a a
r