ToySolver.Data.Boolean

Type classes for lattices and boolean algebras.

Boolean algebra

class MonotoneBoolean a where

Minimal complete definition

(true, (.&&.) | andB), (false, (.||.) | orB)

Methods

true :: a

false :: a

(.&&.) :: a -> a -> a infixr 3

(.||.) :: a -> a -> a infixr 2

andB :: [a] -> a

orB :: [a] -> a

Instances

MonotoneBoolean Bool

Defined in ToySolver.Data.Boolean

Methods

true :: Bool

false :: Bool

(.&&.) :: Bool -> Bool -> Bool

(.||.) :: Bool -> Bool -> Bool

andB :: [Bool] -> Bool

orB :: [Bool] -> Bool

MonotoneBoolean Expr

Defined in ToySolver.SMT

Methods

true :: Expr

false :: Expr

(.&&.) :: Expr -> Expr -> Expr

(.||.) :: Expr -> Expr -> Expr

andB :: [Expr] -> Expr

orB :: [Expr] -> Expr

MonotoneBoolean (DNF lit)

Defined in ToySolver.Data.DNF

Methods

true :: DNF lit

false :: DNF lit

(.&&.) :: DNF lit -> DNF lit -> DNF lit

(.||.) :: DNF lit -> DNF lit -> DNF lit

andB :: [DNF lit] -> DNF lit

orB :: [DNF lit] -> DNF lit

MonotoneBoolean (Formula c)

Defined in ToySolver.Data.FOL.Formula

Methods

true :: Formula c

false :: Formula c

(.&&.) :: Formula c -> Formula c -> Formula c

(.||.) :: Formula c -> Formula c -> Formula c

andB :: [Formula c] -> Formula c

orB :: [Formula c] -> Formula c

MonotoneBoolean (BoolExpr a)

Defined in ToySolver.Data.BoolExpr

Methods

true :: BoolExpr a

false :: BoolExpr a

(.&&.) :: BoolExpr a -> BoolExpr a -> BoolExpr a

(.||.) :: BoolExpr a -> BoolExpr a -> BoolExpr a

andB :: [BoolExpr a] -> BoolExpr a

orB :: [BoolExpr a] -> BoolExpr a

MonotoneBoolean (GenFormula a)

Defined in ToySolver.EUF.FiniteModelFinder

Methods

true :: GenFormula a

false :: GenFormula a

(.&&.) :: GenFormula a -> GenFormula a -> GenFormula a

(.||.) :: GenFormula a -> GenFormula a -> GenFormula a

andB :: [GenFormula a] -> GenFormula a

orB :: [GenFormula a] -> GenFormula a

MonotoneBoolean a => MonotoneBoolean (b -> a)

Defined in ToySolver.Data.Boolean

Methods

true :: b -> a

false :: b -> a

(.&&.) :: (b -> a) -> (b -> a) -> b -> a

(.||.) :: (b -> a) -> (b -> a) -> b -> a

andB :: [b -> a] -> b -> a

orB :: [b -> a] -> b -> a

(MonotoneBoolean a, MonotoneBoolean b) => MonotoneBoolean (a, b)

Defined in ToySolver.Data.Boolean

Methods

true :: (a, b)

false :: (a, b)

(.&&.) :: (a, b) -> (a, b) -> (a, b)

(.||.) :: (a, b) -> (a, b) -> (a, b)

andB :: [(a, b)] -> (a, b)

orB :: [(a, b)] -> (a, b)

class Complement a where

types that can be negated.

Methods

notB :: a -> a

Instances

Complement Bool

Defined in ToySolver.Data.Boolean

Methods

notB :: Bool -> Bool

Complement Atom

Defined in ToySolver.BitVector.Base

Methods

notB :: Atom -> Atom

Complement Lit

Defined in ToySolver.Arith.Cooper.Base

Methods

notB :: Lit -> Lit

Complement Expr

Defined in ToySolver.SMT

Methods

notB :: Expr -> Expr

Complement lit => Complement (DNF lit)

Defined in ToySolver.Data.DNF

Methods

notB :: DNF lit -> DNF lit

Complement (Formula a)

Defined in ToySolver.Data.FOL.Formula

Methods

notB :: Formula a -> Formula a

Complement (BoolExpr a)

Defined in ToySolver.Data.BoolExpr

Methods

notB :: BoolExpr a -> BoolExpr a

Complement (OrdRel c)

Defined in ToySolver.Data.OrdRel

