Copyright	(c) Masahiro Sakai 2012-2015
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Stability	provisional
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010
Extensions	ConstrainedClassMethods MultiParamTypeClasses

ToySolver.Data.Boolean

Contents

Boolean algebra

Description

Type classes for lattices and boolean algebras.

Synopsis

class MonotoneBoolean a where
- true, false :: a
- (.&&.) :: a -> a -> a
- (.||.) :: a -> a -> a
- andB :: [a] -> a
- orB :: [a] -> a
class Complement a where
- notB :: a -> a
class IfThenElse b a where
- ite :: b -> a -> a -> a
iteBoolean :: Boolean a => a -> a -> a -> a
class (MonotoneBoolean a, Complement a, IfThenElse a a) => Boolean a where
- (.=>.), (.<=>.) :: a -> a -> a

Boolean algebra

class MonotoneBoolean a where Source #

Minimal complete definition

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

Methods

true :: a Source #

false :: a Source #

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

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

andB :: [a] -> a Source #

orB :: [a] -> a Source #

Instances

Instances details

MonotoneBoolean Formula Source #
Instance details Defined in ToySolver.SAT.Formula Methods true :: Formula Source # false :: Formula Source # (.&&.) :: Formula -> Formula -> Formula Source # (.\|\|.) :: Formula -> Formula -> Formula Source # andB :: [Formula] -> Formula Source # orB :: [Formula] -> Formula Source #
MonotoneBoolean Expr Source #
Instance details Defined in ToySolver.SMT Methods true :: Expr Source # false :: Expr Source # (.&&.) :: Expr -> Expr -> Expr Source # (.\|\|.) :: Expr -> Expr -> Expr Source # andB :: [Expr] -> Expr Source # orB :: [Expr] -> Expr Source #
MonotoneBoolean Bool Source #
Instance details Defined in ToySolver.Data.Boolean Methods true :: Bool Source # false :: Bool Source # (.&&.) :: Bool -> Bool -> Bool Source # (.\|\|.) :: Bool -> Bool -> Bool Source # andB :: [Bool] -> Bool Source # orB :: [Bool] -> Bool Source #
MonotoneBoolean (BoolExpr a) Source #
Instance details Defined in ToySolver.Data.BoolExpr Methods true :: BoolExpr a Source # false :: BoolExpr a Source # (.&&.) :: BoolExpr a -> BoolExpr a -> BoolExpr a Source # (.\|\|.) :: BoolExpr a -> BoolExpr a -> BoolExpr a Source # andB :: [BoolExpr a] -> BoolExpr a Source # orB :: [BoolExpr a] -> BoolExpr a Source #
MonotoneBoolean (DNF lit) Source #
Instance details Defined in ToySolver.Data.DNF Methods true :: DNF lit Source # false :: DNF lit Source # (.&&.) :: DNF lit -> DNF lit -> DNF lit Source # (.\|\|.) :: DNF lit -> DNF lit -> DNF lit Source # andB :: [DNF lit] -> DNF lit Source # orB :: [DNF lit] -> DNF lit Source #
MonotoneBoolean (Formula c) Source #
Instance details Defined in ToySolver.Data.FOL.Formula Methods true :: Formula c Source # false :: Formula c Source # (.&&.) :: Formula c -> Formula c -> Formula c Source # (.\|\|.) :: Formula c -> Formula c -> Formula c Source # andB :: [Formula c] -> Formula c Source # orB :: [Formula c] -> Formula c Source #
MonotoneBoolean (GenFormula a) Source #
Instance details Defined in ToySolver.EUF.FiniteModelFinder Methods true :: GenFormula a Source # false :: GenFormula a Source # (.&&.) :: GenFormula a -> GenFormula a -> GenFormula a Source # (.\|\|.) :: GenFormula a -> GenFormula a -> GenFormula a Source # andB :: [GenFormula a] -> GenFormula a Source # orB :: [GenFormula a] -> GenFormula a Source #
(MonotoneBoolean a, MonotoneBoolean b) => MonotoneBoolean (a, b) Source #
Instance details Defined in ToySolver.Data.Boolean Methods true :: (a, b) Source # false :: (a, b) Source # (.&&.) :: (a, b) -> (a, b) -> (a, b) Source # (.\|\|.) :: (a, b) -> (a, b) -> (a, b) Source # andB :: [(a, b)] -> (a, b) Source # orB :: [(a, b)] -> (a, b) Source #
MonotoneBoolean a => MonotoneBoolean (b -> a) Source #
Instance details Defined in ToySolver.Data.Boolean Methods true :: b -> a Source # false :: b -> a Source # (.&&.) :: (b -> a) -> (b -> a) -> b -> a Source # (.\|\|.) :: (b -> a) -> (b -> a) -> b -> a Source # andB :: [b -> a] -> b -> a Source # orB :: [b -> a] -> b -> a Source #

class Complement a where Source #

types that can be negated.

Methods

notB :: a -> a Source #

Instances

Instances details

