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

Safe HaskellNone

Language.Fixpoint.Interface

Contents

Synopsis

Containing Constraints

data FInfo a Source

Constructors

FI (HashMap Integer (SubC a)) ![WfC a] !BindEnv !FEnv ![(Symbol, Sort)] Kuts ![Qualifier] 

Invoke Solver on Set of Constraints

solve :: Config -> FilePath -> [FilePath] -> FInfo a -> IO (FixResult (SubC a), HashMap Symbol Pred)Source

Solve a system of horn-clause constraints ----------------------------

Function to determine outcome

Validity Query

checkValid :: Hashable a => a -> [(Symbol, Sort)] -> Pred -> IO (FixResult a)Source

One Shot validity query ----------------------------------------------