Methods

notB :: OrdRel c -> OrdRel c

Complement (GenFormula a)

Defined in ToySolver.EUF.FiniteModelFinder

Methods

notB :: GenFormula a -> GenFormula a

Complement (GenLit a)

Defined in ToySolver.EUF.FiniteModelFinder

Methods

notB :: GenLit a -> GenLit a

Complement a => Complement (b -> a)

Defined in ToySolver.Data.Boolean

Methods

notB :: (b -> a) -> b -> a

(Complement a, Complement b) => Complement (a, b)

Defined in ToySolver.Data.Boolean

Methods

notB :: (a, b) -> (a, b)

class IfThenElse b a where

Methods

ite :: b -> a -> a -> a

Instances

IfThenElse Bool Bool

Defined in ToySolver.Data.Boolean

Methods

ite :: Bool -> Bool -> Bool -> Bool

IfThenElse Expr Expr

Defined in ToySolver.SMT

Methods

ite :: Expr -> Expr -> Expr -> Expr

Complement lit => IfThenElse (DNF lit) (DNF lit)

Defined in ToySolver.Data.DNF

Methods

ite :: DNF lit -> DNF lit -> DNF lit -> DNF lit

IfThenElse (Formula c) (Formula c)

Defined in ToySolver.Data.FOL.Formula

Methods

ite :: Formula c -> Formula c -> Formula c -> Formula c

IfThenElse (BoolExpr a) (BoolExpr a)

Defined in ToySolver.Data.BoolExpr

Methods

ite :: BoolExpr a -> BoolExpr a -> BoolExpr a -> BoolExpr a

IfThenElse (GenFormula a) (GenFormula a)

Defined in ToySolver.EUF.FiniteModelFinder

Methods

ite :: GenFormula a -> GenFormula a -> GenFormula a -> GenFormula a

Boolean a => IfThenElse (b -> a) (b -> a)

Defined in ToySolver.Data.Boolean

Methods

ite :: (b -> a) -> (b -> a) -> (b -> a) -> b -> a

(Boolean a, Boolean b) => IfThenElse (a, b) (a, b)

Defined in ToySolver.Data.Boolean

Methods

ite :: (a, b) -> (a, b) -> (a, b) -> (a, b)

iteBoolean :: Boolean a => a -> a -> a -> a

class (MonotoneBoolean a, Complement a, IfThenElse a a) => Boolean a where

types that can be combined with boolean operations.

Minimal complete definition

Nothing

Methods

(.=>.) :: a -> a -> a infixr 1

(.<=>.) :: a -> a -> a infix 1

Instances

Boolean Bool

Defined in ToySolver.Data.Boolean

Methods

(.=>.) :: Bool -> Bool -> Bool

(.<=>.) :: Bool -> Bool -> Bool

Boolean Expr

Defined in ToySolver.SMT

Methods

(.=>.) :: Expr -> Expr -> Expr

(.<=>.) :: Expr -> Expr -> Expr

Complement lit => Boolean (DNF lit)

Defined in ToySolver.Data.DNF

Methods

(.=>.) :: DNF lit -> DNF lit -> DNF lit

(.<=>.) :: DNF lit -> DNF lit -> DNF lit

Boolean (Formula c)

Defined in ToySolver.Data.FOL.Formula

Methods

(.=>.) :: Formula c -> Formula c -> Formula c

(.<=>.) :: Formula c -> Formula c -> Formula c

Boolean (BoolExpr a)

Defined in ToySolver.Data.BoolExpr

Methods

(.=>.) :: BoolExpr a -> BoolExpr a -> BoolExpr a

(.<=>.) :: BoolExpr a -> BoolExpr a -> BoolExpr a

Boolean (GenFormula a)

Defined in ToySolver.EUF.FiniteModelFinder

Methods

(.=>.) :: GenFormula a -> GenFormula a -> GenFormula a

(.<=>.) :: GenFormula a -> GenFormula a -> GenFormula a

Boolean a => Boolean (b -> a)

Defined in ToySolver.Data.Boolean

Methods

(.=>.) :: (b -> a) -> (b -> a) -> b -> a

(.<=>.) :: (b -> a) -> (b -> a) -> b -> a

(Boolean a, Boolean b) => Boolean (a, b)

Defined in ToySolver.Data.Boolean

Methods

(.=>.) :: (a, b) -> (a, b) -> (a, b)

(.<=>.) :: (a, b) -> (a, b) -> (a, b)