Copyright  (c) 20132016 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 welldefined. * Modifies the set of assumptions.
simplifyProps :: Solver > [DefinedProp Goal] > IO [Goal] Source #
Simplify a bunch of welldefined 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, subgoals)` is the current set is satisfiable.
* The su
is a substitution that may be applied to the current constraint
set without loosing generality.
* The `subgoals` 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 subset that still leads to a contradiction (but is smaller).