simple-smt-0.5.0: A simple way to interact with an SMT solver process.

Safe HaskellSafe
LanguageHaskell2010

SimpleSMT

Contents

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

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.

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

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

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

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