jukebox-0.5.6: A first-order reasoning toolbox
Safe HaskellNone
LanguageHaskell2010

Jukebox.Tools.AnalyseMonotonicity

Documentation

data Extension Source #

Constructors

TrueExtend 
FalseExtend 
CopyExtend 

Instances

Instances details
Show Extension Source # 
Instance details

Defined in Jukebox.Tools.AnalyseMonotonicity

Methods

showsPrec :: Int -> Extension -> ShowS #

show :: Extension -> String #

showList :: [Extension] -> ShowS #

data Var Source #

Constructors

FalseExtended Function 
TrueExtended Function 

Instances

Instances details
Eq Var Source # 
Instance details

Defined in Jukebox.Tools.AnalyseMonotonicity

Methods

(==) :: Var -> Var -> Bool #

(/=) :: Var -> Var -> Bool #

Ord Var Source # 
Instance details

Defined in Jukebox.Tools.AnalyseMonotonicity

Methods

compare :: Var -> Var -> Ordering #

(<) :: Var -> Var -> Bool #

(<=) :: Var -> Var -> Bool #

(>) :: Var -> Var -> Bool #

(>=) :: Var -> Var -> Bool #

max :: Var -> Var -> Var #

min :: Var -> Var -> Var #

analyseMonotonicity :: Problem Clause -> IO (Set Type) 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 #