Cryptol.TypeCheck.Solver.CrySAT

Documentation

withScope :: Solver -> IO a -> IO a

Execute a computation in a new solver scope.

withSolver :: SolverConfig -> (Solver -> IO a) -> IO a

Execute a computation with a fresh solver instance.

assumeProps :: Solver -> [Prop] -> IO [SimpProp]

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]

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)

Attempt to find a substituion that, when applied, makes all of the given properties hold.

check :: Solver -> IO (Maybe (Subst, [Prop]))

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

An SMT solver, and some info about declared variables.

logger :: Solver -> Logger

For debugging

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

data DefinedProp a

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

class DebugLog t where

Minimal complete definition

debugLog

Methods

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

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

Instances

DebugLog Char

Methods

debugLog :: Solver -> Char -> IO ()

debugLogList :: Solver -> [Char] -> IO ()

DebugLog Doc

Methods

debugLog :: Solver -> Doc -> IO ()

debugLogList :: Solver -> [Doc] -> IO ()

DebugLog Type

Methods

debugLog :: Solver -> Type -> IO ()

debugLogList :: Solver -> [Type] -> IO ()

DebugLog Prop

Methods

debugLog :: Solver -> Prop -> IO ()

debugLogList :: Solver -> [Prop] -> IO ()

DebugLog Subst

Methods

debugLog :: Solver -> Subst -> IO ()

debugLogList :: Solver -> [Subst] -> IO ()

DebugLog Goal

Methods

debugLog :: Solver -> Goal -> IO ()

debugLogList :: Solver -> [Goal] -> IO ()

DebugLog a => DebugLog [a]

Methods

debugLog :: Solver -> [a] -> IO ()

debugLogList :: Solver -> [[a]] -> IO ()

DebugLog a => DebugLog (Maybe a)

Methods

debugLog :: Solver -> Maybe a -> IO ()

debugLogList :: Solver -> [Maybe a] -> IO ()

knownDefined :: (a, Prop) -> DefinedProp a

numericRight :: Goal -> Either Goal (Goal, Prop)

Class goals go on the left, numeric goals go on the right.

minimizeContradictionSimpDef :: HasProp a => Solver -> [DefinedProp a] -> IO [a]

Given a list of propositions that together lead to a contradiction, find a sub-set that still leads to a contradiction (but is smaller).

loadFile :: Solver -> FilePath -> IO ()

rawSolver :: Solver -> Solver