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

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

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)

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

Show (SMTFunction arg res)

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)

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)

data Field a f

Represents a field of the datatype a of the type f

Instances

Show (Field a f)

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

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.

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

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

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

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

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)

Eq (BitVector b)

Ord (BitVector b)

Show (BitVector a)

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

type SMTAnnotation (BitVector BVUntyped) = Integer

data BVTyped n

Instances

Eq (BVTyped n)

Ord (BVTyped n)

Show (BVTyped n)

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

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

type SMTAnnotation Untyped = ProxyArg

data UntypedValue

Instances

Eq UntypedValue

Ord UntypedValue

Show 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