| Safe Haskell | None |
|---|---|
| Language | GHC2021 |
SimpleBV
Synopsis
- data SExpr
- data Solver
- defaultConfig :: String -> [String] -> Config
- newLogger :: Int -> IO Logger
- newLoggerWithHandle :: Handle -> Int -> IO Logger
- newSolver :: String -> [String] -> Maybe Logger -> IO Solver
- newSolverWithConfig :: Config -> IO Solver
- solverLogger :: Config -> SolverLogger
- smtSolverLogger :: Logger -> SolverLogger
- setLogic :: Solver -> String -> IO ()
- push :: Solver -> IO ()
- pop :: Solver -> IO ()
- popMany :: Solver -> Integer -> IO ()
- check :: Solver -> IO Result
- data Result
- data Value
- pattern W :: Int -> SExpr
- pattern Byte :: SExpr
- pattern Half :: SExpr
- pattern Word :: SExpr
- pattern Long :: SExpr
- width :: SExpr -> Int
- const :: String -> Int -> SExpr
- declareBV :: Solver -> String -> Int -> IO SExpr
- assert :: Solver -> SExpr -> IO ()
- sexprToVal :: SExpr -> Value
- getValue :: Solver -> SExpr -> IO Value
- getValues :: Solver -> [SExpr] -> IO [(String, Value)]
- toSMT :: SExpr -> SExpr
- ite :: SExpr -> SExpr -> SExpr -> SExpr
- and :: SExpr -> SExpr -> SExpr
- or :: SExpr -> SExpr -> SExpr
- not :: SExpr -> SExpr
- eq :: SExpr -> SExpr -> SExpr
- bvLit :: Int -> Integer -> SExpr
- bvAdd :: SExpr -> SExpr -> SExpr
- bvAShr :: SExpr -> SExpr -> SExpr
- bvLShr :: SExpr -> SExpr -> SExpr
- bvAnd :: SExpr -> SExpr -> SExpr
- bvMul :: SExpr -> SExpr -> SExpr
- bvNeg :: SExpr -> SExpr
- bvOr :: SExpr -> SExpr -> SExpr
- bvSDiv :: SExpr -> SExpr -> SExpr
- bvSLeq :: SExpr -> SExpr -> SExpr
- bvSLt :: SExpr -> SExpr -> SExpr
- bvSGeq :: SExpr -> SExpr -> SExpr
- bvSGt :: SExpr -> SExpr -> SExpr
- bvSRem :: SExpr -> SExpr -> SExpr
- bvShl :: SExpr -> SExpr -> SExpr
- bvSub :: SExpr -> SExpr -> SExpr
- bvUDiv :: SExpr -> SExpr -> SExpr
- bvULeq :: SExpr -> SExpr -> SExpr
- bvUGeq :: SExpr -> SExpr -> SExpr
- bvUGt :: SExpr -> SExpr -> SExpr
- bvULt :: SExpr -> SExpr -> SExpr
- bvURem :: SExpr -> SExpr -> SExpr
- bvXOr :: SExpr -> SExpr -> SExpr
- concat :: SExpr -> SExpr -> SExpr
- extract :: SExpr -> Int -> Int -> SExpr
- signExtend :: Integer -> SExpr -> SExpr
- zeroExtend :: Integer -> SExpr -> SExpr
Documentation
A reasonable default Config value.
newLogger :: Int -> IO Logger #
A simple stdout logger. Shows only messages logged at a level that is greater than or equal to the passed level.
newLoggerWithHandle :: Handle -> Int -> IO Logger #
A simple logger that writes to a Handle. Shows only messages logged at a
level that is greater than or equal to the passed level.
Start a new solver process.
newSolverWithConfig :: Config -> IO Solver #
Start a new solver process using the provided Config options.
solverLogger :: Config -> SolverLogger #
How to log solver-related messages.
smtSolverLogger :: Logger -> SolverLogger #
A SolverLogger that formats log messages into the SMT-LIB file format so
that the resulting log can be parsed as input by an SMT solver.
Results of checking for satisfiability.
Common values returned by SMT solvers.
sexprToVal :: SExpr -> Value Source #