module Data.Presburger.Omega.Rel
(Rel,
rel, functionalRel, fromOmegaRel,
toOmegaRel,
inputDimension, outputDimension,
predicate,
lowerBoundSatisfiable,
upperBoundSatisfiable,
obviousTautology,
definiteTautology,
exact,
inexact,
unknown,
equal,
upperBound, lowerBound,
union, intersection, composition, join,
restrictDomain, restrictRange,
difference, crossProduct,
Effort(..),
gist,
transitiveClosure,
domain, range,
inverse,
complement,
deltas,
approximate
)
where
import System.IO.Unsafe
import Data.Presburger.Omega.Expr
import qualified Data.Presburger.Omega.LowLevel as L
import Data.Presburger.Omega.LowLevel(OmegaRel, Effort(..))
import Data.Presburger.Omega.SetRel
import qualified Data.Presburger.Omega.Set as Set
import Data.Presburger.Omega.Set(Set)
data Rel = Rel
{ relInpDim :: !Int
, relOutDim :: !Int
, relFun :: BoolExp
, relOmegaRel :: OmegaRel
}
instance Show Rel where
showsPrec n r = showParen (n >= 10) $
showString "rel " .
shows (relInpDim r) .
showChar ' ' .
shows (relOutDim r) .
showChar ' ' .
showsPrec 10 (relFun r)
where
showChar c = (c:)
rel :: Int
-> Int
-> BoolExp
-> Rel
rel inDim outDim expr
| variablesWithinRange (inDim + outDim) expr =
Rel
{ relInpDim = inDim
, relOutDim = outDim
, relFun = expr
, relOmegaRel = unsafePerformIO $ mkOmegaRel inDim outDim expr
}
| otherwise = error "rel: Variables out of range"
mkOmegaRel inDim outDim expr =
L.newOmegaRel inDim outDim $ \dom rng -> expToFormula (dom ++ rng) expr
functionalRel :: Int
-> [IntExp]
-> BoolExp
-> Rel
functionalRel dim range domain
| all (variablesWithinRange dim) range &&
variablesWithinRange dim domain =
Rel
{ relInpDim = dim
, relOutDim = length range
, relFun = relationPredicate
, relOmegaRel = unsafePerformIO $
mkFunctionalOmegaRel dim range domain
}
| otherwise = error "functionalRel: Variables out of range"
where
relationPredicate =
conjE (domain : zipWith outputPredicate [dim..] range)
outputPredicate index expr =
varE (nthVariable index) |==| expr
mkFunctionalOmegaRel :: Int -> [IntExp] -> BoolExp -> IO OmegaRel
mkFunctionalOmegaRel dim range domain =
L.newOmegaRel dim (length range) $ \dom rng ->
L.conjunction (domainConstraint dom : rangeConstraints dom rng)
where
domainConstraint dom = expToFormula dom domain
rangeConstraints dom rng = zipWith (rangeConstraint dom) range rng
rangeConstraint dom expr rngVar =
let
vars = dom ++ [rngVar]
expr' = expr |==| varE (nthVariable dim)
in expToFormula vars expr'
fromOmegaRel :: OmegaRel -> IO Rel
fromOmegaRel orel = do
(dim, range, expr) <- relToExpression orel
return $ Rel
{ relInpDim = dim
, relOutDim = range
, relFun = expr
, relOmegaRel = orel
}
omegaRelToRel :: Int -> Int -> OmegaRel -> IO Rel
omegaRelToRel inpDim outDim orel = return $
Rel
{ relInpDim = inpDim
, relOutDim = outDim
, relFun = unsafePerformIO $ do (_, _, expr) <- relToExpression orel
return $ expr
, relOmegaRel = orel
}
useRel :: (OmegaRel -> IO a) -> Rel -> a
useRel f r = unsafePerformIO $ f $ relOmegaRel r
useRelRel :: (OmegaRel -> IO OmegaRel) -> Int -> Int -> Rel -> Rel
useRelRel f inpDim outDim r = unsafePerformIO $ do
omegaRelToRel inpDim outDim =<< f (relOmegaRel r)
useRel2 :: (OmegaRel -> OmegaRel -> IO a) -> Rel -> Rel -> a
useRel2 f r1 r2 = unsafePerformIO $ f (relOmegaRel r1) (relOmegaRel r2)
useRel2Rel :: (OmegaRel -> OmegaRel -> IO OmegaRel)
-> Int -> Int -> Rel -> Rel -> Rel
useRel2Rel f inpDim outDim r1 r2 = unsafePerformIO $ do
omegaRelToRel inpDim outDim =<< f (relOmegaRel r1) (relOmegaRel r2)
inputDimension :: Rel -> Int
inputDimension = relInpDim
outputDimension :: Rel -> Int
outputDimension = relOutDim
toOmegaRel :: Rel -> OmegaRel
toOmegaRel = relOmegaRel
predicate :: Rel -> BoolExp
predicate = relFun
domain :: Rel -> Set
domain r = useRel (\ptr -> Set.fromOmegaSet =<< L.domain ptr) r
range :: Rel -> Set
range r = useRel (\ptr -> Set.fromOmegaSet =<< L.range ptr) r
lowerBoundSatisfiable :: Rel -> Bool
lowerBoundSatisfiable = useRel L.lowerBoundSatisfiable
upperBoundSatisfiable :: Rel -> Bool
upperBoundSatisfiable = useRel L.upperBoundSatisfiable
obviousTautology :: Rel -> Bool
obviousTautology = useRel L.obviousTautology
definiteTautology :: Rel -> Bool
definiteTautology = useRel L.definiteTautology
exact :: Rel -> Bool
exact = useRel L.exact
inexact :: Rel -> Bool
inexact = useRel L.inexact
unknown :: Rel -> Bool
unknown = useRel L.unknown
upperBound :: Rel -> Rel
upperBound r = useRelRel L.upperBound (relInpDim r) (relOutDim r) r
lowerBound :: Rel -> Rel
lowerBound r = useRelRel L.lowerBound (relInpDim r) (relOutDim r) r
equal :: Rel -> Rel -> Bool
equal = useRel2 L.equal
union :: Rel -> Rel -> Rel
union s1 s2 = useRel2Rel L.union (relInpDim s1) (relOutDim s1) s1 s2
intersection :: Rel -> Rel -> Rel
intersection s1 s2 =
useRel2Rel L.intersection (relInpDim s1) (relOutDim s1) s1 s2
composition :: Rel -> Rel -> Rel
composition s1 s2 =
useRel2Rel L.composition (relInpDim s2) (relOutDim s1) s1 s2
join :: Rel -> Rel -> Rel
join r1 r2 = composition r2 r1
restrictDomain :: Rel -> Set -> Rel
restrictDomain r s = unsafePerformIO $
omegaRelToRel (relInpDim r) (relOutDim r) =<<
L.restrictDomain (relOmegaRel r) (Set.toOmegaSet s)
restrictRange :: Rel -> Set -> Rel
restrictRange r s = unsafePerformIO $
omegaRelToRel (relInpDim r) (relOutDim r) =<<
L.restrictRange (relOmegaRel r) (Set.toOmegaSet s)
difference :: Rel -> Rel -> Rel
difference s1 s2 =
useRel2Rel L.difference (relInpDim s1) (relOutDim s1) s1 s2
crossProduct :: Set -> Set -> Rel
crossProduct s1 s2 = unsafePerformIO $
omegaRelToRel (Set.dimension s1) (Set.dimension s2) =<<
L.crossProduct (Set.toOmegaSet s1) (Set.toOmegaSet s2)
gist :: Effort -> Rel -> Rel -> Rel
gist effort r1 r2 =
useRel2Rel (L.gist effort) (relInpDim r1) (relOutDim r1) r1 r2
transitiveClosure :: Rel -> Rel
transitiveClosure r =
useRelRel L.transitiveClosure (relInpDim r) (relOutDim r) r
inverse :: Rel -> Rel
inverse s = useRelRel L.inverse (relOutDim s) (relInpDim s) s
complement :: Rel -> Rel
complement s = useRelRel L.complement (relInpDim s) (relOutDim s) s
deltas :: Rel -> Set
deltas = useRel (\wrel -> Set.fromOmegaSet =<< L.deltas wrel)
approximate :: Rel -> Rel
approximate s = useRelRel L.approximate (relInpDim s) (relOutDim s) s