| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
SoPSat.Satisfier
Synopsis
- type SolverState f c = StateT (State f c) Maybe
- declare :: (Ord f, Ord c) => SoPE f c -> SolverState f c Bool
- assert :: (Ord f, Ord c) => SoPE f c -> SolverState f c Bool
- unify :: (Ord f, Ord c) => SoPE f c -> SolverState f c [SoPE f c]
- range :: (Ord f, Ord c) => SoP f c -> SolverState f c (Maybe (SoP f c), Maybe (SoP f c))
- ranges :: (Ord f, Ord c) => SolverState f c [(Maybe (SoP f c), SoP f c, Maybe (SoP 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
- evalSoP :: (Ord f, Ord c, Floating n) => SoP f c -> Map (Atom f c) n -> n
State
State manipulation
Arguments
| :: (Ord f, Ord c) | |
| => SoPE f c | Expression to declare |
| -> SolverState f c Bool |
State will become |
Declare expression to the state
Arguments
| :: (Ord f, Ord c) | |
| => SoPE f c | Asserted expression |
| -> SolverState f c Bool |
State will become |
Assert if given expression holds in the current environment
Arguments
| :: (Ord f, Ord c) | |
| => SoPE f c | Unified expression |
| -> SolverState f c [SoPE f c] | List of unifiers - Minimal list of unifiers for the expression to hold. The list is empty, if it never holds State will always be valid after a call |
Get unifiers for an expression minimal set of expressions that should hold for the expression to hold
State information
Arguments
| :: (Ord f, Ord c) | |
| => SoP f c | Expression |
| -> SolverState f c (Maybe (SoP f c), Maybe (SoP f c)) | (lower bound, upper bound) - Range for an expression
|
Get range of possible values for an expression
Arguments
| :: (Ord f, Ord c) | |
| => SolverState f c [(Maybe (SoP f c), SoP f c, Maybe (SoP f c))] | (lower bound, symbol, upper bound) - Similar to |
Get list of all ranges stored in a state
State execution
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