Safe Haskell	None
Language	Haskell98

Language.SMTLib2

Contents

SMT Monad
Setting options
Getting informations about the solver
Expressions
Satisfiability
Types
- Numbers
- Lists
Misc

Description

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

import Language.SMTLib2
import Language.SMTLib2.Pipe

program :: Backend b => SMT b (Integer,Integer)
program = do
  x <- declareVar int
  y <- declareVar int
  assert $ x .+. y .==. cint 5
  assert $ x .>. cint 0
  assert $ y .>. cint 0
  checkSat
  IntValue vx <- getValue x
  IntValue vy <- getValue y
  return (vx,vy)

main = withBackend (createPipe "z3" ["-smt2","-in"]) program >>= print

Synopsis

SMT Monad

data SMT b a Source #

The SMT monad is used to perform communication with the SMT solver. The type of solver is given by the b parameter.

Instances

Backend b => Monad (SMT b) Source #
Methods (>>=) :: SMT b a -> (a -> SMT b b) -> SMT b b # (>>) :: SMT b a -> SMT b b -> SMT b b # return :: a -> SMT b a # fail :: String -> SMT b a #
Backend b => Functor (SMT b) Source #
Methods fmap :: (a -> b) -> SMT b a -> SMT b b # (<$) :: a -> SMT b b -> SMT b a #
Backend b => Applicative (SMT b) Source #
Methods pure :: a -> SMT b a # (<>) :: SMT b (a -> b) -> SMT b a -> SMT b b # (>) :: SMT b a -> SMT b b -> SMT b b # (<*) :: SMT b a -> SMT b b -> SMT b a #
(Backend b, MonadIO (SMTMonad b)) => MonadIO (SMT b) Source #
Methods liftIO :: IO a -> SMT b a #
Backend b => MonadState (SMTState b) (SMT b) Source #
Methods get :: SMT b (SMTState b) # put :: SMTState b -> SMT b () # state :: (SMTState b -> (a, SMTState b)) -> SMT b a #
Backend b => Embed (SMT b) (Expr b) Source #
Associated Types type EmVar (SMT b :: * -> ) (Expr b :: Type -> ) :: Type -> * Source # type EmQVar (SMT b :: * -> ) (Expr b :: Type -> ) :: Type -> * Source # type EmFun (SMT b :: * -> ) (Expr b :: Type -> ) :: ([Type], Type) -> * Source # type EmFunArg (SMT b :: * -> ) (Expr b :: Type -> ) :: Type -> * Source # type EmLVar (SMT b :: * -> ) (Expr b :: Type -> ) :: Type -> * Source # Methods embed :: SMT b (EmbedExpr (SMT b) (Expr b) tp) -> SMT b (Expr b tp) Source # embedQuantifier :: Quantifier -> List Type Repr arg -> (forall m e. (Embed m e, Monad m) => List Type (EmQVar m e) arg -> m (e BoolType)) -> SMT b (Expr b BoolType) Source # embedTypeOf :: SMT b (Expr b tp -> Repr tp) Source #
type EmVar (SMT b) (Expr b) Source #
type EmVar (SMT b) (Expr b) = Var b
type EmQVar (SMT b) (Expr b) Source #
type EmQVar (SMT b) (Expr b) = QVar b
type EmFun (SMT b) (Expr b) Source #
type EmFun (SMT b) (Expr b) = Fun b
type EmFunArg (SMT b) (Expr b) Source #
type EmFunArg (SMT b) (Expr b) = FunArg b
type EmLVar (SMT b) (Expr b) Source #
type EmLVar (SMT b) (Expr b) = LVar b

class (Applicative m, GCompare (EmVar m e), GCompare (EmQVar m e), GCompare (EmFun m e), GCompare (EmFunArg m e), GCompare (EmLVar m e)) => Embed m e Source #

A class of Monads that can be used to form SMTLib expressions. The default instance of this class is the SMT monad, together with its associated Expr type. An interesting instance is the Identity monad with the Value type, which allows evaluation of SMTLib expressions.

Minimal complete definition

embed, embedQuantifier, embedTypeOf

Instances

Embed Identity Repr Source #
Associated Types type EmVar (Identity :: * -> ) (Repr :: Type -> ) :: Type -> * Source # type EmQVar (Identity :: * -> ) (Repr :: Type -> ) :: Type -> * Source # type EmFun (Identity :: * -> ) (Repr :: Type -> ) :: ([Type], Type) -> * Source # type EmFunArg (Identity :: * -> ) (Repr :: Type -> ) :: Type -> * Source # type EmLVar (Identity :: * -> ) (Repr :: Type -> ) :: Type -> * Source # Methods embed :: Identity (EmbedExpr Identity Repr tp) -> Identity (Repr tp) Source # embedQuantifier :: Quantifier -> List Type Repr arg -> (forall m e. (Embed m e, Monad m) => List Type (EmQVar m e) arg -> m (e BoolType)) -> Identity (Repr BoolType) Source # embedTypeOf :: Identity (Repr tp -> Repr tp) Source #
Embed Identity Value Source #
Associated Types type EmVar (Identity :: * -> ) (Value :: Type -> ) :: Type -> * Source # type EmQVar (Identity :: * -> ) (Value :: Type -> ) :: Type -> * Source # type EmFun (Identity :: * -> ) (Value :: Type -> ) :: ([Type], Type) -> * Source # type EmFunArg (Identity :: * -> ) (Value :: Type -> ) :: Type -> * Source # type EmLVar (Identity :: * -> ) (Value :: Type -> ) :: Type -> * Source # Methods embed :: Identity (EmbedExpr Identity Value tp) -> Identity (Value tp) Source # embedQuantifier :: Quantifier -> List Type Repr arg -> (forall m e. (Embed m e, Monad m) => List Type (EmQVar m e) arg -> m (e BoolType)) -> Identity (Value BoolType) Source # embedTypeOf :: Identity (Value tp -> Repr tp) Source #
Embed Identity (ValueExt Identity) Source #
Associated Types type EmVar (Identity :: * -> ) (ValueExt Identity :: Type -> ) :: Type -> * Source # type EmQVar (Identity :: * -> ) (ValueExt Identity :: Type -> ) :: Type -> * Source # type EmFun (Identity :: * -> ) (ValueExt Identity :: Type -> ) :: ([Type], Type) -> * Source # type EmFunArg (Identity :: * -> ) (ValueExt Identity :: Type -> ) :: Type -> * Source # type EmLVar (Identity :: * -> ) (ValueExt Identity :: Type -> ) :: Type -> * Source # Methods embed :: Identity (EmbedExpr Identity (ValueExt Identity) tp) -> Identity (ValueExt Identity tp) Source # embedQuantifier :: Quantifier -> List Type Repr arg -> (forall m e. (Embed m e, Monad m) => List Type (EmQVar m e) arg -> m (e BoolType)) -> Identity (ValueExt Identity BoolType) Source # embedTypeOf :: Identity (ValueExt Identity tp -> Repr tp) Source #
(GCompare Type var, GetType var, GCompare Type qvar, GetType qvar, GCompare ([Type], Type) fun, GetFunType fun, GCompare Type farg, GetType farg, GCompare Type lvar, GetType lvar) => Embed Identity (SMTExpr var qvar fun farg lvar) Source #
Associated Types type EmVar (Identity :: * -> ) (SMTExpr var qvar fun farg lvar :: Type -> ) :: Type -> * Source # type EmQVar (Identity :: * -> ) (SMTExpr var qvar fun farg lvar :: Type -> ) :: Type -> * Source # type EmFun (Identity :: * -> ) (SMTExpr var qvar fun farg lvar :: Type -> ) :: ([Type], Type) -> * Source # type EmFunArg (Identity :: * -> ) (SMTExpr var qvar fun farg lvar :: Type -> ) :: Type -> * Source # type EmLVar (Identity :: * -> ) (SMTExpr var qvar fun farg lvar :: Type -> ) :: Type -> * Source # Methods embed :: Identity (EmbedExpr Identity (SMTExpr var qvar fun farg lvar) tp) -> Identity (SMTExpr var qvar fun farg lvar tp) Source # embedQuantifier :: Quantifier -> List Type Repr arg -> (forall m e. (Embed m e, Monad m) => List Type (EmQVar m e) arg -> m (e BoolType)) -> Identity (SMTExpr var qvar fun farg lvar BoolType) Source # embedTypeOf :: Identity (SMTExpr var qvar fun farg lvar tp -> Repr tp) Source #
Backend b => Embed (SMT b) (Expr b) Source #
Associated Types type EmVar (SMT b :: * -> ) (Expr b :: Type -> ) :: Type -> * Source # type EmQVar (SMT b :: * -> ) (Expr b :: Type -> ) :: Type -> * Source # type EmFun (SMT b :: * -> ) (Expr b :: Type -> ) :: ([Type], Type) -> * Source # type EmFunArg (SMT b :: * -> ) (Expr b :: Type -> ) :: Type -> * Source # type EmLVar (SMT b :: * -> ) (Expr b :: Type -> ) :: Type -> * Source # Methods embed :: SMT b (EmbedExpr (SMT b) (Expr b) tp) -> SMT b (Expr b tp) Source # embedQuantifier :: Quantifier -> List Type Repr arg -> (forall m e. (Embed m e, Monad m) => List Type (EmQVar m e) arg -> m (e BoolType)) -> SMT b (Expr b BoolType) Source # embedTypeOf :: SMT b (Expr b tp -> Repr tp) Source #
(Embed m e, Monad m) => Embed (ExceptT err m) e Source #
Associated Types type EmVar (ExceptT err m :: * -> ) (e :: Type -> ) :: Type -> * Source # type EmQVar (ExceptT err m :: * -> ) (e :: Type -> ) :: Type -> * Source # type EmFun (ExceptT err m :: * -> ) (e :: Type -> ) :: ([Type], Type) -> * Source # type EmFunArg (ExceptT err m :: * -> ) (e :: Type -> ) :: Type -> * Source # type EmLVar (ExceptT err m :: * -> ) (e :: Type -> ) :: Type -> * Source # Methods embed :: ExceptT err m (EmbedExpr (ExceptT err m) e tp) -> ExceptT err m (e tp) Source # embedQuantifier :: Quantifier -> List Type Repr arg -> (forall a b. (Embed a b, Monad a) => List Type (EmQVar a b) arg -> a (b BoolType)) -> ExceptT err m (e BoolType) Source # embedTypeOf :: ExceptT err m (e tp -> Repr tp) Source #

