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
}
newSolver :: String -> [String] -> Maybe Logger -> IO Solver
newSolverNotify :: String -> [String] -> Maybe Logger -> Maybe (ExitCode -> IO ()) -> IO Solver
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
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 Terminate the solver.

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

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

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 #
Show SExpr Source #
Instance details Defined in SimpleSMT Methods showsPrec :: Int -> SExpr -> ShowS # show :: SExpr -> String # showList :: [SExpr] -> ShowS #

showsSExpr :: SExpr -> ShowS Source #

Show an s-expression.

ppSExpr :: SExpr -> ShowS Source #

Show an S-expression in a somewhat readbale fashion.

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

Parse an s-expression.

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.

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

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

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

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

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.