Jukebox.Monotonox.Monotonicity

Documentation

data Extension

Constructors

TrueExtend

FalseExtend

CopyExtend

Instances

Show Extension

data Var

Constructors

FalseExtended Function

TrueExtended Function

Instances

Eq Var

Ord Var

Hashable Var

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

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

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

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

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

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

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

guards :: Literal -> Variable -> Form Var