sop-satisfier-0.3.4.5: Check satisfiability of expressions on natural numbers

Safe Haskell	Safe-Inferred
Language	Haskell2010

SoPSat.Internal.SolverMonad

Synopsis

data (Ord f, Ord c) => State f c = State (Map (Atom f c) (Range f c)) [Unifier f c]
type SolverState f c = StateT (State f c) Maybe
maybeFail :: MonadFail m => Maybe a -> m a
getRanges :: (Ord f, Ord c) => SolverState f c (Map (Atom f c) (Range f c))
getRange :: (Ord f, Ord c) => Atom f c -> SolverState f c (Range f c)
getRangeSymbol :: (Ord f, Ord c) => Symbol f c -> SolverState f c (Range f c)
getRangeProduct :: (Ord f, Ord c) => Product f c -> SolverState f c (Range f c)
getRangeSoP :: (Ord f, Ord c) => SoP f c -> SolverState f c (Range f c)
putRange :: (Ord f, Ord c) => Atom f c -> Range f c -> SolverState f c ()
getUnifiers :: (Ord f, Ord c) => SolverState f c [Unifier f c]
putUnifiers :: (Ord f, Ord c) => [Unifier f c] -> SolverState f c ()
withState :: (Ord f, Ord c) => State f c -> SolverState f c ()
runStatements :: (Ord f, Ord c) => SolverState f c a -> Maybe (a, State f c)
evalStatements :: (Ord f, Ord c) => SolverState f c a -> Maybe a

Documentation

data (Ord f, Ord c) => State f c Source #

Constructors

State (Map (Atom f c) (Range f c)) [Unifier f c]

Instances

Instances details

(Ord f, Ord c) => Monoid (State f c) Source #
Instance details Defined in SoPSat.Internal.SolverMonad Methods mempty :: State f c # mappend :: State f c -> State f c -> State f c # mconcat :: [State f c] -> State f c #
(Ord f, Ord c) => Semigroup (State f c) Source #
Instance details Defined in SoPSat.Internal.SolverMonad Methods (<>) :: State f c -> State f c -> State f c # sconcat :: NonEmpty (State f c) -> State f c # stimes :: Integral b => b -> State f c -> State f c #
(Ord f, Ord c, Show f, Show c) => Show (State f c) Source #
Instance details Defined in SoPSat.Internal.SolverMonad Methods showsPrec :: Int -> State f c -> ShowS # show :: State f c -> String # showList :: [State f c] -> ShowS #

type SolverState f c = StateT (State f c) Maybe Source #

maybeFail :: MonadFail m => Maybe a -> m a Source #

getRanges :: (Ord f, Ord c) => SolverState f c (Map (Atom f c) (Range f c)) Source #

getRange :: (Ord f, Ord c) => Atom f c -> SolverState f c (Range f c) Source #

getRangeSymbol :: (Ord f, Ord c) => Symbol f c -> SolverState f c (Range f c) Source #

getRangeProduct :: (Ord f, Ord c) => Product f c -> SolverState f c (Range f c) Source #

getRangeSoP :: (Ord f, Ord c) => SoP f c -> SolverState f c (Range f c) Source #

putRange :: (Ord f, Ord c) => Atom f c -> Range f c -> SolverState f c () Source #

getUnifiers :: (Ord f, Ord c) => SolverState f c [Unifier f c] Source #

putUnifiers :: (Ord f, Ord c) => [Unifier f c] -> SolverState f c () Source #

withState :: (Ord f, Ord c) => State f c -> SolverState f c () Source #

Puts a state to use during computations

runStatements :: (Ord f, Ord c) => SolverState f c a -> Maybe (a, State f c) Source #

Runs computation returning result and resulting state

evalStatements :: (Ord f, Ord c) => SolverState f c a -> Maybe a Source #

Similar to runStatements but does not return final state