jukebox-0.4.2: A first-order reasoning toolbox
Jukebox.Tools.AnalyseMonotonicity
data Extension Source #
Constructors
Defined in Jukebox.Tools.AnalyseMonotonicity
Methods
showsPrec :: Int -> Extension -> ShowS #
show :: Extension -> String #
showList :: [Extension] -> ShowS #
data Var Source #
(==) :: Var -> Var -> Bool #
(/=) :: Var -> Var -> Bool #
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 #