Safe Haskell	Safe
Language	Haskell2010

SimpleSMT

Contents

Basic Solver Interface
- S-Expressions
- Logging and Debugging
Common SmtLib-2 Commands
Convenience Functions for SmtLib-2 Expressions
Convenience Functions for SmtLib-2 identifiers

Description

A module for interacting with an SMT solver, using SmtLib-2 format.

Synopsis

data Solver = Solver {
- command :: SExpr -> IO SExpr
- stop :: IO ExitCode
- forceStop :: IO ExitCode
}
newSolver :: String -> [String] -> Maybe Logger -> IO Solver
newSolverNotify :: String -> [String] -> Maybe Logger -> Maybe (ExitCode -> IO ()) -> IO Solver
newSolverWithConfig :: Config -> IO Solver
data Config = Config {
- solverExecutable :: String
- solverArguments :: [String]
- solverOnExit :: Maybe (ExitCode -> IO ())
- solverLogger :: SolverLogger
}
data SolverLogger = SolverLogger {
- solverLogSend :: SExpr -> IO ()
- solverLogRecv :: SExpr -> IO ()
- solverLogExcn :: IOException -> IO ()
- solverLogStdErr :: String -> IO ()
}
defaultConfig :: String -> [String] -> Config
noSolverLogger :: SolverLogger
heraldSolverLogger :: Logger -> SolverLogger
smtSolverLogger :: Logger -> SolverLogger
ackCommand :: Solver -> SExpr -> IO ()
simpleCommand :: Solver -> [String] -> IO ()
simpleCommandMaybe :: Solver -> [String] -> IO Bool
loadFile :: Solver -> FilePath -> IO ()
loadString :: Solver -> String -> IO ()
data SExpr
- = Atom String
- | List [SExpr]
showsSExpr :: SExpr -> ShowS
ppSExpr :: SExpr -> ShowS
readSExpr :: String -> Maybe (SExpr, String)
data Logger = Logger {
- logMessage :: String -> IO ()
- logLevel :: IO Int
- logSetLevel :: Int -> IO ()
- logTab :: IO ()
- logUntab :: IO ()
}
newLogger :: Int -> IO Logger
newLoggerWithHandle :: Handle -> 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
produceUnsatCores :: Solver -> IO Bool
named :: String -> SExpr -> SExpr
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
defineFunRec :: Solver -> String -> [(String, SExpr)] -> SExpr -> (SExpr -> SExpr) -> IO SExpr
defineFunsRec :: Solver -> [(String, [(String, SExpr)], SExpr, SExpr)] -> IO ()
assert :: Solver -> SExpr -> IO ()
check :: Solver -> IO Result
data Result
- = Sat
- | Unsat
- | Unknown
getExprs :: Solver -> [SExpr] -> IO [(SExpr, Value)]
getExpr :: Solver -> SExpr -> IO Value
getConsts :: Solver -> [String] -> IO [(String, Value)]
getConst :: Solver -> String -> IO Value
getUnsatCore :: Solver -> IO [String]
data Value
- = Bool !Bool
- | Int !Integer
- | Real !Rational
- | Bits !Int !Integer
- | Other !SExpr
sexprToVal :: SExpr -> Value
fam :: String -> [Integer] -> SExpr
fun :: String -> [SExpr] -> SExpr
const :: String -> SExpr
app :: SExpr -> [SExpr] -> SExpr
quoteSymbol :: String -> String
symbol :: String -> SExpr
keyword :: String -> SExpr
as :: SExpr -> SExpr -> 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
toInt :: SExpr -> SExpr
toReal :: 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

data Solver Source #

An interactive solver process.

Constructors

Solver
Fields command :: SExpr -> IO SExpr Send a command to the solver. stop :: IO ExitCode Wait for the solver to finish and exit gracefully. forceStop :: IO ExitCode Terminate the solver without waiting for it to finish.

newSolver Source #

Arguments

:: String	Executable
-> [String]	Arguments
-> Maybe Logger	Optional logging here
-> IO Solver

Start a new solver process.

newSolverNotify Source #

Arguments

:: String	Executable
-> [String]	Arguments
-> Maybe Logger	Optional logging here
-> Maybe (ExitCode -> IO ())	Do this when the solver exits
-> IO Solver

newSolverWithConfig :: Config -> IO Solver Source #

Start a new solver process using the provided Config options.

data Config Source #

Options for configuring how to start, stop, and interact with an SMT solver process.

Constructors

Config
Fields solverExecutable :: String The SMT solver executable. solverArguments :: [String] The command-line arguments to pass to the SMT solver. solverOnExit :: Maybe (ExitCode -> IO ()) Do this when the SMT solver exits. solverLogger :: SolverLogger How to log solver-related messages.

