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

Safe HaskellNone




This module implements the top-level API for interfacing with Fixpoint In particular it exports the functions that solve constraints supplied either as .fq files or as FInfo.


Invoke Solver on an FInfo

solve :: (NFData a, Fixpoint a, Show a, Loc a) => Solver a Source #

Solve FInfo system of horn-clause constraints -----------------------------

type Solver a = Config -> FInfo a -> IO (Result (Integer, a)) Source #

Top level Solvers ----------------------------------------------------

Invoke Solver on a .fq file

solveFQ :: Config -> IO ExitCode Source #

Solve an .fq file ----------------------------------------------------

Function to determine outcome

resultExit :: FixResult a -> ExitCode Source #

Extract ExitCode from Solver Result ---------------------------------------

Parse Qualifiers from File

parseFInfo :: [FilePath] -> IO (FInfo a) Source #

Parse External Qualifiers -------------------------------------------------