cryptol-3.0.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 | Haskell2010

Cryptol.TypeCheck.Solver.SMT

Contents

- Setup
- Debugging
- Proving stuff
- Lower level interactions

Description

Synopsis

- data Solver
- data SolverConfig
- withSolver :: IO () -> SolverConfig -> (Solver -> IO a) -> IO a
- startSolver :: IO () -> SolverConfig -> IO Solver
- stopSolver :: Solver -> IO ()
- isNumeric :: Prop -> Bool
- resetSolver :: Solver -> SolverConfig -> IO ()
- debugBlock :: Solver -> String -> IO a -> IO a
- debugLog :: DebugLog t => Solver -> t -> IO ()
- proveImp :: Solver -> [Prop] -> [Goal] -> IO [Goal]
- checkUnsolvable :: Solver -> [Goal] -> IO Bool
- tryGetModel :: Solver -> [TVar] -> [Prop] -> IO (Maybe [(TVar, Nat')])
- shrinkModel :: Solver -> [TVar] -> [Prop] -> [(TVar, Nat')] -> IO [(TVar, Nat')]
- inNewFrame :: Solver -> IO a -> IO a
- type TVars = Map TVar SExpr
- declareVars :: Solver -> [TVar] -> IO TVars
- assume :: Solver -> TVars -> Prop -> IO ()
- unsolvable :: Solver -> TVars -> [Prop] -> IO Bool

# Setup

data Solver Source #

An SMT solver packed with a logger for debugging.

data SolverConfig Source #

#### Instances

Instances details

Generic SolverConfig Source # |
Instance details Defined in Cryptol.TypeCheck.InferTypes Associated Types type Rep SolverConfig :: Type -> Type Source # Methods from :: SolverConfig -> Rep SolverConfig x Source # to :: Rep SolverConfig x -> SolverConfig Source #
Show SolverConfig Source # |
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods showsPrec :: Int -> SolverConfig -> ShowS Source # show :: SolverConfig -> String Source # showList :: [SolverConfig] -> ShowS Source #
NFData SolverConfig Source # |
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods rnf :: SolverConfig -> () Source #
type Rep SolverConfig Source # |

Instance details

Defined in Cryptol.TypeCheck.InferTypes

type Rep SolverConfig = D1 ('MetaData "SolverConfig" "Cryptol.TypeCheck.InferTypes" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "SolverConfig" 'PrefixI 'True) ((S1 ('MetaSel ('Just "solverPath") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: S1 ('MetaSel ('Just "solverArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])) :*: (S1 ('MetaSel ('Just "solverVerbose") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "solverPreludePath") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FilePath]))))

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

Execute a computation with a fresh solver instance.

startSolver :: IO () -> SolverConfig -> IO Solver Source #

Start a fresh solver instance

stopSolver :: Solver -> IO () Source #

Shut down a solver instance

isNumeric :: Prop -> Bool Source #

Assumes no `And`

resetSolver :: Solver -> SolverConfig -> IO () Source #

# Debugging

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

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

# Proving stuff

proveImp :: Solver -> [Prop] -> [Goal] -> IO [Goal] Source #

Returns goals that were not proved

checkUnsolvable :: Solver -> [Goal] -> IO Bool Source #

Check if the given goals are known to be unsolvable.

tryGetModel :: Solver -> [TVar] -> [Prop] -> IO (Maybe [(TVar, Nat')]) Source #

shrinkModel :: Solver -> [TVar] -> [Prop] -> [(TVar, Nat')] -> IO [(TVar, Nat')] Source #

# Lower level interactions

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

type TVars = Map TVar SExpr Source #

declareVars :: Solver -> [TVar] -> IO TVars Source #

assume :: Solver -> TVars -> Prop -> IO () Source #

unsolvable :: Solver -> TVars -> [Prop] -> IO Bool Source #

Check if some numeric goals are known to be unsolvable.