data SolverLogger Source #

Options for logging SMT solver–related messages.

Constructors

SolverLogger
Fields solverLogSend :: SExpr -> IO () Log an SMT query (`SExpr`) being sent to the SMT solver. solverLogRecv :: SExpr -> IO () Log a response (`SExpr`) being received from the SMT solver. solverLogExcn :: IOException -> IO () Log the SMT solver throwing an `IOException`. solverLogStdErr :: String -> IO () Log the SMT solver displaying an error to `stderr`.

defaultConfig Source #

Arguments

:: String	Solver executable
-> [String]	Solver arguments
-> Config

A reasonable default Config value.

noSolverLogger :: SolverLogger Source #

A trivial SolverLogger that does not perform any logging.

heraldSolverLogger :: Logger -> SolverLogger Source #

A basic SolverLogger that prints out heralds in front of sent and received SMT queries, as well as messages to stderr. This is the approach that newSolver and newSolverNotify use for logging.

smtSolverLogger :: Logger -> SolverLogger Source #

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.

ackCommand :: Solver -> SExpr -> IO () Source #

A command with no interesting result.

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.

loadFile :: Solver -> FilePath -> IO () Source #

Load the contents of a file.

loadString :: Solver -> String -> IO () Source #

Load a raw SMT string.

S-Expressions

data SExpr Source #

S-expressions. These are the basic format for SmtLib-2.

Constructors

Atom String
List [SExpr]

Instances

Instances details

Show SExpr Source #
Instance details Defined in SimpleSMT Methods showsPrec :: Int -> SExpr -> ShowS # show :: SExpr -> String # showList :: [SExpr] -> ShowS #
Eq SExpr Source #
Instance details Defined in SimpleSMT Methods (==) :: SExpr -> SExpr -> Bool # (/=) :: SExpr -> SExpr -> Bool #
Ord SExpr Source #
Instance details Defined in SimpleSMT Methods compare :: SExpr -> SExpr -> Ordering # (<) :: SExpr -> SExpr -> Bool # (<=) :: SExpr -> SExpr -> Bool # (>) :: SExpr -> SExpr -> Bool # (>=) :: SExpr -> SExpr -> Bool # max :: SExpr -> SExpr -> SExpr # min :: SExpr -> SExpr -> SExpr #

showsSExpr :: SExpr -> ShowS Source #

Show an s-expression.

>>> let Just (e, _) = readSExpr "(assert (= ((_ map (- (Int Int) Int)) a1Cl a1Cm) a1Cv))"
>>> putStrLn $ showsSExpr e ""
(assert (= ((_ map (- (Int Int) Int)) a1Cl a1Cm) a1Cv))

ppSExpr :: SExpr -> ShowS Source #

Show an s-expression in a somewhat readable fashion.

>>> let Just (e, _) = readSExpr "(assert (= ((_ map (- (Int Int) Int)) a1Cl a1Cm) a1Cv))"
>>> putStrLn $ ppSExpr e ""
(assert
   (=
      (
        (_
           map
           (-
              (Int Int)
              Int))
        a1Cl
        a1Cm)
      a1Cv))

readSExpr :: String -> Maybe (SExpr, String) Source #

Parse an s-expression.

>>> readSExpr "(_ map (- (Int Int) Int)) a1Cl a1Cm)"
Just (List [Atom "_",Atom "map",List [Atom "-",List [Atom "Int",Atom "Int"],Atom "Int"]]," a1Cl a1Cm)")

Logging and Debugging

data Logger Source #

Log messages with minimal formatting. Mostly for debugging.

Constructors

Logger
Fields logMessage :: String -> IO () Log a message. logLevel :: IO Int logSetLevel :: Int -> IO () logTab :: IO () Increase indentation. logUntab :: IO () Decrease indentation.

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.

newLoggerWithHandle :: Handle -> Int -> IO Logger Source #

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.

withLogLevel :: Logger -> Int -> IO a -> IO a Source #

Run an IO action with the logger set to a specific level, restoring it when done.

logMessageAt :: Logger -> Int -> String -> IO () Source #

Log a message at a specific log level.

logIndented :: Logger -> IO a -> IO a Source #

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.

setOption :: Solver -> String -> String -> IO () Source #

Set a solver option.

setOptionMaybe :: Solver -> String -> String -> IO Bool Source #

Set a solver option, returning False if the option is unsupported.

produceUnsatCores :: Solver -> IO Bool Source #

Request unsat cores. Returns if the solver supports them.

named :: String -> SExpr -> SExpr Source #

push :: Solver -> IO () Source #

Checkpoint state. A special case of pushMany.

pushMany :: Solver -> Integer -> IO () Source #

Push multiple scopes.

