{-# LANGUAGE BangPatterns          #-}

module Language.Fixpoint.Solver.Worklist
       ( -- * Worklist type is opaque
         Worklist, Stats

         -- * Initialize
       , init

         -- * Pop off a constraint
       , pop

         -- * Add a constraint and all its dependencies
       , push

         -- * Constraints with Concrete RHS
       , unsatCandidates

         -- * Statistics
       , wRanks
       )
       where

import           Prelude hiding (init)
import           Language.Fixpoint.Types.PrettyPrint
import qualified Language.Fixpoint.Types   as F
import           Language.Fixpoint.Graph.Types
import           Language.Fixpoint.Graph   (isTarget)

import           Control.Arrow             (first)
import qualified Data.HashMap.Strict       as M
import qualified Data.Set                  as S
import qualified Data.List                 as L
import           Text.PrettyPrint.HughesPJ (text)

-- | Worklist ------------------------------------------------------------------

data Worklist a = WL { forall a. Worklist a -> WorkSet
wCs     :: !WorkSet
                     , forall a. Worklist a -> CMap ()
wPend   :: !(CMap ())
                     , forall a. Worklist a -> CMap [SubcId]
wDeps   :: !(CMap [F.SubcId])
                     , forall a. Worklist a -> CMap (SimpC a)
wCm     :: !(CMap (F.SimpC a))
                     , forall a. Worklist a -> CMap Rank
wRankm  :: !(CMap Rank)
                     , forall a. Worklist a -> Maybe SubcId
wLast   :: !(Maybe F.SubcId)
                     , forall a. Worklist a -> Int
wRanks  :: !Int
                     , forall a. Worklist a -> Int
wTime   :: !Int
                     , forall a. Worklist a -> [SubcId]
wConcCs :: ![F.SubcId]
                     }

data Stats = Stats { Stats -> Int
numKvarCs  :: !Int
                   , Stats -> Int
numConcCs  :: !Int
                   , Stats -> Int
_numSccs   :: !Int
                   } deriving (Stats -> Stats -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Stats -> Stats -> Bool
$c/= :: Stats -> Stats -> Bool
== :: Stats -> Stats -> Bool
$c== :: Stats -> Stats -> Bool
Eq, Int -> Stats -> ShowS
[Stats] -> ShowS
Stats -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Stats] -> ShowS
$cshowList :: [Stats] -> ShowS
show :: Stats -> String
$cshow :: Stats -> String
showsPrec :: Int -> Stats -> ShowS
$cshowsPrec :: Int -> Stats -> ShowS
Show)

instance PPrint (Worklist a) where
  pprintTidy :: Tidy -> Worklist a -> Doc
pprintTidy Tidy
k = forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
S.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Worklist a -> WorkSet
wCs

instance PTable Stats where
  ptable :: Stats -> DocTable
ptable Stats
s = [(Doc, Doc)] -> DocTable
DocTable [ (String -> Doc
text String
"# Sliced Constraints", forall a. PPrint a => a -> Doc
pprint (Stats -> Int
numKvarCs Stats
s))
                      , (String -> Doc
text String
"# Target Constraints", forall a. PPrint a => a -> Doc
pprint (Stats -> Int
numConcCs Stats
s))
                      ]

instance PTable (Worklist a) where
  ptable :: Worklist a -> DocTable
ptable = forall a. PTable a => a -> DocTable
ptable forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Worklist a -> Stats
stats


-- | WorkItems ------------------------------------------------------------

type WorkSet  = S.Set WorkItem

data WorkItem = WorkItem { WorkItem -> SubcId
wiCId  :: !F.SubcId   -- ^ Constraint Id
                         , WorkItem -> Int
wiTime :: !Int   -- ^ Time at which inserted
                         , WorkItem -> Rank
wiRank :: !Rank  -- ^ Rank of constraint
                         } deriving (WorkItem -> WorkItem -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WorkItem -> WorkItem -> Bool
$c/= :: WorkItem -> WorkItem -> Bool
== :: WorkItem -> WorkItem -> Bool
$c== :: WorkItem -> WorkItem -> Bool
Eq, Int -> WorkItem -> ShowS
[WorkItem] -> ShowS
WorkItem -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [WorkItem] -> ShowS
$cshowList :: [WorkItem] -> ShowS
show :: WorkItem -> String
$cshow :: WorkItem -> String
showsPrec :: Int -> WorkItem -> ShowS
$cshowsPrec :: Int -> WorkItem -> ShowS
Show)

