Jukebox.Tools.HornToUnit

Encodes Horn problems as unit equalities.

Documentation

data HornFlags

Constructors

HornFlags

Fields

• allowNonUnitConjectures :: Bool
• allowNonGroundConjectures :: Bool
• asymmetricEncoding :: Bool

Instances

Show HornFlags

Methods

showsPrec :: Int -> HornFlags -> ShowS

show :: HornFlags -> String

showList :: [HornFlags] -> ShowS

hornFlags :: OptionParser HornFlags

hornToUnit :: HornFlags -> Problem Clause -> Either (Input Clause) (Problem Clause)

eliminatePredicates :: Problem Clause -> Problem Clause

eliminateUnsuitableConjectures :: HornFlags -> Problem Clause -> Problem Clause

eliminateHornClauses :: Problem Clause -> Either (Input Clause) (Problem Clause)