Jukebox.Tools.HornToUnit

Encodes Horn problems as unit equalities.

Documentation

data HornFlags

Constructors

HornFlags

Fields

• allowConjunctiveConjectures :: Bool
• allowDisjunctiveConjectures :: Bool
• allowNonGroundConjectures :: Bool
• allowCompoundConjectures :: Bool
• dropNonHorn :: Bool
• nonHornToOr :: Bool
• passivise :: Bool
• multi :: Bool
• smaller :: Bool
• encoding :: Encoding

Instances

Show HornFlags

Methods

showsPrec :: Int -> HornFlags -> ShowS

show :: HornFlags -> String

showList :: [HornFlags] -> ShowS

data Encoding

Constructors

Symmetric

Asymmetric1

Asymmetric2

Asymmetric3

Instances

Eq Encoding

Methods

(==) :: Encoding -> Encoding -> Bool

(/=) :: Encoding -> Encoding -> Bool

Show Encoding

Methods

showsPrec :: Int -> Encoding -> ShowS

show :: Encoding -> String

showList :: [Encoding] -> ShowS

hornFlags :: OptionParser HornFlags

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

encodeNonHorn :: HornFlags -> Name -> Type -> (Term -> Term -> Term) -> Term -> Term -> (Term -> Term -> Term) -> Problem Clause -> Problem Clause

eliminatePredicates :: Type -> Term -> Problem Clause -> Problem Clause

eliminateMultiplePreconditions :: HornFlags -> Problem Clause -> Problem Clause

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

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

encodeTypesSmartly :: Problem Clause -> IO (Either Answer (Problem Clause -> Problem Clause))

hasSizeOneModel :: Problem Clause -> IO Bool