{-# LANGUAGE CPP                #-}
{-# LANGUAGE RecordWildCards    #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric      #-}
{-# LANGUAGE OverloadedStrings  #-}
module Language.Fixpoint.Solver.Stats where

import           Control.DeepSeq
import           Data.Data
import           Data.Serialize                (Serialize (..))
import           GHC.Generics
import           Text.PrettyPrint.HughesPJ (text)
import qualified Data.Binary              as B
import qualified Language.Fixpoint.Types.PrettyPrint as F

#if !MIN_VERSION_base(4,14,0)
import           Data.Semigroup            (Semigroup (..))
#endif

data Stats = Stats 
  { Stats -> Int
numCstr      :: !Int -- ^ # Horn Constraints
  , Stats -> Int
numIter      :: !Int -- ^ # Refine Iterations
  , Stats -> Int
numBrkt      :: !Int -- ^ # smtBracket    calls (push/pop)
  , Stats -> Int
numChck      :: !Int -- ^ # smtCheckUnsat calls
  , Stats -> Int
numVald      :: !Int -- ^ # times SMT said RHS Valid
  } deriving (Typeable Stats
DataType
Constr
Typeable Stats
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Stats -> c Stats)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Stats)
-> (Stats -> Constr)
-> (Stats -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Stats))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Stats))
-> ((forall b. Data b => b -> b) -> Stats -> Stats)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Stats -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Stats -> r)
-> (forall u. (forall d. Data d => d -> u) -> Stats -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Stats -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Stats -> m Stats)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Stats -> m Stats)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Stats -> m Stats)
-> Data Stats
Stats -> DataType
Stats -> Constr
(forall b. Data b => b -> b) -> Stats -> Stats
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Stats -> c Stats
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Stats
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Stats -> u
forall u. (forall d. Data d => d -> u) -> Stats -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Stats -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Stats -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Stats -> m Stats
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Stats -> m Stats
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Stats
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Stats -> c Stats
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Stats)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Stats)
$cStats :: Constr
$tStats :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Stats -> m Stats
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Stats -> m Stats
gmapMp :: (forall d. Data d => d -> m d) -> Stats -> m Stats
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Stats -> m Stats
gmapM :: (forall d. Data d => d -> m d) -> Stats -> m Stats
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Stats -> m Stats
gmapQi :: Int -> (forall d. Data d => d -> u) -> Stats -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Stats -> u
gmapQ :: (forall d. Data d => d -> u) -> Stats -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Stats -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Stats -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Stats -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Stats -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Stats -> r
gmapT :: (forall b. Data b => b -> b) -> Stats -> Stats
$cgmapT :: (forall b. Data b => b -> b) -> Stats -> Stats
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Stats)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Stats)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Stats)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Stats)
dataTypeOf :: Stats -> DataType
$cdataTypeOf :: Stats -> DataType
toConstr :: Stats -> Constr
$ctoConstr :: Stats -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Stats
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Stats
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Stats -> c Stats
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Stats -> c Stats
$cp1Data :: Typeable Stats
Data, Int -> Stats -> ShowS
[Stats] -> ShowS
Stats -> String
(Int -> Stats -> ShowS)
-> (Stats -> String) -> ([Stats] -> ShowS) -> Show Stats
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, (forall x. Stats -> Rep Stats x)
-> (forall x. Rep Stats x -> Stats) -> Generic Stats
forall x. Rep Stats x -> Stats
forall x. Stats -> Rep Stats x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Stats x -> Stats
$cfrom :: forall x. Stats -> Rep Stats x
Generic, Stats -> Stats -> Bool
(Stats -> Stats -> Bool) -> (Stats -> Stats -> Bool) -> Eq Stats
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)

instance NFData Stats
instance B.Binary Stats
instance Serialize Stats

instance F.PTable Stats where
  ptable :: Stats -> DocTable
ptable Stats
s = [(Doc, Doc)] -> DocTable
F.DocTable [ (String -> Doc
text String
"# Constraints"                       , Int -> Doc
forall a. PPrint a => a -> Doc
F.pprint (Stats -> Int
numCstr      Stats
s))
                        , (String -> Doc
text String
"# Refine Iterations"                 , Int -> Doc
forall a. PPrint a => a -> Doc
F.pprint (Stats -> Int
numIter      Stats
s))
                        , (String -> Doc
text String
"# SMT Brackets"                      , Int -> Doc
forall a. PPrint a => a -> Doc
F.pprint (Stats -> Int
numBrkt      Stats
s))
                        , (String -> Doc
text String
"# SMT Queries (Valid)"               , Int -> Doc
forall a. PPrint a => a -> Doc
F.pprint (Stats -> Int
numVald      Stats
s))
                        , (String -> Doc
text String
"# SMT Queries (Total)"               , Int -> Doc
forall a. PPrint a => a -> Doc
F.pprint (Stats -> Int
numChck      Stats
s))
                        ]

instance Semigroup Stats where
  Stats
s1 <> :: Stats -> Stats -> Stats
<> Stats
s2 = 
    Stats :: Int -> Int -> Int -> Int -> Int -> Stats
Stats { numCstr :: Int
numCstr      = Stats -> Int
numCstr Stats
s1      Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Stats -> Int
numCstr Stats
s2
          , numIter :: Int
numIter      = Stats -> Int
numIter Stats
s1      Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Stats -> Int
numIter Stats
s2
          , numBrkt :: Int
numBrkt      = Stats -> Int
numBrkt Stats
s1      Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Stats -> Int
numBrkt Stats
s2
          , numChck :: Int
numChck      = Stats -> Int
numChck Stats
s1      Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Stats -> Int
numChck Stats
s2
          , numVald :: Int
numVald      = Stats -> Int
numVald Stats
s1      Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Stats -> Int
numVald Stats
s2
          }

instance Monoid Stats where
  mempty :: Stats
mempty  = Int -> Int -> Int -> Int -> Int -> Stats
Stats Int
0 Int
0 Int
0 Int
0 Int
0
  mappend :: Stats -> Stats -> Stats
mappend = Stats -> Stats -> Stats
forall a. Semigroup a => a -> a -> a
(<>)

-- | Returns the Horn clauses checked.
checked :: Stats -> Int
checked :: Stats -> Int
checked = Stats -> Int
numCstr

-- | Returns a number which can be used in the 'Safe' constructor of a 'FixResult' to show
-- \"the work done\".
totalWork :: Stats -> Int
totalWork :: Stats -> Int
totalWork Stats{Int
numVald :: Int
numChck :: Int
numBrkt :: Int
numIter :: Int
numCstr :: Int
numVald :: Stats -> Int
numChck :: Stats -> Int
numBrkt :: Stats -> Int
numIter :: Stats -> Int
numCstr :: Stats -> Int
..} = Int
numCstr Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
numIter Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
numBrkt Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
numChck Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
numVald