Language.Fixpoint.Horn.Solve

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

Documentation

solveHorn :: Config -> IO ExitCode

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