Safe Haskell	Safe-Inferred
Language	Haskell2010

SoPSat.SoP

Contents

SoP Types
Operators
Relations
Related
Predicates

Synopsis

data Atom f c
data Symbol f c
data Product f c
data SoP f c
data SoPE f c = SoPE {
- lhs :: SoP f c
- rhs :: SoP f c
- op :: OrdRel
}
class (Ord f, Ord c) => ToSoP f c a where
- toSoP :: a -> SoP f c
(|+|) :: (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
(|-|) :: (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
(|*|) :: (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
(|/|) :: (Ord f, Ord c) => SoP f c -> SoP f c -> (SoP f c, SoP f c)
(|^|) :: (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c
data OrdRel
- = LeR
- | EqR
- | GeR
constants :: (Ord f, Ord c) => SoP f c -> Set c
atoms :: (Ord f, Ord c) => SoP f c -> Set (Atom f c)
int :: Integer -> SoP f c
cons :: c -> SoP f c
symbol :: Atom f c -> SoP f c
func :: (Ord f, Ord c) => f -> [SoP f c] -> SoP f c
isConst :: Atom f c -> Bool
isFunction :: Atom f c -> Bool

SoP Types

data Atom f c Source #

Atomic part of a SoP like constants and unknown functions

Instances

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 #

data Symbol f c Source #

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

Instances

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 #

data Product f c Source #

Product of symbols

Instances

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 #

data SoP f c Source #

Sum of Products

Instances

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 #

data SoPE f c Source #

Expression

Constructors

SoPE
Fields lhs :: SoP f c Left hand side of the expression rhs :: SoP f c Right hand side of the expression op :: OrdRel Relationship between sides

Instances

Instances details

(Show f, Show c) => Show (SoPE f c) Source #
Instance details Defined in SoPSat.SoP Methods showsPrec :: Int -> SoPE f c -> ShowS # show :: SoPE f c -> String # showList :: [SoPE f c] -> ShowS #
(Eq f, Eq c) => Eq (SoPE f c) Source #
Instance details Defined in SoPSat.SoP Methods (==) :: SoPE f c -> SoPE f c -> Bool # (/=) :: SoPE f c -> SoPE f c -> Bool #

class (Ord f, Ord c) => ToSoP f c a where Source #

Convertable to a sum of products with f being type to represent functions and c being type to represent constants

Methods

toSoP :: a -> SoP f c Source #

Instances

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 #
(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 #
(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 #

Operators

(|+|) :: (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c infixl 6 Source #

Addition of SoPs

(|-|) :: (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c infixl 6 Source #

Subtraction of SoPs

(|*|) :: (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c infixl 7 Source #

Multiplication of SoPs

(|/|) :: (Ord f, Ord c) => SoP f c -> SoP f c -> (SoP f c, SoP f c) infixl 7 Source #

Division of SoPs

Produces a tuple of a quotient and a remainder NB. Not implemented

(|^|) :: (Ord f, Ord c) => SoP f c -> SoP f c -> SoP f c infixr 8 Source #

Exponentiation of SoPs

Relations

data OrdRel Source #

Order relationship

Constructors

LeR	Less than or equal relationship
EqR	Equality relationship
GeR	Greater than or equal relationship

Instances

Instances details

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

Predicates

isConst :: Atom f c -> Bool Source #

Predicate for constant Atoms

isFunction :: Atom f c -> Bool Source #

Predicate for function Atoms

SoP Types

Instances

Instances

Instances

Instances

Instances

Instances

Operators

Relations

Instances

Related

Predicates