instance PPrint WorkItem where
  pprintTidy :: Tidy -> WorkItem -> Doc
pprintTidy Tidy
_ = String -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show

instance Ord WorkItem where
  compare :: WorkItem -> WorkItem -> Ordering
compare (WorkItem SubcId
i1 Int
t1 Rank
r1) (WorkItem SubcId
i2 Int
t2 Rank
r2)
    = forall a. Monoid a => [a] -> a
mconcat [ forall a. Ord a => a -> a -> Ordering
compare (Rank -> Int
rScc Rank
r1) (Rank -> Int
rScc Rank
r2)   -- SCC
              , forall a. Ord a => a -> a -> Ordering
compare Int
t1 Int
t2                 -- TimeStamp
              , forall a. Ord a => a -> a -> Ordering
compare (Rank -> Int
rIcc Rank
r1) (Rank -> Int
rIcc Rank
r2)   -- Inner SCC
              , forall a. Ord a => a -> a -> Ordering
compare (Rank -> Tag
rTag Rank
r1) (Rank -> Tag
rTag Rank
r2)   -- Tag
              , forall a. Ord a => a -> a -> Ordering
compare SubcId
i1         SubcId
i2         -- Otherwise Set drops items
              ]

--------------------------------------------------------------------------------
-- | Initialize worklist and slice out irrelevant constraints ------------------
--------------------------------------------------------------------------------
init :: SolverInfo a b -> Worklist a
--------------------------------------------------------------------------------
init :: forall a b. SolverInfo a b -> Worklist a
init SolverInfo a b
sI    = WL { wCs :: WorkSet
wCs     = WorkSet
items
                , wPend :: CMap ()
wPend   = CMap () -> [SubcId] -> CMap ()
addPends forall k v. HashMap k v
M.empty [SubcId]
kvarCs
                , wDeps :: CMap [SubcId]
wDeps   = CDeps -> CMap [SubcId]
cSucc CDeps
cd
                , wCm :: CMap (SimpC a)
wCm     = CMap (SimpC a)
cm
                , wRankm :: CMap Rank
wRankm  = {- F.tracepp "W.init ranks" -} CMap Rank
rankm
                , wLast :: Maybe SubcId
wLast   = forall a. Maybe a
Nothing
                , wRanks :: Int
wRanks  = CDeps -> Int
cNumScc CDeps
cd
                , wTime :: Int
wTime   = Int
0
                , wConcCs :: [SubcId]
wConcCs = [SubcId]
concCs
                }
  where
    cm :: CMap (SimpC a)
cm        = forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
F.cm  (forall a b. SolverInfo a b -> SInfo a
siQuery SolverInfo a b
sI)
    cd :: CDeps
cd        = forall a b. SolverInfo a b -> CDeps
siDeps SolverInfo a b
sI
    rankm :: CMap Rank
rankm     = CDeps -> CMap Rank
cRank CDeps
cd
    items :: WorkSet
items     = forall a. Ord a => [a] -> Set a
S.fromList forall a b. (a -> b) -> a -> b
$ CMap Rank -> Int -> SubcId -> WorkItem
workItemsAt CMap Rank
rankm Int
0 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SubcId]
kvarCs
    concCs :: [SubcId]
concCs    = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(SubcId, SimpC a)]
ics
    kvarCs :: [SubcId]
kvarCs    = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(SubcId, SimpC a)]
iks
    ([(SubcId, SimpC a)]
ics,[(SubcId, SimpC a)]
iks) = forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (forall (c :: * -> *) a. TaggedC c a => c a -> Bool
isTarget forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) (forall k v. HashMap k v -> [(k, v)]
M.toList CMap (SimpC a)
cm)

