Language.Fixpoint.Solver.Stats
data Stats Source #
Constructors
Fields
# Horn Constraints
# Refine Iterations
# smtBracket calls (push/pop)
# smtCheckUnsat calls
# times SMT said RHS Valid
Defined in Language.Fixpoint.Solver.Stats
Methods
parseJSON :: Value -> Parser Stats #
parseJSONList :: Value -> Parser [Stats] #
omittedField :: Maybe Stats #
toJSON :: Stats -> Value #
toEncoding :: Stats -> Encoding #
toJSONList :: [Stats] -> Value #
toEncodingList :: [Stats] -> Encoding #
omitField :: Stats -> Bool #
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Stats -> c Stats #
gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Stats #
toConstr :: Stats -> Constr #
dataTypeOf :: Stats -> DataType #
dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Stats) #
dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Stats) #
gmapT :: (forall b. Data b => b -> b) -> Stats -> Stats #
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Stats -> r #
gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Stats -> r #
gmapQ :: (forall d. Data d => d -> u) -> Stats -> [u] #
gmapQi :: Int -> (forall d. Data d => d -> u) -> Stats -> u #
gmapM :: Monad m => (forall d. Data d => d -> m d) -> Stats -> m Stats #
gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Stats -> m Stats #
gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Stats -> m Stats #
mempty :: Stats #
mappend :: Stats -> Stats -> Stats #
mconcat :: [Stats] -> Stats #
(<>) :: Stats -> Stats -> Stats #
sconcat :: NonEmpty Stats -> Stats #
stimes :: Integral b => b -> Stats -> Stats #
Associated Types
from :: Stats -> Rep Stats x #
to :: Rep Stats x -> Stats #
showsPrec :: Int -> Stats -> ShowS #
show :: Stats -> String #
showList :: [Stats] -> ShowS #
put :: Putter Stats #
get :: Get Stats #
rnf :: Stats -> () #
(==) :: Stats -> Stats -> Bool #
(/=) :: Stats -> Stats -> Bool #
ptable :: Stats -> DocTable Source #
size :: Size Stats #
poke :: Stats -> Poke () #
peek :: Peek Stats #
checked :: Stats -> Int Source #
Returns the Horn clauses checked.
totalWork :: Stats -> Int Source #
Returns a number which can be used in the Safe constructor of a FixResult to show "the work done".
Safe
FixResult