uuagc-0.9.53: src/LOAG/Chordal.hs
{-# LANGUAGE CPP #-}
module LOAG.Chordal where
#ifdef WITH_LOAG
import LOAG.Common
import LOAG.Graphs
import LOAG.Optimise
import LOAG.Solver.MiniSat
import Options
import Control.Monad (unless, forM, when, foldM)
import Control.Monad.ST
import qualified Data.Array as A
import Data.Array.IO
import Data.Array.ST as ST
import qualified Data.IntMap as IM
import qualified Data.IntSet as IS
import qualified Data.Map as M
import Data.Maybe (isNothing, catMaybes)
import qualified Data.Set as S
import Data.STRef
type Neigh = (Vertex, EdgeType)
data EdgeType = Sib MyVar -- Edge between siblings
| Any MyVar -- Unknown
| NSib MyVar -- Edge between non-siblings
deriving (Show)
extract (Sib l) = l
extract (Any l) = l
extract (NSib l)= l
neg :: EdgeType -> EdgeType
neg (Sib p) = Sib $ varnot p
neg (NSib p) = NSib $ varnot p
neg (Any p) = Any $ varnot p
type NtGraph = IM.IntMap [(Vertex,MyVar)]
type ToChordal = IM.IntMap [Neigh]
type SatEdge = (Vertex, Neigh)
addClauses :: Sat -> [[EdgeType]] -> IO ()
addClauses sat = mapM_ (addClause sat . map extract)
toChordal :: [(Edge,EdgeType)] -> IO ToChordal
toChordal es =
let edges = concatMap (\((a,b),c) -> [(a,[(b,c)]),(b,[(a,neg c)])]) es
in return $ IM.fromListWith (++) edges
toNtGraph :: [(Edge,MyVar)] -> IO NtGraph
toNtGraph es =
let edges = concatMap (\((a,b),c) -> [(a,[(b,c)]),(b,[(a,varnot c)])]) es
in return $ IM.fromListWith (++) edges
remove :: Vertex -> [Neigh] -> ToChordal -> ToChordal
remove v ns g = foldr (IM.adjust remN . fst) (IM.delete v g) ns
where remN ns = filter ((/= v).fst) ns
adds :: ToChordal -> [SatEdge] -> ToChordal
adds g = foldl add g
add :: ToChordal -> SatEdge -> ToChordal
add g (v,n@(v2,c)) = IM.adjust (n:) v
$ IM.adjust ((v,neg c):) v2 g
removeNt :: Vertex -> [(Vertex,MyVar)] -> NtGraph -> NtGraph
removeNt v ns g = foldr (IM.adjust remN . fst) (IM.delete v g) ns
where remN ns = filter ((/= v).fst) ns
addsNt g = foldl addNt g
addNt g (v,n@(v2,c)) = IM.adjust (n:) v
$ IM.adjust ((v,varnot c):) v2 g
scheduleLOAG :: Ag -> (String -> IO ()) -> Options -> IO LOAGRes
scheduleLOAG ag@(Ag nbounds pbounds dps nts) putStrLn opts = do
let optim | minvisits opts = [MinVisits] -- todo: allow specification of more optimisations
| otherwise = []
putStrLn "--- Starting ---"
sat <- newSolvable
varMap <- noNtCycles sat nts putStrLn
noPrCycles sat prs varMap putStrLn
(v,p) <- satValues sat
putStrLn $ "nr. of variables: " ++ show v
putStrLn $ "nr. of clauses: " ++ show p
putStrLn "--- Solving ---"
b <- satsolve sat []
if not b then error "Not LOAG"
else do putStrLn "--- Constructing Interfaces ---"
(ids,edp,interfaces) <- loagRes sat varMap dps
let oldct = getVisCount nts interfaces
when (minvisits opts) $
putStrLn "--- Minimising #Visit"
optimise sat varMap optim nbounds nts interfaces
(ids',edp',interfaces') <- loagRes sat varMap dps
let visC@newct = getVisCount nts interfaces'
when (minvisits opts) $ do
putStrLn ("--- #Visits (max,sum,avg) " ++(show oldct)
++" --> " ++(show newct))
putStrLn "--- Code Generation ---"
return (Just edp',interfaces',[])
where loagRes sat varMap dps = do
(ids,edp) <- mkGraphs sat varMap dps
interfaces <- mkInterfaces ids
return (ids,edp,interfaces)
prs = [ p | (Nt _ _ _ _ _ ps) <- nts, p <- ps]
mkInterfaces ids = return $ runST $ do
schedA <- newArray nbounds Nothing
schedS <- newSTRef $ foldr (\(Nt nt _ _ _ _ _) ->
M.insert nt (IM.singleton 1 []))
M.empty nts
completing ids (schedA, schedS) nts
mkGraphs :: Sat -> M.Map Edge MyVar -> [Edge] ->
IO (FrGraph,TDPRes)
mkGraphs sat varMap dps = do
idsf <- newArray nbounds IS.empty :: IO (IOArray Vertex Vertices)
idst <- newArray nbounds IS.empty :: IO (IOArray Vertex Vertices)
edp <- newArray pbounds IS.empty :: IO (IOArray Vertex Vertices)
let (ids) = (idsf,idst)
sequence_ [ do v <- value sat pred
case v of
Nothing -> error "no val"
Just True -> addEdges (i,s) (zip ios sos) ids edp
Just False-> addEdges (s,i) (zip sos ios) ids edp
| Nt _ _ _ inhs outs _ <- nts
, (i,ios,_) <- inhs
, (s,sos,_) <- outs
, let pred = varMap M.! (i,s)
]
forM dps $ \(f,t) -> do
modifyArray edp t (f `IS.insert`)
f_idsf <- freeze idsf
f_idst <- freeze idst
f_edp <- freeze edp
return ((f_idsf,f_idst),f_edp)
where addEdges (f,t) es (idsf,idst) edp = do
modifyArray idsf f (t `IS.insert`)
modifyArray idst t (f `IS.insert`)
forM es $ \(f,t) -> do --edp does not reflect flow
modifyArray edp t (f `IS.insert`)
noCyclesNt :: Sat -> NtGraph -> IO ()
noCyclesNt sat g | IM.null g = return ()
| otherwise = do
news <- sequence [ noTriangleNt sat g p q | (p,q) <- pairs neighs]
let g' = addsNt (removeNt node neighs g) (concat news)
noCyclesNt sat g'
where
node = snd $ minimum [ (length xs, a) | (a,xs) <- IM.toList g ]
Just neighs = IM.lookup node g
noTriangleNt :: Sat -> NtGraph -> (Vertex, MyVar) ->
(Vertex, MyVar) -> IO [(Vertex,(Vertex,MyVar))]
noTriangleNt sat g e1@(t1,c1) e2@(t2,c2) =
case IM.lookup t1 g of
Just ns ->
case [ c | (t2',c) <- ns, t2' == t2 ] of
[] -> do c3 <- newLit sat
ruleOut c1 c2 c3
return [(t1,(t2,c3))]
[c3] -> ruleOut c1 c2 c3 >> return []
_ -> error "multiple edges between two nodes"
Nothing -> error "pointer outside of graph"
where
ruleOut ea eb ab= do addClause sat [ea, ab, varnot eb]
addClause sat [varnot ea,varnot ab,eb]
noCyclesPr :: Sat -> ToChordal -> IO ()
noCyclesPr sat g | IM.null g = return ()
| otherwise = do
news <- sequence [ noTriangle sat g p q | (p,q) <- validPairs neighs]
let g' = adds (remove node neighs g) (concat news)
noCyclesPr sat g'
where
node = snd $ minimum [ (weight xs, a)
| (a,xs) <- IM.toList g ]
Just neighs = IM.lookup node g
validPairs ns = [ (p,q) | p <- sibs, q <- nsibs ] ++
[ (p,q) | p <- nsibs, q <- anys ] ++
[ (p,q) | p <- sibs, q <- anys ]
++ (pairs anys)
where sibs = [ n | n@(_,Sib _) <- ns ]
nsibs= [ n | n@(_,NSib _) <- ns ]
anys = [ n | n@(_,Any _) <- ns ]
weight :: [Neigh] -> Int
weight xs = ss*3 * (ds + cs) + (ds + cs)^2
where
ss = length [ x | x@(_,Sib _) <- xs ]
ds = length [ x | x@(_,NSib _) <- xs ]
cs = length [ x | x@(_,Any _) <- xs ]
noTriangle :: Sat -> ToChordal -> Neigh -> Neigh -> IO [SatEdge]
noTriangle sat g e1@(t1,c1) e2@(t2,c2) =
case IM.lookup t1 g of
Just ns ->
case [ c | (t2',c) <- ns, t2' == t2 ] of
[] -> do p <- newLit sat
ruleOut c1 c2 (Any p)
return [(t1,(t2,(Any p)))]
[c3] -> ruleOut c1 c2 c3 >> return []
_ -> error "multiple edges between two nodes"
Nothing -> error "pointer outside of graph"
where ruleOut ea eb ab= addClauses sat [[ea, ab, neg eb],[neg ea,neg ab,eb]]
noNtCycles :: Sat -> [Nt] -> (String -> IO ()) -> IO VarMap
noNtCycles sat tps putStrLn = do
putStrLn "--- Non-Terminals ---"
maps <- mapM forNt tps
return $ M.unions maps
where -- at non-terminal level, all cycles are between siblings
-- that is why we force all the edges to be the same
-- (not filtered by validPairs)
forNt tp@(Nt tid dpf dpt inhs syns _) = do
vars <- satValues sat
putStrLn ("nt : " ++ tid ++ " ... " ++
show vars ++ " ...")
when (not $ S.null $ S.fromList dpf `S.intersection`
S.fromList (map (\(a,b) -> (b,a)) dpt)) $
error "Type 2 cycle of length 2"
ass <- sequence $
[ return ((i,s),VarTrue) | ((i,s)) <- dpf ]++
[ return ((i,s),VarFalse)| ((s,i)) <- dpt ]
let assM = M.fromList ass
mvars<- sequence
[ if new then do
p <- newLit sat
return $ Just ((i,s),p) else return Nothing
| (i,_,_) <- inhs
, (s,_,_) <- syns
, let mmv = maybe (M.lookup (s,i) assM) Just
(M.lookup (i,s) assM)
new = isNothing mmv ]
let vars = ass ++ catMaybes mvars
g <- toNtGraph vars
noCyclesNt sat g
return $ M.fromList vars
noPrCycles :: Sat -> [Pr] -> VarMap -> (String -> IO ()) -> IO ()
noPrCycles sat prods varMap putStrLn = do
putStrLn "--- Productions ---"
mapM_ forProd prods
where forProd (Pr prod es ses fs) | length fs ==1 = return () --taken care of
| otherwise = do
vars <- satValues sat
putStrLn ("prod: " ++ show prod ++ " ... " ++
show vars ++ " ...")
g <- toChordal (sibs ++ dps)
noCyclesPr sat g
where sibs= [ ((f,t),Sib c) | (e@(f,t),ge,_) <- ses
, let c = case M.lookup ge varMap of
Just p -> p
Nothing -> error "no var found"]
dps = [ (e,NSib VarTrue) | e <- es ]
#else
scheduleLOAG = error "You need to install uuagc with the -fwith-loag flag in order to use the --loag option."
#endif