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

data SExpr #

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

Constructors

Atom String
List [SExpr]

Instances

Eq SExpr #
Methods (==) :: SExpr -> SExpr -> Bool # (/=) :: SExpr -> SExpr -> Bool #
Ord SExpr #
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 #
Methods showsPrec :: Int -> SExpr -> ShowS # show :: SExpr -> String # showList :: [SExpr] -> ShowS #

showsSExpr :: SExpr -> ShowS #

Show an s-expression.

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

Parse an s-expression.

Logging and Debugging

data Logger #

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 #

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 #

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

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

Log a message at a specific log level.

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

Common SmtLib-2 Commands

setLogic :: Solver -> String -> IO () #

Set the solver's logic. Usually, this should be done first.

setLogicMaybe :: Solver -> String -> IO Bool #

Set the solver's logic, returning False if the logic is unsupported.

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

Set a solver option.

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

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

push :: Solver -> IO () #

Checkpoint state. A special case of pushMany.

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

Push multiple scopes.

pop :: Solver -> IO () #

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

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

Pop multiple scopes.

declare :: Solver -> String -> SExpr -> IO SExpr #

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 #

Declare a function or a constant. For convenience, returns an the declared name as a constant expression.

define #

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 #

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.

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

Assume a fact.

check :: Solver -> IO Result #

Check if the current set of assertion is consistent.

data Result #

Results of checking for satisfiability.

Constructors

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

Instances

Eq Result #
Methods (==) :: Result -> Result -> Bool # (/=) :: Result -> Result -> Bool #
Show Result #
Methods showsPrec :: Int -> Result -> ShowS # show :: Result -> String # showList :: [Result] -> ShowS #

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

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

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

Get the value of a single expression.

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

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 #

Get the value of a single constant.

data Value #

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

Eq Value #
Methods (==) :: Value -> Value -> Bool # (/=) :: Value -> Value -> Bool #
Show Value #
Methods showsPrec :: Int -> Value -> ShowS # show :: Value -> String # showList :: [Value] -> ShowS #

Convenienct Functoins for SmtLib-2 Epxressions

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

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

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

An SMT function.

const :: String -> SExpr #

An SMT constant. A special case of fun.

Types

tInt :: SExpr #

The type of integers.

tBool :: SExpr #

The type of booleans.

tReal :: SExpr #

The type of reals.

tArray #

Arguments

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

The type of arrays.

tBits #

Arguments

:: Integer	Number of bits
-> SExpr

The type of bit vectors.

Literals

int :: Integer -> SExpr #

Integer literals.

real :: Rational -> SExpr #

Real (well, reational) literals.

bool :: Bool -> SExpr #

Boolean literals.

bvBin #

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 #

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 #

Render a value as an expression. Bit-vectors are rendered in hex, if their width is a multiple of 4, and in binary otherwise.