cryptol-2.6.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

Description

Synopsis

- data Solver
- withSolver :: SolverConfig -> (Solver -> IO a) -> IO a
- isNumeric :: Prop -> Bool
- 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')]

# Setup

data Solver Source #

An SMT solver packed with a logger for debugging.

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

Execute a computation with a fresh solver instance.

isNumeric :: Prop -> Bool Source #

Assumes no `And`

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