Safe Haskell	Safe-Inferred
Language	Haskell2010

SoPSat.Internal.SoP

Synopsis

data Atom f c
- = C c
- | F f [SoP f c]
data Symbol f c
- = I Integer
- | A (Atom f c)
- | E (SoP f c) (Product f c)
newtype Product f c = P {
- unP :: [Symbol f c]
}
newtype SoP f c = S {
- unS :: [Product f c]
}
mergeWith :: (a -> a -> Either a a) -> [a] -> [a]
reduceExp :: (Ord f, Ord c) => Symbol f c -> Symbol f c
mergeS :: (Ord f, Ord c) => Symbol f c -> Symbol f c -> Either (Symbol f c) (Symbol f c)
mergeP :: (Eq f, Eq c) => Product f c -> Product f c -> Either (Product f c) (Product f c)
normaliseExp :: (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
zeroP :: Product f c -> Bool
mkNonEmpty :: (Ord f, Ord c) => SoP f c -> SoP f c
simplifySoP :: (Ord f, Ord c) => SoP f c -> SoP f c
mergeSoPAdd :: (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
mergeSoPMul :: (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
mergeSoPSub :: (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
mergeSoPDiv :: (Ord f, Ord c) => SoP f c -> SoP f c -> (SoP f c, SoP f c)

Documentation

Atomic part of a SoP like constants and unknown functions

Constructors

C c	Constant
F f [SoP f c]	Unknown function

Instances details

(Show f, Show c) => Show (Atom f c) Source #
Instance details Defined in SoPSat.Internal.SoP Methods showsPrec :: Int -> Atom f c -> ShowS # show :: Atom f c -> String # showList :: [Atom f c] -> ShowS #
(Eq c, Eq f) => Eq (Atom f c) Source #
Instance details Defined in SoPSat.Internal.SoP Methods (==) :: Atom f c -> Atom f c -> Bool # (/=) :: Atom f c -> Atom f c -> Bool #
(Ord c, Ord f) => Ord (Atom f c) Source #
Instance details Defined in SoPSat.Internal.SoP Methods compare :: Atom f c -> Atom f c -> Ordering # (<) :: Atom f c -> Atom f c -> Bool # (<=) :: Atom f c -> Atom f c -> Bool # (>) :: Atom f c -> Atom f c -> Bool # (>=) :: Atom f c -> Atom f c -> Bool # max :: Atom f c -> Atom f c -> Atom f c # min :: Atom f c -> Atom f c -> Atom f c #

The most basic part used during reasoning: - Numbers - Atoms - Exponents

Constructors

Instances details

(Ord f, Ord c) => ToSoP f c (Symbol f c) Source #
Instance details Defined in SoPSat.SoP Methods toSoP :: Symbol f c -> SoP f c Source #
(Show f, Show c) => Show (Symbol f c) Source #
Instance details Defined in SoPSat.Internal.SoP Methods showsPrec :: Int -> Symbol f c -> ShowS # show :: Symbol f c -> String # showList :: [Symbol f c] -> ShowS #
(Eq c, Eq f) => Eq (Symbol f c) Source #
Instance details Defined in SoPSat.Internal.SoP Methods (==) :: Symbol f c -> Symbol f c -> Bool # (/=) :: Symbol f c -> Symbol f c -> Bool #
(Ord c, Ord f) => Ord (Symbol f c) Source #
Instance details Defined in SoPSat.Internal.SoP Methods compare :: Symbol f c -> Symbol f c -> Ordering # (<) :: Symbol f c -> Symbol f c -> Bool # (<=) :: Symbol f c -> Symbol f c -> Bool # (>) :: Symbol f c -> Symbol f c -> Bool # (>=) :: Symbol f c -> Symbol f c -> Bool # max :: Symbol f c -> Symbol f c -> Symbol f c # min :: Symbol f c -> Symbol f c -> Symbol f c #

Product of symbols

Constructors

P
Fields unP :: [Symbol f c]

Instances details

(Ord f, Ord c) => ToSoP f c (Product f c) Source #
Instance details Defined in SoPSat.SoP Methods toSoP :: Product f c -> SoP f c Source #
(Show f, Show c) => Show (Product f c) Source #
Instance details Defined in SoPSat.Internal.SoP Methods showsPrec :: Int -> Product f c -> ShowS # show :: Product f c -> String # showList :: [Product f c] -> ShowS #
(Eq f, Eq c) => Eq (Product f c) Source #
Instance details Defined in SoPSat.Internal.SoP Methods (==) :: Product f c -> Product f c -> Bool # (/=) :: Product f c -> Product f c -> Bool #
(Ord f, Ord c) => Ord (Product f c) Source #
Instance details Defined in SoPSat.Internal.SoP Methods compare :: Product f c -> Product f c -> Ordering # (<) :: Product f c -> Product f c -> Bool # (<=) :: Product f c -> Product f c -> Bool # (>) :: Product f c -> Product f c -> Bool # (>=) :: Product f c -> Product f c -> Bool # max :: Product f c -> Product f c -> Product f c # min :: Product f c -> Product f c -> Product f c #

newtype SoP f c Source #

Sum of Products

Constructors

S
Fields unS :: [Product f c]

Instances details

(Ord f, Ord c) => ToSoP f c (SoP f c) Source #
Instance details Defined in SoPSat.SoP Methods toSoP :: SoP f c -> SoP f c Source #
(Show f, Show c) => Show (SoP f c) Source #
Instance details Defined in SoPSat.Internal.SoP Methods showsPrec :: Int -> SoP f c -> ShowS # show :: SoP f c -> String # showList :: [SoP f c] -> ShowS #
(Eq f, Eq c) => Eq (SoP f c) Source #
Instance details Defined in SoPSat.Internal.SoP Methods (==) :: SoP f c -> SoP f c -> Bool # (/=) :: SoP f c -> SoP f c -> Bool #
(Ord f, Ord c) => Ord (SoP f c) Source #
Instance details Defined in SoPSat.Internal.SoP Methods compare :: SoP f c -> SoP f c -> Ordering # (<) :: SoP f c -> SoP f c -> Bool # (<=) :: SoP f c -> SoP f c -> Bool # (>) :: SoP f c -> SoP f c -> Bool # (>=) :: SoP f c -> SoP f c -> Bool # max :: SoP f c -> SoP f c -> SoP f c # min :: SoP f c -> SoP f c -> SoP f c #

mergeWith :: (a -> a -> Either a a) -> [a] -> [a] Source #

normaliseExp :: (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c Source #

mkNonEmpty :: (Ord f, Ord c) => SoP f c -> SoP f c Source #

mergeSoPAdd :: (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c Source #

mergeSoPMul :: (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c Source #

mergeSoPSub :: (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c Source #

mergeSoPDiv :: (Ord f, Ord c) => SoP f c -> SoP f c -> (SoP f c, SoP f c) Source #