liquid-fixpoint-0.7.0.7: 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 ------------------------------------------------------------------

data Stats Source #

Instances

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