Language.SMTLib2.Internals

Documentation

data SMTRequest response where

Constructors

SMTSetLogic :: String -> SMTRequest ()

SMTGetInfo :: SMTInfo i -> SMTRequest i

SMTSetOption :: SMTOption -> SMTRequest ()

SMTAssert :: SMTExpr Bool -> Maybe InterpolationGroup -> Maybe ClauseId -> SMTRequest ()

SMTCheckSat :: Maybe Tactic -> CheckSatLimits -> SMTRequest CheckSatResult

SMTDeclaredDataTypes :: SMTRequest DataTypeInfo

SMTDeclareDataTypes :: TypeCollection -> SMTRequest ()

SMTDeclareSort :: String -> Integer -> SMTRequest ()

SMTPush :: SMTRequest ()

SMTPop :: SMTRequest ()

SMTDefineFun :: (Args arg, SMTType res) => Maybe String -> Proxy arg -> ArgAnnotation arg -> SMTExpr res -> SMTRequest Integer

SMTDeclareFun :: FunInfo -> SMTRequest Integer

SMTGetValue :: SMTValue t => SMTExpr t -> SMTRequest t

SMTGetModel :: SMTRequest SMTModel

SMTGetProof :: SMTRequest (SMTExpr Bool)

SMTGetUnsatCore :: SMTRequest [ClauseId]

SMTSimplify :: SMTType t => SMTExpr t -> SMTRequest (SMTExpr t)

SMTGetInterpolant :: [InterpolationGroup] -> SMTRequest (SMTExpr Bool)

SMTInterpolate :: [SMTExpr Bool] -> SMTRequest [SMTExpr Bool]

SMTComment :: String -> SMTRequest ()

SMTExit :: SMTRequest ()

SMTApply :: Tactic -> SMTRequest [SMTExpr Bool]

SMTNameExpr :: SMTType t => String -> SMTExpr t -> SMTRequest Integer

SMTNewInterpolationGroup :: SMTRequest InterpolationGroup

SMTNewClauseId :: SMTRequest ClauseId

data SMTModel

Constructors

SMTModel

Fields

• modelFunctions :: Map Integer (Integer, [ProxyArg], SMTExpr Untyped)

Instances

Show SMTModel

Methods

showsPrec :: Int -> SMTModel -> ShowS

show :: SMTModel -> String

showList :: [SMTModel] -> ShowS

data CheckSatLimits

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

Constructors

CheckSatLimits

Fields

• limitTime :: Maybe Integer

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

• limitMemory :: Maybe Integer

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

Instances

Eq CheckSatLimits

Methods

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

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

Ord CheckSatLimits

Methods

compare :: CheckSatLimits -> CheckSatLimits -> Ordering

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

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

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

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

max :: CheckSatLimits -> CheckSatLimits -> CheckSatLimits

min :: CheckSatLimits -> CheckSatLimits -> CheckSatLimits

Show CheckSatLimits

Methods

showsPrec :: Int -> CheckSatLimits -> ShowS

show :: CheckSatLimits -> String

showList :: [CheckSatLimits] -> ShowS

data CheckSatResult

The result of a check-sat query

Constructors

Sat

The formula is satisfiable

Unsat

The formula is unsatisfiable

Unknown

The solver cannot determine the satisfiability of a formula

Instances

Eq CheckSatResult

Methods

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

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

Ord CheckSatResult

Methods

compare :: CheckSatResult -> CheckSatResult -> Ordering

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

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

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

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

max :: CheckSatResult -> CheckSatResult -> CheckSatResult

min :: CheckSatResult -> CheckSatResult -> CheckSatResult

Show CheckSatResult

Methods

showsPrec :: Int -> CheckSatResult -> ShowS

show :: CheckSatResult -> String

showList :: [CheckSatResult] -> ShowS

class Monad m => SMTBackend a m where

Minimal complete definition

smtHandle, smtGetNames, smtNextName

Methods

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

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

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

Instances

MonadIO m => SMTBackend SMTPipe m

Methods

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

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

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

Monad m => SMTBackend (AnyBackend m) m

Methods

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

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

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

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

Haskell types which can be represented in SMT

Minimal complete definition

getSort, asValueType, annotationFromSort, defaultExpr

Associated Types

