ToySolver.Data.ArithRel

Arithmetic relations

Relational operators

data RelOp

relational operators

Constructors

Lt

Le

Ge

Gt

Eql

NEq

Instances

Eq RelOp

Ord RelOp

Show RelOp

flipOp :: RelOp -> RelOp

flipping relational operator

rel (flipOp op) a b is equivalent to rel op b a

negOp :: RelOp -> RelOp

negating relational operator

rel (negOp op) a b is equivalent to notB (rel op a b)

showOp :: RelOp -> String

operator symbol

evalOp :: Ord a => RelOp -> a -> a -> Bool

evaluate an operator into a comparision function

Relation

data Rel e

Atomic formula

Constructors

Rel e RelOp e

Instances

Functor Rel

IsRel e (Rel e)

Eq e => Eq (Rel e)

Ord e => Ord (Rel e)

Show e => Show (Rel e)

Complement (Rel c)

Variables e => Variables (Rel e)

IsRel (Expr c) (Formula (Atom c))

DSL

class IsRel e r | r -> e where

type class for constructing relational formula

Methods

rel :: RelOp -> e -> e -> r

Instances

IsRel e (Rel e)

IsRel (Expr Integer) QFFormula

IsRel (Expr c) (Formula (Atom c))

(.<.) :: IsRel e r => e -> e -> r infix 4

constructing relational formula

(.<=.) :: IsRel e r => e -> e -> r infix 4

constructing relational formula

(.>=.) :: IsRel e r => e -> e -> r infix 4

constructing relational formula

(.>.) :: IsRel e r => e -> e -> r infix 4

constructing relational formula

(.==.) :: IsRel e r => e -> e -> r infix 4

constructing relational formula

(./=.) :: IsRel e r => e -> e -> r infix 4

constructing relational formula