Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Solver.Stats

Synopsis

data Stats = Stats {
- numCstr :: !Int
- numIter :: !Int
- numBrkt :: !Int
- numChck :: !Int
- numVald :: !Int
}
checked :: Stats -> Int
totalWork :: Stats -> Int

Documentation

data Stats Source #

Constructors

Stats
Fields numCstr :: !Int # Horn Constraints numIter :: !Int # Refine Iterations numBrkt :: !Int # smtBracket calls (push/pop) numChck :: !Int # smtCheckUnsat calls numVald :: !Int # times SMT said RHS Valid

Instances

Eq Stats Source #
Instance details Defined in Language.Fixpoint.Solver.Stats Methods (==) :: Stats -> Stats -> Bool # (/=) :: Stats -> Stats -> Bool #
Data Stats Source #
Instance details Defined in Language.Fixpoint.Solver.Stats Methods 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 :: (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 #
Show Stats Source #
Instance details Defined in Language.Fixpoint.Solver.Stats Methods showsPrec :: Int -> Stats -> ShowS # show :: Stats -> String # showList :: [Stats] -> ShowS #
Generic Stats Source #
Instance details Defined in Language.Fixpoint.Solver.Stats Associated Types type Rep Stats :: Type -> Type # Methods from :: Stats -> Rep Stats x # to :: Rep Stats x -> Stats #
Semigroup Stats Source #
Instance details Defined in Language.Fixpoint.Solver.Stats Methods (<>) :: Stats -> Stats -> Stats # sconcat :: NonEmpty Stats -> Stats # stimes :: Integral b => b -> Stats -> Stats #
Monoid Stats Source #
Instance details Defined in Language.Fixpoint.Solver.Stats Methods mempty :: Stats # mappend :: Stats -> Stats -> Stats # mconcat :: [Stats] -> Stats #
Binary Stats Source #
Instance details Defined in Language.Fixpoint.Solver.Stats Methods put :: Stats -> Put # get :: Get Stats # putList :: [Stats] -> Put #
Serialize Stats Source #
Instance details Defined in Language.Fixpoint.Solver.Stats Methods put :: Putter Stats # get :: Get Stats #
NFData Stats Source #
Instance details Defined in Language.Fixpoint.Solver.Stats Methods rnf :: Stats -> () #
PTable Stats Source #
Instance details Defined in Language.Fixpoint.Solver.Stats Methods ptable :: Stats -> DocTable Source #
type Rep Stats Source #
Instance details Defined in Language.Fixpoint.Solver.Stats type Rep Stats = D1 (MetaData "Stats" "Language.Fixpoint.Solver.Stats" "liquid-fixpoint-0.8.0.2-EGSzGwrlcJrCaUaEYLNzOY" False) (C1 (MetaCons "Stats" PrefixI True) ((S1 (MetaSel (Just "numCstr") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Int) :: S1 (MetaSel (Just "numIter") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Int)) :: (S1 (MetaSel (Just "numBrkt") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Int) :: (S1 (MetaSel (Just "numChck") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Int) :: S1 (MetaSel (Just "numVald") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Int)))))

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".