| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Language.REST.SMT
Description
This module contains functionality for creating SMTLIB expressions and interacting with an SMT solver.
Synopsis
- checkSat :: SMTExpr Bool -> IO Bool
- checkSat' :: (Handle, Handle) -> SMTExpr Bool -> IO Bool
- getModel :: Handle -> IO ()
- parseModel :: String -> Z3Model
- killZ3 :: SolverHandle -> IO ()
- spawnZ3 :: IO SolverHandle
- smtAdd :: [SMTExpr Int] -> SMTExpr Int
- smtAnd :: SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool
- smtFalse :: SMTExpr Bool
- smtGTE :: SMTExpr Int -> SMTExpr Int -> SMTExpr Bool
- smtTrue :: SMTExpr Bool
- withZ3 :: MonadIO m => (SolverHandle -> m b) -> m b
- type SolverHandle = (Handle, Handle)
- data SMTExpr a where
- And :: [SMTExpr Bool] -> SMTExpr Bool
- Add :: [SMTExpr Int] -> SMTExpr Int
- Or :: [SMTExpr Bool] -> SMTExpr Bool
- Equal :: [SMTExpr a] -> SMTExpr Bool
- Greater :: SMTExpr Int -> SMTExpr Int -> SMTExpr Bool
- GTE :: SMTExpr Int -> SMTExpr Int -> SMTExpr Bool
- Implies :: SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool
- Var :: SMTVar a -> SMTExpr a
- Const :: Int -> SMTExpr Int
- newtype SMTVar a = SMTVar Text
- class ToSMT a b where
- class ToSMTVar a b | a -> b where
- type Z3Model = Map String String
Documentation
checkSat :: SMTExpr Bool -> IO Bool Source #
checkSat expr launches Z3, to checks satisfiability of expr, terminating Z3
afterwards. Just a utility wrapper for checkSat'
checkSat' :: (Handle, Handle) -> SMTExpr Bool -> IO Bool Source #
checkSat' handles expr checks satisfiability of expr in an instantiated SMT solver.
This is wrapped in a push / pop, so it does not change the SMT environment
getModel :: Handle -> IO () Source #
getModel instructs an instantiated SMT solver to produce its model.
killZ3 :: SolverHandle -> IO () Source #
Kills the Z3 instance by closing the standard input stream
spawnZ3 :: IO SolverHandle Source #
Instantiates a Z3 instance, returning the solver handle for interaction
smtAdd :: [SMTExpr Int] -> SMTExpr Int Source #
Returns an SMT expression that adds all elements in the list. If the list is empty,
returns Const 0.
smtAnd :: SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool Source #
`smtAnd t u` returns an smt expression representing \( t \land u \).
smtGTE :: SMTExpr Int -> SMTExpr Int -> SMTExpr Bool Source #
`smtGTE t u` returns an SMT expression \( t \geqslant u \). If t == u, returns smtTrue.
withZ3 :: MonadIO m => (SolverHandle -> m b) -> m b Source #
withZ3 f instantiates a Z3 instance, runs f with that instance,
and then closes the instance and returns the result
type SolverHandle = (Handle, Handle) Source #
The handle (stdIn, stdOut) used for interacting with Z3
SMTLib expressions
Constructors
| And :: [SMTExpr Bool] -> SMTExpr Bool | |
| Add :: [SMTExpr Int] -> SMTExpr Int | |
| Or :: [SMTExpr Bool] -> SMTExpr Bool | |
| Equal :: [SMTExpr a] -> SMTExpr Bool | |
| Greater :: SMTExpr Int -> SMTExpr Int -> SMTExpr Bool | |
| GTE :: SMTExpr Int -> SMTExpr Int -> SMTExpr Bool | |
| Implies :: SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool | |
| Var :: SMTVar a -> SMTExpr a | |
| Const :: Int -> SMTExpr Int |
Instances
| Show (SMTExpr a) Source # | |
| Eq (SMTExpr a) Source # | |
| Ord (SMTExpr a) Source # | |
| Hashable (SMTExpr a) Source # | |
Defined in Language.REST.SMT | |
An SMT variable
class ToSMT a b where Source #
This class allows elements of type a to be used as SMT expressions of type
b