jukebox-0.1.6: A first-order reasoning toolbox

Safe Haskell	None
Language	Haskell98

Jukebox.Monotonox.Monotonicity

Documentation

data Extension Source

Constructors

TrueExtend
FalseExtend
CopyExtend

Instances

Show Extension Source

data Var Source

Constructors

FalseExtended Function
TrueExtended Function

Instances

Eq Var Source
Ord Var Source
Hashable Var Source

annotateMonotonicity :: Problem Clause -> IO (Problem Clause) Source

monotone :: [Clause] -> IO (NameMap (Type ::: Maybe (NameMap (Function ::: Extension)))) Source

fromModel :: [Function] -> Type -> (Var -> Bool) -> NameMap (Function ::: Extension) Source

extension :: Function -> (Var -> Bool) -> Extension Source

clause :: [Literal] -> Sat Var Type () Source

literal :: [Literal] -> Literal -> Sat Var Type () Source

safe :: [Literal] -> Term -> Form Var Source

guards :: Literal -> Variable -> Form Var Source