Complement Lit Source #
Instance details Defined in ToySolver.Arith.Cooper.Base Methods notB :: Lit -> Lit Source #
Complement Atom Source #
Instance details Defined in ToySolver.BitVector.Base Methods notB :: Atom -> Atom Source #
Complement Formula Source #
Instance details Defined in ToySolver.SAT.Formula Methods notB :: Formula -> Formula Source #
Complement Expr Source #
Instance details Defined in ToySolver.SMT Methods notB :: Expr -> Expr Source #
Complement Bool Source #
Instance details Defined in ToySolver.Data.Boolean Methods notB :: Bool -> Bool Source #
Complement (BoolExpr a) Source #
Instance details Defined in ToySolver.Data.BoolExpr Methods notB :: BoolExpr a -> BoolExpr a Source #
Complement lit => Complement (DNF lit) Source #
Instance details Defined in ToySolver.Data.DNF Methods notB :: DNF lit -> DNF lit Source #
Complement (Formula a) Source #
Instance details Defined in ToySolver.Data.FOL.Formula Methods notB :: Formula a -> Formula a Source #
Complement (OrdRel c) Source #
Instance details Defined in ToySolver.Data.OrdRel Methods notB :: OrdRel c -> OrdRel c Source #
Complement (GenFormula a) Source #
Instance details Defined in ToySolver.EUF.FiniteModelFinder Methods notB :: GenFormula a -> GenFormula a Source #
Complement (GenLit a) Source #
Instance details Defined in ToySolver.EUF.FiniteModelFinder Methods notB :: GenLit a -> GenLit a Source #
(Complement a, Complement b) => Complement (a, b) Source #
Instance details Defined in ToySolver.Data.Boolean Methods notB :: (a, b) -> (a, b) Source #
Complement a => Complement (b -> a) Source #
Instance details Defined in ToySolver.Data.Boolean Methods notB :: (b -> a) -> b -> a Source #

class IfThenElse b a where Source #

Methods

ite :: b -> a -> a -> a Source #

Instances

Instances details

IfThenElse Formula Formula Source #
Instance details Defined in ToySolver.SAT.Formula Methods ite :: Formula -> Formula -> Formula -> Formula Source #
IfThenElse Expr Expr Source #
Instance details Defined in ToySolver.SMT Methods ite :: Expr -> Expr -> Expr -> Expr Source #
IfThenElse Bool Bool Source #
Instance details Defined in ToySolver.Data.Boolean Methods ite :: Bool -> Bool -> Bool -> Bool Source #
IfThenElse (BoolExpr a) (BoolExpr a) Source #
Instance details Defined in ToySolver.Data.BoolExpr Methods ite :: BoolExpr a -> BoolExpr a -> BoolExpr a -> BoolExpr a Source #
Complement lit => IfThenElse (DNF lit) (DNF lit) Source #
Instance details Defined in ToySolver.Data.DNF Methods ite :: DNF lit -> DNF lit -> DNF lit -> DNF lit Source #
IfThenElse (Formula c) (Formula c) Source #
Instance details Defined in ToySolver.Data.FOL.Formula Methods ite :: Formula c -> Formula c -> Formula c -> Formula c Source #
IfThenElse (GenFormula a) (GenFormula a) Source #
Instance details Defined in ToySolver.EUF.FiniteModelFinder Methods ite :: GenFormula a -> GenFormula a -> GenFormula a -> GenFormula a Source #
(Boolean a, Boolean b) => IfThenElse (a, b) (a, b) Source #
Instance details Defined in ToySolver.Data.Boolean Methods ite :: (a, b) -> (a, b) -> (a, b) -> (a, b) Source #
Boolean a => IfThenElse (b -> a) (b -> a) Source #
Instance details Defined in ToySolver.Data.Boolean Methods ite :: (b -> a) -> (b -> a) -> (b -> a) -> b -> a Source #

iteBoolean :: Boolean a => a -> a -> a -> a Source #

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

types that can be combined with boolean operations.

Minimal complete definition

Nothing

Methods

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

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

Instances

Instances details

Boolean Formula Source #
Instance details Defined in ToySolver.SAT.Formula Methods (.=>.) :: Formula -> Formula -> Formula Source # (.<=>.) :: Formula -> Formula -> Formula Source #
Boolean Expr Source #
Instance details Defined in ToySolver.SMT Methods (.=>.) :: Expr -> Expr -> Expr Source # (.<=>.) :: Expr -> Expr -> Expr Source #
Boolean Bool Source #
Instance details Defined in ToySolver.Data.Boolean Methods (.=>.) :: Bool -> Bool -> Bool Source # (.<=>.) :: Bool -> Bool -> Bool Source #
Boolean (BoolExpr a) Source #
Instance details Defined in ToySolver.Data.BoolExpr Methods (.=>.) :: BoolExpr a -> BoolExpr a -> BoolExpr a Source # (.<=>.) :: BoolExpr a -> BoolExpr a -> BoolExpr a Source #
Complement lit => Boolean (DNF lit) Source #
Instance details Defined in ToySolver.Data.DNF Methods (.=>.) :: DNF lit -> DNF lit -> DNF lit Source # (.<=>.) :: DNF lit -> DNF lit -> DNF lit Source #
Boolean (Formula c) Source #
Instance details Defined in ToySolver.Data.FOL.Formula Methods (.=>.) :: Formula c -> Formula c -> Formula c Source # (.<=>.) :: Formula c -> Formula c -> Formula c Source #
Boolean (GenFormula a) Source #
Instance details Defined in ToySolver.EUF.FiniteModelFinder Methods (.=>.) :: GenFormula a -> GenFormula a -> GenFormula a Source # (.<=>.) :: GenFormula a -> GenFormula a -> GenFormula a Source #
(Boolean a, Boolean b) => Boolean (a, b) Source #
Instance details Defined in ToySolver.Data.Boolean Methods (.=>.) :: (a, b) -> (a, b) -> (a, b) Source # (.<=>.) :: (a, b) -> (a, b) -> (a, b) Source #
Boolean a => Boolean (b -> a) Source #
Instance details Defined in ToySolver.Data.Boolean Methods (.=>.) :: (b -> a) -> (b -> a) -> b -> a Source # (.<=>.) :: (b -> a) -> (b -> a) -> b -> a Source #