Copyright | (c) 2013-2016 Galois, Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell98 |
- withScope :: Solver -> IO a -> IO a
- withSolver :: SolverConfig -> (Solver -> IO a) -> IO a
- assumeProps :: Solver -> [Prop] -> IO [SimpProp]
- simplifyProps :: Solver -> [DefinedProp Goal] -> IO [Goal]
- getModel :: Solver -> [Prop] -> IO (Maybe Subst)
- check :: Solver -> IO (Maybe (Subst, [Prop]))
- data Solver
- logger :: Solver -> Logger
- getIntervals :: Solver -> IO (Either TVar (Map TVar Interval))
- data DefinedProp a = DefinedProp {
- dpData :: a
- dpSimpProp :: SimpProp
- dpSimpExprProp :: Prop
- debugBlock :: Solver -> String -> IO a -> IO a
- class DebugLog t where
- knownDefined :: (a, Prop) -> DefinedProp a
- numericRight :: Goal -> Either Goal (Goal, Prop)
- minimizeContradictionSimpDef :: HasProp a => Solver -> [DefinedProp a] -> IO [a]
Documentation
withSolver :: SolverConfig -> (Solver -> IO a) -> IO a Source #
Execute a computation with a fresh solver instance.
assumeProps :: Solver -> [Prop] -> IO [SimpProp] Source #
Add the given constraints as assumptions. * We assume that the constraints are well-defined. * Modifies the set of assumptions.
simplifyProps :: Solver -> [DefinedProp Goal] -> IO [Goal] Source #
Simplify a bunch of well-defined properties. * Eliminates properties that are implied by the rest. * Does not modify the set of assumptions.
getModel :: Solver -> [Prop] -> IO (Maybe Subst) Source #
Attempt to find a substituion that, when applied, makes all of the given properties hold.
check :: Solver -> IO (Maybe (Subst, [Prop])) Source #
Check if the current set of assumptions is satisfiable, and find some facts that must hold in any models of the current assumptions.
Returns Nothing
if the currently asserted constraints are known to
be unsatisfiable.
Returns `Just (su, sub-goals)` is the current set is satisfiable.
* The su
is a substitution that may be applied to the current constraint
set without loosing generality.
* The `sub-goals` are additional constraints that must hold if the
constraint set is to be satisfiable.
data DefinedProp a Source #
dpSimpProp
and dpSimpExprProp
should be logically equivalent,
to each other, and to whatever a
represents (usually a
is a Goal
).
DefinedProp | |
|
knownDefined :: (a, Prop) -> DefinedProp a Source #
numericRight :: Goal -> Either Goal (Goal, Prop) Source #
Class goals go on the left, numeric goals go on the right.
minimizeContradictionSimpDef :: HasProp a => Solver -> [DefinedProp a] -> IO [a] Source #
Given a list of propositions that together lead to a contradiction, find a sub-set that still leads to a contradiction (but is smaller).