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

SimpleSMT

Description

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

Synopsis

Basic Solver Interface

data Solver Source #

An interactive solver process.

Constructors

Solver 

Fields

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
Eq SExpr Source # 
Instance details

Defined in SimpleSMT

Methods

(==) :: SExpr -> SExpr -> Bool #

(/=) :: SExpr -> SExpr -> Bool #

Ord SExpr Source # 
Instance details

Defined in SimpleSMT

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 Source # 
Instance details

Defined in SimpleSMT

Methods

showsPrec :: Int -> SExpr -> ShowS #

show :: SExpr -> String #

showList :: [SExpr] -> ShowS #

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

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.

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.

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
Eq Result Source # 
Instance details

Defined in SimpleSMT

Methods

(==) :: Result -> Result -> Bool #

(/=) :: Result -> Result -> Bool #

Show Result Source # 
Instance details

Defined in SimpleSMT

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
Eq Value Source # 
Instance details

Defined in SimpleSMT

Methods

(==) :: Value -> Value -> Bool #

(/=) :: Value -> Value -> Bool #

Show Value Source # 
Instance details

Defined in SimpleSMT

Methods

showsPrec :: Int -> Value -> ShowS #

show :: Value -> String #

showList :: [Value] -> ShowS #

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.

Convenience Functions for SmtLib-2 identifiers

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.

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 #

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

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