jukebox-0.2.6: 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 (Map Type (Maybe (Map Function Extension))) Source

fromModel :: [Function] -> Type -> (Var -> Bool) -> Map 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