ToySolver.Data.FOL.Formula

Formula of first order logic.

Overloaded operations for formula.

module ToySolver.Data.Boolean

Concrete formula

data Formula a

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)

Defined in ToySolver.Data.FOL.Formula

Methods

(==) :: Formula a -> Formula a -> Bool

(/=) :: Formula a -> Formula a -> Bool

Ord a => Ord (Formula a)

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

Show a => Show (Formula a)

Defined in ToySolver.Data.FOL.Formula

Methods

showsPrec :: Int -> Formula a -> ShowS

show :: Formula a -> String

showList :: [Formula a] -> ShowS

Boolean (Formula c)

Defined in ToySolver.Data.FOL.Formula

Methods

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

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

Complement (Formula a)

Defined in ToySolver.Data.FOL.Formula

Methods

notB :: Formula a -> Formula a

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

Variables a => Variables (Formula a)

Defined in ToySolver.Data.FOL.Formula

Methods

vars :: Formula a -> VarSet

IfThenElse (Formula c) (Formula c)

Defined in ToySolver.Data.FOL.Formula

Methods

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

IsOrdRel (Expr c) (Formula (Atom c))

Defined in ToySolver.Data.FOL.Arith

Methods

(.<.) :: Expr c -> Expr c -> Formula (Atom c)

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

(.>.) :: Expr c -> Expr c -> Formula (Atom c)

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

ordRel :: RelOp -> Expr c -> Expr c -> Formula (Atom c)

IsEqRel (Expr c) (Formula (Atom c))

Defined in ToySolver.Data.FOL.Arith

Methods

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

(./=.) :: Expr c -> Expr c -> Formula (Atom c)

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

convert a formula into negation normal form