module Data.Presburger.Omega.Set
(Set,
set, fromOmegaSet,
toOmegaSet,
dimension, predicate,
lowerBoundSatisfiable,
upperBoundSatisfiable,
obviousTautology,
definiteTautology,
exact,
inexact,
unknown,
equal,
upperBound, lowerBound,
union, intersection, difference,
Effort(..),
gist,
complement,
approximate
)
where
import System.IO.Unsafe
import Data.Presburger.Omega.Expr
import qualified Data.Presburger.Omega.LowLevel as L
import Data.Presburger.Omega.LowLevel(OmegaSet, Effort(..))
import Data.Presburger.Omega.SetRel
data Set = Set
{ setDim :: !Int
, setExp :: BoolExp
, setOmegaSet :: OmegaSet
}
instance Show Set where
showsPrec n s = showParen (n >= 10) $
showString "set " .
shows (setDim s) .
showChar ' ' .
showsPrec 10 (setExp s)
set :: Int
-> ([Var] -> BoolExp)
-> Set
set dim mk_expr
| variablesWithinRange dim expr =
Set
{ setDim = dim
, setExp = expr
, setOmegaSet = unsafePerformIO $ mkOmegaSet dim expr
}
| otherwise = error "set: Variables out of range"
where
expr = mk_expr (takeFreeVariables dim)
mkOmegaSet :: Int -> BoolExp -> IO OmegaSet
mkOmegaSet dim expr = L.newOmegaSet dim (\vars -> expToFormula vars expr)
fromOmegaSet :: OmegaSet -> IO Set
fromOmegaSet oset = do
(dim, expr) <- setToExpression oset
return $ Set
{ setDim = dim
, setExp = expr
, setOmegaSet = oset
}
omegaSetToSet :: Int -> OmegaSet -> IO Set
omegaSetToSet dim oset = return $
Set
{ setDim = dim
, setExp = unsafePerformIO $ do (_, expr) <- setToExpression oset
return expr
, setOmegaSet = oset
}
useSet :: (OmegaSet -> IO a) -> Set -> a
useSet f s = unsafePerformIO $ f (setOmegaSet s)
useSetSet :: (OmegaSet -> IO OmegaSet) -> Int -> Set -> Set
useSetSet f dim s = unsafePerformIO $ do
omegaSetToSet dim =<< f (setOmegaSet s)
useSet2 :: (OmegaSet -> OmegaSet -> IO a) -> Set -> Set -> a
useSet2 f s1 s2 = unsafePerformIO $ f (setOmegaSet s1) (setOmegaSet s2)
useSet2Set :: (OmegaSet -> OmegaSet -> IO OmegaSet)
-> Int
-> Set
-> Set
-> Set
useSet2Set f dim s1 s2 = unsafePerformIO $ do
omegaSetToSet dim =<< f (setOmegaSet s1) (setOmegaSet s2)
dimension :: Set -> Int
dimension = setDim
predicate :: Set -> BoolExp
predicate = setExp
toOmegaSet :: Set -> OmegaSet
toOmegaSet = setOmegaSet
upperBound :: Set -> Set
upperBound s = useSetSet L.upperBound (setDim s) s
lowerBound :: Set -> Set
lowerBound s = useSetSet L.lowerBound (setDim s) s
lowerBoundSatisfiable :: Set -> Bool
lowerBoundSatisfiable = useSet L.lowerBoundSatisfiable
upperBoundSatisfiable :: Set -> Bool
upperBoundSatisfiable = useSet L.upperBoundSatisfiable
obviousTautology :: Set -> Bool
obviousTautology = useSet L.obviousTautology
definiteTautology :: Set -> Bool
definiteTautology = useSet L.definiteTautology
exact :: Set -> Bool
exact = useSet L.exact
inexact :: Set -> Bool
inexact = useSet L.inexact
unknown :: Set -> Bool
unknown = useSet L.unknown
equal :: Set -> Set -> Bool
equal = useSet2 L.equal
union :: Set -> Set -> Set
union s1 s2 = useSet2Set L.union (setDim s1) s1 s2
intersection :: Set -> Set -> Set
intersection s1 s2 = useSet2Set L.intersection (setDim s1) s1 s2
difference :: Set -> Set -> Set
difference s1 s2 = useSet2Set L.difference (setDim s1) s1 s2
gist :: Effort -> Set -> Set -> Set
gist effort s1 s2 = useSet2Set (L.gist effort) (setDim s1) s1 s2
complement :: Set -> Set
complement s = useSetSet L.complement (setDim s) s
approximate :: Set -> Set
approximate s = useSetSet L.approximate (setDim s) s