Jikka.Core.Language.AssertedHint

Documentation

data AssertedHint

Constructors

NotEqualHint ArithmeticExpr

NotEqualHint n for a integer variable x means x /= n

BoundHint (Maybe ArithmeticExpr) (Maybe ArithmeticExpr)

BoundHint l r for a integer variable x means l <= x < r

LengthHint Type AssertedHint

LengthHint t hint for a list variable xs means length xs satisfies hint

AllHint Type AssertedHint

AllHint t hint for a list variable xs means that x satisfies hint for all x in xs

Instances

Eq AssertedHint

Defined in Jikka.Core.Language.AssertedHint

Methods

(==) :: AssertedHint -> AssertedHint -> Bool

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

Ord AssertedHint

Defined in Jikka.Core.Language.AssertedHint

Methods

compare :: AssertedHint -> AssertedHint -> Ordering

(<) :: AssertedHint -> AssertedHint -> Bool

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

(>) :: AssertedHint -> AssertedHint -> Bool

(>=) :: AssertedHint -> AssertedHint -> Bool

max :: AssertedHint -> AssertedHint -> AssertedHint

min :: AssertedHint -> AssertedHint -> AssertedHint

Show AssertedHint

Defined in Jikka.Core.Language.AssertedHint

Methods

showsPrec :: Int -> AssertedHint -> ShowS

show :: AssertedHint -> String

showList :: [AssertedHint] -> ShowS

pattern EqualHint :: ArithmeticExpr -> AssertedHint

parseHints :: Expr -> [(VarName, AssertedHint)]

Functions using hints

lowerBoundWithHints :: [(VarName, AssertedHint)] -> Expr -> Maybe Integer

upperBoundWithHints :: [(VarName, AssertedHint)] -> Expr -> Maybe Integer

isZeroWithHints :: [(VarName, AssertedHint)] -> Expr -> Maybe Bool

nullWithHints :: [(VarName, AssertedHint)] -> Expr -> Maybe Bool

lengthWithHints :: [(VarName, AssertedHint)] -> Expr -> Maybe Integer