SimpleSMT

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

Basic Solver Interface

data Solver

An interactive solver process.

newSolver

Arguments

:: String

Executable

-> [String]

Argumetns

-> Maybe Logger

Optional logging here

-> IO Solver

Start a new solver process.

command :: Solver -> SExpr -> IO SExpr

Send a command to the solver.

stop :: Solver -> IO ExitCode

Terminate the solver.

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

A command with no interesting result.

simpleCommand :: Solver -> [String] -> IO ()

A command entirely made out of atoms, with no interesting result.

simpleCommandMaybe :: Solver -> [String] -> IO Bool

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.

Connectives

not :: SExpr -> SExpr

Logical negation.

and :: SExpr -> SExpr -> SExpr

Conjucntion.

or :: SExpr -> SExpr -> SExpr

Disjunction.

xor :: SExpr -> SExpr -> SExpr

Exclusive-or.

implies :: SExpr -> SExpr -> SExpr

Implication.

If-then-else

ite :: SExpr -> SExpr -> SExpr -> SExpr

If-then-else. This is polymorphic and can be used to construct any term.

Relational Predicates

eq :: SExpr -> SExpr -> SExpr

Equality.

gt :: SExpr -> SExpr -> SExpr

Greather-then

lt :: SExpr -> SExpr -> SExpr

Less-then.

geq :: SExpr -> SExpr -> SExpr

Greater-than-or-equal-to.

leq :: SExpr -> SExpr -> SExpr

Less-than-or-equal-to.

bvULt :: SExpr -> SExpr -> SExpr

Unsigned less-than on bit-vectors.

bvULeq :: SExpr -> SExpr -> SExpr

Unsigned less-than-or-equal on bit-vectors.

bvSLt :: SExpr -> SExpr -> SExpr

Signed less-than on bit-vectors.

bvSLeq :: SExpr -> SExpr -> SExpr

Signed less-than-or-equal on bit-vectors.

Arithmetic

add :: SExpr -> SExpr -> SExpr

Addition. See also bvAdd

sub :: SExpr -> SExpr -> SExpr

Subtraction.

neg :: SExpr -> SExpr

Arithmetic negation for integers and reals. See also bvNeg.

mul :: SExpr -> SExpr -> SExpr

Multiplication.

abs :: SExpr -> SExpr

Absolute value.

div :: SExpr -> SExpr -> SExpr

Integer division.

mod :: SExpr -> SExpr -> SExpr

Modulus.

divisible :: SExpr -> Integer -> SExpr

Is the number divisible by the given constante.

realDiv :: SExpr -> SExpr -> SExpr

Division of real numbers.

Bit Vectors

concat :: SExpr -> SExpr -> SExpr

Bit vector concatenation.

extract :: SExpr -> Integer -> Integer -> SExpr

Extract a sub-sequence of a bit vector.

bvNot :: SExpr -> SExpr

Bitwise negation.

bvNeg :: SExpr -> SExpr

Bit vector arithmetic negation.

bvAnd :: SExpr -> SExpr -> SExpr

Bitwise conjuction.

bvXOr :: SExpr -> SExpr -> SExpr

Bitwsie exclusive or.

bvOr :: SExpr -> SExpr -> SExpr

Bitwsie disjucntion.

bvAdd :: SExpr -> SExpr -> SExpr

Addition of bit vectors.

bvSub :: SExpr -> SExpr -> SExpr

Subtraction of bit vectors.

bvMul :: SExpr -> SExpr -> SExpr

Multiplication of bit vectors.

bvUDiv :: SExpr -> SExpr -> SExpr

Bit vector unsigned division.

bvURem :: SExpr -> SExpr -> SExpr

Bit vector unsigned reminder.

bvSDiv :: SExpr -> SExpr -> SExpr

Bit vector signed division.

bvSRem :: SExpr -> SExpr -> SExpr

Bit vector signed reminder.

bvShl

Arguments

:: SExpr

value

-> SExpr

shift amount

-> SExpr

Shift left.

bvLShr

Arguments

:: SExpr

value

-> SExpr

shift amount

-> SExpr

Logical shift right.

bvAShr

Arguments

:: SExpr

value

-> SExpr

shift amount

-> SExpr

Arithemti shift right (copies most significant bit).

signExtend :: Integer -> SExpr -> SExpr

Extend to the signed equivalent bitvector by i bits

zeroExtend :: Integer -> SExpr -> SExpr

Extend with zeros to the unsigned equivalent bitvector by i bits

Arrays

select

Arguments

:: SExpr

array

-> SExpr

index

-> SExpr

Get an elemeent of an array.

store

Arguments

:: SExpr

array

-> SExpr

index

-> SExpr

new value

-> SExpr

Update an array