Safe Haskell	Safe-Inferred
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

Instances details

FromJSON Stats Source #
Instance details Defined in Language.Fixpoint.Solver.Stats Methods parseJSON :: Value -> Parser Stats # parseJSONList :: Value -> Parser [Stats] # omittedField :: Maybe Stats #
ToJSON Stats Source #
Instance details Defined in Language.Fixpoint.Solver.Stats Methods toJSON :: Stats -> Value # toEncoding :: Stats -> Encoding # toJSONList :: [Stats] -> Value # toEncodingList :: [Stats] -> Encoding # omitField :: 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 :: 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 #
Monoid Stats Source #
Instance details Defined in Language.Fixpoint.Solver.Stats Methods mempty :: Stats # mappend :: Stats -> Stats -> Stats # mconcat :: [Stats] -> 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 #
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 #
Show Stats Source #
Instance details Defined in Language.Fixpoint.Solver.Stats Methods showsPrec :: Int -> Stats -> ShowS # show :: Stats -> String # showList :: [Stats] -> ShowS #
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 -> () #
Eq Stats Source #
Instance details Defined in Language.Fixpoint.Solver.Stats Methods (==) :: Stats -> Stats -> Bool # (/=) :: Stats -> Stats -> Bool #
PTable Stats Source #
Instance details Defined in Language.Fixpoint.Solver.Stats Methods ptable :: Stats -> DocTable Source #
Store Stats Source #
Instance details Defined in Language.Fixpoint.Solver.Stats Methods size :: Size Stats # poke :: Stats -> Poke () # peek :: Peek Stats #
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.9.6.3-Fxo1c9HahAZtZcvzlvNkk" '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".