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

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Horn.Solve

Description

This module defines a function to solve NNF constraints, by reducing them to the standard FInfo.

Documentation

solveHorn :: Config -> IO ExitCode Source #

solve :: (PPrint a, NFData a, Loc a, Show a, Fixpoint a) => Config -> Query a -> IO (Result (Integer, a)) Source #