type SMTAnnotation t

Methods

getSort :: t -> SMTAnnotation t -> Sort

asDataType :: t -> SMTAnnotation t -> Maybe (String, TypeCollection)

asValueType :: t -> SMTAnnotation t -> (forall v. SMTValue v => v -> SMTAnnotation v -> r) -> Maybe r

getProxyArgs :: t -> SMTAnnotation t -> [ProxyArg]

additionalConstraints :: t -> SMTAnnotation t -> Maybe (SMTExpr t -> [SMTExpr Bool])

annotationFromSort :: t -> Sort -> SMTAnnotation t

defaultExpr :: SMTAnnotation t -> SMTExpr t

data ArgumentSort' a

Constructors

ArgumentSort Integer

NormalSort (Sort' a)

type ArgumentSort = Fix ArgumentSort'

data Unmangling a

Constructors

PrimitiveUnmangling (Value -> SMTAnnotation a -> Maybe a)

ComplexUnmangling (forall m s. Monad m => (forall b. SMTValue b => s -> SMTExpr b -> SMTAnnotation b -> m (b, s)) -> s -> SMTExpr a -> SMTAnnotation a -> m (Maybe a, s))

data Mangling a

Constructors

PrimitiveMangling (a -> SMTAnnotation a -> Value)

ComplexMangling (a -> SMTAnnotation a -> SMTExpr a)

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

Haskell values which can be represented as SMT constants

Minimal complete definition

unmangle, mangle

Methods

unmangle :: Unmangling t

mangle :: Mangling t

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

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

class SMTType t => SMTOrd t where

Lifts the Ord class into SMT

Minimal complete definition

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

Methods

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

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

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

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

data SMTArray i v

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

Constructors

SMTArray

Instances

Eq (SMTArray i v)

Methods

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

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

Ord (SMTArray i v)

Methods

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

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

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

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

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

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

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

type SMTAnnotation (SMTArray idx val)

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

data FunInfo

Constructors

(Args arg, SMTType r) => FunInfo

Fields

• funInfoProxy :: Proxy (arg, r)
• funInfoArgAnn :: ArgAnnotation arg
• funInfoResAnn :: SMTAnnotation r
• funInfoName :: Maybe String

data AnyBackend m

Constructors

SMTBackend b m => AnyBackend b

Instances

Monad m => SMTBackend (AnyBackend m) m

Methods

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

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

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

data SMT' m a

The SMT monad used for communating with the SMT solver

Constructors

SMT

Fields

• runSMT :: forall b. SMTBackend b m => b -> m (a, b)

Instances

MonadTrans SMT'

Methods

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

Monad m => Monad (SMT' m)

Methods

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

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

return :: a -> SMT' m a

fail :: String -> SMT' m a

Functor m => Functor (SMT' m)

Methods

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

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

MonadFix m => MonadFix (SMT' m)

Methods

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

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

Methods

pure :: a -> SMT' m a

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

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

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

MonadIO m => MonadIO (SMT' m)

Methods

liftIO :: IO a -> SMT' m a

type SMT = SMT' IO

smtBackend :: Monad m => (forall b. SMTBackend b m => b -> m (res, b)) -> SMT' m res

data Untyped

Constructors

SMTType t => Untyped t

Instances

Eq Untyped

Methods

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

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

Ord Untyped

Methods

compare :: Untyped -> Untyped -> Ordering

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

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

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

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

max :: Untyped -> Untyped -> Untyped

min :: Untyped -> Untyped -> Untyped

type SMTAnnotation Untyped

type SMTAnnotation Untyped = ProxyArg

data UntypedValue

Constructors

SMTValue t => UntypedValue t

Instances

Eq UntypedValue

Methods

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

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

Ord UntypedValue

Methods

compare :: UntypedValue -> UntypedValue -> Ordering

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

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

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

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

max :: UntypedValue -> UntypedValue -> UntypedValue

min :: UntypedValue -> UntypedValue -> UntypedValue

Show UntypedValue

Methods

showsPrec :: Int -> UntypedValue -> ShowS

show :: UntypedValue -> String

showList :: [UntypedValue] -> ShowS

type SMTAnnotation UntypedValue

type SMTAnnotation UntypedValue = ProxyArgValue

data SMTExpr t where

An abstract SMT expression

Constructors

Var :: SMTType t => Integer -> SMTAnnotation t -> SMTExpr t

QVar :: SMTType t => Integer -> Integer -> SMTAnnotation t -> SMTExpr t

FunArg :: SMTType t => Integer -> SMTAnnotation t -> SMTExpr t

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

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

Forall :: Integer -> [ProxyArg] -> SMTExpr Bool -> SMTExpr Bool

Exists :: Integer -> [ProxyArg] -> SMTExpr Bool -> SMTExpr Bool

Let :: Integer -> [SMTExpr Untyped] -> SMTExpr b -> SMTExpr b

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

Named :: SMTExpr a -> Integer -> SMTExpr a

InternalObj :: (SMTType t, Typeable a, Ord a, Show a) => a -> SMTAnnotation t -> SMTExpr t

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

UntypedExprValue :: SMTValue t => SMTExpr t -> SMTExpr UntypedValue

Instances

Show (SMTExpr t)

Methods

showsPrec :: Int -> SMTExpr t -> ShowS

show :: SMTExpr t -> String

showList :: [SMTExpr t] -> ShowS

type Unpacked (SMTExpr a)

type Unpacked (SMTExpr a) = a

type ArgAnnotation (SMTExpr a)

type ArgAnnotation (SMTExpr a) = SMTAnnotation a

type Lifted [SMTExpr a] i

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

type Lifted (SMTExpr a) i

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

data Sort' a

Constructors

BoolSort

IntSort

RealSort

BVSort

Fields

• bvSortWidth :: Integer
• bvSortUntyped :: Bool

ArraySort [a] a

NamedSort String [a]

Instances

Functor Sort'

Methods

fmap :: (a -> b) -> Sort' a -> Sort' b

(<$) :: a -> Sort' b -> Sort' a

Foldable Sort'

Methods

fold :: Monoid m => Sort' m -> m

foldMap :: Monoid m => (a -> m) -> Sort' a -> m

foldr :: (a -> b -> b) -> b -> Sort' a -> b

foldr' :: (a -> b -> b) -> b -> Sort' a -> b

foldl :: (b -> a -> b) -> b -> Sort' a -> b

foldl' :: (b -> a -> b) -> b -> Sort' a -> b

foldr1 :: (a -> a -> a) -> Sort' a -> a

foldl1 :: (a -> a -> a) -> Sort' a -> a

toList :: Sort' a -> [a]

null :: Sort' a -> Bool

length :: Sort' a -> Int

elem :: Eq a => a -> Sort' a -> Bool

maximum :: Ord a => Sort' a -> a

minimum :: Ord a => Sort' a -> a

sum :: Num a => Sort' a -> a

product :: Num a => Sort' a -> a

Traversable Sort'

Methods

traverse :: Applicative f => (a -> f b) -> Sort' a -> f (Sort' b)

sequenceA :: Applicative f => Sort' (f a) -> f (Sort' a)

mapM :: Monad m => (a -> m b) -> Sort' a -> m (Sort' b)

sequence :: Monad m => Sort' (m a) -> m (Sort' a)

Eq a => Eq (Sort' a)

Methods

(==) :: Sort' a -> Sort' a -> Bool

(/=) :: Sort' a -> Sort' a -> Bool

Ord a => Ord (Sort' a)

Methods

compare :: Sort' a -> Sort' a -> Ordering

(<) :: Sort' a -> Sort' a -> Bool

(<=) :: Sort' a -> Sort' a -> Bool

(>) :: Sort' a -> Sort' a -> Bool

(>=) :: Sort' a -> Sort' a -> Bool

max :: Sort' a -> Sort' a -> Sort' a

min :: Sort' a -> Sort' a -> Sort' a

Show a => Show (Sort' a)

Methods

showsPrec :: Int -> Sort' a -> ShowS

show :: Sort' a -> String

showList :: [Sort' a] -> ShowS

type Sort = Fix Sort'

data Value

Constructors

BoolValue Bool

IntValue Integer

RealValue (Ratio Integer)

BVValue

Fields

• bvValueWidth :: Integer
• bvValueValue :: Integer

ConstrValue String [Value] (Maybe (String, [Sort]))

Instances

Eq Value

Methods

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

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

Ord Value

Methods

compare :: Value -> Value -> Ordering

(<) :: Value -> Value -> Bool

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

(>) :: Value -> Value -> Bool

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

max :: Value -> Value -> Value

min :: Value -> Value -> Value

Show Value

Methods

showsPrec :: Int -> Value -> ShowS

show :: Value -> String

showList :: [Value] -> ShowS

data SMTFunction arg res where

Constructors

SMTEq :: SMTType a => SMTFunction [SMTExpr a] Bool

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

SMTFun :: (Args arg, SMTType res) => Integer -> SMTAnnotation res -> SMTFunction arg res

SMTBuiltIn :: (Liftable arg, SMTType res) => String -> SMTAnnotation res -> SMTFunction arg res

SMTOrd :: SMTArith a => SMTOrdOp -> SMTFunction (SMTExpr a, SMTExpr a) Bool

SMTArith :: SMTArith a => SMTArithOp -> SMTFunction [SMTExpr a] a

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

SMTIntArith :: SMTIntArithOp -> SMTFunction (SMTExpr Integer, SMTExpr Integer) Integer

SMTDivide :: SMTFunction (SMTExpr Rational, SMTExpr Rational) Rational

SMTNeg :: (SMTType a, Num a) => SMTFunction (SMTExpr a) a

SMTAbs :: (SMTType a, Num a) => SMTFunction (SMTExpr a) a

SMTNot :: SMTFunction (SMTExpr Bool) Bool

SMTLogic :: SMTLogicOp -> SMTFunction [SMTExpr Bool] Bool

SMTDistinct :: SMTType a => SMTFunction [SMTExpr a] Bool

SMTToReal :: SMTFunction (SMTExpr Integer) Rational

SMTToInt :: SMTFunction (SMTExpr Rational) Integer

SMTITE :: SMTType a => SMTFunction (SMTExpr Bool, SMTExpr a, SMTExpr a) a

SMTBVComp :: IsBitVector a => SMTBVCompOp -> SMTFunction (SMTExpr (BitVector a), SMTExpr (BitVector a)) Bool

SMTBVBin :: IsBitVector a => SMTBVBinOp -> SMTFunction (SMTExpr (BitVector a), SMTExpr (BitVector a)) (BitVector a)

SMTBVUn :: IsBitVector a => SMTBVUnOp -> SMTFunction (SMTExpr (BitVector a)) (BitVector a)

SMTSelect :: (Liftable i, SMTType v) => SMTFunction (SMTExpr (SMTArray i v), i) v

SMTStore :: (Liftable i, SMTType v) => SMTFunction (SMTExpr (SMTArray i v), i, SMTExpr v) (SMTArray i v)

SMTConstArray :: (Args i, SMTType v) => ArgAnnotation i -> SMTFunction (SMTExpr v) (SMTArray i v)

SMTConcat :: Concatable a b => SMTFunction (SMTExpr (BitVector a), SMTExpr (BitVector b)) (BitVector (ConcatResult a b))

SMTExtract :: (TypeableNat start, TypeableNat len, Extractable from len') => Proxy start -> Proxy len -> SMTFunction (SMTExpr (BitVector from)) (BitVector len')

SMTConstructor :: (Args arg, SMTType dt) => Constructor arg dt -> SMTFunction arg dt

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

SMTFieldSel :: (SMTType a, SMTType f) => Field a f -> SMTFunction (SMTExpr a) f

SMTDivisible :: Integer -> SMTFunction (SMTExpr Integer) Bool

Instances

Show (SMTFunction arg res)

Methods

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

show :: SMTFunction arg res -> String

showList :: [SMTFunction arg res] -> ShowS

class SMTValue (BitVector a) => IsBitVector a where

Minimal complete definition

getBVSize

Methods

getBVSize :: Proxy a -> SMTAnnotation (BitVector a) -> Integer

class (IsBitVector a, IsBitVector b, IsBitVector (ConcatResult a b)) => Concatable a b where

Minimal complete definition

concatAnnotation

Associated Types

type ConcatResult a b

Methods

concatAnnotation :: a -> b -> SMTAnnotation (BitVector a) -> SMTAnnotation (BitVector b) -> SMTAnnotation (BitVector (ConcatResult a b))

class (IsBitVector a, IsBitVector b) => Extractable a b where

Minimal complete definition

extractAnn, getExtractLen

Methods

extractAnn :: a -> b -> Integer -> SMTAnnotation (BitVector a) -> SMTAnnotation (BitVector b)

getExtractLen :: a -> b -> SMTAnnotation (BitVector b) -> Integer

data Constructor arg res

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

Constructors

Constructor [ProxyArg] DataType Constr

Instances

Show (Constructor arg res)

Methods

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

show :: Constructor arg res -> String

showList :: [Constructor arg res] -> ShowS

data Field a f

Represents a field of the datatype a of the type f

Constructors

Field [ProxyArg] DataType Constr DataField

Instances

Show (Field a f)

Methods

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

show :: Field a f -> String

showList :: [Field a f] -> ShowS

newtype InterpolationGroup

Constructors

InterpolationGroup Integer

Instances

Eq InterpolationGroup

Methods

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

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

Ord InterpolationGroup

Methods

compare :: InterpolationGroup -> InterpolationGroup -> Ordering

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

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

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

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

max :: InterpolationGroup -> InterpolationGroup -> InterpolationGroup

min :: InterpolationGroup -> InterpolationGroup -> InterpolationGroup

Show InterpolationGroup

Methods

showsPrec :: Int -> InterpolationGroup -> ShowS

show :: InterpolationGroup -> String

showList :: [InterpolationGroup] -> ShowS

newtype ClauseId

Identifies a clause in an unsatisfiable core

Constructors

ClauseId Integer

Instances

Eq ClauseId

Methods

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

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

Ord ClauseId

Methods

compare :: ClauseId -> ClauseId -> Ordering

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

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

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

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

max :: ClauseId -> ClauseId -> ClauseId

min :: ClauseId -> ClauseId -> ClauseId

Show ClauseId

Methods

showsPrec :: Int -> ClauseId -> ShowS

show :: ClauseId -> String

showList :: [ClauseId] -> ShowS

data SMTOption

Options controling the behaviour of the SMT solver

Constructors

PrintSuccess Bool

Whether or not to print "success" after each operation

ProduceModels Bool

Produce a satisfying assignment after each successful checkSat

ProduceProofs Bool

Produce a proof of unsatisfiability after each failed checkSat

ProduceUnsatCores Bool

Enable the querying of unsatisfiable cores after a failed checkSat

ProduceInterpolants Bool

Enable the generation of craig interpolants

Instances

Eq SMTOption

Methods

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

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

Ord SMTOption

Methods

compare :: SMTOption -> SMTOption -> Ordering

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

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

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

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

max :: SMTOption -> SMTOption -> SMTOption

min :: SMTOption -> SMTOption -> SMTOption

Show SMTOption

Methods

showsPrec :: Int -> SMTOption -> ShowS

show :: SMTOption -> String

showList :: [SMTOption] -> ShowS

data SMTInfo i where

Constructors

SMTSolverName :: SMTInfo String

SMTSolverVersion :: SMTInfo String

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

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

Minimal complete definition

foldsExprs, extractArgAnnotation, toArgs, getTypes, getArgAnnotation

Associated Types

type ArgAnnotation a

Methods

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

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

extractArgAnnotation :: a -> ArgAnnotation a

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

fromArgs :: a -> [SMTExpr Untyped]

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

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

Instances

Args ()

Associated Types

type ArgAnnotation () :: *

Methods

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

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

extractArgAnnotation :: () -> ArgAnnotation ()

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

fromArgs :: () -> [SMTExpr Untyped]

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

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

getSorts :: Args a => a -> ArgAnnotation a -> [Sort]

foldExprsId :: Args a => (forall t. SMTType t => s -> SMTExpr t -> SMTAnnotation t -> (s, SMTExpr t)) -> s -> a -> ArgAnnotation a -> (s, a)

foldsExprsId :: Args a => (forall t. SMTType t => s -> [(SMTExpr t, b)] -> SMTAnnotation t -> (s, [SMTExpr t], SMTExpr t)) -> s -> [(a, b)] -> ArgAnnotation a -> (s, [a], a)

class Args a => Liftable a where

Minimal complete definition

getLiftedArgumentAnn, inferLiftedAnnotation, getConstraint

Associated Types

type Lifted a i

Methods

getLiftedArgumentAnn :: a -> i -> ArgAnnotation a -> ArgAnnotation i -> ArgAnnotation (Lifted a i)

inferLiftedAnnotation :: a -> i -> ArgAnnotation (Lifted a i) -> (ArgAnnotation i, ArgAnnotation a)

getConstraint :: Args i => p (a, i) -> Dict (Liftable (Lifted a i))

argSorts :: Args a => a -> ArgAnnotation a -> [Sort]

unpackArgs :: Args a => (forall t. SMTType t => SMTExpr t -> SMTAnnotation t -> s -> (c, s)) -> a -> ArgAnnotation a -> s -> ([c], s)

class Args a => LiftArgs a where

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

Minimal complete definition

liftArgs, unliftArgs

Associated Types

type Unpacked a

Methods

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

Converts a haskell value into its SMT representation.

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

Converts a SMT representation back into a haskell value.

firstJust :: [Maybe a] -> Maybe a

getUndef :: SMTExpr t -> t

getFunUndef :: SMTFunction arg res -> (arg, res)

getArrayUndef :: Args i => SMTExpr (SMTArray i v) -> (i, Unpacked i, v)

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

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

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

funInfoSort :: FunInfo -> Sort

funInfoArgSorts :: FunInfo -> [Sort]

argsSignature :: Args a => a -> ArgAnnotation a -> [Sort]

argumentSortToSort :: Monad m => (Integer -> m Sort) -> ArgumentSort -> m Sort

sortToArgumentSort :: Sort -> ArgumentSort

declareType :: (Monad m, SMTType t) => t -> SMTAnnotation t -> SMT' m ()

data DataTypeInfo

Constructors

DataTypeInfo

Fields

• structures :: [TypeCollection]
• datatypes :: Map String (DataType, TypeCollection)
• constructors :: Map String (Constr, DataType, TypeCollection)
• fields :: Map String (DataField, Constr, DataType, TypeCollection)

data TypeCollection

Constructors

TypeCollection

Fields

• argCount :: Integer
• dataTypes :: [DataType]

data ProxyArg

Constructors

SMTType t => ProxyArg t (SMTAnnotation t)

Instances

Eq ProxyArg

Methods

(==) :: ProxyArg -> ProxyArg -> Bool

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

Ord ProxyArg

Methods

compare :: ProxyArg -> ProxyArg -> Ordering

(<) :: ProxyArg -> ProxyArg -> Bool

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

(>) :: ProxyArg -> ProxyArg -> Bool

(>=) :: ProxyArg -> ProxyArg -> Bool

max :: ProxyArg -> ProxyArg -> ProxyArg

min :: ProxyArg -> ProxyArg -> ProxyArg

Show ProxyArg

Methods

showsPrec :: Int -> ProxyArg -> ShowS

show :: ProxyArg -> String

showList :: [ProxyArg] -> ShowS

data ProxyArgValue

Constructors

SMTValue t => ProxyArgValue t (SMTAnnotation t)

Instances

Eq ProxyArgValue

Methods

(==) :: ProxyArgValue -> ProxyArgValue -> Bool

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

Ord ProxyArgValue

Methods

compare :: ProxyArgValue -> ProxyArgValue -> Ordering

(<) :: ProxyArgValue -> ProxyArgValue -> Bool

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

(>) :: ProxyArgValue -> ProxyArgValue -> Bool

(>=) :: ProxyArgValue -> ProxyArgValue -> Bool

max :: ProxyArgValue -> ProxyArgValue -> ProxyArgValue

min :: ProxyArgValue -> ProxyArgValue -> ProxyArgValue

Show ProxyArgValue

Methods

showsPrec :: Int -> ProxyArgValue -> ShowS

show :: ProxyArgValue -> String

showList :: [ProxyArgValue] -> ShowS

withProxyArg :: ProxyArg -> (forall t. SMTType t => t -> SMTAnnotation t -> a) -> a

withProxyArgValue :: ProxyArgValue -> (forall t. SMTValue t => t -> SMTAnnotation t -> a) -> a

data AnyValue

Constructors

SMTType t => AnyValue [ProxyArg] t (SMTAnnotation t)

withAnyValue :: AnyValue -> (forall t. SMTType t => [ProxyArg] -> t -> SMTAnnotation t -> a) -> a

castAnyValue :: SMTType t => AnyValue -> Maybe (t, SMTAnnotation t)

data DataType

Constructors

DataType

Fields

• dataTypeName :: String
• dataTypeConstructors :: [Constr]
• dataTypeGetUndefined :: forall r. [ProxyArg] -> (forall t. SMTType t => t -> SMTAnnotation t -> r) -> r

data Constr

Constructors

Constr

Fields

• conName :: String
• conFields :: [DataField]
• construct :: forall r. [Maybe ProxyArg] -> [AnyValue] -> (forall t. SMTType t => [ProxyArg] -> t -> SMTAnnotation t -> r) -> r
• conUndefinedArgs :: forall r. [ProxyArg] -> (forall arg. Args arg => arg -> ArgAnnotation arg -> r) -> r
• conTest :: forall t. SMTType t => [ProxyArg] -> t -> Bool

data DataField

Constructors

DataField

Fields

• fieldName :: String
• fieldSort :: ArgumentSort
• fieldGet :: forall r t. SMTType t => [ProxyArg] -> t -> (forall f. SMTType f => f -> SMTAnnotation f -> r) -> r

emptyDataTypeInfo :: DataTypeInfo

containsTypeCollection :: TypeCollection -> DataTypeInfo -> Bool

addDataTypeStructure :: TypeCollection -> DataTypeInfo -> DataTypeInfo

getNewTypeCollections :: SMTType t => Proxy t -> SMTAnnotation t -> DataTypeInfo -> ([TypeCollection], DataTypeInfo)

Get all the type collections which are not yet declared from a type.

asNamedSort :: Sort -> Maybe (String, [Sort])

escapeName :: Either (String, Integer) Integer -> String

escapeName' :: String -> String

unescapeName :: String -> Maybe (Either (String, Integer) Integer)

unescapeName' :: String -> Maybe (String, Integer)

data SMTState

Constructors

SMTState

Fields

• nextVar :: Integer
• nextInterpolationGroup :: Integer
• nextClauseId :: Integer
• allVars :: Map Integer (FunInfo, Integer)
• namedVars :: Map (String, Integer) Integer
• nameCount :: Map String Integer
• declaredDataTypes :: DataTypeInfo

emptySMTState :: SMTState

smtStateAddFun :: FunInfo -> SMTState -> (Integer, String, SMTState)

data Z

Constructors

Z

Instances

TypeableNat Z

Methods

reflectNat :: Proxy * Z -> Integer -> Integer

type Add Z n

type Add Z n = n

data S a

Constructors

S

Instances

TypeableNat n => TypeableNat (S n)

Methods

reflectNat :: Proxy * (S n) -> Integer -> Integer

type Add (S n1) n2

type Add (S n1) n2 = S (Add n1 n2)

class Typeable a => TypeableNat a where

Minimal complete definition

reflectNat

Methods

reflectNat :: Proxy a -> Integer -> Integer

Instances

TypeableNat Z

Methods

reflectNat :: Proxy * Z -> Integer -> Integer

TypeableNat n => TypeableNat (S n)

Methods

reflectNat :: Proxy * (S n) -> Integer -> Integer

type family Add n1 n2

Instances

type Add Z n

type Add Z n = n

type Add (S n1) n2

type Add (S n1) n2 = S (Add n1 n2)

data BVUntyped

Constructors

BVUntyped

Instances

Eq BVUntyped

Methods

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

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

Ord BVUntyped

Methods

compare :: BVUntyped -> BVUntyped -> Ordering

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

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

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

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

max :: BVUntyped -> BVUntyped -> BVUntyped

min :: BVUntyped -> BVUntyped -> BVUntyped

Show BVUntyped

Methods

showsPrec :: Int -> BVUntyped -> ShowS

show :: BVUntyped -> String

showList :: [BVUntyped] -> ShowS

type ConcatResult BVUntyped BVUntyped

type ConcatResult BVUntyped BVUntyped = BVUntyped

type ConcatResult BVUntyped (BVTyped n2)

type ConcatResult BVUntyped (BVTyped n2) = BVUntyped

type SMTAnnotation (BitVector BVUntyped)

type SMTAnnotation (BitVector BVUntyped) = Integer

type ConcatResult (BVTyped n1) BVUntyped

type ConcatResult (BVTyped n1) BVUntyped = BVUntyped

data BVTyped n

Constructors

BVTyped

Instances

Eq (BVTyped n)

Methods

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

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

Ord (BVTyped n)

Methods

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

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

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

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

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

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

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

Show (BVTyped n)

Methods

showsPrec :: Int -> BVTyped n -> ShowS

show :: BVTyped n -> String

showList :: [BVTyped n] -> ShowS

type ConcatResult BVUntyped (BVTyped n2)

type ConcatResult BVUntyped (BVTyped n2) = BVUntyped

type SMTAnnotation (BitVector (BVTyped n))

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

type ConcatResult (BVTyped n1) BVUntyped

type ConcatResult (BVTyped n1) BVUntyped = BVUntyped

type ConcatResult (BVTyped n1) (BVTyped n2)

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

reifyNat :: (Num a, Ord a) => a -> (forall n. TypeableNat n => Proxy n -> r) -> r

reifySum :: (Num a, Ord a) => a -> a -> (forall n1 n2. (TypeableNat n1, TypeableNat n2, TypeableNat (Add n1 n2)) => Proxy n1 -> Proxy n2 -> Proxy (Add n1 n2) -> r) -> r

reifyExtract :: (Num a, Ord a) => a -> a -> a -> (forall n1 n2 n3 n4. (TypeableNat n1, TypeableNat n2, TypeableNat n3, TypeableNat n4, Add n4 n2 ~ S n3) => Proxy n1 -> Proxy n2 -> Proxy n3 -> Proxy n4 -> r) -> r

data BitVector b

Constructors

BitVector Integer

Instances

Enum (BitVector a)

Methods

succ :: BitVector a -> BitVector a

pred :: BitVector a -> BitVector a

toEnum :: Int -> BitVector a

fromEnum :: BitVector a -> Int

enumFrom :: BitVector a -> [BitVector a]

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

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

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

Eq (BitVector b)

Methods

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

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

Ord (BitVector b)

Methods

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

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

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

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

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

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

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

Show (BitVector a)

Methods

showsPrec :: Int -> BitVector a -> ShowS

show :: BitVector a -> String

showList :: [BitVector a] -> ShowS

type SMTAnnotation (BitVector (BVTyped n))

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

type SMTAnnotation (BitVector BVUntyped)

type SMTAnnotation (BitVector BVUntyped) = Integer

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

type BV8 = BitVector (BVTyped N8)

type BV16 = BitVector (BVTyped N16)

type BV32 = BitVector (BVTyped N32)

type BV64 = BitVector (BVTyped N64)

newtype Bound

Constructors

Bound Integer

Instances

Eq Bound

Methods

(==) :: Bound -> Bound -> Bool

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

Ord Bound

Methods

compare :: Bound -> Bound -> Ordering

(<) :: Bound -> Bound -> Bool

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

(>) :: Bound -> Bound -> Bool

(>=) :: Bound -> Bound -> Bool

max :: Bound -> Bound -> Bound

min :: Bound -> Bound -> Bound

Show Bound

Methods

showsPrec :: Int -> Bound -> ShowS

show :: Bound -> String

showList :: [Bound] -> ShowS

showExpr :: Int -> SMTExpr t -> ShowS

noLimits :: CheckSatLimits

newtype Quantified

Constructors

Quantified Integer

Instances

Eq Quantified

Methods

(==) :: Quantified -> Quantified -> Bool

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

Ord Quantified

Methods

compare :: Quantified -> Quantified -> Ordering

(<) :: Quantified -> Quantified -> Bool

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

(>) :: Quantified -> Quantified -> Bool

(>=) :: Quantified -> Quantified -> Bool

max :: Quantified -> Quantified -> Quantified

min :: Quantified -> Quantified -> Quantified

Show Quantified

Methods

showsPrec :: Int -> Quantified -> ShowS

show :: Quantified -> String

showList :: [Quantified] -> ShowS

quantificationLevel :: SMTExpr t -> Integer

inferSorts :: ArgumentSort -> Sort -> Map Integer Sort -> Map Integer Sort

valueSort :: DataTypeInfo -> Value -> Sort