Copyright	(c) Masahiro Sakai 2011-2015
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Stability	provisional
Portability	portable
Safe Haskell	Safe
Language	Haskell2010

ToySolver.Data.FOL.Formula

Contents

Overloaded operations for formula.
Concrete formula

Description

Formula of first order logic.

Synopsis

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

Eq a => Eq (Formula a) Source #
Methods (==) :: Formula a -> Formula a -> Bool # (/=) :: Formula a -> Formula a -> Bool #
Ord a => Ord (Formula a) Source #
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 #
Show a => Show (Formula a) Source #
Methods showsPrec :: Int -> Formula a -> ShowS # show :: Formula a -> String # showList :: [Formula a] -> ShowS #
Variables a => Variables (Formula a) Source #
Methods vars :: Formula a -> VarSet Source #
Boolean (Formula c) Source #
Methods (.=>.) :: Formula c -> Formula c -> Formula c Source # (.<=>.) :: Formula c -> Formula c -> Formula c Source #
Complement (Formula a) Source #
Methods notB :: Formula a -> Formula a Source #
MonotoneBoolean (Formula c) Source #
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 #
IfThenElse (Formula c) (Formula c) Source #
Methods ite :: Formula c -> Formula c -> Formula c -> Formula c Source #
IsOrdRel (Expr c) (Formula (Atom c)) Source #
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 #
IsEqRel (Expr c) (Formula (Atom c)) Source #
Methods (.==.) :: Expr c -> Expr c -> Formula (Atom c) Source # (./=.) :: Expr c -> Expr c -> Formula (Atom c) Source #

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

convert a formula into negation normal form