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'

Monad m => Monad (SMT' m)

Functor m => Functor (SMT' m)

MonadFix m => MonadFix (SMT' m)

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

MonadIO m => MonadIO (SMT' m)

type SMT = SMT' IO

class Monad m => SMTBackend a m

Minimal complete definition

smtHandle, smtGetNames, smtNextName

Instances

MonadIO m => SMTBackend SMTPipe m

Monad m => SMTBackend (AnyBackend m) m

data AnyBackend m

Constructors

forall b . SMTBackend b m => AnyBackend b

Instances

Monad m => SMTBackend (AnyBackend m) m

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

Instances

SMTType Bool

SMTType Integer

SMTType UntypedValue

SMTType Untyped

(Typeable * a, SMTType a) => SMTType [a]

SMTType (Ratio Integer)

SMTType a => SMTType (Maybe a)

TypeableNat n => SMTType (BitVector (BVTyped n))

SMTType (BitVector BVUntyped)

(Args idx, SMTType val) => SMTType (SMTArray idx val)

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

Haskell values which can be represented as SMT constants

Minimal complete definition

unmangle, mangle

Instances

SMTValue Bool

SMTValue Integer

SMTValue UntypedValue

(Typeable * a, SMTValue a) => SMTValue [a]

SMTValue (Ratio Integer)

SMTValue a => SMTValue (Maybe a)

TypeableNat n => SMTValue (BitVector (BVTyped n))

SMTValue (BitVector BVUntyped)

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

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

Instances

SMTArith Integer

SMTArith (Ratio Integer)

class SMTType t => SMTOrd t where

Lifts the Ord class into SMT

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

Instances

SMTOrd Integer

SMTOrd (Ratio Integer)

data SMTExpr t

An abstract SMT expression

Instances

Enum (SMTExpr Integer)

Eq a => Eq (SMTExpr a)

Fractional (SMTExpr (Ratio Integer))

Num (SMTExpr Integer)

Num (SMTExpr (Ratio Integer))

TypeableNat n => Num (SMTExpr (BitVector (BVTyped n)))

SMTType t => Ord (SMTExpr t)

Show (SMTExpr t)

SMTValue a => LiftArgs (SMTExpr a)

SMTType a => Liftable [SMTExpr a]

SMTType a => Liftable (SMTExpr a)

SMTType a => Args (SMTExpr a)

Typeable (* -> *) SMTExpr

type Unpacked (SMTExpr a) = a

type ArgAnnotation (SMTExpr a) = SMTAnnotation a

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

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

data SMTFunction arg res

Instances

Args arg => Eq (SMTFunction arg res)

Args arg => Ord (SMTFunction arg res)

Show (SMTFunction arg res)

Typeable (* -> * -> *) SMTFunction

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

Ord SMTOption

Show SMTOption

data SMTArray i v

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

Instances

Eq (SMTArray i v)

Ord (SMTArray i v)

(Args idx, SMTType val) => SMTType (SMTArray idx val)

Typeable (* -> * -> *) SMTArray

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

Eq (Constructor arg res)

Ord (Constructor arg res)

Show (Constructor arg res)

Typeable (* -> * -> *) Constructor

data Field a f

Represents a field of the datatype a of the type f

Instances

Eq (Field a f)

Ord (Field a f)

Show (Field a f)

Typeable (* -> * -> *) Field

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

Args a => Args [a]

Args a => Args (Maybe a)

SMTType a => Args (SMTExpr a)

(Args a, Args b) => Args (Either a b)

(Args a, Args b) => Args (a, b)

(Typeable * a, Show a, Args b, Ord a) => Args (Map a b)

(Args a, Args b, Args c) => Args (a, b, c)

(Args a, Args b, Args c, Args d) => Args (a, b, c, d)

(Args a, Args b, Args c, Args d, Args e) => Args (a, b, c, d, e)

(Args a, Args b, Args c, Args d, Args e, Args f) => Args (a, b, c, d, e, f)

class Args a => LiftArgs a where

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

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.

Instances

LiftArgs a => LiftArgs [a]

LiftArgs a => LiftArgs (Maybe a)

SMTValue a => LiftArgs (SMTExpr a)

(LiftArgs a, LiftArgs b) => LiftArgs (Either a b)

(LiftArgs a, LiftArgs b) => LiftArgs (a, b)

(Typeable * a, Show a, Ord a, LiftArgs b) => LiftArgs (Map a b)

(LiftArgs a, LiftArgs b, LiftArgs c) => LiftArgs (a, b, c)

(LiftArgs a, LiftArgs b, LiftArgs c, LiftArgs d) => LiftArgs (a, b, c, d)

(LiftArgs a, LiftArgs b, LiftArgs c, LiftArgs d, LiftArgs e) => LiftArgs (a, b, c, d, e)

(LiftArgs a, LiftArgs b, LiftArgs c, LiftArgs d, LiftArgs e, LiftArgs f) => LiftArgs (a, b, c, d, e, f)

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

Ord CheckSatResult

Show CheckSatResult

Typeable * CheckSatResult

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

Ord CheckSatLimits

Show CheckSatLimits

Typeable * CheckSatLimits

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

Ord ClauseId

Show ClauseId

Typeable * ClauseId

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

Ord InterpolationGroup

Show InterpolationGroup

Typeable * InterpolationGroup

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)

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)

Eq (BitVector b)

TypeableNat n => Num (BitVector (BVTyped n))

TypeableNat n => Num (SMTExpr (BitVector (BVTyped n)))

Ord (BitVector b)

Show (BitVector a)

TypeableNat n => SMTValue (BitVector (BVTyped n))

SMTValue (BitVector BVUntyped)

TypeableNat n => SMTType (BitVector (BVTyped n))

SMTType (BitVector BVUntyped)

Typeable (* -> *) BitVector

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

type SMTAnnotation (BitVector BVUntyped) = Integer

data BVTyped n

Instances

TypeableNat n => Extractable BVUntyped (BVTyped n)

TypeableNat n2 => Concatable BVUntyped (BVTyped n2)

Eq (BVTyped n)

TypeableNat n => Num (BitVector (BVTyped n))

TypeableNat n => Num (SMTExpr (BitVector (BVTyped n)))

Ord (BVTyped n)

Show (BVTyped n)

TypeableNat n => IsBitVector (BVTyped n)

TypeableNat n => SMTValue (BitVector (BVTyped n))

TypeableNat n => SMTType (BitVector (BVTyped n))

TypeableNat n => Extractable (BVTyped n) BVUntyped

TypeableNat n1 => Concatable (BVTyped n1) BVUntyped

(TypeableNat n1, TypeableNat n2) => Extractable (BVTyped n1) (BVTyped n2)

(TypeableNat n1, TypeableNat n2, TypeableNat (Add n1 n2)) => Concatable (BVTyped n1) (BVTyped n2)

Typeable (* -> *) BVTyped

type ConcatResult BVUntyped (BVTyped n2) = BVUntyped

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

type ConcatResult (BVTyped n1) BVUntyped = BVUntyped

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

data BVUntyped

Instances

Eq BVUntyped

Ord BVUntyped

Show BVUntyped

IsBitVector BVUntyped

Typeable * BVUntyped

Extractable BVUntyped BVUntyped

Concatable BVUntyped BVUntyped

TypeableNat n => Extractable BVUntyped (BVTyped n)

TypeableNat n2 => Concatable BVUntyped (BVTyped n2)

SMTValue (BitVector BVUntyped)

SMTType (BitVector BVUntyped)

TypeableNat n => Extractable (BVTyped n) BVUntyped

TypeableNat n1 => Concatable (BVTyped n1) BVUntyped

type ConcatResult BVUntyped BVUntyped = BVUntyped

type ConcatResult BVUntyped (BVTyped n2) = BVUntyped

type SMTAnnotation (BitVector BVUntyped) = Integer

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

Ord Untyped

SMTType Untyped

Typeable * Untyped

type SMTAnnotation Untyped = ProxyArg

data UntypedValue

Instances

Eq UntypedValue

Ord UntypedValue

Show UntypedValue

SMTValue UntypedValue

SMTType UntypedValue

Typeable * 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