liquid-fixpoint-0.8.0.2: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Solver.Worklist

Contents

Synopsis

Worklist type is opaque

data Worklist a Source #

Worklist ------------------------------------------------------------------

Instances
PTable (Worklist a) Source # 
Instance details

Defined in Language.Fixpoint.Solver.Worklist

PPrint (Worklist a) Source # 
Instance details

Defined in Language.Fixpoint.Solver.Worklist

data Stats Source #

Instances
Eq Stats Source # 
Instance details

Defined in Language.Fixpoint.Solver.Worklist

Methods

(==) :: Stats -> Stats -> Bool #

(/=) :: Stats -> Stats -> Bool #

Show Stats Source # 
Instance details

Defined in Language.Fixpoint.Solver.Worklist

Methods

showsPrec :: Int -> Stats -> ShowS #

show :: Stats -> String #

showList :: [Stats] -> ShowS #

PTable Stats Source # 
Instance details

Defined in Language.Fixpoint.Solver.Worklist

Initialize

init :: SolverInfo a b -> Worklist a Source #

Initialize worklist and slice out irrelevant constraints ------------------

Pop off a constraint

Add a constraint and all its dependencies

Constraints with Concrete RHS

unsatCandidates :: Worklist a -> [SimpC a] Source #

Candidate Constraints to be checked AFTER computing Fixpoint ---------

Statistics