Copyright	(c) Masahiro Sakai 2011
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Stability	provisional
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010
Extensions	UndecidableInstances TypeSynonymInstances FlexibleInstances ConstrainedClassMethods MultiParamTypeClasses FunctionalDependencies

ToySolver.Data.OrdRel

Contents

Relational operators
Relation
DSL

Description

Ordering relations

Synopsis

data RelOp
- = Lt
- | Le
- | Ge
- | Gt
- | Eql
- | NEq
flipOp :: RelOp -> RelOp
negOp :: RelOp -> RelOp
showOp :: RelOp -> String
evalOp :: Ord a => RelOp -> a -> a -> Bool
data OrdRel e = OrdRel e RelOp e
fromOrdRel :: IsOrdRel e r => OrdRel e -> r
class IsEqRel e r | r -> e where
- (.==.) :: e -> e -> r
- (./=.) :: e -> e -> r
class IsEqRel e r => IsOrdRel e r | r -> e where
- (.<.), (.<=.), (.>.), (.>=.) :: e -> e -> r
- ordRel :: RelOp -> e -> e -> r

Relational operators

data RelOp Source #

relational operators

Constructors

Lt
Le
Ge
Gt
Eql
NEq

Instances

Instances details

Show RelOp Source #
Instance details Defined in ToySolver.Data.OrdRel Methods showsPrec :: Int -> RelOp -> ShowS # show :: RelOp -> String # showList :: [RelOp] -> ShowS #
Eq RelOp Source #
Instance details Defined in ToySolver.Data.OrdRel Methods (==) :: RelOp -> RelOp -> Bool # (/=) :: RelOp -> RelOp -> Bool #
Ord RelOp Source #
Instance details 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 #

flipOp :: RelOp -> RelOp Source #

flipping relational operator

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

negOp :: RelOp -> RelOp Source #

negating relational operator

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

showOp :: RelOp -> String Source #

operator symbol

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

evaluate an operator into a comparision function

Relation

data OrdRel e Source #

Atomic formula

Constructors

OrdRel e RelOp e

Instances

Instances details

Functor OrdRel Source #
Instance details Defined in ToySolver.Data.OrdRel Methods fmap :: (a -> b) -> OrdRel a -> OrdRel b # (<$) :: a -> OrdRel b -> OrdRel a #
IsEqRel e (OrdRel e) Source #
Instance details Defined in ToySolver.Data.OrdRel Methods (.==.) :: e -> e -> OrdRel e Source # (./=.) :: e -> e -> OrdRel e Source #
IsOrdRel e (OrdRel e) Source #
Instance details Defined in ToySolver.Data.OrdRel Methods (.<.) :: e -> e -> OrdRel e Source # (.<=.) :: e -> e -> OrdRel e Source # (.>.) :: e -> e -> OrdRel e Source # (.>=.) :: e -> e -> OrdRel e Source # ordRel :: RelOp -> e -> e -> OrdRel e Source #
(Eval m e a, Ord a) => Eval m (OrdRel e) Bool Source #
Instance details Defined in ToySolver.Data.OrdRel Methods eval :: m -> OrdRel e -> Bool Source #
Show e => Show (OrdRel e) Source #
Instance details Defined in ToySolver.Data.OrdRel Methods showsPrec :: Int -> OrdRel e -> ShowS # show :: OrdRel e -> String # showList :: [OrdRel e] -> ShowS #
Eq e => Eq (OrdRel e) Source #
Instance details Defined in ToySolver.Data.OrdRel Methods (==) :: OrdRel e -> OrdRel e -> Bool # (/=) :: OrdRel e -> OrdRel e -> Bool #
Ord e => Ord (OrdRel e) Source #
Instance details 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 #
Complement (OrdRel c) Source #
Instance details Defined in ToySolver.Data.OrdRel Methods notB :: OrdRel c -> OrdRel c Source #
Variables e => Variables (OrdRel e) Source #
Instance details Defined in ToySolver.Data.OrdRel Methods vars :: OrdRel e -> VarSet 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 #

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

DSL

class IsEqRel e r | r -> e where Source #

type class for constructing relational formula

Methods

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

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

Instances

Instances details

IsEqRel BV Bool Source #
Instance details Defined in ToySolver.BitVector.Base Methods (.==.) :: BV -> BV -> Bool Source # (./=.) :: BV -> BV -> Bool Source #
IsEqRel Expr Atom Source #
Instance details Defined in ToySolver.BitVector.Base Methods (.==.) :: Expr -> Expr -> Atom Source # (./=.) :: Expr -> Expr -> Atom Source #
IsEqRel Expr Expr Source #
Instance details Defined in ToySolver.SMT Methods (.==.) :: Expr -> Expr -> Expr Source # (./=.) :: Expr -> Expr -> Expr Source #
IsEqRel e (OrdRel e) Source #
Instance details Defined in ToySolver.Data.OrdRel Methods (.==.) :: e -> e -> OrdRel e Source # (./=.) :: e -> e -> OrdRel e Source #
IsEqRel (Expr Integer) QFFormula Source #
Instance details Defined in ToySolver.Arith.Cooper.Base Methods (.==.) :: Expr Integer -> Expr Integer -> QFFormula Source # (./=.) :: Expr Integer -> Expr Integer -> QFFormula 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 #

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

type class for constructing relational formula

Minimal complete definition

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

Methods

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

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

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

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

ordRel :: RelOp -> e -> e -> r Source #

Instances

Instances details

IsOrdRel Expr Expr Source #
Instance details Defined in ToySolver.SMT Methods (.<.) :: Expr -> Expr -> Expr Source # (.<=.) :: Expr -> Expr -> Expr Source # (.>.) :: Expr -> Expr -> Expr Source # (.>=.) :: Expr -> Expr -> Expr Source # ordRel :: RelOp -> Expr -> Expr -> Expr Source #
IsOrdRel e (OrdRel e) Source #
Instance details Defined in ToySolver.Data.OrdRel Methods (.<.) :: e -> e -> OrdRel e Source # (.<=.) :: e -> e -> OrdRel e Source # (.>.) :: e -> e -> OrdRel e Source # (.>=.) :: e -> e -> OrdRel e Source # ordRel :: RelOp -> e -> e -> OrdRel e Source #
IsOrdRel (Expr Integer) QFFormula Source #
Instance details Defined in ToySolver.Arith.Cooper.Base Methods (.<.) :: Expr Integer -> Expr Integer -> QFFormula Source # (.<=.) :: Expr Integer -> Expr Integer -> QFFormula Source # (.>.) :: Expr Integer -> Expr Integer -> QFFormula Source # (.>=.) :: Expr Integer -> Expr Integer -> QFFormula Source # ordRel :: RelOp -> Expr Integer -> Expr Integer -> QFFormula 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 #