cryptol-2.3.0: Cryptol: The Language of Cryptography

Copyright(c) 2013-2016 Galois, Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell98

Cryptol.TypeCheck.Solver.CrySAT

Description

 

Synopsis

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

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