pop :: Solver -> IO () Source #

Restore to last check-point. A special case of popMany.

popMany :: Solver -> Integer -> IO () Source #

Pop multiple scopes.

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.

declareDatatype Source #

Arguments

:: Solver
-> String	datatype name
-> [String]	sort parameters
-> [(String, [(String, SExpr)])]	constructors
-> IO ()

Declare an ADT using the format introduced in SmtLib 2.6.

define Source #

Arguments

:: Solver
-> String	New symbol
-> SExpr	Symbol type
-> SExpr	Symbol definition
-> IO SExpr

Declare a constant. A common abbreviation for declareFun. For convenience, returns the defined name as a constant expression.

defineFun Source #

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.

defineFunRec Source #

Arguments

:: Solver
-> String	New symbol
-> [(String, SExpr)]	Parameters, with types
-> SExpr	Type of result
-> (SExpr -> SExpr)	Definition
-> IO SExpr

Define a recursive function or a constant. For convenience, returns an the defined name as a constant expression. This body takes the function name as an argument.

defineFunsRec :: Solver -> [(String, [(String, SExpr)], SExpr, SExpr)] -> IO () Source #

Define a recursive function or a constant. For convenience, returns an the defined name as a constant expression. This body takes the function name as an argument.

assert :: Solver -> SExpr -> IO () Source #

Assume a fact.

check :: Solver -> IO Result Source #

Check if the current set of assertion is consistent.

data Result Source #

Results of checking for satisfiability.

Constructors

Sat	The assertions are satisfiable
Unsat	The assertions are unsatisfiable
Unknown	The result is inconclusive

Instances

Instances details

Show Result Source #
Instance details Defined in SimpleSMT Methods showsPrec :: Int -> Result -> ShowS # show :: Result -> String # showList :: [Result] -> ShowS #
Eq Result Source #
Instance details Defined in SimpleSMT Methods (==) :: Result -> Result -> Bool # (/=) :: Result -> Result -> Bool #

getExprs :: Solver -> [SExpr] -> IO [(SExpr, Value)] Source #

Get the values of some s-expressions. Only valid after a Sat result.

getExpr :: Solver -> SExpr -> IO Value Source #

Get the value of a single expression.

getConsts :: Solver -> [String] -> IO [(String, Value)] Source #

Get the values of some constants in the current model. A special case of getExprs. Only valid after a Sat result.

getConst :: Solver -> String -> IO Value Source #

Get the value of a single constant.

getUnsatCore :: Solver -> IO [String] Source #

Returns the names of the (named) formulas involved in a contradiction.

data Value Source #

Common values returned by SMT solvers.

Constructors

Bool !Bool	Boolean value
Int !Integer	Integral value
Real !Rational	Rational value
Bits !Int !Integer	Bit vector: width, value
Other !SExpr	Some other value

Instances

Instances details

Show Value Source #
Instance details Defined in SimpleSMT Methods showsPrec :: Int -> Value -> ShowS # show :: Value -> String # showList :: [Value] -> ShowS #
Eq Value Source #
Instance details Defined in SimpleSMT Methods (==) :: Value -> Value -> Bool # (/=) :: Value -> Value -> Bool #

sexprToVal :: SExpr -> Value Source #

Convert an s-expression to a value.

Convenience Functions for SmtLib-2 Expressions

fam :: String -> [Integer] -> SExpr Source #

A constant, corresponding to a family indexed by some integers.

fun :: String -> [SExpr] -> SExpr Source #

An SMT function.

const :: String -> SExpr Source #

An SMT constant. A special case of fun.

app :: SExpr -> [SExpr] -> SExpr Source #

Convenience Functions for SmtLib-2 identifiers

quoteSymbol :: String -> String Source #

symbol :: String -> SExpr Source #

keyword :: String -> SExpr Source #

as :: SExpr -> SExpr -> SExpr Source #

Generate a type annotation for a symbol

Types

tInt :: SExpr Source #

The type of integers.

tBool :: SExpr Source #

The type of booleans.

tReal :: SExpr Source #

The type of reals.

tArray Source #

Arguments

:: SExpr	Type of indexes
-> SExpr	Type of elements
-> SExpr

The type of arrays.

tBits Source #

Arguments

:: Integer	Number of bits
-> SExpr

The type of bit vectors.

Literals

int :: Integer -> SExpr Source #

Integer literals.

real :: Rational -> SExpr Source #

Real (well, rational) literals.

bool :: Bool -> SExpr Source #

Boolean literals.

bvBin Source #

Arguments

:: Int	Width, in bits
-> Integer	Value
-> SExpr

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.

bvHex Source #

Arguments

:: Int	Width, in bits
-> Integer	Value
-> SExpr

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.