class (Typeable b, Functor (SMTMonad b), Monad (SMTMonad b), GetType (Expr b), GetType (Var b), GetType (QVar b), GetFunType (Fun b), GetType (FunArg b), GetType (LVar b), Typeable (Expr b), Typeable (Var b), Typeable (QVar b), Typeable (Fun b), Typeable (FunArg b), Typeable (LVar b), Typeable (ClauseId b), GCompare (Expr b), GShow (Expr b), GCompare (Var b), GShow (Var b), GCompare (QVar b), GShow (QVar b), GCompare (Fun b), GShow (Fun b), GCompare (FunArg b), GShow (FunArg b), GCompare (LVar b), GShow (LVar b), Ord (ClauseId b), Show (ClauseId b), Ord (Proof b), Show (Proof b), Show (Model b)) => Backend b Source #

A backend represents a specific type of SMT solver.

Minimal complete definition

setOption, getInfo, push, pop, declareVar, createQVar, createFunArg, defineVar, declareFun, defineFun, assert, assertId, assertPartition, checkSat, getUnsatCore, getValue, getModel, modelEvaluate, getProof, analyzeProof, simplify, toBackend, fromBackend, declareDatatypes, interpolate, exit

Associated Types

type SMTMonad b :: * -> * Source #

The monad in which the backend executes queries.

data Expr b :: Type -> * Source #

The internal type of expressions.

type ClauseId b :: * Source #

type Model b :: * Source #

withBackend Source #

Arguments

:: Backend b
=> SMTMonad b b	An action that creates a fresh backend.
-> SMT b a	The SMT action to perform.
-> SMTMonad b a

Execute an SMT action on a given backend.

withBackendExitCleanly :: (Backend b, SMTMonad b ~ IO) => IO b -> SMT b a -> IO a Source #

Like withBackend but specialized to the IO monad so exeptions can be handled by gracefully exiting the solver.

Setting options

setOption :: Backend b => SMTOption -> SMT b () Source #

Set an option controlling the behaviour of the SMT solver. Many solvers require you to specify what kind of queries you'll ask them after the model is specified.

For example, when using interpolation, it is often required to do the following:

do
  setOption (ProduceInterpolants True)
  -- Declare model
  interp <- getInterpolant
  -- Use interpolant

data SMTOption Source #

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
SMTLogic String

Instances

Eq SMTOption Source #
Methods (==) :: SMTOption -> SMTOption -> Bool # (/=) :: SMTOption -> SMTOption -> Bool #
Ord SMTOption Source #
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 Source #
Methods showsPrec :: Int -> SMTOption -> ShowS # show :: SMTOption -> String # showList :: [SMTOption] -> ShowS #

Getting informations about the solver

getInfo :: Backend b => SMTInfo i -> SMT b i Source #

Query the solver for information about itself.

Example:

isZ3Solver :: Backend b => SMT b Bool
isZ3Solver = do
  name <- getInfo SMTSolverName
  return $ name=="Z3"

data SMTInfo i where Source #

Solver information query type. Used with getInfo.

Constructors

SMTSolverName :: SMTInfo String
SMTSolverVersion :: SMTInfo String

Expressions

Declaring variables

declareVar Source #

Arguments

:: Backend b
=> Repr t	The type of the variable
-> SMT b (Expr b t)

Create a fresh variable of a given type.

Example:

do
  -- Declare a single integer variable
  v <- declareVar int
  -- Use variable v

declareVarNamed Source #

Arguments

:: Backend b
=> Repr t	Type of the variable
-> String	Name of the variable
-> SMT b (Expr b t)

Create a fresh variable (like declareVar), but also give it a name. Note that the name is a hint to the SMT solver that it may ignore.

Example:

do
  -- Declare a single boolean variable called "x"
  x <- declareVarNamed bool "x"
  -- Use variable x

Defining variables

defineVar Source #

Arguments

:: (Backend b, HasMonad expr, MatchMonad expr (SMT b), MonadResult expr ~ Expr b t)
=> expr	The definition expression
-> SMT b (Expr b t)

Create a new variable that is defined by a given expression.

Example:

do
  -- x is an integer
  x <- declareVar int
  -- y is defined to be x+5
  y <- defineVar $ x .+. cint 5
  -- Use x and y

defineVarNamed Source #

Arguments

:: (Backend b, HasMonad expr, MatchMonad expr (SMT b), MonadResult expr ~ Expr b t)
=> String	Name of the resulting variable
-> expr	Definition of the variable
-> SMT b (Expr b t)

Create a new named variable that is defined by a given expression (like defineVar).

Declaring functions

declareFun Source #

Arguments

