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

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Solver

Contents

Description

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.

Synopsis

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

Parse Qualifiers from File

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

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

Simplified Info

simplifyFInfo :: (NFData a, Fixpoint a, Show a, Loc a) => Config -> FInfo a -> IO (SInfo a) Source #