Language.SMTLib2

Example usage: This program tries to find two numbers greater than zero which sum up to 5.

import Language.SMTLib2
import Language.SMTLib2.Solver

program :: SMT (Integer,Integer)
program = do
  x <- var
  y <- var
  assert $ (plus [x,y]) .==. (constant 5)
  assert $ x .>. (constant 0)
  assert $ y .>. (constant 0)
  checkSat
  vx <- getValue x
  vy <- getValue y
  return (vx,vy)

main = withZ3 program >>= print
     

Data types

data SMT' m a

The SMT monad used for communating with the SMT solver

Instances

MonadTrans SMT'

Methods

lift :: Monad m => m a -> SMT' m a

Monad m => Monad (SMT' m)

Methods

(>>=) :: SMT' m a -> (a -> SMT' m b) -> SMT' m b

(>>) :: SMT' m a -> SMT' m b -> SMT' m b

return :: a -> SMT' m a

fail :: String -> SMT' m a

Functor m => Functor (SMT' m)

Methods

fmap :: (a -> b) -> SMT' m a -> SMT' m b

(<$) :: a -> SMT' m b -> SMT' m a

MonadFix m => MonadFix (SMT' m)

Methods

mfix :: (a -> SMT' m a) -> SMT' m a

(Monad m, Functor m) => Applicative (SMT' m)

Methods

pure :: a -> SMT' m a

(<*>) :: SMT' m (a -> b) -> SMT' m a -> SMT' m b

(*>) :: SMT' m a -> SMT' m b -> SMT' m b

(<*) :: SMT' m a -> SMT' m b -> SMT' m a

MonadIO m => MonadIO (SMT' m)

Methods

liftIO :: IO a -> SMT' m a

type SMT = SMT' IO

class Monad m => SMTBackend a m

Minimal complete definition

smtHandle, smtGetNames, smtNextName

Instances

MonadIO m => SMTBackend SMTPipe m

Methods

smtHandle :: Typeable * response => SMTPipe -> SMTRequest response -> m (response, SMTPipe)

smtGetNames :: SMTPipe -> m (Integer -> String)

smtNextName :: SMTPipe -> m (Maybe String -> String)

Monad m => SMTBackend (AnyBackend m) m

Methods

smtHandle :: Typeable * response => AnyBackend m -> SMTRequest response -> m (response, AnyBackend m)

smtGetNames :: AnyBackend m -> m (Integer -> String)

smtNextName :: AnyBackend m -> m (Maybe String -> String)

data AnyBackend m

Constructors

SMTBackend b m => AnyBackend b

Instances

Monad m => SMTBackend (AnyBackend m) m

Methods

smtHandle :: Typeable * response => AnyBackend m -> SMTRequest response -> m (response, AnyBackend m)

smtGetNames :: AnyBackend m -> m (Integer -> String)

smtNextName :: AnyBackend m -> m (Maybe String -> String)

class (Ord t, Typeable t, Ord (SMTAnnotation t), Typeable (SMTAnnotation t), Show (SMTAnnotation t)) => SMTType t

Haskell types which can be represented in SMT

Minimal complete definition

getSort, asValueType, annotationFromSort, defaultExpr

Associated Types

type SMTAnnotation t

class (SMTType t, Show t) => SMTValue t

Haskell values which can be represented as SMT constants

Minimal complete definition

unmangle, mangle

class (SMTValue t, Num t, SMTAnnotation t ~ ()) => SMTArith t

A type class for all types which support arithmetic operations in SMT

class SMTType t => SMTOrd t where

Lifts the Ord class into SMT

Minimal complete definition

(.<.), (.>=.), (.>.), (.<=.)

Methods

(.<.) :: SMTExpr t -> SMTExpr t -> SMTExpr Bool infix 4

(.>=.) :: SMTExpr t -> SMTExpr t -> SMTExpr Bool infix 4

(.>.) :: SMTExpr t -> SMTExpr t -> SMTExpr Bool infix 4

(.<=.) :: SMTExpr t -> SMTExpr t -> SMTExpr Bool infix 4

data SMTExpr t

An abstract SMT expression

Instances

Show (SMTExpr t)

Methods

showsPrec :: Int -> SMTExpr t -> ShowS

show :: SMTExpr t -> String

showList :: [SMTExpr t] -> ShowS

type Unpacked (SMTExpr a)

type Unpacked (SMTExpr a) = a

type ArgAnnotation (SMTExpr a)

type ArgAnnotation (SMTExpr a) = SMTAnnotation a

type Lifted [SMTExpr a] i

type Lifted [SMTExpr a] i = [SMTExpr (SMTArray i a)]

type Lifted (SMTExpr a) i

type Lifted (SMTExpr a) i = SMTExpr (SMTArray i a)

data SMTFunction arg res

Instances

Show (SMTFunction arg res)

Methods

showsPrec :: Int -> SMTFunction arg res -> ShowS

show :: SMTFunction arg res -> String

showList :: [SMTFunction arg res] -> ShowS

data SMTOption

Options controling the behaviour of the SMT solver

Constructors

PrintSuccess Bool

Whether or not to print "success" after each operation

ProduceModels Bool

Produce a satisfying assignment after each successful checkSat

ProduceProofs Bool

Produce a proof of unsatisfiability after each failed checkSat

ProduceUnsatCores Bool

Enable the querying of unsatisfiable cores after a failed checkSat

ProduceInterpolants Bool

Enable the generation of craig interpolants

Instances

Eq SMTOption

Methods

(==) :: SMTOption -> SMTOption -> Bool

(/=) :: SMTOption -> SMTOption -> Bool

Ord SMTOption

Methods

compare :: SMTOption -> SMTOption -> Ordering

(<) :: SMTOption -> SMTOption -> Bool

(<=) :: SMTOption -> SMTOption -> Bool

(>) :: SMTOption -> SMTOption -> Bool

(>=) :: SMTOption -> SMTOption -> Bool

max :: SMTOption -> SMTOption -> SMTOption

min :: SMTOption -> SMTOption -> SMTOption

Show SMTOption

Methods

showsPrec :: Int -> SMTOption -> ShowS

show :: SMTOption -> String

showList :: [SMTOption] -> ShowS

data SMTArray i v

An array which maps indices of type i to elements of type v.

Instances

Eq (SMTArray i v)

Methods

(==) :: SMTArray i v -> SMTArray i v -> Bool

(/=) :: SMTArray i v -> SMTArray i v -> Bool

Ord (SMTArray i v)

Methods

compare :: SMTArray i v -> SMTArray i v -> Ordering

(<) :: SMTArray i v -> SMTArray i v -> Bool

(<=) :: SMTArray i v -> SMTArray i v -> Bool

(>) :: SMTArray i v -> SMTArray i v -> Bool

(>=) :: SMTArray i v -> SMTArray i v -> Bool

max :: SMTArray i v -> SMTArray i v -> SMTArray i v

min :: SMTArray i v -> SMTArray i v -> SMTArray i v

type SMTAnnotation (SMTArray idx val)

type SMTAnnotation (SMTArray idx val) = (ArgAnnotation idx, SMTAnnotation val)

data Constructor arg res

Represents a constructor of a datatype a Can be obtained by using the template haskell extension module

Instances

Show (Constructor arg res)

Methods

showsPrec :: Int -> Constructor arg res -> ShowS

show :: Constructor arg res -> String

showList :: [Constructor arg res] -> ShowS

data Field a f

Represents a field of the datatype a of the type f

Instances

Show (Field a f)

Methods

showsPrec :: Int -> Field a f -> ShowS

show :: Field a f -> String

showList :: [Field a f] -> ShowS

class (Ord a, Typeable a, Show a, Ord (ArgAnnotation a), Typeable (ArgAnnotation a), Show (ArgAnnotation a)) => Args a where

Instances of this class may be used as arguments for constructed functions and quantifiers.

Minimal complete definition

foldsExprs, extractArgAnnotation, toArgs, getTypes, getArgAnnotation

Associated Types

type ArgAnnotation a

Methods

foldExprs :: Monad m => (forall t. SMTType t => s -> SMTExpr t -> SMTAnnotation t -> m (s, SMTExpr t)) -> s -> a -> ArgAnnotation a -> m (s, a)

foldsExprs :: Monad m => (forall t. SMTType t => s -> [(SMTExpr t, b)] -> SMTAnnotation t -> m (s, [SMTExpr t], SMTExpr t)) -> s -> [(a, b)] -> ArgAnnotation a -> m (s, [a], a)

extractArgAnnotation :: a -> ArgAnnotation a

toArgs :: ArgAnnotation a -> [SMTExpr Untyped] -> Maybe (a, [SMTExpr Untyped])

fromArgs :: a -> [SMTExpr Untyped]

getTypes :: a -> ArgAnnotation a -> [ProxyArg]

getArgAnnotation :: a -> [Sort] -> (ArgAnnotation a, [Sort])

Instances

Args ()

Associated Types

type ArgAnnotation () :: *

Methods

foldExprs :: Monad m => (forall t. SMTType t => s -> SMTExpr t -> SMTAnnotation t -> m (s, SMTExpr t)) -> s -> () -> ArgAnnotation () -> m (s, ())

foldsExprs :: Monad m => (forall t. SMTType t => s -> [(SMTExpr t, b)] -> SMTAnnotation t -> m (s, [SMTExpr t], SMTExpr t)) -> s -> [((), b)] -> ArgAnnotation () -> m (s, [()], ())

extractArgAnnotation :: () -> ArgAnnotation ()

toArgs :: ArgAnnotation () -> [SMTExpr Untyped] -> Maybe ((), [SMTExpr Untyped])

fromArgs :: () -> [SMTExpr Untyped]

getTypes :: () -> ArgAnnotation () -> [ProxyArg]

getArgAnnotation :: () -> [Sort] -> (ArgAnnotation (), [Sort])

class Args a => LiftArgs a where

An extension of the Args class: Instances of this class can be represented as native haskell data types.

Minimal complete definition

liftArgs, unliftArgs

Associated Types

type Unpacked a

Methods

liftArgs :: Unpacked a -> ArgAnnotation a -> a

Converts a haskell value into its SMT representation.

unliftArgs :: Monad m => a -> (forall t. SMTValue t => SMTExpr t -> m t) -> m (Unpacked a)

Converts a SMT representation back into a haskell value.

Environment

withSMTBackend :: SMTBackend a m => a -> SMT' m b -> m b

withSMTBackendExitCleanly :: SMTBackend b IO => b -> SMT a -> IO a

setOption :: Monad m => SMTOption -> SMT' m ()

Set an option for the underlying SMT solver

getInfo :: (Monad m, Typeable i) => SMTInfo i -> SMT' m i

Get information about the underlying SMT solver

setLogic :: Monad m => String -> SMT' m ()

Sets the logic used for the following program (Not needed for many solvers).

data SMTInfo i where

Constructors

SMTSolverName :: SMTInfo String

SMTSolverVersion :: SMTInfo String

assert :: Monad m => SMTExpr Bool -> SMT' m ()

Asserts that a boolean expression is true

push :: Monad m => SMT' m ()

Push a new context on the stack

pop :: Monad m => SMT' m ()

Pop a new context from the stack

stack :: Monad m => SMT' m a -> SMT' m a

Perform a stacked operation, meaning that every assertion and declaration made in it will be undone after the operation.

checkSat :: Monad m => SMT' m Bool

Check if the model is satisfiable (e.g. if there is a value for each variable so that every assertion holds)

checkSat' :: Monad m => Maybe Tactic -> CheckSatLimits -> SMT' m CheckSatResult

Like checkSat, but gives you more options like choosing a tactic (Z3 only) or providing memory/time-limits

checkSatUsing :: Monad m => Tactic -> SMT' m Bool

Check if the model is satisfiable using a given tactic. (Works only with Z3)

apply :: Monad m => Tactic -> SMT' m [SMTExpr Bool]

Apply the given tactic to the current assertions. (Works only with Z3)

data CheckSatResult

The result of a check-sat query

Constructors

Sat

The formula is satisfiable

Unsat

The formula is unsatisfiable

Unknown

The solver cannot determine the satisfiability of a formula

Instances

Eq CheckSatResult

Methods

(==) :: CheckSatResult -> CheckSatResult -> Bool

(/=) :: CheckSatResult -> CheckSatResult -> Bool

Ord CheckSatResult

Methods

compare :: CheckSatResult -> CheckSatResult -> Ordering

(<) :: CheckSatResult -> CheckSatResult -> Bool

(<=) :: CheckSatResult -> CheckSatResult -> Bool

(>) :: CheckSatResult -> CheckSatResult -> Bool

(>=) :: CheckSatResult -> CheckSatResult -> Bool

max :: CheckSatResult -> CheckSatResult -> CheckSatResult

min :: CheckSatResult -> CheckSatResult -> CheckSatResult

Show CheckSatResult

Methods

showsPrec :: Int -> CheckSatResult -> ShowS

show :: CheckSatResult -> String

showList :: [CheckSatResult] -> ShowS

data CheckSatLimits

Describe limits on the ressources that an SMT-solver can use

Constructors

CheckSatLimits

Fields

• limitTime :: Maybe Integer

  A limit on the amount of time the solver can spend on the problem (in milliseconds)

• limitMemory :: Maybe Integer

  A limit on the amount of memory the solver can use (in megabytes)

Instances

Eq CheckSatLimits

Methods

(==) :: CheckSatLimits -> CheckSatLimits -> Bool

(/=) :: CheckSatLimits -> CheckSatLimits -> Bool

Ord CheckSatLimits

Methods

compare :: CheckSatLimits -> CheckSatLimits -> Ordering

(<) :: CheckSatLimits -> CheckSatLimits -> Bool

(<=) :: CheckSatLimits -> CheckSatLimits -> Bool

(>) :: CheckSatLimits -> CheckSatLimits -> Bool

(>=) :: CheckSatLimits -> CheckSatLimits -> Bool

max :: CheckSatLimits -> CheckSatLimits -> CheckSatLimits

min :: CheckSatLimits -> CheckSatLimits -> CheckSatLimits

Show CheckSatLimits

Methods

showsPrec :: Int -> CheckSatLimits -> ShowS

show :: CheckSatLimits -> String

showList :: [CheckSatLimits] -> ShowS

noLimits :: CheckSatLimits

getValue :: (SMTValue t, Monad m) => SMTExpr t -> SMT' m t

getValues :: (LiftArgs arg, Monad m) => arg -> SMT' m (Unpacked arg)

getModel :: Monad m => SMT' m SMTModel

Extract all assigned values of the model

comment :: Monad m => String -> SMT' m ()

Insert a comment into the SMTLib2 command stream. If you aren't looking at the command stream for debugging, this will do nothing.

getProof :: Monad m => SMT' m (SMTExpr Bool)

After an unsuccessful checkSat this method extracts a proof from the SMT solver that the instance is unsatisfiable.

simplify :: (SMTType t, Monad m) => SMTExpr t -> SMT' m (SMTExpr t)

Use the SMT solver to simplify a given expression. Currently only works with Z3.

Unsatisfiable Core

data ClauseId

Identifies a clause in an unsatisfiable core

Instances

Eq ClauseId

Methods

(==) :: ClauseId -> ClauseId -> Bool

(/=) :: ClauseId -> ClauseId -> Bool

Ord ClauseId

Methods

compare :: ClauseId -> ClauseId -> Ordering

(<) :: ClauseId -> ClauseId -> Bool

(<=) :: ClauseId -> ClauseId -> Bool

(>) :: ClauseId -> ClauseId -> Bool

(>=) :: ClauseId -> ClauseId -> Bool

max :: ClauseId -> ClauseId -> ClauseId

min :: ClauseId -> ClauseId -> ClauseId

Show ClauseId

Methods

showsPrec :: Int -> ClauseId -> ShowS

show :: ClauseId -> String

showList :: [ClauseId] -> ShowS

assertId :: Monad m => SMTExpr Bool -> SMT' m ClauseId

Assert a boolean expression and track it for an unsat core call later

getUnsatCore :: Monad m => SMT' m [ClauseId]

After an unsuccessful checkSat, return a list of clauses which make the instance unsatisfiable.

Interpolation

data InterpolationGroup

Instances

Eq InterpolationGroup

Methods

(==) :: InterpolationGroup -> InterpolationGroup -> Bool

(/=) :: InterpolationGroup -> InterpolationGroup -> Bool

Ord InterpolationGroup

Methods

compare :: InterpolationGroup -> InterpolationGroup -> Ordering

(<) :: InterpolationGroup -> InterpolationGroup -> Bool

(<=) :: InterpolationGroup -> InterpolationGroup -> Bool

(>) :: InterpolationGroup -> InterpolationGroup -> Bool

(>=) :: InterpolationGroup -> InterpolationGroup -> Bool

max :: InterpolationGroup -> InterpolationGroup -> InterpolationGroup

min :: InterpolationGroup -> InterpolationGroup -> InterpolationGroup

Show InterpolationGroup

Methods

showsPrec :: Int -> InterpolationGroup -> ShowS

show :: InterpolationGroup -> String

showList :: [InterpolationGroup] -> ShowS

interpolationGroup :: Monad m => SMT' m InterpolationGroup

Create a new interpolation group

assertInterp :: Monad m => SMTExpr Bool -> InterpolationGroup -> SMT' m ()

Assert a boolean expression to be true and assign it to an interpolation group

getInterpolant :: Monad m => [InterpolationGroup] -> SMT' m (SMTExpr Bool)

interpolate :: Monad m => [SMTExpr Bool] -> SMT' m [SMTExpr Bool]

Expressions

var :: (SMTType t, Typeable t, Unit (SMTAnnotation t), Monad m) => SMT' m (SMTExpr t)

Create a fresh new variable

varNamed :: (SMTType t, Typeable t, Unit (SMTAnnotation t), Monad m) => String -> SMT' m (SMTExpr t)

Create a new named variable

varNamedAnn :: (SMTType t, Typeable t, Monad m) => String -> SMTAnnotation t -> SMT' m (SMTExpr t)

Create a named and annotated variable.

varAnn :: (SMTType t, Typeable t, Monad m) => SMTAnnotation t -> SMT' m (SMTExpr t)

Create a annotated variable

argVars :: (Args a, Unit (ArgAnnotation a), Monad m) => SMT' m a

Like argVarsAnn, but can only be used for unit type annotations.

argVarsAnn :: (Args a, Monad m) => ArgAnnotation a -> SMT' m a

Like argVarsAnnNamed, but defaults the name to "var"

argVarsAnnNamed :: (Args a, Monad m) => String -> ArgAnnotation a -> SMT' m a

Create annotated named SMT variables of the Args class. If more than one variable is needed, they get a numerical suffix.

untypedVar :: Monad m => Sort -> SMT' m (SMTExpr Untyped)

Create a fresh untyped variable

untypedNamedVar :: Monad m => String -> Sort -> SMT' m (SMTExpr Untyped)

Create a fresh untyped variable with a name

constant :: (SMTValue t, Unit (SMTAnnotation t)) => t -> SMTExpr t

A constant expression.

constantAnn :: SMTValue t => t -> SMTAnnotation t -> SMTExpr t

An annotated constant expression.

extractAnnotation :: SMTExpr a -> SMTAnnotation a

Reconstruct the type annotation for a given SMT expression.

let' :: (Args a, Unit (ArgAnnotation a), SMTType b) => a -> (a -> SMTExpr b) -> SMTExpr b

Binds an expression to a variable. Can be used to prevent blowups in the command stream if expressions are used multiple times. let' x f is functionally equivalent to f x.

lets :: (Args a, Unit (ArgAnnotation a), SMTType b) => [a] -> ([a] -> SMTExpr b) -> SMTExpr b

Like let', but can define multiple variables of the same type.

letAnn :: (Args a, SMTType b) => ArgAnnotation a -> a -> (a -> SMTExpr b) -> SMTExpr b

Like let', but can be given an additional type annotation for the argument of the function.

named :: (SMTType a, SMTAnnotation a ~ (), Monad m) => String -> SMTExpr a -> SMT' m (SMTExpr a, SMTExpr a)

Given an arbitrary expression, this creates a named version of it and a name to reference it later on.

named' :: (SMTType a, SMTAnnotation a ~ (), Monad m) => SMTExpr a -> SMT' m (SMTExpr a, SMTExpr a)

Like named, but defaults the name to "named".

optimizeExpr :: SMTExpr t -> Maybe (SMTExpr t)

optimizeExpr' :: SMTExpr a -> SMTExpr a

foldExpr :: SMTType a => (forall t. SMTType t => s -> SMTExpr t -> (s, SMTExpr t)) -> s -> SMTExpr a -> (s, SMTExpr a)

Recursively fold a function over all sub-expressions of this expression. It is implemented as a special case of foldExprM.

foldExprM :: (SMTType a, Monad m) => (forall t. SMTType t => s -> SMTExpr t -> m (s, [SMTExpr t])) -> s -> SMTExpr a -> m (s, [SMTExpr a])

Recursively fold a monadic function over all sub-expressions of this expression

foldArgs :: Args a => (forall t. SMTType t => s -> SMTExpr t -> (s, SMTExpr t)) -> s -> a -> (s, a)

Recursively fold a function over all sub-expressions of the argument. It is implemented as a special case of foldArgsM.

foldArgsM :: (Args a, Monad m) => (forall t. SMTType t => s -> SMTExpr t -> m (s, [SMTExpr t])) -> s -> a -> m (s, [a])

Recursively fold a monadic function over all sub-expressions of the argument

Basic logic

(.==.) :: SMTType a => SMTExpr a -> SMTExpr a -> SMTExpr Bool infix 4

Two expressions shall be equal

argEq :: Args a => a -> a -> SMTExpr Bool

A generalized version of .==.

distinct :: SMTType a => [SMTExpr a] -> SMTExpr Bool

Declares all arguments to be distinct

ite

Arguments

:: SMTType a

=> SMTExpr Bool

If this expression is true

-> SMTExpr a

Then return this expression

-> SMTExpr a

Else this one

-> SMTExpr a

If-then-else construct

(.&&.) :: SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool

(.||.) :: SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool

and' :: SMTFunction [SMTExpr Bool] Bool

Boolean conjunction

or' :: SMTFunction [SMTExpr Bool] Bool

Boolean disjunction

xor :: SMTFunction [SMTExpr Bool] Bool

Exclusive or: Return true if exactly one argument is true.

not' :: SMTExpr Bool -> SMTExpr Bool

Negates a boolean expression

not'' :: SMTFunction (SMTExpr Bool) Bool

(.=>.)

Arguments

:: SMTExpr Bool

If this expression is true

-> SMTExpr Bool

This one must be as well

-> SMTExpr Bool

Implication

forAll :: (Args a, Unit (ArgAnnotation a)) => (a -> SMTExpr Bool) -> SMTExpr Bool

If the supplied function returns true for all possible values, the forall quantification returns true.

exists :: (Args a, Unit (ArgAnnotation a)) => (a -> SMTExpr Bool) -> SMTExpr Bool

If the supplied function returns true for at least one possible value, the exists quantification returns true.

forAllAnn :: Args a => ArgAnnotation a -> (a -> SMTExpr Bool) -> SMTExpr Bool

An annotated version of forAll.

existsAnn :: Args a => ArgAnnotation a -> (a -> SMTExpr Bool) -> SMTExpr Bool

An annotated version of exists.

forAllList

Arguments

:: (Args a, Unit (ArgAnnotation a))

=> Integer

Number of variables to quantify

-> ([a] -> SMTExpr Bool)

Function which takes a list of the quantified variables

-> SMTExpr Bool

Like forAll, but can quantify over more than one variable (of the same type).

existsList

Arguments

:: (Args a, Unit (ArgAnnotation a))

=> Integer

Number of variables to quantify

-> ([a] -> SMTExpr Bool)

Function which takes a list of the quantified variables

-> SMTExpr Bool

Like exists, but can quantify over more than one variable (of the same type).

Arithmetic

plus :: SMTArith a => SMTFunction [SMTExpr a] a

Calculate the sum of arithmetic expressions

minus :: SMTArith a => SMTFunction (SMTExpr a, SMTExpr a) a

Subtracts two expressions

mult :: SMTArith a => SMTFunction [SMTExpr a] a

Calculate the product of arithmetic expressions

div' :: SMTExpr Integer -> SMTExpr Integer -> SMTExpr Integer

Divide an arithmetic expression by another

mod' :: SMTExpr Integer -> SMTExpr Integer -> SMTExpr Integer

Perform a modulo operation on an arithmetic expression

rem' :: SMTExpr Integer -> SMTExpr Integer -> SMTExpr Integer

Calculate the remainder of the division of two integer expressions

neg :: SMTArith a => SMTFunction (SMTExpr a) a

For an expression x, this returns the expression -x.

divide :: SMTExpr Rational -> SMTExpr Rational -> SMTExpr Rational

Divide a rational expression by another one

toReal :: SMTExpr Integer -> SMTExpr Rational

Convert an integer expression to a real expression

toInt :: SMTExpr Rational -> SMTExpr Integer

Convert a real expression into an integer expression

Arrays

select :: (Liftable i, SMTType v) => SMTExpr (SMTArray i v) -> i -> SMTExpr v

Extracts an element of an array by its index

store :: (Liftable i, SMTType v) => SMTExpr (SMTArray i v) -> i -> SMTExpr v -> SMTExpr (SMTArray i v)

The expression store arr i v stores the value v in the array arr at position i and returns the resulting new array.

arrayEquals :: (LiftArgs i, Liftable i, SMTValue v, Ix (Unpacked i), Unit (ArgAnnotation i), Unit (SMTAnnotation v)) => SMTExpr (SMTArray i v) -> Array (Unpacked i) v -> SMTExpr Bool

Create a boolean expression that encodes that the array is equal to the supplied constant array.

unmangleArray :: (Liftable i, LiftArgs i, Ix (Unpacked i), SMTValue v, Unit (ArgAnnotation i), Monad m) => (Unpacked i, Unpacked i) -> SMTExpr (SMTArray i v) -> SMT' m (Array (Unpacked i) v)

Extract all values of an array by giving the range of indices.

asArray :: (Args arg, Unit (ArgAnnotation arg), SMTType res) => SMTFunction arg res -> SMTExpr (SMTArray arg res)

Interpret a function f from i to v as an array with indices i and elements v. Such that: f `app` j .==. select (asArray f) j for all indices j.

constArray

Arguments

:: (Args i, SMTType v)

=> SMTExpr v

This element will be at every index of the array

-> ArgAnnotation i

Annotations of the index type

-> SMTExpr (SMTArray i v)

Create an array where each element is the same.

Bitvectors

bvand :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector and

bvor :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector or

bvxor :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector or

bvnot :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector not

bvneg :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector signed negation

bvadd :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector addition

bvsub :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector subtraction

bvmul :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector multiplication

bvurem :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector unsigned remainder

bvsrem :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector signed remainder

bvudiv :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector unsigned division

bvsdiv :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector signed division

bvule :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

Bitvector unsigned less-or-equal

bvult :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

Bitvector unsigned less-than

bvuge :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

Bitvector unsigned greater-or-equal

bvugt :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

Bitvector unsigned greater-than

bvsle :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

Bitvector signed less-or-equal

bvslt :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

Bitvector signed less-than

bvsge :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

Bitvector signed greater-or-equal

bvsgt :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

Bitvector signed greater-than

bvshl :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector shift left

bvlshr :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector logical right shift

bvashr :: IsBitVector t => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

Bitvector arithmetical right shift

data BitVector b

Constructors

BitVector Integer

Instances

Enum (BitVector a)

Methods

succ :: BitVector a -> BitVector a

pred :: BitVector a -> BitVector a

toEnum :: Int -> BitVector a

fromEnum :: BitVector a -> Int

enumFrom :: BitVector a -> [BitVector a]

enumFromThen :: BitVector a -> BitVector a -> [BitVector a]

enumFromTo :: BitVector a -> BitVector a -> [BitVector a]

enumFromThenTo :: BitVector a -> BitVector a -> BitVector a -> [BitVector a]

Eq (BitVector b)

Methods

(==) :: BitVector b -> BitVector b -> Bool

(/=) :: BitVector b -> BitVector b -> Bool

Ord (BitVector b)

Methods

compare :: BitVector b -> BitVector b -> Ordering

(<) :: BitVector b -> BitVector b -> Bool

(<=) :: BitVector b -> BitVector b -> Bool

(>) :: BitVector b -> BitVector b -> Bool

(>=) :: BitVector b -> BitVector b -> Bool

max :: BitVector b -> BitVector b -> BitVector b

min :: BitVector b -> BitVector b -> BitVector b

Show (BitVector a)

Methods

showsPrec :: Int -> BitVector a -> ShowS

show :: BitVector a -> String

showList :: [BitVector a] -> ShowS

type SMTAnnotation (BitVector (BVTyped n))

type SMTAnnotation (BitVector (BVTyped n)) = ()

type SMTAnnotation (BitVector BVUntyped)

type SMTAnnotation (BitVector BVUntyped) = Integer

data BVTyped n

Instances

Eq (BVTyped n)

Methods

(==) :: BVTyped n -> BVTyped n -> Bool

(/=) :: BVTyped n -> BVTyped n -> Bool

Ord (BVTyped n)

Methods

compare :: BVTyped n -> BVTyped n -> Ordering

(<) :: BVTyped n -> BVTyped n -> Bool

(<=) :: BVTyped n -> BVTyped n -> Bool

(>) :: BVTyped n -> BVTyped n -> Bool

(>=) :: BVTyped n -> BVTyped n -> Bool

max :: BVTyped n -> BVTyped n -> BVTyped n

min :: BVTyped n -> BVTyped n -> BVTyped n

Show (BVTyped n)

Methods

showsPrec :: Int -> BVTyped n -> ShowS

show :: BVTyped n -> String

showList :: [BVTyped n] -> ShowS

type ConcatResult BVUntyped (BVTyped n2)

type ConcatResult BVUntyped (BVTyped n2) = BVUntyped

type SMTAnnotation (BitVector (BVTyped n))

type SMTAnnotation (BitVector (BVTyped n)) = ()

type ConcatResult (BVTyped n1) BVUntyped

type ConcatResult (BVTyped n1) BVUntyped = BVUntyped

type ConcatResult (BVTyped n1) (BVTyped n2)

type ConcatResult (BVTyped n1) (BVTyped n2) = BVTyped (Add n1 n2)

data BVUntyped

Instances

Eq BVUntyped

Methods

(==) :: BVUntyped -> BVUntyped -> Bool

(/=) :: BVUntyped -> BVUntyped -> Bool

Ord BVUntyped

Methods

compare :: BVUntyped -> BVUntyped -> Ordering

(<) :: BVUntyped -> BVUntyped -> Bool

(<=) :: BVUntyped -> BVUntyped -> Bool

(>) :: BVUntyped -> BVUntyped -> Bool

(>=) :: BVUntyped -> BVUntyped -> Bool

max :: BVUntyped -> BVUntyped -> BVUntyped

min :: BVUntyped -> BVUntyped -> BVUntyped

Show BVUntyped

Methods

showsPrec :: Int -> BVUntyped -> ShowS

show :: BVUntyped -> String

showList :: [BVUntyped] -> ShowS

type ConcatResult BVUntyped BVUntyped

type ConcatResult BVUntyped BVUntyped = BVUntyped

type ConcatResult BVUntyped (BVTyped n2)

type ConcatResult BVUntyped (BVTyped n2) = BVUntyped

type SMTAnnotation (BitVector BVUntyped)

type SMTAnnotation (BitVector BVUntyped) = Integer

type ConcatResult (BVTyped n1) BVUntyped

type ConcatResult (BVTyped n1) BVUntyped = BVUntyped

type BV8 = BitVector (BVTyped N8)

type BV16 = BitVector (BVTyped N16)

type BV32 = BitVector (BVTyped N32)

type BV64 = BitVector (BVTyped N64)

type N0 = Z

type N1 = S N0

type N2 = S N1

type N3 = S N2

type N4 = S N3

type N5 = S N4

type N6 = S N5

type N7 = S N6

type N8 = S N7

type N9 = S N8

type N10 = S N9

type N11 = S N10

type N12 = S N11

type N13 = S N12

type N14 = S N13

type N15 = S N14

type N16 = S N15

type N17 = S N16

type N18 = S N17

type N19 = S N18

type N20 = S N19

type N21 = S N20

type N22 = S N21

type N23 = S N22

type N24 = S N23

type N25 = S N24

type N26 = S N25

type N27 = S N26

type N28 = S N27

type N29 = S N28

type N30 = S N29

type N31 = S N30

type N32 = S N31

type N33 = S N32

type N34 = S N33

type N35 = S N34

type N36 = S N35

type N37 = S N36

type N38 = S N37

type N39 = S N38

type N40 = S N39

type N41 = S N40

type N42 = S N41

type N43 = S N42

type N44 = S N43

type N45 = S N44

type N46 = S N45

type N47 = S N46

type N48 = S N47

type N49 = S N48

type N50 = S N49

type N51 = S N50

type N52 = S N51

type N53 = S N52

type N54 = S N53

type N55 = S N54

type N56 = S N55

type N57 = S N56

type N58 = S N57

type N59 = S N58

type N60 = S N59

type N61 = S N60

type N62 = S N61

type N63 = S N62

type N64 = S N63

bvconcat :: Concatable t1 t2 => SMTExpr (BitVector t1) -> SMTExpr (BitVector t2) -> SMTExpr (BitVector (ConcatResult t1 t2))

Concats two bitvectors into one.

bvsplitu16to8 :: SMTExpr BV16 -> (SMTExpr BV8, SMTExpr BV8)

Safely split a 16-bit bitvector into two 8-bit bitvectors.

bvsplitu32to16 :: SMTExpr BV32 -> (SMTExpr BV16, SMTExpr BV16)

Safely split a 32-bit bitvector into two 16-bit bitvectors.

bvsplitu32to8 :: SMTExpr BV32 -> (SMTExpr BV8, SMTExpr BV8, SMTExpr BV8, SMTExpr BV8)

Safely split a 32-bit bitvector into four 8-bit bitvectors.

bvsplitu64to32 :: SMTExpr BV64 -> (SMTExpr BV32, SMTExpr BV32)

Safely split a 64-bit bitvector into two 32-bit bitvectors.

bvsplitu64to16 :: SMTExpr BV64 -> (SMTExpr BV16, SMTExpr BV16, SMTExpr BV16, SMTExpr BV16)

Safely split a 64-bit bitvector into four 16-bit bitvectors.

bvsplitu64to8 :: SMTExpr BV64 -> (SMTExpr BV8, SMTExpr BV8, SMTExpr BV8, SMTExpr BV8, SMTExpr BV8, SMTExpr BV8, SMTExpr BV8, SMTExpr BV8)

Safely split a 64-bit bitvector into eight 8-bit bitvectors.

bvextract

Arguments

:: (TypeableNat start, TypeableNat len, Extractable tp len')

=> Proxy start

The start of the extracted region

-> Proxy len

-> SMTExpr (BitVector tp)

The bitvector to extract from

-> SMTExpr (BitVector len')

Extract a sub-vector out of a given bitvector.

bvextract' :: Integer -> Integer -> SMTExpr (BitVector BVUntyped) -> SMTExpr (BitVector BVUntyped)

Functions

funAnn :: (Liftable a, SMTType r, Monad m) => ArgAnnotation a -> SMTAnnotation r -> SMT' m (SMTFunction a r)

Create a new uniterpreted function with annotations for the argument and the return type.

funAnnNamed :: (Liftable a, SMTType r, Monad m) => String -> ArgAnnotation a -> SMTAnnotation r -> SMT' m (SMTFunction a r)

Create a new uninterpreted named function with annotation for the argument and the return type.

funAnnRet :: (Liftable a, SMTType r, Unit (ArgAnnotation a), Monad m) => SMTAnnotation r -> SMT' m (SMTFunction a r)

funAnn with an annotation only for the return type.

fun :: (Liftable a, SMTType r, SMTAnnotation r ~ (), Unit (ArgAnnotation a), Monad m) => SMT' m (SMTFunction a r)

Create a new uninterpreted function.

app :: (Args arg, SMTType res) => SMTFunction arg res -> arg -> SMTExpr res

Apply a function to an argument

defFun :: (Args a, SMTType r, Unit (ArgAnnotation a), Monad m) => (a -> SMTExpr r) -> SMT' m (SMTFunction a r)

Define a new function with a body

defConst :: (SMTType r, Monad m) => SMTExpr r -> SMT' m (SMTExpr r)

Define a new constant.

defConstNamed :: (SMTType r, Monad m) => String -> SMTExpr r -> SMT' m (SMTExpr r)

Define a new constant with a name

defFunAnn :: (Args a, SMTType r, Monad m) => ArgAnnotation a -> (a -> SMTExpr r) -> SMT' m (SMTFunction a r)

Like defFunAnnNamed, but defaults the function name to "fun".

defFunAnnNamed :: (Args a, SMTType r, Monad m) => String -> ArgAnnotation a -> (a -> SMTExpr r) -> SMT' m (SMTFunction a r)

Define a new function with a body and custom type annotations for arguments and result.

map' :: (Liftable arg, Args i, SMTType res) => SMTFunction arg res -> SMTFunction (Lifted arg i) (SMTArray i res)

Lift a function to arrays

Data types

is :: (Args arg, SMTType dt) => SMTExpr dt -> Constructor arg dt -> SMTExpr Bool

Checks if the expression is formed a specific constructor.

(.#) :: (SMTType a, SMTType f) => SMTExpr a -> Field a f -> SMTExpr f

Access a field of an expression

Lists

head' :: (SMTType a, Unit (SMTAnnotation a)) => SMTExpr [a] -> SMTExpr a

Takes the first element of a list

tail' :: (SMTType a, Unit (SMTAnnotation a)) => SMTExpr [a] -> SMTExpr [a]

Drops the first element from a list

insert' :: SMTType a => SMTAnnotation a -> Constructor (SMTExpr a, SMTExpr [a]) [a]

isNil :: SMTType a => SMTExpr [a] -> SMTExpr Bool

Checks if a list is empty.

isInsert :: (SMTType a, Unit (SMTAnnotation a)) => SMTExpr [a] -> SMTExpr Bool

Checks if a list is non-empty.

Untyped expressions

data Untyped

Instances

Eq Untyped

Methods

(==) :: Untyped -> Untyped -> Bool

(/=) :: Untyped -> Untyped -> Bool

Ord Untyped

Methods

compare :: Untyped -> Untyped -> Ordering

(<) :: Untyped -> Untyped -> Bool

(<=) :: Untyped -> Untyped -> Bool

(>) :: Untyped -> Untyped -> Bool

(>=) :: Untyped -> Untyped -> Bool

max :: Untyped -> Untyped -> Untyped

min :: Untyped -> Untyped -> Untyped

type SMTAnnotation Untyped

type SMTAnnotation Untyped = ProxyArg

data UntypedValue

Instances

Eq UntypedValue

Methods

(==) :: UntypedValue -> UntypedValue -> Bool

(/=) :: UntypedValue -> UntypedValue -> Bool

Ord UntypedValue

Methods

compare :: UntypedValue -> UntypedValue -> Ordering

(<) :: UntypedValue -> UntypedValue -> Bool

(<=) :: UntypedValue -> UntypedValue -> Bool

(>) :: UntypedValue -> UntypedValue -> Bool

(>=) :: UntypedValue -> UntypedValue -> Bool

max :: UntypedValue -> UntypedValue -> UntypedValue

min :: UntypedValue -> UntypedValue -> UntypedValue

Show UntypedValue

Methods

showsPrec :: Int -> UntypedValue -> ShowS

show :: UntypedValue -> String

showList :: [UntypedValue] -> ShowS

type SMTAnnotation UntypedValue

type SMTAnnotation UntypedValue = ProxyArgValue

entype :: (forall a. SMTType a => SMTExpr a -> b) -> SMTExpr Untyped -> b

entypeValue :: (forall a. SMTValue a => SMTExpr a -> b) -> SMTExpr UntypedValue -> b

castUntypedExpr :: SMTType t => SMTExpr Untyped -> SMTExpr t

castUntypedExprValue :: SMTType t => SMTExpr UntypedValue -> SMTExpr t