:: Backend b
=> List Repr args	Function argument types
-> Repr res	Function result type
-> SMT b (Fun b '(args, res))

Create a new uninterpreted function by specifying its signature.

Example:

do
  -- Create a function from (int,bool) to int
  f <- declareFun (int ::: bool ::: Nil) int
  -- Use f

declareFunNamed Source #

Arguments

:: Backend b
=> List Repr args	Function argument types
-> Repr res	Function result type
-> String	Function name
-> SMT b (Fun b '(args, res))

Create a new uninterpreted function by specifying its signature (like declareFun), but also give it a name.

Defining functions

defineFun Source #

Arguments

:: (Backend b, HasMonad def, MatchMonad def (SMT b), MonadResult def ~ Expr b res)
=> List Repr args	Function argument types
-> (List (Expr b) args -> def)	Function definition
-> SMT b (Fun b '(args, res))

Create a new interpreted function with a definition. Given a signature and a (haskell) function from the arguments to the resulting expression.

Example:

do
  -- Create a function from (int,int) to int that calculates the maximum
  max <- defineFun (int ::: int ::: Nil) $
           (x ::: y ::: Nil) -> ite (x .>. y) x y
  -- Use max function

defineFunNamed :: (Backend b, HasMonad def, MatchMonad def (SMT b), MonadResult def ~ Expr b res) => String -> List Repr args -> (List (Expr b) args -> def) -> SMT b (Fun b '(args, res)) Source #

Create a new interpreted function with a definition (like defineFun) but also give it a name.

Constants

constant :: Embed m e => Value tp -> m (e tp) Source #

Create a constant, for example an integer:

Example:

do
  x <- declareVar int
  -- x is greater than 5
  assert $ x .>. constant (IntValue 5)

data Value a where Source #

Values that can be used as constants in expressions.

Constructors

BoolValue :: Bool -> Value BoolType
IntValue :: Integer -> Value IntType
RealValue :: Rational -> Value RealType
BitVecValue :: Integer -> BitWidth bw -> Value (BitVecType bw)
DataValue :: (IsDatatype dt, Length par ~ Parameters dt) => dt par Value -> Value (DataType dt par)

Instances

GetType Value Source #
Methods getType :: Value tp -> Repr tp Source #
GCompare Type Value Source #
Methods gcompare :: f a -> f b -> GOrdering Value a b #
GEq Type Value Source #
Methods geq :: f a -> f b -> Maybe ((Value := a) b) #
GShow Type Value Source #
Methods gshowsPrec :: Int -> t a -> ShowS #
Embed Identity Value Source #
Associated Types type EmVar (Identity :: * -> ) (Value :: Type -> ) :: Type -> * Source # type EmQVar (Identity :: * -> ) (Value :: Type -> ) :: Type -> * Source # type EmFun (Identity :: * -> ) (Value :: Type -> ) :: ([Type], Type) -> * Source # type EmFunArg (Identity :: * -> ) (Value :: Type -> ) :: Type -> * Source # type EmLVar (Identity :: * -> ) (Value :: Type -> ) :: Type -> * Source # Methods embed :: Identity (EmbedExpr Identity Value tp) -> Identity (Value tp) Source # embedQuantifier :: Quantifier -> List Type Repr arg -> (forall m e. (Embed m e, Monad m) => List Type (EmQVar m e) arg -> m (e BoolType)) -> Identity (Value BoolType) Source # embedTypeOf :: Identity (Value tp -> Repr tp) Source #
Bounded (Value BoolType) Source #
Methods minBound :: Value BoolType # maxBound :: Value BoolType #
KnownNat bw => Bounded (Value (BitVecType bw)) Source #
Methods minBound :: Value (BitVecType bw) # maxBound :: Value (BitVecType bw) #
Enum (Value BoolType) Source #
Methods succ :: Value BoolType -> Value BoolType # pred :: Value BoolType -> Value BoolType # toEnum :: Int -> Value BoolType # fromEnum :: Value BoolType -> Int # enumFrom :: Value BoolType -> [Value BoolType] # enumFromThen :: Value BoolType -> Value BoolType -> [Value BoolType] # enumFromTo :: Value BoolType -> Value BoolType -> [Value BoolType] # enumFromThenTo :: Value BoolType -> Value BoolType -> Value BoolType -> [Value BoolType] #
Enum (Value IntType) Source #
Methods succ :: Value IntType -> Value IntType # pred :: Value IntType -> Value IntType # toEnum :: Int -> Value IntType # fromEnum :: Value IntType -> Int # enumFrom :: Value IntType -> [Value IntType] # enumFromThen :: Value IntType -> Value IntType -> [Value IntType] # enumFromTo :: Value IntType -> Value IntType -> [Value IntType] # enumFromThenTo :: Value IntType -> Value IntType -> Value IntType -> [Value IntType] #
KnownNat bw => Enum (Value (BitVecType bw)) Source #
Methods succ :: Value (BitVecType bw) -> Value (BitVecType bw) # pred :: Value (BitVecType bw) -> Value (BitVecType bw) # toEnum :: Int -> Value (BitVecType bw) # fromEnum :: Value (BitVecType bw) -> Int # enumFrom :: Value (BitVecType bw) -> [Value (BitVecType bw)] # enumFromThen :: Value (BitVecType bw) -> Value (BitVecType bw) -> [Value (BitVecType bw)] # enumFromTo :: Value (BitVecType bw) -> Value (BitVecType bw) -> [Value (BitVecType bw)] # enumFromThenTo :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw) -> [Value (BitVecType bw)] #
Eq (Value t) Source #
Methods (==) :: Value t -> Value t -> Bool # (/=) :: Value t -> Value t -> Bool #
Fractional (Value RealType) Source #
Methods (/) :: Value RealType -> Value RealType -> Value RealType # recip :: Value RealType -> Value RealType # fromRational :: Rational -> Value RealType #
Integral (Value IntType) Source #
Methods quot :: Value IntType -> Value IntType -> Value IntType # rem :: Value IntType -> Value IntType -> Value IntType # div :: Value IntType -> Value IntType -> Value IntType # mod :: Value IntType -> Value IntType -> Value IntType # quotRem :: Value IntType -> Value IntType -> (Value IntType, Value IntType) # divMod :: Value IntType -> Value IntType -> (Value IntType, Value IntType) # toInteger :: Value IntType -> Integer #
KnownNat bw => Integral (Value (BitVecType bw)) Source #
Methods quot :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw) # rem :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw) # div :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw) # mod :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw) # quotRem :: Value (BitVecType bw) -> Value (BitVecType bw) -> (Value (BitVecType bw), Value (BitVecType bw)) # divMod :: Value (BitVecType bw) -> Value (BitVecType bw) -> (Value (BitVecType bw), Value (BitVecType bw)) # toInteger :: Value (BitVecType bw) -> Integer #
Num (Value IntType) Source #
Methods (+) :: Value IntType -> Value IntType -> Value IntType # (-) :: Value IntType -> Value IntType -> Value IntType # (*) :: Value IntType -> Value IntType -> Value IntType # negate :: Value IntType -> Value IntType # abs :: Value IntType -> Value IntType # signum :: Value IntType -> Value IntType # fromInteger :: Integer -> Value IntType #
Num (Value RealType) Source #
Methods (+) :: Value RealType -> Value RealType -> Value RealType # (-) :: Value RealType -> Value RealType -> Value RealType # (*) :: Value RealType -> Value RealType -> Value RealType # negate :: Value RealType -> Value RealType # abs :: Value RealType -> Value RealType # signum :: Value RealType -> Value RealType # fromInteger :: Integer -> Value RealType #
KnownNat bw => Num (Value (BitVecType bw)) Source #
Methods (+) :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw) # (-) :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw) # (*) :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw) # negate :: Value (BitVecType bw) -> Value (BitVecType bw) # abs :: Value (BitVecType bw) -> Value (BitVecType bw) # signum :: Value (BitVecType bw) -> Value (BitVecType bw) # fromInteger :: Integer -> Value (BitVecType bw) #
Ord (Value t) Source #
Methods compare :: Value t -> Value t -> Ordering # (<) :: Value t -> Value t -> Bool # (<=) :: Value t -> Value t -> Bool # (>) :: Value t -> Value t -> Bool # (>=) :: Value t -> Value t -> Bool # max :: Value t -> Value t -> Value t # min :: Value t -> Value t -> Value t #
Real (Value IntType) Source #
Methods toRational :: Value IntType -> Rational #
Real (Value RealType) Source #
Methods toRational :: Value RealType -> Rational #
KnownNat bw => Real (Value (BitVecType bw)) Source #
Methods toRational :: Value (BitVecType bw) -> Rational #
RealFrac (Value RealType) Source #
Methods properFraction :: Integral b => Value RealType -> (b, Value RealType) # truncate :: Integral b => Value RealType -> b # round :: Integral b => Value RealType -> b # ceiling :: Integral b => Value RealType -> b # floor :: Integral b => Value RealType -> b #
Show (Value tp) Source #
Methods showsPrec :: Int -> Value tp -> ShowS # show :: Value tp -> String # showList :: [Value tp] -> ShowS #
KnownNat bw => Bits (Value (BitVecType bw)) Source #
Methods (.&.) :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw) # (.\|.) :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw) # xor :: Value (BitVecType bw) -> Value (BitVecType bw) -> Value (BitVecType bw) # complement :: Value (BitVecType bw) -> Value (BitVecType bw) # shift :: Value (BitVecType bw) -> Int -> Value (BitVecType bw) # rotate :: Value (BitVecType bw) -> Int -> Value (BitVecType bw) # zeroBits :: Value (BitVecType bw) # bit :: Int -> Value (BitVecType bw) # setBit :: Value (BitVecType bw) -> Int -> Value (BitVecType bw) # clearBit :: Value (BitVecType bw) -> Int -> Value (BitVecType bw) # complementBit :: Value (BitVecType bw) -> Int -> Value (BitVecType bw) # testBit :: Value (BitVecType bw) -> Int -> Bool # bitSizeMaybe :: Value (BitVecType bw) -> Maybe Int # bitSize :: Value (BitVecType bw) -> Int # isSigned :: Value (BitVecType bw) -> Bool # shiftL :: Value (BitVecType bw) -> Int -> Value (BitVecType bw) # unsafeShiftL :: Value (BitVecType bw) -> Int -> Value (BitVecType bw) # shiftR :: Value (BitVecType bw) -> Int -> Value (BitVecType bw) # unsafeShiftR :: Value (BitVecType bw) -> Int -> Value (BitVecType bw) # rotateL :: Value (BitVecType bw) -> Int -> Value (BitVecType bw) # rotateR :: Value (BitVecType bw) -> Int -> Value (BitVecType bw) # popCount :: Value (BitVecType bw) -> Int #
KnownNat bw => FiniteBits (Value (BitVecType bw)) Source #
Methods finiteBitSize :: Value (BitVecType bw) -> Int # countLeadingZeros :: Value (BitVecType bw) -> Int # countTrailingZeros :: Value (BitVecType bw) -> Int #
type EmVar Identity Value Source #
type EmVar Identity Value = NoVar
type EmQVar Identity Value Source #
type EmQVar Identity Value = NoVar
type EmFun Identity Value Source #
type EmFun Identity Value = UserFun Identity Value
type EmFunArg Identity Value Source #
type EmFunArg Identity Value = NoVar
type EmLVar Identity Value Source #
type EmLVar Identity Value = NoVar

Boolean constants

pattern ConstBool :: forall rtp v qv fun fv lv e. () => (~) Type rtp BoolType => Bool -> Expression v qv fun fv lv e rtp Source #

Matches constant boolean expressions (true or false).

cbool :: Embed m e => Bool -> m (e BoolType) Source #

Create a boolean constant expression.

true :: Embed m e => m (e BoolType) Source #

Create the boolean expression "true".

false :: Embed m e => m (e BoolType) Source #

Create the boolean expression "false".

Integer constants

pattern ConstInt :: forall rtp v qv fun fv lv e. () => (~) Type rtp IntType => Integer -> Expression v qv fun fv lv e rtp Source #

cint :: Embed m e => Integer -> m (e IntType) Source #

Create an integer constant expression.

Real constants

pattern ConstReal :: forall rtp v qv fun fv lv e. () => (~) Type rtp RealType => Rational -> Expression v qv fun fv lv e rtp Source #

creal :: Embed m e => Rational -> m (e RealType) Source #

Create a real constant expression.

Example:

import Data.Ratio

x = creal (5 % 4)

Bitvector constants

data BitWidth bw Source #

Instances

GCompare Nat BitWidth Source #
Methods gcompare :: f a -> f b -> GOrdering BitWidth a b #
GEq Nat BitWidth Source #
Methods geq :: f a -> f b -> Maybe ((BitWidth := a) b) #
Eq (BitWidth bw) Source #
Methods (==) :: BitWidth bw -> BitWidth bw -> Bool # (/=) :: BitWidth bw -> BitWidth bw -> Bool #
Show (BitWidth bw) Source #
Methods showsPrec :: Int -> BitWidth bw -> ShowS # show :: BitWidth bw -> String # showList :: [BitWidth bw] -> ShowS #

bw :: KnownNat bw => Proxy bw -> BitWidth bw Source #

pattern ConstBV :: forall rtp v qv fun fv lv e. () => forall bw. (~) Type rtp (BitVecType bw) => Integer -> BitWidth bw -> Expression v qv fun fv lv e rtp Source #

cbv Source #

Arguments

:: Embed m e
=> Integer	The value (negative values will be stored in two's-complement).
-> BitWidth bw	The bitwidth of the bitvector value.
-> m (e (BitVecType bw))

Create a constant bitvector expression.

cbvUntyped Source #

Arguments

:: (Embed m e, Monad m)
=> Integer	The value (negative values will be stored in two's-complement).
-> Integer	The bitwidth (must be >= 0).
-> (forall bw. e (BitVecType bw) -> m b)
-> m b

Create an untyped constant bitvector expression.

Datatype constants

cdt :: (Embed m e, IsDatatype t, Length par ~ Parameters t) => t par Value -> m (e (DataType t par)) Source #

Quantification

exists :: (Embed m e, Monad m) => List Repr tps -> (forall m e. (Embed m e, Monad m) => List e tps -> m (e BoolType)) -> m (e BoolType) Source #

forall :: (Embed m e, Monad m) => List Repr tps -> (forall m e. (Embed m e, Monad m) => List e tps -> m (e BoolType)) -> m (e BoolType) Source #

Functions

pattern Fun :: forall t t1 t2 t3 t4 t5 t6. () => forall arg arg1 res. (~#) ([Type], Type) ([Type], Type) ((,) [Type] Type arg t) ((,) [Type] Type arg1 res) => t5 ((,) [Type] Type arg1 res) -> List Type t6 arg -> Expression t4 t3 t5 t2 t1 t6 t Source #

app :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ List e args) => Function (EmFun m e) '(args, res) -> a -> m (e res) Source #

Create an expression by applying a function to a list of arguments.

fun :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ List e args) => EmFun m e '(args, res) -> a -> m (e res) Source #

Equality

pattern EqLst :: forall e rtp v qv fun fv lv. GetType e => forall tp. (~) Type rtp BoolType => [e tp] -> Expression v qv fun fv lv e rtp Source #

pattern Eq :: forall e rtp v qv fun fv lv. GetType e => forall tps. ((~) Type rtp BoolType, Same tps) => List Type e tps -> Expression v qv fun fv lv e rtp Source #

pattern (:==:) :: forall e rtp v qv fun fv lv. GetType e => forall tp. (~) Type rtp BoolType => e tp -> e tp -> Expression v qv fun fv lv e rtp Source #

eq :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp) => [a] -> m (e BoolType) Source #

(.==.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType) infix 4 Source #

Create a boolean expression that encodes that two expressions have the same value.

Example:

is5 :: Backend b => Expr b IntType -> SMT b BoolType
is5 e = e .==. cint 5

pattern DistinctLst :: forall e rtp v qv fun fv lv. GetType e => forall tp. (~) Type rtp BoolType => [e tp] -> Expression v qv fun fv lv e rtp Source #

pattern Distinct :: forall e rtp v qv fun fv lv. GetType e => forall tps. ((~) Type rtp BoolType, Same tps) => List Type e tps -> Expression v qv fun fv lv e rtp Source #

pattern (:/=:) :: forall e rtp v qv fun fv lv. GetType e => forall tp. (~) Type rtp BoolType => e tp -> e tp -> Expression v qv fun fv lv e rtp Source #

distinct :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp) => [a] -> m (e BoolType) Source #

