liquid-fixpoint-0.8.10.2: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver
Language.Fixpoint.Horn.Solve
Description
This module defines a function to solve NNF constraints, by reducing them to the standard FInfo.
solveHorn :: Config -> IO ExitCode Source #
solve :: (PPrint a, NFData a, Loc a, Show a, Fixpoint a) => Config -> Query a -> IO (Result (Integer, a)) Source #