jukebox-0.1.4: A first-order reasoning toolbox

Safe HaskellNone
LanguageHaskell98

Jukebox.Monotonox.Monotonicity

Documentation

data Extension Source

Constructors

TrueExtend 
FalseExtend 
CopyExtend 

Instances

data Var Source

Constructors

FalseExtended Function 
TrueExtended Function 

Instances

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