(./=.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType) infix 4 Source #

Map

map' :: (Embed m e, HasMonad arg, MatchMonad arg m, MonadResult arg ~ List e (Lifted tps idx), Unlift tps idx, GetType e, GetFunType (EmFun m e)) => Function (EmFun m e) '(tps, res) -> arg -> m (e (ArrayType idx res)) Source #

Comparison

pattern Ord :: forall rtp e v qv fun fv lv. () => forall tp. ((~) Type rtp BoolType, IsSMTNumber tp) => OrdOp -> e tp -> e tp -> Expression v qv fun fv lv e rtp Source #

pattern (:>=:) :: forall rtp e v qv fun fv lv. () => forall tp. ((~) Type rtp BoolType, IsSMTNumber tp) => e tp -> e tp -> Expression v qv fun fv lv e rtp Source #

pattern (:>:) :: forall rtp e v qv fun fv lv. () => forall tp. ((~) Type rtp BoolType, IsSMTNumber tp) => e tp -> e tp -> Expression v qv fun fv lv e rtp Source #

pattern (:<=:) :: forall rtp e v qv fun fv lv. () => forall tp. ((~) Type rtp BoolType, IsSMTNumber tp) => e tp -> e tp -> Expression v qv fun fv lv e rtp Source #

pattern (:<:) :: forall rtp e v qv fun fv lv. () => forall tp. ((~) Type rtp BoolType, IsSMTNumber tp) => e tp -> e tp -> Expression v qv fun fv lv e rtp Source #

ord :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => OrdOp -> a -> b -> m (e BoolType) Source #

(.>=.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType) infix 4 Source #

(.>.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType) infix 4 Source #

(.<=.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType) infix 4 Source #

(.<.) :: (Embed m e, IsSMTNumber tp, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp) => a -> b -> m (e BoolType) infix 4 Source #

Arithmetic

pattern ArithLst :: forall tp e v qv fun fv lv. () => IsSMTNumber tp => ArithOp -> [e tp] -> Expression v qv fun fv lv e tp Source #

pattern Arith :: forall tp e v qv fun fv lv. () => forall tps. (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps)) => ArithOp -> List Type e tps -> Expression v qv fun fv lv e tp Source #

arith :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => ArithOp -> [a] -> m (e tp) Source #

pattern PlusLst :: forall lv fv fun qv v tp e. () => IsSMTNumber tp => [e tp] -> Expression v qv fun fv lv e tp Source #

pattern Plus :: forall tp lv fv fun qv v e. () => forall tps. (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps)) => List Type e tps -> Expression v qv fun fv lv e tp Source #

pattern (:+:) :: forall tp lv fv fun qv v e. () => forall tps x xs x1 xs1. (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps), (~#) [Type] [Type] tps ((:) Type x xs), (~#) [Type] [Type] xs ((:) Type x1 xs1), (~#) [Type] [Type] xs1 ([] Type)) => e x -> e x1 -> Expression v qv fun fv lv e tp Source #

plus :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => [a] -> m (e tp) Source #

(.+.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp, IsSMTNumber tp) => a -> b -> m (e tp) infixl 6 Source #

pattern MultLst :: forall lv fv fun qv v tp e. () => IsSMTNumber tp => [e tp] -> Expression v qv fun fv lv e tp Source #

pattern Mult :: forall tp lv fv fun qv v e. () => forall tps. (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps)) => List Type e tps -> Expression v qv fun fv lv e tp Source #

pattern (:*:) :: forall tp lv fv fun qv v e. () => forall tps x xs x1 xs1. (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps), (~#) [Type] [Type] tps ((:) Type x xs), (~#) [Type] [Type] xs ((:) Type x1 xs1), (~#) [Type] [Type] xs1 ([] Type)) => e x -> e x1 -> Expression v qv fun fv lv e tp Source #

mult :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => [a] -> m (e tp) Source #

(.*.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp, IsSMTNumber tp) => a -> b -> m (e tp) infixl 7 Source #

pattern MinusLst :: forall lv fv fun qv v tp e. () => IsSMTNumber tp => [e tp] -> Expression v qv fun fv lv e tp Source #

pattern Minus :: forall tp lv fv fun qv v e. () => forall tps. (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps)) => List Type e tps -> Expression v qv fun fv lv e tp Source #

pattern (:-:) :: forall tp lv fv fun qv v e. () => forall tps x xs x1 xs1. (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps), (~#) [Type] [Type] tps ((:) Type x xs), (~#) [Type] [Type] xs ((:) Type x1 xs1), (~#) [Type] [Type] xs1 ([] Type)) => e x -> e x1 -> Expression v qv fun fv lv e tp Source #

pattern Neg :: forall tp lv fv fun qv v e. () => forall tps x xs. (IsSMTNumber tp, Same tps, (~) Type tp (SameType tps), (~#) [Type] [Type] tps ((:) Type x xs), (~#) [Type] [Type] xs ([] Type)) => e x -> Expression v qv fun fv lv e tp Source #

minus :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => [a] -> m (e tp) Source #

(.-.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e tp, MonadResult b ~ e tp, IsSMTNumber tp) => a -> b -> m (e tp) infixl 6 Source #

neg :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => a -> m (e tp) Source #

pattern Div :: forall t t1 t2 t3 t4 t5 t6. () => forall arg x xs x1 xs1. ((~#) ([Type], Type) ([Type], Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type IntType ((:) Type IntType ([] Type))) IntType), (~#) [Type] [Type] arg ((:) Type x xs), (~#) [Type] [Type] xs ((:) Type x1 xs1), (~#) [Type] [Type] xs1 ([] Type)) => t6 x -> t6 x1 -> Expression t5 t4 t3 t2 t1 t6 t Source #

pattern Mod :: forall t t1 t2 t3 t4 t5 t6. () => forall arg x xs x1 xs1. ((~#) ([Type], Type) ([Type], Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type IntType ((:) Type IntType ([] Type))) IntType), (~#) [Type] [Type] arg ((:) Type x xs), (~#) [Type] [Type] xs ((:) Type x1 xs1), (~#) [Type] [Type] xs1 ([] Type)) => t6 x -> t6 x1 -> Expression t5 t4 t3 t2 t1 t6 t Source #

pattern Rem :: forall t t1 t2 t3 t4 t5 t6. () => forall arg x xs x1 xs1. ((~#) ([Type], Type) ([Type], Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type IntType ((:) Type IntType ([] Type))) IntType), (~#) [Type] [Type] arg ((:) Type x xs), (~#) [Type] [Type] xs ((:) Type x1 xs1), (~#) [Type] [Type] xs1 ([] Type)) => t6 x -> t6 x1 -> Expression t5 t4 t3 t2 t1 t6 t Source #

div' :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e IntType, MonadResult b ~ e IntType) => a -> b -> m (e IntType) infixl 7 Source #

mod' :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e IntType, MonadResult b ~ e IntType) => a -> b -> m (e IntType) infixl 7 Source #

rem' :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e IntType, MonadResult b ~ e IntType) => a -> b -> m (e IntType) infixl 7 Source #

pattern (:/:) :: forall t t1 t2 t3 t4 t5 t6. () => forall arg x xs x1 xs1. ((~#) ([Type], Type) ([Type], Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type RealType ((:) Type RealType ([] Type))) RealType), (~#) [Type] [Type] arg ((:) Type x xs), (~#) [Type] [Type] xs ((:) Type x1 xs1), (~#) [Type] [Type] xs1 ([] Type)) => t6 x -> t6 x1 -> Expression t5 t4 t3 t2 t1 t6 t Source #

(./.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e RealType, MonadResult b ~ e RealType) => a -> b -> m (e RealType) infixl 7 Source #

pattern Abs :: forall tp e v qv fun fv lv. () => IsSMTNumber tp => e tp -> Expression v qv fun fv lv e tp Source #

abs' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp, IsSMTNumber tp) => a -> m (e tp) Source #

Logic

pattern Not :: forall t t1 t2 t3 t4 t5 t6. () => forall arg x xs. ((~#) ([Type], Type) ([Type], Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type BoolType ([] Type)) BoolType), (~#) [Type] [Type] arg ((:) Type x xs), (~#) [Type] [Type] xs ([] Type)) => t6 x -> Expression t5 t4 t3 t2 t1 t6 t Source #

not' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => a -> m (e BoolType) Source #

pattern LogicLst :: forall rtp e v qv fun fv lv. () => (~) Type rtp BoolType => LogicOp -> [e BoolType] -> Expression v qv fun fv lv e rtp Source #

pattern Logic :: forall rtp e v qv fun fv lv. () => forall tps. ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => LogicOp -> List Type e tps -> Expression v qv fun fv lv e rtp Source #

logic :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => LogicOp -> [a] -> m (e BoolType) Source #

pattern AndLst :: forall rtp lv fv fun qv v e. () => (~) Type rtp BoolType => [e BoolType] -> Expression v qv fun fv lv e rtp Source #

pattern And :: forall rtp lv fv fun qv v e. () => forall tps. ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => List Type e tps -> Expression v qv fun fv lv e rtp Source #

pattern (:&:) :: forall rtp e v qv fun fv lv. () => (~) Type rtp BoolType => e BoolType -> e BoolType -> Expression v qv fun fv lv e rtp Source #

and' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType) Source #

(.&.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e BoolType, MonadResult b ~ e BoolType) => a -> b -> m (e BoolType) infixr 3 Source #

pattern OrLst :: forall rtp lv fv fun qv v e. () => (~) Type rtp BoolType => [e BoolType] -> Expression v qv fun fv lv e rtp Source #

pattern Or :: forall rtp lv fv fun qv v e. () => forall tps. ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => List Type e tps -> Expression v qv fun fv lv e rtp Source #

pattern (:|:) :: forall rtp e v qv fun fv lv. () => (~) Type rtp BoolType => e BoolType -> e BoolType -> Expression v qv fun fv lv e rtp Source #

or' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType) Source #

(.|.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e BoolType, MonadResult b ~ e BoolType) => a -> b -> m (e BoolType) infixr 2 Source #

pattern XOrLst :: forall rtp lv fv fun qv v e. () => (~) Type rtp BoolType => [e BoolType] -> Expression v qv fun fv lv e rtp Source #

pattern XOr :: forall rtp lv fv fun qv v e. () => forall tps. ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => List Type e tps -> Expression v qv fun fv lv e rtp Source #

xor' :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType) Source #

pattern ImpliesLst :: forall rtp lv fv fun qv v e. () => (~) Type rtp BoolType => [e BoolType] -> Expression v qv fun fv lv e rtp Source #

pattern Implies :: forall rtp lv fv fun qv v e. () => forall tps. ((~) Type rtp BoolType, Same tps, (~) Type (SameType tps) BoolType) => List Type e tps -> Expression v qv fun fv lv e rtp Source #

pattern (:=>:) :: forall rtp e v qv fun fv lv. () => (~) Type rtp BoolType => e BoolType -> e BoolType -> Expression v qv fun fv lv e rtp Source #

implies :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e BoolType) => [a] -> m (e BoolType) Source #

(.=>.) :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e BoolType, MonadResult b ~ e BoolType) => a -> b -> m (e BoolType) infixr 2 Source #

Conversion

pattern ToReal :: forall t t1 t2 t3 t4 t5 t6. () => forall arg x xs. ((~#) ([Type], Type) ([Type], Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type IntType ([] Type)) RealType), (~#) [Type] [Type] arg ((:) Type x xs), (~#) [Type] [Type] xs ([] Type)) => t6 x -> Expression t5 t4 t3 t2 t1 t6 t Source #

pattern ToInt :: forall t t1 t2 t3 t4 t5 t6. () => forall arg x xs. ((~#) ([Type], Type) ([Type], Type) ((,) [Type] Type arg t) ((,) [Type] Type ((:) Type RealType ([] Type)) IntType), (~#) [Type] [Type] arg ((:) Type x xs), (~#) [Type] [Type] xs ([] Type)) => t6 x -> Expression t5 t4 t3 t2 t1 t6 t Source #

toReal :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e IntType) => a -> m (e RealType) Source #

toInt :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e RealType) => a -> m (e IntType) Source #

If-then-else

pattern ITE :: forall e tp v qv fun fv lv. GetType e => e BoolType -> e tp -> e tp -> Expression v qv fun fv lv e tp Source #

ite :: (Embed m e, HasMonad a, HasMonad b, HasMonad c, MatchMonad a m, MatchMonad b m, MatchMonad c m, MonadResult a ~ e BoolType, MonadResult b ~ e tp, MonadResult c ~ e tp) => a -> b -> c -> m (e tp) Source #

Bitvectors

pattern BVComp :: forall e rtp v qv fun fv lv. GetType e => forall bw. (~) Type rtp BoolType => BVCompOp -> e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp Source #

pattern BVULE :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp BoolType => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp Source #

pattern BVULT :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp BoolType => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp Source #

pattern BVUGE :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp BoolType => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp Source #

pattern BVUGT :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp BoolType => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp Source #

pattern BVSLE :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp BoolType => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp Source #

pattern BVSLT :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp BoolType => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp Source #

pattern BVSGE :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp BoolType => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp Source #

pattern BVSGT :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp BoolType => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp Source #

bvcomp :: forall m e a b bw. (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => BVCompOp -> a -> b -> m (e BoolType) Source #

bvule :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType) Source #

bvult :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType) Source #

bvuge :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType) Source #

bvugt :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType) Source #

bvsle :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType) Source #

bvslt :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType) Source #

bvsge :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType) Source #

bvsgt :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e BoolType) Source #

pattern BVBin :: forall e rtp v qv fun fv lv. GetType e => forall bw. (~) Type rtp (BitVecType bw) => BVBinOp -> e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp Source #

pattern BVAdd :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp Source #

pattern BVSub :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp Source #

pattern BVMul :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp Source #

pattern BVURem :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp Source #

pattern BVSRem :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp Source #

pattern BVUDiv :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp Source #

pattern BVSDiv :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp Source #

pattern BVSHL :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp Source #

pattern BVLSHR :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp Source #

pattern BVASHR :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp Source #

pattern BVXor :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp Source #

pattern BVAnd :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp Source #

pattern BVOr :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp Source #

bvbin :: forall m e a b bw. (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => BVBinOp -> a -> b -> m (e (BitVecType bw)) Source #

bvadd :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw)) Source #

bvsub :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw)) Source #

bvmul :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw)) Source #

bvurem :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw)) Source #

