{-# 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.Store              as S
import qualified Language.Fixpoint.Types.PrettyPrint as F
import Data.Aeson

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
Stats -> DataType
Stats -> Constr
(forall b. Data b => b -> b) -> Stats -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> Stats -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Stats -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Stats -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Stats -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, 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, 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
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 S.Store 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"                       , forall a. PPrint a => a -> Doc
F.pprint (Stats -> Int
numCstr      Stats
s))
                        , (String -> Doc
text String
"# Refine Iterations"                 , forall a. PPrint a => a -> Doc
F.pprint (Stats -> Int
numIter      Stats
s))
                        , (String -> Doc
text String
"# SMT Brackets"                      , forall a. PPrint a => a -> Doc
F.pprint (Stats -> Int
numBrkt      Stats
s))
                        , (String -> Doc
text String
"# SMT Queries (Valid)"               , forall a. PPrint a => a -> Doc
F.pprint (Stats -> Int
numVald      Stats
s))
                        , (String -> Doc
text String
"# SMT Queries (Total)"               , 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 { numCstr :: Int
numCstr      = Stats -> Int
numCstr Stats
s1      forall a. Num a => a -> a -> a
+ Stats -> Int
numCstr Stats
s2
          , numIter :: Int
numIter      = Stats -> Int
numIter Stats
s1      forall a. Num a => a -> a -> a
+ Stats -> Int
numIter Stats
s2
          , numBrkt :: Int
numBrkt      = Stats -> Int
numBrkt Stats
s1      forall a. Num a => a -> a -> a
+ Stats -> Int
numBrkt Stats
s2
          , numChck :: Int
numChck      = Stats -> Int
numChck Stats
s1      forall a. Num a => a -> a -> a
+ Stats -> Int
numChck Stats
s2
          , numVald :: Int
numVald      = Stats -> Int
numVald Stats
s1      forall a. Num a => a -> a -> a
+ Stats -> Int
numVald Stats
s2
          }

instance ToJSON Stats where
  toJSON :: Stats -> Value
toJSON = forall a.
(Generic a, GToJSON' Value Zero (Rep a)) =>
Options -> a -> Value
genericToJSON Options
defaultOptions
  toEncoding :: Stats -> Encoding
toEncoding = forall a.
(Generic a, GToJSON' Encoding Zero (Rep a)) =>
Options -> a -> Encoding
genericToEncoding Options
defaultOptions

instance FromJSON Stats

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 = 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 forall a. Num a => a -> a -> a
+ Int
numIter forall a. Num a => a -> a -> a
+ Int
numBrkt forall a. Num a => a -> a -> a
+ Int
numChck forall a. Num a => a -> a -> a
+ Int
numVald