---------------------------------------------------------------------------
-- | Candidate Constraints to be checked AFTER computing Fixpoint ---------
---------------------------------------------------------------------------
unsatCandidates   :: Worklist a -> [F.SimpC a]
---------------------------------------------------------------------------
unsatCandidates :: forall a. Worklist a -> [SimpC a]
unsatCandidates Worklist a
w = [ forall a. (?callStack::CallStack) => CMap a -> SubcId -> a
lookupCMap (forall a. Worklist a -> CMap (SimpC a)
wCm Worklist a
w) SubcId
i | SubcId
i <- forall a. Worklist a -> [SubcId]
wConcCs Worklist a
w ]


---------------------------------------------------------------------------
pop  :: Worklist a -> Maybe (F.SimpC a, Worklist a, Bool, Int)
---------------------------------------------------------------------------
pop :: forall a. Worklist a -> Maybe (SimpC a, Worklist a, Bool, Int)
pop Worklist a
w = do
  (SubcId
i, WorkSet
is) <- WorkSet -> Maybe (SubcId, WorkSet)
sPop forall a b. (a -> b) -> a -> b
$ forall a. Worklist a -> WorkSet
wCs Worklist a
w
  forall a. a -> Maybe a
Just ( forall a. (?callStack::CallStack) => CMap a -> SubcId -> a
lookupCMap (forall a. Worklist a -> CMap (SimpC a)
wCm Worklist a
w) SubcId
i
       , forall a. Worklist a -> SubcId -> WorkSet -> Worklist a
popW Worklist a
w SubcId
i WorkSet
is
       , forall a. Worklist a -> SubcId -> Bool
newSCC Worklist a
w SubcId
i
       , forall a. Worklist a -> SubcId -> Int
rank Worklist a
w SubcId
i
       )

popW :: Worklist a -> F.SubcId -> WorkSet -> Worklist a
popW :: forall a. Worklist a -> SubcId -> WorkSet -> Worklist a
popW Worklist a
w SubcId
i WorkSet
is = Worklist a
w { wCs :: WorkSet
wCs   = WorkSet
is
                , wLast :: Maybe SubcId
wLast = forall a. a -> Maybe a
Just SubcId
i
                , wPend :: CMap ()
wPend = CMap () -> SubcId -> CMap ()
remPend (forall a. Worklist a -> CMap ()
wPend Worklist a
w) SubcId
i }


newSCC :: Worklist a -> F.SubcId -> Bool
newSCC :: forall a. Worklist a -> SubcId -> Bool
newSCC Worklist a
oldW SubcId
i = (Rank -> Int
rScc forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Rank
oldRank) forall a. Eq a => a -> a -> Bool
/= (Rank -> Int
rScc forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Rank
newRank)
  where
    oldRank :: Maybe Rank
oldRank   = forall a. (?callStack::CallStack) => CMap a -> SubcId -> a
lookupCMap CMap Rank
rankm forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Worklist a -> Maybe SubcId
wLast Worklist a
oldW
    newRank :: Maybe Rank
newRank   = forall a. a -> Maybe a
Just              forall a b. (a -> b) -> a -> b
$  forall a. (?callStack::CallStack) => CMap a -> SubcId -> a
lookupCMap CMap Rank
rankm SubcId
i
    rankm :: CMap Rank
rankm     = forall a. Worklist a -> CMap Rank
wRankm Worklist a
oldW

rank :: Worklist a -> F.SubcId -> Int
rank :: forall a. Worklist a -> SubcId -> Int
rank Worklist a
w SubcId
i = Rank -> Int
rScc forall a b. (a -> b) -> a -> b
$ forall a. (?callStack::CallStack) => CMap a -> SubcId -> a
lookupCMap (forall a. Worklist a -> CMap Rank
wRankm Worklist a
w) SubcId
i

