jukebox-0.3: A first-order reasoning toolbox
Jukebox.Tools.HornToUnit
Description
Encodes Horn problems as unit equalities.
data HornFlags Source #
Constructors
Fields
Instances
Methods
showsPrec :: Int -> HornFlags -> ShowS #
show :: HornFlags -> String #
showList :: [HornFlags] -> ShowS #
hornFlags :: OptionParser HornFlags Source #
hornToUnit :: HornFlags -> Problem Clause -> Either (Input Clause) (Problem Clause) Source #
eliminatePredicates :: Problem Clause -> Problem Clause Source #
eliminateUnsuitableConjectures :: HornFlags -> Problem Clause -> Problem Clause Source #
eliminateHornClauses :: Problem Clause -> Either (Input Clause) (Problem Clause) Source #