packages feed

moonlight-core-0.1.0.0: src-solver/Moonlight/Core/Fixpoint/Dense/Internal/Scc.hs

-- | Strongly-connected-component condensation over CSR digraphs: the SCC plan
-- (vertex→component map, members, forward/backward condensation), frozen
-- digraph construction, and component expansion back to vertices.
module Moonlight.Core.Fixpoint.Dense.Internal.Scc
  ( SccPlan (..),
    FrozenDigraph (..),
    frozenDigraphFromSuccessors,
    expandComponents,
  )
where

import Data.Graph qualified as Graph
import Data.IntMap.Strict qualified as IntMap
import Data.IntSet (IntSet)
import Data.IntSet qualified as IntSet
import Data.Kind (Type)
import Data.List qualified as List
import Data.Vector.Unboxed (Vector)
import Data.Vector.Unboxed qualified as U
import Moonlight.Core.Fixpoint.Dense.Internal.Csr
  ( GraphCsr,
    RowCsr,
    csrFromBoundedRows,
    csrFromRows,
    csrTargetsForKey,
    csrTargetsSet,
    csrTranspose,
    csrVertexCount,
  )
import Prelude

type SccPlan :: Type
data SccPlan = SccPlan
  { sccOfVertex :: !(Vector Int),
    sccMembers :: !RowCsr,
    condensation :: !GraphCsr,
    condensationBackward :: !GraphCsr
  }
  deriving stock (Eq, Show)

type FrozenDigraph :: Type
data FrozenDigraph = FrozenDigraph
  { graphForward :: !GraphCsr,
    graphBackward :: !GraphCsr,
    graphSccPlan :: !SccPlan
  }
  deriving stock (Eq, Show)

frozenDigraphFromSuccessors :: Int -> (Int -> IntSet) -> FrozenDigraph
frozenDigraphFromSuccessors size successors =
  FrozenDigraph
    { graphForward = forward,
      graphBackward = backward,
      graphSccPlan = sccPlanFromCsr forward
    }
  where
    n = max 0 size
    forward = csrFromBoundedRows n [IntSet.toAscList (successors v) | v <- [0 .. n - 1]]
    backward = csrTranspose forward
{-# INLINE frozenDigraphFromSuccessors #-}

sccPlanFromCsr :: GraphCsr -> SccPlan
sccPlanFromCsr forward =
  SccPlan
    { sccOfVertex = vertexComponents,
      sccMembers = csrFromRows componentCount (fmap List.sort components),
      condensation = condensationForward,
      condensationBackward = csrTranspose condensationForward
    }
  where
    components =
      fmap sccVertices $
        Graph.stronglyConnComp
          [(v, v, U.toList (csrTargetsForKey forward v)) | v <- [0 .. csrVertexCount forward - 1]]
    componentCount = length components
    componentEntries = zip [0 ..] components
    vertexComponentMap =
      IntMap.fromList [(v, componentId) | (componentId, vs) <- componentEntries, v <- vs]
    vertexComponents =
      U.generate (csrVertexCount forward) (\v -> IntMap.findWithDefault v v vertexComponentMap)
    condensationForward =
      csrFromBoundedRows componentCount [IntSet.toAscList (successors componentId vs) | (componentId, vs) <- componentEntries]
    successors componentId vs =
      IntSet.delete componentId $
        IntSet.fromList
          [ targetComponent
            | v <- vs,
              target <- U.toList (csrTargetsForKey forward v),
              Just targetComponent <- [vertexComponents U.!? target]
          ]
    sccVertices :: Graph.SCC Int -> [Int]
    sccVertices scc =
      case scc of
        Graph.AcyclicSCC v -> [v]
        Graph.CyclicSCC vs -> List.sort vs
{-# INLINE sccPlanFromCsr #-}

expandComponents :: SccPlan -> IntSet -> IntSet
expandComponents plan =
  IntSet.foldl' (\acc component -> IntSet.union acc (csrTargetsSet (sccMembers plan) component)) IntSet.empty
{-# INLINE expandComponents #-}