jukebox-0.5.5: A first-order reasoning toolbox
Safe HaskellSafe-Inferred
LanguageHaskell2010

Jukebox.Tools.HornToUnit

Description

Encodes Horn problems as unit equalities.

Documentation

data HornFlags Source #

Constructors

HornFlags 

Fields

Instances

Instances details
Show HornFlags Source # 
Instance details

Defined in Jukebox.Tools.HornToUnit

Methods

showsPrec :: Int -> HornFlags -> ShowS #

show :: HornFlags -> String #

showList :: [HornFlags] -> ShowS #

data Encoding Source #

Constructors

Symmetric 
Asymmetric1 
Asymmetric2 
Asymmetric3 

Instances

Instances details
Show Encoding Source # 
Instance details

Defined in Jukebox.Tools.HornToUnit

Methods

showsPrec :: Int -> Encoding -> ShowS #

show :: Encoding -> String #

showList :: [Encoding] -> ShowS #

Eq Encoding Source # 
Instance details

Defined in Jukebox.Tools.HornToUnit

Methods

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

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

hornFlags :: OptionParser HornFlags Source #

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

eliminatePredicates :: Problem Clause -> Problem Clause Source #

eliminateMultiplePreconditions :: HornFlags -> Problem Clause -> Problem Clause Source #

eliminateUnsuitableConjectures :: HornFlags -> Problem Clause -> Problem Clause Source #

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

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

hasSizeOneModel :: Problem Clause -> IO Bool Source #