| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
SimpleSMT
Contents
Description
A module for interacting with an SMT solver, using SmtLib-2 format.
- data Solver = Solver {}
- newSolver :: String -> [String] -> Maybe Logger -> IO Solver
- ackCommand :: Solver -> SExpr -> IO ()
- simpleCommand :: Solver -> [String] -> IO ()
- simpleCommandMaybe :: Solver -> [String] -> IO Bool
- loadFile :: Solver -> FilePath -> IO ()
- data SExpr
- showsSExpr :: SExpr -> ShowS
- readSExpr :: String -> Maybe (SExpr, String)
- data Logger = Logger {}
- newLogger :: Int -> IO Logger
- withLogLevel :: Logger -> Int -> IO a -> IO a
- logMessageAt :: Logger -> Int -> String -> IO ()
- logIndented :: Logger -> IO a -> IO a
- setLogic :: Solver -> String -> IO ()
- setLogicMaybe :: Solver -> String -> IO Bool
- setOption :: Solver -> String -> String -> IO ()
- setOptionMaybe :: Solver -> String -> String -> IO Bool
- push :: Solver -> IO ()
- pushMany :: Solver -> Integer -> IO ()
- pop :: Solver -> IO ()
- popMany :: Solver -> Integer -> IO ()
- inNewScope :: Solver -> IO a -> IO a
- declare :: Solver -> String -> SExpr -> IO SExpr
- declareFun :: Solver -> String -> [SExpr] -> SExpr -> IO SExpr
- declareDatatype :: Solver -> String -> [String] -> [(String, [(String, SExpr)])] -> IO ()
- define :: Solver -> String -> SExpr -> SExpr -> IO SExpr
- defineFun :: Solver -> String -> [(String, SExpr)] -> SExpr -> SExpr -> IO SExpr
- assert :: Solver -> SExpr -> IO ()
- check :: Solver -> IO Result
- data Result
- getExprs :: Solver -> [SExpr] -> IO [(SExpr, Value)]
- getExpr :: Solver -> SExpr -> IO Value
- getConsts :: Solver -> [String] -> IO [(String, Value)]
- getConst :: Solver -> String -> IO Value
- data Value
- fam :: String -> [Integer] -> SExpr
- fun :: String -> [SExpr] -> SExpr
- const :: String -> SExpr
- tInt :: SExpr
- tBool :: SExpr
- tReal :: SExpr
- tArray :: SExpr -> SExpr -> SExpr
- tBits :: Integer -> SExpr
- int :: Integer -> SExpr
- real :: Rational -> SExpr
- bool :: Bool -> SExpr
- bvBin :: Int -> Integer -> SExpr
- bvHex :: Int -> Integer -> SExpr
- value :: Value -> SExpr
- not :: SExpr -> SExpr
- and :: SExpr -> SExpr -> SExpr
- andMany :: [SExpr] -> SExpr
- or :: SExpr -> SExpr -> SExpr
- orMany :: [SExpr] -> SExpr
- xor :: SExpr -> SExpr -> SExpr
- implies :: SExpr -> SExpr -> SExpr
- ite :: SExpr -> SExpr -> SExpr -> SExpr
- eq :: SExpr -> SExpr -> SExpr
- distinct :: [SExpr] -> SExpr
- gt :: SExpr -> SExpr -> SExpr
- lt :: SExpr -> SExpr -> SExpr
- geq :: SExpr -> SExpr -> SExpr
- leq :: SExpr -> SExpr -> SExpr
- bvULt :: SExpr -> SExpr -> SExpr
- bvULeq :: SExpr -> SExpr -> SExpr
- bvSLt :: SExpr -> SExpr -> SExpr
- bvSLeq :: SExpr -> SExpr -> SExpr
- add :: SExpr -> SExpr -> SExpr
- addMany :: [SExpr] -> SExpr
- sub :: SExpr -> SExpr -> SExpr
- neg :: SExpr -> SExpr
- mul :: SExpr -> SExpr -> SExpr
- abs :: SExpr -> SExpr
- div :: SExpr -> SExpr -> SExpr
- mod :: SExpr -> SExpr -> SExpr
- divisible :: SExpr -> Integer -> SExpr
- realDiv :: SExpr -> SExpr -> SExpr
- concat :: SExpr -> SExpr -> SExpr
- extract :: SExpr -> Integer -> Integer -> SExpr
- bvNot :: SExpr -> SExpr
- bvNeg :: SExpr -> SExpr
- bvAnd :: SExpr -> SExpr -> SExpr
- bvXOr :: SExpr -> SExpr -> SExpr
- bvOr :: SExpr -> SExpr -> SExpr
- bvAdd :: SExpr -> SExpr -> SExpr
- bvSub :: SExpr -> SExpr -> SExpr
- bvMul :: SExpr -> SExpr -> SExpr
- bvUDiv :: SExpr -> SExpr -> SExpr
- bvURem :: SExpr -> SExpr -> SExpr
- bvSDiv :: SExpr -> SExpr -> SExpr
- bvSRem :: SExpr -> SExpr -> SExpr
- bvShl :: SExpr -> SExpr -> SExpr
- bvLShr :: SExpr -> SExpr -> SExpr
- bvAShr :: SExpr -> SExpr -> SExpr
- signExtend :: Integer -> SExpr -> SExpr
- zeroExtend :: Integer -> SExpr -> SExpr
- select :: SExpr -> SExpr -> SExpr
- store :: SExpr -> SExpr -> SExpr -> SExpr
Basic Solver Interface
An interactive solver process.
Start a new solver process.
simpleCommand :: Solver -> [String] -> IO () Source #
A command entirely made out of atoms, with no interesting result.
simpleCommandMaybe :: Solver -> [String] -> IO Bool Source #
Run a command and return True if successful, and False if unsupported. This is useful for setting options that unsupported by some solvers, but used by others.
S-Expressions
S-expressions. These are the basic format for SmtLib-2.
showsSExpr :: SExpr -> ShowS Source #
Show an s-expression.
Logging and Debugging
Log messages with minimal formatting. Mostly for debugging.
newLogger :: Int -> IO Logger Source #
A simple stdout logger. Shows only messages logged at a level that is greater than or equal to the passed level.
withLogLevel :: Logger -> Int -> IO a -> IO a Source #
Run an IO action with the logger set to a specific level, restoring it when done.
Common SmtLib-2 Commands
setLogic :: Solver -> String -> IO () Source #
Set the solver's logic. Usually, this should be done first.
setLogicMaybe :: Solver -> String -> IO Bool Source #
Set the solver's logic, returning False if the logic is unsupported.
setOptionMaybe :: Solver -> String -> String -> IO Bool Source #
Set a solver option, returning False if the option is unsupported.
inNewScope :: Solver -> IO a -> IO a Source #
Execute the IO action in a new solver scope (push before, pop after)
declare :: Solver -> String -> SExpr -> IO SExpr Source #
Declare a constant. A common abbreviation for declareFun.
For convenience, returns an the declared name as a constant expression.
declareFun :: Solver -> String -> [SExpr] -> SExpr -> IO SExpr Source #
Declare a function or a constant. For convenience, returns an the declared name as a constant expression.
Arguments
| :: Solver | |
| -> String | datatype name |
| -> [String] | sort parameters |
| -> [(String, [(String, SExpr)])] | constructors |
| -> IO () |
Declare an ADT using the format introduced in SmtLib 2.6.
Declare a constant. A common abbreviation for declareFun.
For convenience, returns the defined name as a constant expression.
Arguments
| :: Solver | |
| -> String | New symbol |
| -> [(String, SExpr)] | Parameters, with types |
| -> SExpr | Type of result |
| -> SExpr | Definition |
| -> IO SExpr |
Define a function or a constant. For convenience, returns an the defined name as a constant expression.
Results of checking for satisfiability.
getExprs :: Solver -> [SExpr] -> IO [(SExpr, Value)] Source #
Get the values of some s-expressions.
Only valid after a Sat result.
Common values returned by SMT solvers.
Convenience Functions for SmtLib-2 Epxressions
fam :: String -> [Integer] -> SExpr Source #
A constant, corresponding to a family indexed by some integers.
Types
The type of arrays.
Literals
A bit vector represented in binary.
- If the value does not fit in the bits, then the bits will be increased.
- The width should be strictly positive.
A bit vector represented in hex.
- If the value does not fit in the bits, the bits will be increased to the next multiple of 4 that will fit the value.
- If the width is not a multiple of 4, it will be rounded up so that it is.
- The width should be strictly positive.
value :: Value -> SExpr Source #
Render a value as an expression. Bit-vectors are rendered in hex, if their width is a multiple of 4, and in binary otherwise.
Connectives
If-then-else
ite :: SExpr -> SExpr -> SExpr -> SExpr Source #
If-then-else. This is polymorphic and can be used to construct any term.
Relational Predicates
Arithmetic
Bit Vectors
Arithemti shift right (copies most significant bit).
zeroExtend :: Integer -> SExpr -> SExpr Source #
Extend with zeros to the unsigned equivalent bitvector
by i bits