Jukebox.Monotonox.Monotonicity

Documentation

data Extension

Constructors

TrueExtend

FalseExtend

CopyExtend

Instances

Show Extension

Methods

showsPrec :: Int -> Extension -> ShowS

show :: Extension -> String

showList :: [Extension] -> ShowS

data Var

Constructors

FalseExtended Function

TrueExtended Function

Instances

Eq Var

Methods

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

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

Ord Var

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

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

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

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