bvsrem :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw)) Source #

bvudiv :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw)) Source #

bvsdiv :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw)) Source #

bvshl :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw)) Source #

bvlshr :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw)) Source #

bvashr :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw)) Source #

bvxor :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw)) Source #

bvand :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw)) Source #

bvor :: (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType bw), MonadResult b ~ e (BitVecType bw)) => a -> b -> m (e (BitVecType bw)) Source #

pattern BVUn :: forall e rtp v qv fun fv lv. GetType e => forall bw. (~) Type rtp (BitVecType bw) => BVUnOp -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp Source #

pattern BVNot :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> Expression v qv fun fv lv e rtp Source #

pattern BVNeg :: forall rtp lv fv fun qv v e. GetType e => forall bw. (~) Type rtp (BitVecType bw) => e (BitVecType bw) -> Expression v qv fun fv lv e rtp Source #

bvun :: forall m e a bw. (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw)) => BVUnOp -> a -> m (e (BitVecType bw)) Source #

bvnot :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw)) => a -> m (e (BitVecType bw)) Source #

bvneg :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw)) => a -> m (e (BitVecType bw)) Source #

pattern Concat :: forall e rtp v qv fun fv lv. GetType e => forall n1 n2. (~) Type rtp (BitVecType ((+) n1 n2)) => e (BitVecType n1) -> e (BitVecType n2) -> Expression v qv fun fv lv e rtp Source #

pattern Extract :: forall e rtp v qv fun fv lv. GetType e => forall len start bw. (~) Type rtp (BitVecType len) => BitWidth start -> BitWidth len -> e (BitVecType bw) -> Expression v qv fun fv lv e rtp Source #

concat' :: forall m e a b n1 n2. (Embed m e, HasMonad a, HasMonad b, MatchMonad a m, MatchMonad b m, MonadResult a ~ e (BitVecType n1), MonadResult b ~ e (BitVecType n2)) => a -> b -> m (e (BitVecType (n1 + n2))) Source #

extract' :: forall m e a bw start len. (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw), (start + len) <= bw) => BitWidth start -> BitWidth len -> a -> m (e (BitVecType len)) Source #

extractChecked :: forall m e a bw start len. (Embed m e, HasMonad a, MatchMonad a m, KnownNat start, KnownNat len, MonadResult a ~ e (BitVecType bw)) => BitWidth start -> BitWidth len -> a -> m (e (BitVecType len)) Source #

extractUntypedStart :: forall m e a bw len. (Embed m e, HasMonad a, MatchMonad a m, KnownNat len, MonadResult a ~ e (BitVecType bw)) => Integer -> BitWidth len -> a -> m (e (BitVecType len)) Source #

extractUntyped :: forall m e a bw b. (Embed m e, Monad m, HasMonad a, MatchMonad a m, MonadResult a ~ e (BitVecType bw)) => Integer -> Integer -> a -> (forall len. e (BitVecType len) -> m b) -> m b Source #

Arrays

pattern Select :: forall e rtp v qv fun fv lv. GetType e => forall val idx. (~) Type rtp val => e (ArrayType idx val) -> List Type e idx -> Expression v qv fun fv lv e rtp Source #

pattern Store :: forall e rtp v qv fun fv lv. GetType e => forall idx val. (~) Type rtp (ArrayType idx val) => e (ArrayType idx val) -> List Type e idx -> e val -> Expression v qv fun fv lv e rtp Source #

pattern ConstArray :: forall e rtp v qv fun fv lv. GetType e => forall idx val. (~) Type rtp (ArrayType idx val) => List Type Repr idx -> e val -> Expression v qv fun fv lv e rtp Source #

select :: (Embed m e, HasMonad arr, MatchMonad arr m, MonadResult arr ~ e (ArrayType idx el), HasMonad i, MatchMonad i m, MonadResult i ~ List e idx) => arr -> i -> m (e el) Source #

Access an array element. The following law holds:

   select (store arr i e) i .==. e

select1 :: (Embed m e, HasMonad arr, HasMonad idx, MatchMonad arr m, MatchMonad idx m, MonadResult arr ~ e (ArrayType '[idx'] el), MonadResult idx ~ e idx') => arr -> idx -> m (e el) Source #

A specialized version of select when the index is just a single element.

store :: (Embed m e, HasMonad arr, MatchMonad arr m, MonadResult arr ~ e (ArrayType idx el), HasMonad i, MatchMonad i m, MonadResult i ~ List e idx, HasMonad nel, MatchMonad nel m, MonadResult nel ~ e el) => arr -> i -> nel -> m (e (ArrayType idx el)) Source #

Write an element into an array and return the resulting array. The following laws hold (forall i/=j):

   select (store arr i e) i .==. e
   select (store arr i e) j .==. select arr j

store1 :: (Embed m e, HasMonad arr, HasMonad idx, HasMonad el, MatchMonad arr m, MatchMonad idx m, MatchMonad el m, MonadResult arr ~ e (ArrayType '[idx'] el'), MonadResult idx ~ e idx', MonadResult el ~ e el') => arr -> idx -> el -> m (e (ArrayType '[idx'] el')) Source #

A specialized version of store when the index is just a single element.

constArray :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e tp) => List Repr idx -> a -> m (e (ArrayType idx tp)) Source #

Create an array where every element is the same. The following holds:

   select (constArray tp e) i .==. e

Datatypes