---------------------------------------------------------------------------
push :: F.SimpC a -> Worklist a -> Worklist a
---------------------------------------------------------------------------
push :: forall a. SimpC a -> Worklist a -> Worklist a
push SimpC a
c Worklist a
w = Worklist a
w { wCs :: WorkSet
wCs   = WorkSet -> [WorkItem] -> WorkSet
sAdds (forall a. Worklist a -> WorkSet
wCs Worklist a
w) [WorkItem]
wis'
             , wTime :: Int
wTime = Int
1 forall a. Num a => a -> a -> a
+ Int
t
             , wPend :: CMap ()
wPend = CMap () -> [SubcId] -> CMap ()
addPends CMap ()
wp [SubcId]
is'
             }
  where
    i :: SubcId
i    = forall (c :: * -> *) a. TaggedC c a => c a -> SubcId
F.subcId SimpC a
c
    is' :: [SubcId]
is'  = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. CMap () -> SubcId -> Bool
isPend CMap ()
wp) forall a b. (a -> b) -> a -> b
$ forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault [] SubcId
i (forall a. Worklist a -> CMap [SubcId]
wDeps Worklist a
w)
    wis' :: [WorkItem]
wis' = CMap Rank -> Int -> SubcId -> WorkItem
workItemsAt (forall a. Worklist a -> CMap Rank
wRankm Worklist a
w) Int
t forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SubcId]
is'
    t :: Int
t    = forall a. Worklist a -> Int
wTime Worklist a
w
    wp :: CMap ()
wp   = forall a. Worklist a -> CMap ()
wPend Worklist a
w

workItemsAt :: CMap Rank -> Int -> F.SubcId -> WorkItem
workItemsAt :: CMap Rank -> Int -> SubcId -> WorkItem
workItemsAt !CMap Rank
r !Int
t !SubcId
i = WorkItem { wiCId :: SubcId
wiCId  = SubcId
i
                                , wiTime :: Int
wiTime = Int
t
                                , wiRank :: Rank
wiRank = forall a. (?callStack::CallStack) => CMap a -> SubcId -> a
lookupCMap CMap Rank
r SubcId
i }



---------------------------------------------------------------------------
stats :: Worklist a -> Stats
---------------------------------------------------------------------------
stats :: forall a. Worklist a -> Stats
stats Worklist a
w = Int -> Int -> Int -> Stats
Stats (forall a. Worklist a -> Int
kn Worklist a
w) (forall a. Worklist a -> Int
cn Worklist a
w) (forall a. Worklist a -> Int
wRanks Worklist a
w)
  where
    kn :: Worklist a -> Int
kn  = forall k v. HashMap k v -> Int
M.size forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Worklist a -> CMap (SimpC a)
wCm
    cn :: Worklist a -> Int
cn  = forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Worklist a -> [SubcId]
wConcCs

---------------------------------------------------------------------------
-- | Pending API
---------------------------------------------------------------------------

addPends :: CMap () -> [F.SubcId] -> CMap ()
addPends :: CMap () -> [SubcId] -> CMap ()
addPends = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' CMap () -> SubcId -> CMap ()
addPend

addPend :: CMap () -> F.SubcId -> CMap ()
addPend :: CMap () -> SubcId -> CMap ()
addPend CMap ()
m SubcId
i = forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert SubcId
i () CMap ()
m

remPend :: CMap () -> F.SubcId -> CMap ()
remPend :: CMap () -> SubcId -> CMap ()
remPend CMap ()
m SubcId
i = forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
M.delete SubcId
i CMap ()
m

isPend :: CMap () -> F.SubcId -> Bool
isPend :: CMap () -> SubcId -> Bool
isPend CMap ()
w SubcId
i = forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
M.member SubcId
i CMap ()
w

---------------------------------------------------------------------------
-- | Set API --------------------------------------------------------------
---------------------------------------------------------------------------

sAdds :: WorkSet -> [WorkItem] -> WorkSet
sAdds :: WorkSet -> [WorkItem] -> WorkSet
sAdds = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. Ord a => a -> Set a -> Set a
S.insert)

sPop :: WorkSet -> Maybe (F.SubcId, WorkSet)
sPop :: WorkSet -> Maybe (SubcId, WorkSet)
sPop = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first WorkItem -> SubcId
wiCId) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> Maybe (a, Set a)
S.minView