Copyright	(c) Masahiro Sakai 2011-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.FOL.Formula

Contents

Overloaded operations for formula.
Concrete formula

Description

Formula of first order logic.

Synopsis

module ToySolver.Data.Boolean
data Formula a
- = T
- | F
- | Atom a
- | And (Formula a) (Formula a)
- | Or (Formula a) (Formula a)
- | Not (Formula a)
- | Imply (Formula a) (Formula a)
- | Equiv (Formula a) (Formula a)
- | Forall Var (Formula a)
- | Exists Var (Formula a)
pushNot :: Complement a => Formula a -> Formula a

Overloaded operations for formula.

module ToySolver.Data.Boolean

Concrete formula

data Formula a Source #

formulas of first order logic

Constructors

T
F
Atom a
And (Formula a) (Formula a)
Or (Formula a) (Formula a)
Not (Formula a)
Imply (Formula a) (Formula a)
Equiv (Formula a) (Formula a)
Forall Var (Formula a)
Exists Var (Formula a)

Instances

Instances details

Show a => Show (Formula a) Source #
Instance details Defined in ToySolver.Data.FOL.Formula Methods showsPrec :: Int -> Formula a -> ShowS # show :: Formula a -> String # showList :: [Formula a] -> ShowS #
Eq a => Eq (Formula a) Source #
Instance details Defined in ToySolver.Data.FOL.Formula Methods (==) :: Formula a -> Formula a -> Bool # (/=) :: Formula a -> Formula a -> Bool #
Ord a => Ord (Formula a) Source #
Instance details Defined in ToySolver.Data.FOL.Formula Methods compare :: Formula a -> Formula a -> Ordering # (<) :: Formula a -> Formula a -> Bool # (<=) :: Formula a -> Formula a -> Bool # (>) :: Formula a -> Formula a -> Bool # (>=) :: Formula a -> Formula a -> Bool # max :: Formula a -> Formula a -> Formula a # min :: Formula a -> Formula a -> Formula a #
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 #
Complement (Formula a) Source #
Instance details Defined in ToySolver.Data.FOL.Formula Methods notB :: Formula a -> Formula a 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 #
Variables a => Variables (Formula a) Source #
Instance details Defined in ToySolver.Data.FOL.Formula Methods vars :: Formula a -> VarSet 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 #
IsEqRel (Expr c) (Formula (Atom c)) Source #
Instance details Defined in ToySolver.Data.FOL.Arith Methods (.==.) :: Expr c -> Expr c -> Formula (Atom c) Source # (./=.) :: Expr c -> Expr c -> Formula (Atom c) Source #
IsOrdRel (Expr c) (Formula (Atom c)) Source #
Instance details Defined in ToySolver.Data.FOL.Arith Methods (.<.) :: Expr c -> Expr c -> Formula (Atom c) Source # (.<=.) :: Expr c -> Expr c -> Formula (Atom c) Source # (.>.) :: Expr c -> Expr c -> Formula (Atom c) Source # (.>=.) :: Expr c -> Expr c -> Formula (Atom c) Source # ordRel :: RelOp -> Expr c -> Expr c -> Formula (Atom c) Source #

pushNot :: Complement a => Formula a -> Formula a Source #

convert a formula into negation normal form