pattern Mk :: forall t t1 t2 t3 t4 t5 t6. () => forall arg dt par sig. ((~#) ([Type], Type) ([Type], Type) ((,) [Type] Type arg t) ((,) [Type] Type (Instantiated sig par) (DataType ([Type] -> (Type -> *) -> *) dt par)), IsDatatype dt, (~) Nat (Length Type par) (Parameters dt)) => Datatype dt -> List Type Repr par -> Constr dt sig -> List Type t6 arg -> Expression t5 t4 t3 t2 t1 t6 t Source #

mk :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ List e (Instantiated sig par), IsDatatype dt, Length par ~ Parameters dt) => Datatype dt -> List Repr par -> Constr dt sig -> a -> m (e (DataType dt par)) Source #

pattern Is :: forall e rtp v qv fun fv lv. GetType e => forall dt sig par. (~) Type rtp BoolType => Constr dt sig -> e (DataType ([Type] -> (Type -> *) -> *) dt par) -> Expression v qv fun fv lv e rtp Source #

is :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (DataType dt par), IsDatatype dt) => a -> Constr dt sig -> m (e BoolType) Source #

(.#.) :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e (DataType dt par), IsDatatype dt) => a -> Field dt tp -> m (e (CType tp par)) Source #

Misc

pattern Divisible :: forall rtp e v qv fun fv lv. () => (~) Type rtp BoolType => Integer -> e IntType -> Expression v qv fun fv lv e rtp Source #

divisible :: (Embed m e, HasMonad a, MatchMonad a m, MonadResult a ~ e IntType) => Integer -> a -> m (e BoolType) Source #

Analyzation

getExpr :: Backend b => Expr b tp -> SMT b (Expression (Var b) (QVar b) (Fun b) (FunArg b) (LVar b) (Expr b) tp) Source #

Convert an expression in the SMT solver-specific format into a more general, pattern-matchable format.

Example:

isGE :: Backend b => Expr b tp -> SMT b Bool
isGE e = do
  e' <- getExpr e
  case e' of
    _ :>=: _ -> return True
    _ -> return False

Satisfiability

assert :: (Backend b, HasMonad expr, MatchMonad expr (SMT b), MonadResult expr ~ Expr b BoolType) => expr -> SMT b () Source #

Asserts a boolean expression to be true. A successive successful checkSat calls mean that the generated model is consistent with the assertion.

checkSat :: Backend b => SMT b CheckSatResult Source #

Checks if the set of asserted expressions is satisfiable.

checkSatWith :: Backend b => Maybe Tactic -> CheckSatLimits -> SMT b CheckSatResult Source #

The same as checkSat, but can specify an optional Tactic that is used to give hints to the SMT solver on how to solve the problem and limits on the amount of time and memory that the solver is allowed to use. If the limits are exhausted, the solver must return Unknown.

data CheckSatResult Source #

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 Source #
Methods (==) :: CheckSatResult -> CheckSatResult -> Bool # (/=) :: CheckSatResult -> CheckSatResult -> Bool #
Ord CheckSatResult Source #
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 Source #
Methods showsPrec :: Int -> CheckSatResult -> ShowS # show :: CheckSatResult -> String # showList :: [CheckSatResult] -> ShowS #

data CheckSatLimits Source #

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 Source #
Methods (==) :: CheckSatLimits -> CheckSatLimits -> Bool # (/=) :: CheckSatLimits -> CheckSatLimits -> Bool #
Ord CheckSatLimits Source #
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 Source #
Methods showsPrec :: Int -> CheckSatLimits -> ShowS # show :: CheckSatLimits -> String # showList :: [CheckSatLimits] -> ShowS #

noLimits :: CheckSatLimits Source #

Unsatisfiable core

assertId :: (Backend b, HasMonad expr, MatchMonad expr (SMT b), MonadResult expr ~ Expr b BoolType) => expr -> SMT b (ClauseId b) Source #

Works like assert, but additionally allows the user to find the unsatisfiable core of a set of assignments using getUnsatCore.

getUnsatCore :: Backend b => SMT b [ClauseId b] Source #

After a checkSat query that returned Unsat, we can ask the SMT solver for a subset of the assertions that are enough to make the specified problem unsatisfiable. These assertions have to be created using assertId.

Example:

do
  setOption (ProduceUnsatCores True)
  x <- declareVar int
  y <- declareVar int
  cl1 <- assertId $ x .>. y
  cl2 <- assertId $ x .>. cint 5
  cl3 <- assertId $ y .>. x
  checkSat
  core <- getUnsatCore
  -- core will contain cl1 and cl3

Interpolation

assertPartition :: (Backend b, HasMonad expr, MatchMonad expr (SMT b), MonadResult expr ~ Expr b BoolType) => expr -> Partition -> SMT b () Source #

When using interpolation, use this function to specify if an assertion is part of the A-partition or the B-partition of the original formula.

data Partition Source #

The interpolation partition

Constructors

PartitionA
PartitionB

Instances

Eq Partition Source #
Methods (==) :: Partition -> Partition -> Bool # (/=) :: Partition -> Partition -> Bool #
Ord Partition Source #
Methods compare :: Partition -> Partition -> Ordering # (<) :: Partition -> Partition -> Bool # (<=) :: Partition -> Partition -> Bool # (>) :: Partition -> Partition -> Bool # (>=) :: Partition -> Partition -> Bool # max :: Partition -> Partition -> Partition # min :: Partition -> Partition -> Partition #
Show Partition Source #
Methods showsPrec :: Int -> Partition -> ShowS # show :: Partition -> String # showList :: [Partition] -> ShowS #

getInterpolant :: Backend b => SMT b (Expr b BoolType) Source #

After a checkSat query that returned Unsat, we can ask the SMT solver for a formula C such that A (the A-partition) and (not C) is unsatisfiable while B (the B-partition) and C is unsatisfiable. Furthermore, C will only mention variables that occur in both A and B.

Example:

do
  setOption (ProduceInterpolants True)
  p <- declareVar bool
  q <- declareVar bool
  r <- declareVar bool
  t <- declareVar bool
  assertPartition ((not' (p .&. q)) .=>. ((not' r) .&. q)) PartitionA
  assertPartition t PartitionB
  assertPartition r PartitionB
  assertPartition (not' p) PartitionB
  checkSat
  getInterpolant

Proofs

getProof :: Backend b => SMT b (Proof b) Source #

After a checkSat query that returned Unsat, we can ask the solver for a proof that the given instance is indeed unsatisfiable.

analyzeProof :: Backend b => Proof b -> SMT b (Proof String (Expr b) (Proof b)) Source #

Convert the solver-specific proof encoding into a more general, pattern-matchable format.

Stack

push :: Backend b => SMT b () Source #

Push a fresh frame on the solver stack. All variable definitions and assertions made in a frame are forgotten when it is pop'ed.

pop :: Backend b => SMT b () Source #

Pop a frame from the solver stack.

stack :: Backend b => SMT b a -> SMT b a Source #

Perform an SMT action by executing it in a fresh stack frame. The frame is pop'ed once the action has been performed.

Models

getValue :: (Backend b, HasMonad expr, MatchMonad expr (SMT b), MonadResult expr ~ Expr b t) => expr -> SMT b (Value t) Source #

After a successful checkSat query, query the concrete value for a given expression that the SMT solver assigned to it.

getModel :: Backend b => SMT b (Model b) Source #

After a successful checkSat query, return a satisfying assignment that makes all asserted formula true.

modelEvaluate :: (Backend b, HasMonad expr, MatchMonad expr (SMT b), MonadResult expr ~ Expr b t) => Model b -> expr -> SMT b (Value t) Source #

Evaluate an expression in a model, yielding a concrete value.

Types

registerDatatype :: (Backend b, IsDatatype dt) => Datatype dt -> SMT b () Source #

data Type Source #

Describes the kind of all SMT types. It is only used in promoted form, for a concrete representation see Repr.

Constructors

BoolType
IntType
RealType
BitVecType Nat
ArrayType [Type] Type
DataType a [Type]
ParameterType Nat

Instances

GCompare Type NumRepr Source #
Methods gcompare :: f a -> f b -> GOrdering NumRepr a b #
GCompare Type Repr Source #
Methods gcompare :: f a -> f b -> GOrdering Repr a b #
GCompare Type Value Source #
Methods gcompare :: f a -> f b -> GOrdering Value a b #
GCompare Type NoVar #
Methods gcompare :: f a -> f b -> GOrdering NoVar a b #
GEq Type NumRepr Source #
Methods geq :: f a -> f b -> Maybe ((NumRepr := a) b) #
GEq Type Repr Source #
Methods geq :: f a -> f b -> Maybe ((Repr := a) b) #
GEq Type Value Source #
Methods geq :: f a -> f b -> Maybe ((Value := a) b) #
GEq Type NoVar #
Methods geq :: f a -> f b -> Maybe ((NoVar := a) b) #
GShow Type NumRepr Source #
Methods gshowsPrec :: Int -> t a -> ShowS #
GShow Type Repr Source #
Methods gshowsPrec :: Int -> t a -> ShowS #
GShow Type Value Source #
Methods gshowsPrec :: Int -> t a -> ShowS #
GShow Type NoVar #
Methods gshowsPrec :: Int -> t a -> ShowS #
GCompare Type (Field (DynamicValue l sig)) Source #
Methods gcompare :: f a -> f b -> GOrdering (Field (DynamicValue l sig)) a b #
GCompare ([Type], Type) fun => GCompare Type (EvalResult fun) #
Methods gcompare :: f a -> f b -> GOrdering (EvalResult fun) a b #
Ord v => GCompare Type (UntypedVar v) #
Methods gcompare :: f a -> f b -> GOrdering (UntypedVar v) a b #
GCompare Type (ValueExt m) #
Methods gcompare :: f a -> f b -> GOrdering (ValueExt m) a b #
GEq Type (Field (DynamicValue l sig)) Source #
Methods geq :: f a -> f b -> Maybe ((Field (DynamicValue l sig) := a) b) #
GEq ([Type], Type) fun => GEq Type (EvalResult fun) #
Methods geq :: f a -> f b -> Maybe ((EvalResult fun := a) b) #
Eq v => GEq Type (UntypedVar v) #
Methods geq :: f a -> f b -> Maybe ((UntypedVar v := a) b) #
GEq Type (ValueExt m) #
Methods geq :: f a -> f b -> Maybe ((ValueExt m := a) b) #
GShow ([Type], Type) fun => GShow Type (EvalResult fun) #
Methods gshowsPrec :: Int -> t a -> ShowS #
Show v => GShow Type (UntypedVar v) #
Methods gshowsPrec :: Int -> t a -> ShowS #
GShow Type (ValueExt m) #
Methods gshowsPrec :: Int -> t a -> ShowS #
(GCompare Type v, GCompare Type e) => GCompare Type (LetBinding v e) #
Methods gcompare :: f a -> f b -> GOrdering (LetBinding v e) a b #
(GEq Type v, GEq Type e) => GEq Type (LetBinding v e) #
Methods geq :: f a -> f b -> Maybe ((LetBinding v e := a) b) #
GShow ([Type], Type) fun => GShow Type (ArrayModel fun idx) #
Methods gshowsPrec :: Int -> t a -> ShowS #
(GCompare Type v, GCompare Type qv, GCompare ([Type], Type) fun, GCompare Type fv, GCompare Type lv, GCompare Type e) => GCompare Type (Expression v qv fun fv lv e) #
Methods gcompare :: f a -> f b -> GOrdering (Expression v qv fun fv lv e) a b #
(GEq Type v, GEq Type qv, GEq ([Type], Type) fun, GEq Type fv, GEq Type lv, GEq Type e) => GEq Type (Expression v qv fun fv lv e) #
Methods geq :: f a -> f b -> Maybe ((Expression v qv fun fv lv e := a) b) #
(GShow Type v, GShow Type qv, GShow ([Type], Type) fun, GShow Type fv, GShow Type lv, GShow Type e) => GShow Type (Expression v qv fun fv lv e) #
Methods gshowsPrec :: Int -> t a -> ShowS #
HasMonad (m (List Type e tp)) Source #
Associated Types type MatchMonad (m (List Type e tp)) (m :: * -> ) :: Constraint Source # type MonadResult (m (List Type e tp)) :: Source # Methods embedM :: (Applicative m, MatchMonad (m (List Type e tp)) m) => m (List Type e tp) -> m (MonadResult (m (List Type e tp))) Source #
GCompare [Type] (DynamicConstructor sig) Source #
Methods gcompare :: f a -> f b -> GOrdering (DynamicConstructor sig) a b #
GCompare [Type] (Constr (DynamicValue l sig)) Source #
Methods gcompare :: f a -> f b -> GOrdering (Constr (DynamicValue l sig)) a b #
GEq [Type] (DynamicConstructor sig) Source #
Methods geq :: f a -> f b -> Maybe ((DynamicConstructor sig := a) b) #
GEq [Type] (Constr (DynamicValue l sig)) Source #
Methods geq :: f a -> f b -> Maybe ((Constr (DynamicValue l sig) := a) b) #
GCompare ([Type], *) NoCon #
Methods gcompare :: f a -> f b -> GOrdering NoCon a b #
GCompare ([Type], Type) FunRepr Source #
Methods gcompare :: f a -> f b -> GOrdering FunRepr a b #
GCompare ([Type], Type) NoFun #
Methods gcompare :: f a -> f b -> GOrdering NoFun a b #
GCompare (*, Type) NoField #
Methods gcompare :: f a -> f b -> GOrdering NoField a b #
GEq ([Type], *) NoCon #
Methods geq :: f a -> f b -> Maybe ((NoCon := a) b) #
GEq ([Type], Type) FunRepr Source #
Methods geq :: f a -> f b -> Maybe ((FunRepr := a) b) #
GEq ([Type], Type) NoFun #
Methods geq :: f a -> f b -> Maybe ((NoFun := a) b) #
GEq (*, Type) NoField #
Methods geq :: f a -> f b -> Maybe ((NoField := a) b) #
GShow ([Type], *) NoCon #
Methods gshowsPrec :: Int -> t a -> ShowS #
GShow ([Type], Type) NoFun #
Methods gshowsPrec :: Int -> t a -> ShowS #
GShow (*, Type) NoField #
Methods gshowsPrec :: Int -> t a -> ShowS #
GCompare ([Type], Type) fun => GCompare ([Type], Type) (Function fun) #
Methods gcompare :: f a -> f b -> GOrdering (Function fun) a b #
Ord v => GCompare ([Type], Type) (UntypedFun v) #
Methods gcompare :: f a -> f b -> GOrdering (UntypedFun v) a b #
GEq ([Type], Type) fun => GEq ([Type], Type) (Function fun) #
Methods geq :: f a -> f b -> Maybe ((Function fun := a) b) #
Eq v => GEq ([Type], Type) (UntypedFun v) #
Methods geq :: f a -> f b -> Maybe ((UntypedFun v := a) b) #
GShow ([Type], Type) fun => GShow ([Type], Type) (Function fun) #
Methods gshowsPrec :: Int -> t a -> ShowS #
Show v => GShow ([Type], Type) (UntypedFun v) #
Methods gshowsPrec :: Int -> t a -> ShowS #
GCompare ([Type], Type) (UserFun m e) #
Methods gcompare :: f a -> f b -> GOrdering (UserFun m e) a b #
GEq ([Type], Type) (UserFun m e) #
Methods geq :: f a -> f b -> Maybe ((UserFun m e := a) b) #
GShow ([Type], Type) (UserFun m e) #
Methods gshowsPrec :: Int -> t a -> ShowS #
HasMonad (List Type e tp) Source #
Associated Types type MatchMonad (List Type e tp) (m :: * -> ) :: Constraint Source # type MonadResult (List Type e tp) :: Source # Methods embedM :: (Applicative m, MatchMonad (List Type e tp) m) => List Type e tp -> m (MonadResult (List Type e tp)) Source #
(Same ((:) Type tp tps), (~) Type tp (SameType ((:) Type tp tps))) => Same ((:) Type tp ((:) Type tp tps)) Source #
Associated Types type SameType ((:) Type tp ((:) Type tp tps) :: [Type]) :: Type Methods sameType :: List Type Repr ((Type ': tp) ((Type ': tp) tps)) -> Repr (SameType ((Type ': tp) ((Type ': tp) tps))) sameToAllEq :: List Type e ((Type ': tp) ((Type ': tp) tps)) -> List Type e (AllEq (SameType ((Type ': tp) ((Type ': tp) tps))) (Length Type ((Type ': tp) ((Type ': tp) tps))))
Same ((:) Type tp ([] Type)) Source #
Associated Types type SameType ((:) Type tp ([] Type) :: [Type]) :: Type Methods sameType :: List Type Repr ((Type ': tp) [Type]) -> Repr (SameType ((Type ': tp) [Type])) sameToAllEq :: List Type e ((Type ': tp) [Type]) -> List Type e (AllEq (SameType ((Type ': tp) [Type])) (Length Type ((Type ': tp) [Type])))
Unlift ((:) Type t2 ts) idx => Unlift ((:) Type t1 ((:) Type t2 ts)) idx Source #
Methods unliftType :: List Type Repr (Lifted ((Type ': t1) ((Type ': t2) ts)) idx) -> (List Type Repr ((Type ': t1) ((Type ': t2) ts)), List Type Repr idx) Source # unliftTypeWith :: List Type Repr (Lifted ((Type ': t1) ((Type ': t2) ts)) idx) -> List Type Repr ((Type ': t1) ((Type ': t2) ts)) -> List Type Repr idx Source #
Unlift ((:) Type tp ([] Type)) idx Source #
Methods unliftType :: List Type Repr (Lifted ((Type ': tp) [Type]) idx) -> (List Type Repr ((Type ': tp) [Type]), List Type Repr idx) Source # unliftTypeWith :: List Type Repr (Lifted ((Type ': tp) [Type]) idx) -> List Type Repr ((Type ': tp) [Type]) -> List Type Repr idx Source #
type MonadResult (m (List Type e tp)) Source #
type MonadResult (m (List Type e tp)) = List Type e tp
type MatchMonad (m (List Type e tp)) m' Source #
type MatchMonad (m (List Type e tp)) m' = (~) (* -> *) m m'
type MonadResult (List Type e tp) Source #
type MonadResult (List Type e tp) = List Type e tp
type MatchMonad (List Type e tp) m Source #
type MatchMonad (List Type e tp) m = ()

data Repr t where Source #

A concrete representation of an SMT type. For aesthetic reasons, it's recommended to use the functions bool, int, real, bitvec or array.

Constructors

BoolRepr :: Repr BoolType
IntRepr :: Repr IntType
RealRepr :: Repr RealType
BitVecRepr :: BitWidth bw -> Repr (BitVecType bw)
ArrayRepr :: List Repr idx -> Repr val -> Repr (ArrayType idx val)
DataRepr :: (IsDatatype dt, Length par ~ Parameters dt) => Datatype dt -> List Repr par -> Repr (DataType dt par)
ParameterRepr :: Natural p -> Repr (ParameterType p)

Instances

GetType Repr Source #
Methods getType :: Repr tp -> Repr tp Source #
GCompare Type Repr Source #
Methods gcompare :: f a -> f b -> GOrdering Repr a b #
GEq Type Repr Source #
Methods geq :: f a -> f b -> Maybe ((Repr := a) b) #
GShow Type Repr Source #
Methods gshowsPrec :: Int -> t a -> ShowS #
Embed Identity Repr Source #
Associated Types type EmVar (Identity :: * -> ) (Repr :: Type -> ) :: Type -> * Source # type EmQVar (Identity :: * -> ) (Repr :: Type -> ) :: Type -> * Source # type EmFun (Identity :: * -> ) (Repr :: Type -> ) :: ([Type], Type) -> * Source # type EmFunArg (Identity :: * -> ) (Repr :: Type -> ) :: Type -> * Source # type EmLVar (Identity :: * -> ) (Repr :: Type -> ) :: Type -> * Source # Methods embed :: Identity (EmbedExpr Identity Repr tp) -> Identity (Repr tp) Source # embedQuantifier :: Quantifier -> List Type Repr arg -> (forall m e. (Embed m e, Monad m) => List Type (EmQVar m e) arg -> m (e BoolType)) -> Identity (Repr BoolType) Source # embedTypeOf :: Identity (Repr tp -> Repr tp) Source #
Eq (Repr tp) Source #
Methods (==) :: Repr tp -> Repr tp -> Bool # (/=) :: Repr tp -> Repr tp -> Bool #
Ord (Repr tp) Source #
Methods compare :: Repr tp -> Repr tp -> Ordering # (<) :: Repr tp -> Repr tp -> Bool # (<=) :: Repr tp -> Repr tp -> Bool # (>) :: Repr tp -> Repr tp -> Bool # (>=) :: Repr tp -> Repr tp -> Bool # max :: Repr tp -> Repr tp -> Repr tp # min :: Repr tp -> Repr tp -> Repr tp #
Show (Repr t) Source #
Methods showsPrec :: Int -> Repr t -> ShowS # show :: Repr t -> String # showList :: [Repr t] -> ShowS #
type EmVar Identity Repr Source #
type EmVar Identity Repr = Repr
type EmQVar Identity Repr Source #
type EmQVar Identity Repr = Repr
type EmFun Identity Repr Source #
type EmFun Identity Repr = FunRepr
type EmFunArg Identity Repr Source #
type EmFunArg Identity Repr = Repr
type EmLVar Identity Repr Source #
type EmLVar Identity Repr = Repr

class GetType v where Source #

Minimal complete definition

getType

Methods

getType :: v tp -> Repr tp Source #

Instances

GetType NumRepr Source #
Methods getType :: NumRepr tp -> Repr tp Source #
GetType Repr Source #
Methods getType :: Repr tp -> Repr tp Source #
GetType Value Source #
Methods getType :: Value tp -> Repr tp Source #
GetType NoVar Source #
Methods getType :: NoVar tp -> Repr tp Source #
GetFunType fun => GetType (EvalResult fun) Source #
Methods getType :: EvalResult fun tp -> Repr tp Source #
GetType (UntypedVar v) Source #
Methods getType :: UntypedVar v tp -> Repr tp Source #
GetType (ValueExt m) Source #
Methods getType :: ValueExt m tp -> Repr tp Source #
(GetType var, GetType qvar, GetFunType fun, GetType farg, GetType lvar) => GetType (SMTExpr var qvar fun farg lvar) Source #
Methods getType :: SMTExpr var qvar fun farg lvar tp -> Repr tp Source #
(GetType v, GetType qv, GetFunType fun, GetType fv, GetType lv, GetType e) => GetType (Expression v qv fun fv lv e) Source #
Methods getType :: Expression v qv fun fv lv e tp -> Repr tp Source #

bool :: Repr BoolType Source #

A representation of the SMT Bool type. Holds the values true or false. Constants can be created using cbool.

int :: Repr IntType Source #

A representation of the SMT Int type. Holds the unbounded positive and negative integers. Constants can be created using cint.

real :: Repr RealType Source #

A representation of the SMT Real type. Holds positive and negative reals x/y where x and y are integers. Constants can be created using creal.

bitvec Source #

Arguments

:: BitWidth bw	The width of the bitvector
-> Repr (BitVecType bw)

A typed representation of the SMT BitVec type. Holds bitvectors (a vector of booleans) of a certain bitwidth. Constants can be created using cbv.

array :: List Repr idx -> Repr el -> Repr (ArrayType idx el) Source #

A representation of the SMT Array type. Has a list of index types and an element type. Stores one value of the element type for each combination of the index types. Constants can be created using constArray.

dt :: (IsDatatype dt, Parameters dt ~ Z) => Datatype dt -> Repr (DataType dt '[]) Source #

A representation of a user-defined datatype without parameters.

dt' :: (IsDatatype dt, Length par ~ Parameters dt) => Datatype dt -> List Repr par -> Repr (DataType dt par) Source #

A representation of a user-defined datatype with parameters.

Numbers

data Nat Source #

Natural numbers on the type-level.

Constructors

Z
S Nat

Instances

Enum Nat Source #
Methods succ :: Nat -> Nat # pred :: Nat -> Nat # toEnum :: Int -> Nat # fromEnum :: Nat -> Int # enumFrom :: Nat -> [Nat] # enumFromThen :: Nat -> Nat -> [Nat] # enumFromTo :: Nat -> Nat -> [Nat] # enumFromThenTo :: Nat -> Nat -> Nat -> [Nat] #
Eq Nat Source #
Methods (==) :: Nat -> Nat -> Bool # (/=) :: Nat -> Nat -> Bool #
Integral Nat Source #
Methods quot :: Nat -> Nat -> Nat # rem :: Nat -> Nat -> Nat # div :: Nat -> Nat -> Nat # mod :: Nat -> Nat -> Nat # quotRem :: Nat -> Nat -> (Nat, Nat) # divMod :: Nat -> Nat -> (Nat, Nat) # toInteger :: Nat -> Integer #
Num Nat Source #
Methods (+) :: Nat -> Nat -> Nat # (-) :: Nat -> Nat -> Nat # (*) :: Nat -> Nat -> Nat # negate :: Nat -> Nat # abs :: Nat -> Nat # signum :: Nat -> Nat # fromInteger :: Integer -> Nat #
Ord Nat Source #
Methods compare :: Nat -> Nat -> Ordering # (<) :: Nat -> Nat -> Bool # (<=) :: Nat -> Nat -> Bool # (>) :: Nat -> Nat -> Bool # (>=) :: Nat -> Nat -> Bool # max :: Nat -> Nat -> Nat # min :: Nat -> Nat -> Nat #
Real Nat Source #
Methods toRational :: Nat -> Rational #
GCompare Nat Natural Source #
Methods gcompare :: f a -> f b -> GOrdering Natural a b #
GEq Nat Natural Source #
Methods geq :: f a -> f b -> Maybe ((Natural := a) b) #
GShow Nat Natural Source #
Methods gshowsPrec :: Int -> t a -> ShowS #

data Natural n where Source #

A concrete representation of the Nat type.

Constructors

Zero :: Natural Z
Succ :: Natural n -> Natural (S n)

Instances

GCompare Nat Natural Source #
Methods gcompare :: f a -> f b -> GOrdering Natural a b #
GEq Nat Natural Source #
Methods geq :: f a -> f b -> Maybe ((Natural := a) b) #
GShow Nat Natural Source #
Methods gshowsPrec :: Int -> t a -> ShowS #
Eq (Natural n) Source #
Methods (==) :: Natural n -> Natural n -> Bool # (/=) :: Natural n -> Natural n -> Bool #
Ord (Natural n) Source #
Methods compare :: Natural n -> Natural n -> Ordering # (<) :: Natural n -> Natural n -> Bool # (<=) :: Natural n -> Natural n -> Bool # (>) :: Natural n -> Natural n -> Bool # (>=) :: Natural n -> Natural n -> Bool # max :: Natural n -> Natural n -> Natural n # min :: Natural n -> Natural n -> Natural n #
Show (Natural n) Source #
Methods showsPrec :: Int -> Natural n -> ShowS # show :: Natural n -> String # showList :: [Natural n] -> ShowS #

nat :: (Num a, Ord a) => a -> ExpQ Source #

natT :: (Num a, Ord a) => a -> TypeQ Source #

A template haskell function to create nicer looking number types.

Example:

>>> $(nat 5) :: Natural $(natT 5)
5

reifyNat :: Nat -> (forall n. Natural n -> r) -> r Source #

Get a static representation for a dynamically created natural number.

Example:

>>> reifyNat (S (S Z)) show
"2"

Lists

data List e tp where Source #

Strongly typed heterogenous lists.

A List e '[tp1,tp2,tp3] contains 3 elements of types e tp1, e tp2 and e tp3 respectively.

As an example, the following list contains two types:

>>> int ::: bool ::: Nil :: List Repr '[IntType,BoolType]
[IntRepr,BoolRepr]

Constructors

Nil :: List e '[]
(:::) :: e x -> List e xs -> List e (x ': xs) infixr 9

Instances

HasMonad (m (List Type e tp)) Source #
Associated Types type MatchMonad (m (List Type e tp)) (m :: * -> ) :: Constraint Source # type MonadResult (m (List Type e tp)) :: Source # Methods embedM :: (Applicative m, MatchMonad (m (List Type e tp)) m) => m (List Type e tp) -> m (MonadResult (m (List Type e tp))) Source #
GCompare a e => GCompare [a] (List a e) Source #
Methods gcompare :: f a -> f b -> GOrdering (List a e) a b #
GEq a e => GEq [a] (List a e) Source #
Methods geq :: f a -> f b -> Maybe ((List a e := a) b) #
GShow a e => GShow [a] (List a e) Source #
Methods gshowsPrec :: Int -> t a -> ShowS #
GEq a e => Eq (List a e lst) Source #
Methods (==) :: List a e lst -> List a e lst -> Bool # (/=) :: List a e lst -> List a e lst -> Bool #
GCompare a e => Ord (List a e lst) Source #
Methods compare :: List a e lst -> List a e lst -> Ordering # (<) :: List a e lst -> List a e lst -> Bool # (<=) :: List a e lst -> List a e lst -> Bool # (>) :: List a e lst -> List a e lst -> Bool # (>=) :: List a e lst -> List a e lst -> Bool # max :: List a e lst -> List a e lst -> List a e lst # min :: List a e lst -> List a e lst -> List a e lst #
GShow a e => Show (List a e lst) Source #
Methods showsPrec :: Int -> List a e lst -> ShowS # show :: List a e lst -> String # showList :: [List a e lst] -> ShowS #
HasMonad (List Type e tp) Source #
Associated Types type MatchMonad (List Type e tp) (m :: * -> ) :: Constraint Source # type MonadResult (List Type e tp) :: Source # Methods embedM :: (Applicative m, MatchMonad (List Type e tp) m) => List Type e tp -> m (MonadResult (List Type e tp)) Source #
type MonadResult (m (List Type e tp)) Source #
type MonadResult (m (List Type e tp)) = List Type e tp
type MatchMonad (m (List Type e tp)) m' Source #
type MatchMonad (m (List Type e tp)) m' = (~) (* -> *) m m'
type MonadResult (List Type e tp) Source #
type MonadResult (List Type e tp) = List Type e tp
type MatchMonad (List Type e tp) m Source #
type MatchMonad (List Type e tp) m = ()

reifyList :: (forall r'. a -> (forall tp. e tp -> r') -> r') -> [a] -> (forall tp. List e tp -> r) -> r Source #

Get a static representation of a dynamic list.

For example, to convert a list of strings into a list of types:

>>> reifyList (\name f -> case name of { "int" -> f int ; "bool" -> f bool }) ["bool","int"] show
"[BoolRepr,IntRepr]"

(.:.) :: (HasMonad a, MonadResult a ~ e tp, MatchMonad a m, Applicative m) => a -> m (List e tps) -> m (List e (tp ': tps)) infixr 5 Source #

Create a typed list by appending an element to the front of another list.

nil :: Applicative m => m (List e '[]) Source #

Create an empty list.

Misc

comment :: Backend b => String -> SMT b () Source #

Inject a comment into the SMT command stream. Only useful when using the smtlib2-debug package to inspect the command stream.

simplify :: Backend b => Expr b tp -> SMT b (Expr b tp) Source #

Use the SMT solver to simplify a given expression.