cryptol-2.4.0: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2016 Galois Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | Safe
Language | Haskell98

Cryptol.TypeCheck.Solver.CrySAT

Description

Synopsis

- 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

withScope :: Solver -> IO a -> IO a Source #

Execute a computation in a new solver scope.

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 Solver Source #

An SMT solver, and some info about declared variables.

logger :: Solver -> Logger Source #

For debugging

getIntervals :: Solver -> IO (Either TVar (Map TVar Interval)) Source #

data DefinedProp a Source #

`dpSimpProp` and `dpSimpExprProp` should be logically equivalent, to each other, and to whatever `a` represents (usually `a` is a `Goal`).

Constructors

DefinedProp |

Fields

- dpData :: a

  Optional data to associate with prop. Often, the original `Goal` from which the prop was extracted.

- dpSimpProp :: SimpProp

  Fully simplified: may mention ORs, and named non-linear terms. These are what we send to the prover, and we don't attempt to convert them back into Cryptol types.

- dpSimpExprProp :: Prop

  A version of the proposition where just the expression terms have been simplified. These should not contain ORs or named non-linear terms because we want to import them back into Crytpol types.

debugBlock :: Solver -> String -> IO a -> IO a Source #

class DebugLog t where Source #

Minimal complete definition

debugLog

Methods

debugLog :: Solver -> t -> IO () Source #

debugLogList :: Solver -> [t] -> IO () Source #

Instances

DebugLog Char Source # |
Methods debugLog :: Solver -> Char -> IO () Source # debugLogList :: Solver -> [Char] -> IO () Source #
DebugLog Doc Source # |
Methods debugLog :: Solver -> Doc -> IO () Source # debugLogList :: Solver -> [Doc] -> IO () Source #
DebugLog Type Source # |
Methods debugLog :: Solver -> Type -> IO () Source # debugLogList :: Solver -> [Type] -> IO () Source #
DebugLog Prop Source # |
Methods debugLog :: Solver -> Prop -> IO () Source # debugLogList :: Solver -> [Prop] -> IO () Source #
DebugLog Subst Source # |
Methods debugLog :: Solver -> Subst -> IO () Source # debugLogList :: Solver -> [Subst] -> IO () Source #
DebugLog Goal Source # |
Methods debugLog :: Solver -> Goal -> IO () Source # debugLogList :: Solver -> [Goal] -> IO () Source #
DebugLog a => DebugLog [a] Source # |
Methods debugLog :: Solver -> [a] -> IO () Source # debugLogList :: Solver -> [[a]] -> IO () Source #
DebugLog a => DebugLog (Maybe a) Source # |
Methods debugLog :: Solver -> Maybe a -> IO () Source # debugLogList :: Solver -> [Maybe a] -> IO () Source #

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).