ToySolver.Data.OrdRel

Ordering relations

Relational operators

data RelOp

relational operators

Constructors

Lt

Le

Ge

Gt

Eql

NEq

Instances

Eq RelOp

Defined in ToySolver.Data.OrdRel

Methods

(==) :: RelOp -> RelOp -> Bool

(/=) :: RelOp -> RelOp -> Bool

Ord RelOp

Defined in ToySolver.Data.OrdRel

Methods

compare :: RelOp -> RelOp -> Ordering

(<) :: RelOp -> RelOp -> Bool

(<=) :: RelOp -> RelOp -> Bool

(>) :: RelOp -> RelOp -> Bool

(>=) :: RelOp -> RelOp -> Bool

max :: RelOp -> RelOp -> RelOp

min :: RelOp -> RelOp -> RelOp

Show RelOp

Defined in ToySolver.Data.OrdRel

Methods

showsPrec :: Int -> RelOp -> ShowS

show :: RelOp -> String

showList :: [RelOp] -> ShowS

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 OrdRel e

Atomic formula

Constructors

OrdRel e RelOp e

Instances

Functor OrdRel

Defined in ToySolver.Data.OrdRel

Methods

fmap :: (a -> b) -> OrdRel a -> OrdRel b

(<$) :: a -> OrdRel b -> OrdRel a

IsOrdRel e (OrdRel e)

Defined in ToySolver.Data.OrdRel

Methods

(.<.) :: e -> e -> OrdRel e

(.<=.) :: e -> e -> OrdRel e

(.>.) :: e -> e -> OrdRel e

(.>=.) :: e -> e -> OrdRel e

ordRel :: RelOp -> e -> e -> OrdRel e

IsEqRel e (OrdRel e)

Defined in ToySolver.Data.OrdRel

Methods

(.==.) :: e -> e -> OrdRel e

(./=.) :: e -> e -> OrdRel e

(Eval m e a, Ord a) => Eval m (OrdRel e) Bool

Defined in ToySolver.Data.OrdRel

Methods

eval :: m -> OrdRel e -> Bool

Eq e => Eq (OrdRel e)

Defined in ToySolver.Data.OrdRel

Methods

(==) :: OrdRel e -> OrdRel e -> Bool

(/=) :: OrdRel e -> OrdRel e -> Bool

Ord e => Ord (OrdRel e)

Defined in ToySolver.Data.OrdRel

Methods

compare :: OrdRel e -> OrdRel e -> Ordering

(<) :: OrdRel e -> OrdRel e -> Bool

(<=) :: OrdRel e -> OrdRel e -> Bool

(>) :: OrdRel e -> OrdRel e -> Bool

(>=) :: OrdRel e -> OrdRel e -> Bool

max :: OrdRel e -> OrdRel e -> OrdRel e

min :: OrdRel e -> OrdRel e -> OrdRel e

Show e => Show (OrdRel e)

Defined in ToySolver.Data.OrdRel

Methods

showsPrec :: Int -> OrdRel e -> ShowS

show :: OrdRel e -> String

showList :: [OrdRel e] -> ShowS

Complement (OrdRel c)

Defined in ToySolver.Data.OrdRel

Methods

notB :: OrdRel c -> OrdRel c

Variables e => Variables (OrdRel e)

Defined in ToySolver.Data.OrdRel

Methods

vars :: OrdRel e -> VarSet

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)

fromOrdRel :: IsOrdRel e r => OrdRel e -> r

DSL

class IsEqRel e r | r -> e where

type class for constructing relational formula

Methods

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

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

Instances

IsEqRel Expr Atom

Defined in ToySolver.BitVector.Base

Methods

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

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

IsEqRel BV Bool

Defined in ToySolver.BitVector.Base

Methods

(.==.) :: BV -> BV -> Bool

(./=.) :: BV -> BV -> Bool

IsEqRel Expr Expr

Defined in ToySolver.SMT

Methods

(.==.) :: Expr -> Expr -> Expr

(./=.) :: Expr -> Expr -> Expr

IsEqRel e (OrdRel e)

Defined in ToySolver.Data.OrdRel

Methods

(.==.) :: e -> e -> OrdRel e

(./=.) :: e -> e -> OrdRel e

IsEqRel (Expr Integer) QFFormula

Defined in ToySolver.Arith.Cooper.Base

Methods

(.==.) :: Expr Integer -> Expr Integer -> QFFormula

(./=.) :: Expr Integer -> Expr Integer -> QFFormula

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)

class IsEqRel e r => IsOrdRel e r | r -> e where

type class for constructing relational formula

Minimal complete definition

(.<.), (.<=.), (.>.), (.>=.) | ordRel

Methods

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

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

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

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

ordRel :: RelOp -> e -> e -> r

Instances

IsOrdRel Expr Expr

Defined in ToySolver.SMT

Methods

(.<.) :: Expr -> Expr -> Expr

(.<=.) :: Expr -> Expr -> Expr

(.>.) :: Expr -> Expr -> Expr

(.>=.) :: Expr -> Expr -> Expr

ordRel :: RelOp -> Expr -> Expr -> Expr

IsOrdRel e (OrdRel e)

Defined in ToySolver.Data.OrdRel

Methods

(.<.) :: e -> e -> OrdRel e

(.<=.) :: e -> e -> OrdRel e

(.>.) :: e -> e -> OrdRel e

(.>=.) :: e -> e -> OrdRel e

ordRel :: RelOp -> e -> e -> OrdRel e

IsOrdRel (Expr Integer) QFFormula

Defined in ToySolver.Arith.Cooper.Base

Methods

(.<.) :: Expr Integer -> Expr Integer -> QFFormula

(.<=.) :: Expr Integer -> Expr Integer -> QFFormula

(.>.) :: Expr Integer -> Expr Integer -> QFFormula

(.>=.) :: Expr Integer -> Expr Integer -> QFFormula

ordRel :: RelOp -> Expr Integer -> Expr Integer -> QFFormula

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)