| 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
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')]
Setup
data SolverConfig Source #
Instances
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
resetSolver :: Solver -> SolverConfig -> IO () Source #