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

Safe Haskell	Safe-Inferred
Language	Haskell98

Language.Fixpoint.Solver.Solution

Contents

Create Initial Solution
Update Solution
Lookup Solution

Synopsis

init :: Fixpoint a => Config -> SInfo a -> HashSet KVar -> Solution
update :: Sol a QBind -> [KVar] -> [(KVar, EQual)] -> (Bool, Sol a QBind)
lhsPred :: Loc a => IBindEnv -> BindEnv a -> Solution -> SimpC a -> Expr
nonCutsResult :: BindEnv ann -> Sol a QBind -> HashMap KVar Expr

Create Initial Solution

init :: Fixpoint a => Config -> SInfo a -> HashSet KVar -> Solution Source #

Initial Solution (from Qualifiers and WF constraints) ---------------------

Update Solution

update :: Sol a QBind -> [KVar] -> [(KVar, EQual)] -> (Bool, Sol a QBind) Source #

Update Solution -----------------------------------------------------------

Lookup Solution

lhsPred :: Loc a => IBindEnv -> BindEnv a -> Solution -> SimpC a -> Expr Source #

Predicate corresponding to LHS of constraint in current solution

nonCutsResult :: BindEnv ann -> Sol a QBind -> HashMap KVar Expr Source #