Safe Haskell	Safe
Language	Haskell2010

SimpleSMT

Contents

Basic Solver Interface
- S-Expressions
- Logging and Debugging
Common SmtLib-2 Commands
Convenienct Functoins for SmtLib-2 Epxressions

Description

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

Synopsis

Basic Solver Interface

data Solver Source

An interactive solver process.

newSolver Source

Arguments

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

Start a new solver process.

command :: Solver -> SExpr -> IO SExpr Source

Send a command to the solver.

stop :: Solver -> IO ExitCode Source

Terminate the 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.

S-Expressions

data SExpr Source

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

Constructors

Atom String
List [SExpr]

Instances

Eq SExpr
Ord SExpr
Show SExpr

showsSExpr :: SExpr -> ShowS Source

Show an s-expression.

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. logTab :: IO () Increase indentation. logUntab :: IO () Decrease indentation.

newLogger :: IO Logger Source

A simple stdout logger.

Common SmtLib-2 Commands

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

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

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

Set a solver option.

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 sepcial case of popMany.

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

Pop multiple scopes.

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.

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.

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

Eq Result
Show Result

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.

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

Eq Value
Show Value

Convenienct Functoins for SmtLib-2 Epxressions

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.

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, reational) 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.

Connectives

not :: SExpr -> SExpr Source

Logical negation.

and :: SExpr -> SExpr -> SExpr Source

Conjucntion.

or :: SExpr -> SExpr -> SExpr Source

Disjunction.

xor :: SExpr -> SExpr -> SExpr Source

Exclusive-or.

implies :: SExpr -> SExpr -> SExpr Source

Implication.

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

eq :: SExpr -> SExpr -> SExpr Source

Equality.

gt :: SExpr -> SExpr -> SExpr Source

Greather-then

lt :: SExpr -> SExpr -> SExpr Source

Less-then.

geq :: SExpr -> SExpr -> SExpr Source

Greater-than-or-equal-to.

leq :: SExpr -> SExpr -> SExpr Source

Less-than-or-equal-to.

bvULt :: SExpr -> SExpr -> SExpr Source

Unsigned less-than on bit-vectors.

bvULeq :: SExpr -> SExpr -> SExpr Source

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

bvSLt :: SExpr -> SExpr -> SExpr Source

Signed less-than on bit-vectors.

bvSLeq :: SExpr -> SExpr -> SExpr Source

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

Arithmetic

add :: SExpr -> SExpr -> SExpr Source

Addition. See also bvAdd

sub :: SExpr -> SExpr -> SExpr Source

Subtraction.

neg :: SExpr -> SExpr Source

Arithmetic negation for integers and reals. See also bvNeg.

mul :: SExpr -> SExpr -> SExpr Source

Multiplication.

abs :: SExpr -> SExpr Source

Absolute value.

div :: SExpr -> SExpr -> SExpr Source

Integer division.

mod :: SExpr -> SExpr -> SExpr Source

Modulus.

divisible :: SExpr -> Integer -> SExpr Source

Is the number divisible by the given constante.

realDiv :: SExpr -> SExpr -> SExpr Source

Division of real numbers.

Bit Vectors

concat :: SExpr -> SExpr -> SExpr Source

Bit vector concatenation.

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

Extract a sub-sequence of a bit vector.

bvNot :: SExpr -> SExpr Source

Bitwise negation.

bvNeg :: SExpr -> SExpr Source

Bit vector arithmetic negation.

bvAnd :: SExpr -> SExpr -> SExpr Source

Bitwise conjuction.

bvXOr :: SExpr -> SExpr -> SExpr Source

Bitwsie exclusive or.

bvOr :: SExpr -> SExpr -> SExpr Source

Bitwsie disjucntion.

bvAdd :: SExpr -> SExpr -> SExpr Source

Addition of bit vectors.

bvSub :: SExpr -> SExpr -> SExpr Source

Subtraction of bit vectors.

bvMul :: SExpr -> SExpr -> SExpr Source

Multiplication of bit vectors.

bvUDiv :: SExpr -> SExpr -> SExpr Source

Bit vector unsigned division.

bvURem :: SExpr -> SExpr -> SExpr Source

Bit vector unsigned reminder.

bvSDiv :: SExpr -> SExpr -> SExpr Source

Bit vector signed division.

bvSRem :: SExpr -> SExpr -> SExpr Source

Bit vector signed reminder.

bvShl Source

Arguments

:: SExpr	value
-> SExpr	shift amount
-> SExpr

Shift left.

bvLShr Source

Arguments

:: SExpr	value
-> SExpr	shift amount
-> SExpr

Logical shift right.

bvAShr Source

Arguments

:: SExpr	value
-> SExpr	shift amount
-> SExpr

Arithemti shift right (copies most significant bit).

signExtend :: Integer -> SExpr -> SExpr Source

Extend to the signed equivalent bitvector by i bits

zeroExtend :: Integer -> SExpr -> SExpr Source

Extend with zeros to the unsigned equivalent bitvector by i bits

Arrays

select Source

Arguments

:: SExpr	array
-> SExpr	index
-> SExpr

Get an elemeent of an array.

store Source

Arguments

:: SExpr	array
-> SExpr	index
-> SExpr	new value
-> SExpr

Update an array