Copyright | (c) 2013-2016 Galois Inc. |
---|---|

License | BSD3 |

Maintainer | cryptol@galois.com |

Stability | provisional |

Portability | portable |

Safe Haskell | Safe |

Language | Haskell2010 |

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

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

Execute a computation with a fresh solver instance.