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

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
  - Types
  - Literals
  - Connectives
  - If-then-else
  - Relational Predicates
  - Arithmetic
  - Bit Vectors
  - Arrays

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

Show SExpr Source # |
Instance details Defined in SimpleSMT Methods showsPrec :: Int -> SExpr -> ShowS Source # show :: SExpr -> String Source # showList :: [SExpr] -> ShowS Source #
Eq SExpr Source # |
Instance details Defined in SimpleSMT Methods (==) :: SExpr -> SExpr -> Bool Source # (/=) :: SExpr -> SExpr -> Bool Source #
Ord SExpr Source # |
Instance details Defined in SimpleSMT Methods compare :: SExpr -> SExpr -> Ordering Source # (<) :: SExpr -> SExpr -> Bool Source # (<=) :: SExpr -> SExpr -> Bool Source # (>) :: SExpr -> SExpr -> Bool Source # (>=) :: SExpr -> SExpr -> Bool Source # max :: SExpr -> SExpr -> SExpr Source # min :: SExpr -> SExpr -> SExpr Source #

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

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

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

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

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.

## Connectives

not :: SExpr -> SExpr Source #

Logical negation.

and :: SExpr -> SExpr -> SExpr Source #

Conjunction.

andMany :: [SExpr] -> SExpr Source #

or :: SExpr -> SExpr -> SExpr Source #

Disjunction.

orMany :: [SExpr] -> SExpr Source #

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.

distinct :: [SExpr] -> SExpr Source #

gt :: SExpr -> SExpr -> SExpr Source #

Greater-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`

addMany :: [SExpr] -> SExpr Source #

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

realDiv :: SExpr -> SExpr -> SExpr Source #

Division of real numbers.

toInt :: SExpr -> SExpr Source #

Satisfies `toInt x <= x` (i.e., this is like Haskell's `floor`)

toReal :: SExpr -> SExpr Source #

Promote an integer to a real

## 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 #

Bitwise exclusive or.

bvOr :: SExpr -> SExpr -> SExpr Source #

Bitwise disjunction.

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