| Copyright | (c) 2013-2016 Galois Inc. |
|---|---|
| License | BSD3 |
| Maintainer | cryptol@galois.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | Trustworthy |
| Language | Haskell2010 |
Cryptol.TypeCheck.Solver.SMT
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
- push :: Solver -> IO ()
- pop :: Solver -> IO ()
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 #
Debugging
Proving stuff
checkUnsolvable :: Solver -> [Goal] -> IO Bool Source #
Check if the given goals are known to be unsolvable.