-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | A type-safe interface to communicate with an SMT solver.
--   
--   A type-safe interface to communicate with an SMT solver.
@package smtlib2
@version 0.3


-- | This module is used to express the fact that any tuple which is
--   composed only from empty tuples holds the same amount of information
--   as an empty tuple.
module Data.Unit

-- | The unit class expresses the fact that all tuples composed from only
--   empty tuples hold the same amount of information as the empty tuple
--   and can thus all be constructed by a call to <a>unit</a>.
class Unit t

-- | Constructs a unit type
unit :: Unit t => t
instance Data.Unit.Unit ()
instance (Data.Unit.Unit a, Data.Unit.Unit b) => Data.Unit.Unit (a, b)
instance (Data.Unit.Unit a, Data.Unit.Unit b, Data.Unit.Unit c) => Data.Unit.Unit (a, b, c)
instance (Data.Unit.Unit a, Data.Unit.Unit b, Data.Unit.Unit c, Data.Unit.Unit d) => Data.Unit.Unit (a, b, c, d)
instance (Data.Unit.Unit a, Data.Unit.Unit b, Data.Unit.Unit c, Data.Unit.Unit d, Data.Unit.Unit e) => Data.Unit.Unit (a, b, c, d, e)
instance (Data.Unit.Unit a, Data.Unit.Unit b, Data.Unit.Unit c, Data.Unit.Unit d, Data.Unit.Unit e, Data.Unit.Unit f) => Data.Unit.Unit (a, b, c, d, e, f)

module Language.SMTLib2.Internals.Operators
data SMTOrdOp
Ge :: SMTOrdOp
Gt :: SMTOrdOp
Le :: SMTOrdOp
Lt :: SMTOrdOp
data SMTArithOp
Plus :: SMTArithOp
Mult :: SMTArithOp
data SMTIntArithOp
Div :: SMTIntArithOp
Mod :: SMTIntArithOp
Rem :: SMTIntArithOp
data SMTLogicOp
And :: SMTLogicOp
Or :: SMTLogicOp
XOr :: SMTLogicOp
Implies :: SMTLogicOp
data SMTBVCompOp
BVULE :: SMTBVCompOp
BVULT :: SMTBVCompOp
BVUGE :: SMTBVCompOp
BVUGT :: SMTBVCompOp
BVSLE :: SMTBVCompOp
BVSLT :: SMTBVCompOp
BVSGE :: SMTBVCompOp
BVSGT :: SMTBVCompOp
data SMTBVBinOp
BVAdd :: SMTBVBinOp
BVSub :: SMTBVBinOp
BVMul :: SMTBVBinOp
BVURem :: SMTBVBinOp
BVSRem :: SMTBVBinOp
BVUDiv :: SMTBVBinOp
BVSDiv :: SMTBVBinOp
BVSHL :: SMTBVBinOp
BVLSHR :: SMTBVBinOp
BVASHR :: SMTBVBinOp
BVXor :: SMTBVBinOp
BVAnd :: SMTBVBinOp
BVOr :: SMTBVBinOp
data SMTBVUnOp
BVNot :: SMTBVUnOp
BVNeg :: SMTBVUnOp
instance GHC.Show.Show Language.SMTLib2.Internals.Operators.SMTBVUnOp
instance GHC.Classes.Ord Language.SMTLib2.Internals.Operators.SMTBVUnOp
instance GHC.Classes.Eq Language.SMTLib2.Internals.Operators.SMTBVUnOp
instance GHC.Show.Show Language.SMTLib2.Internals.Operators.SMTBVBinOp
instance GHC.Classes.Ord Language.SMTLib2.Internals.Operators.SMTBVBinOp
instance GHC.Classes.Eq Language.SMTLib2.Internals.Operators.SMTBVBinOp
instance GHC.Show.Show Language.SMTLib2.Internals.Operators.SMTBVCompOp
instance GHC.Classes.Ord Language.SMTLib2.Internals.Operators.SMTBVCompOp
instance GHC.Classes.Eq Language.SMTLib2.Internals.Operators.SMTBVCompOp
instance GHC.Show.Show Language.SMTLib2.Internals.Operators.SMTLogicOp
instance GHC.Classes.Ord Language.SMTLib2.Internals.Operators.SMTLogicOp
instance GHC.Classes.Eq Language.SMTLib2.Internals.Operators.SMTLogicOp
instance GHC.Show.Show Language.SMTLib2.Internals.Operators.SMTIntArithOp
instance GHC.Classes.Ord Language.SMTLib2.Internals.Operators.SMTIntArithOp
instance GHC.Classes.Eq Language.SMTLib2.Internals.Operators.SMTIntArithOp
instance GHC.Show.Show Language.SMTLib2.Internals.Operators.SMTArithOp
instance GHC.Classes.Ord Language.SMTLib2.Internals.Operators.SMTArithOp
instance GHC.Classes.Eq Language.SMTLib2.Internals.Operators.SMTArithOp
instance GHC.Show.Show Language.SMTLib2.Internals.Operators.SMTOrdOp
instance GHC.Classes.Ord Language.SMTLib2.Internals.Operators.SMTOrdOp
instance GHC.Classes.Eq Language.SMTLib2.Internals.Operators.SMTOrdOp

module Language.SMTLib2.Strategy
data Tactic
Skip :: Tactic
AndThen :: [Tactic] -> Tactic
OrElse :: [Tactic] -> Tactic
ParOr :: [Tactic] -> Tactic
ParThen :: Tactic -> Tactic -> Tactic
TryFor :: Tactic -> Integer -> Tactic
If :: (Probe Bool) -> Tactic -> Tactic -> Tactic
FailIf :: (Probe Bool) -> Tactic
UsingParams :: (BuiltInTactic p) -> [p] -> Tactic
data Probe a
ProbeBoolConst :: Bool -> Probe Bool
ProbeIntConst :: Integer -> Probe Integer
ProbeAnd :: [Probe Bool] -> Probe Bool
ProbeOr :: [Probe Bool] -> Probe Bool
ProbeNot :: Probe Bool -> Probe Bool
ProbeEq :: Probe a -> Probe a -> Probe Bool
ProbeCompare :: SMTOrdOp -> Probe Integer -> Probe Integer -> Probe Bool
IsPB :: Probe Bool
ArithMaxDeg :: Probe Integer
ArithAvgDeg :: Probe Integer
ArithMaxBW :: Probe Integer
ArithAvgBW :: Probe Integer
IsQFLIA :: Probe Bool
IsQFLRA :: Probe Bool
IsQFLIRA :: Probe Bool
IsILP :: Probe Bool
IsQFNIA :: Probe Bool
IsQFNRA :: Probe Bool
IsNIA :: Probe Bool
IsNRA :: Probe Bool
IsUnbounded :: Probe Bool
Memory :: Probe Integer
Depth :: Probe Integer
Size :: Probe Integer
NumExprs :: Probe Integer
NumConsts :: Probe Integer
NumBoolConsts :: Probe Integer
NumArithConsts :: Probe Integer
NumBVConsts :: Probe Integer
ProduceProofs :: Probe Bool
ProduceModel :: Probe Bool
ProduceUnsatCores :: Probe Bool
HasPatterns :: Probe Bool
IsPropositional :: Probe Bool
IsQFBV :: Probe Bool
IsQFBVEQ :: Probe Bool
data AnyPar
ParBool :: Bool -> AnyPar
ParInt :: Integer -> AnyPar
ParDouble :: Double -> AnyPar
data BuiltInTactic p
QFLRATactic :: BuiltInTactic QFLRATacticP
CustomTactic :: String -> BuiltInTactic (String, AnyPar)
data QFLRATacticP
ArithBranchCutRatio :: Integer -> QFLRATacticP
instance GHC.Show.Show Language.SMTLib2.Strategy.QFLRATacticP
instance GHC.Show.Show Language.SMTLib2.Strategy.AnyPar
instance GHC.Show.Show Language.SMTLib2.Strategy.Tactic
instance GHC.Show.Show (Language.SMTLib2.Strategy.BuiltInTactic p)
instance GHC.Show.Show a => GHC.Show.Show (Language.SMTLib2.Strategy.Probe a)

module Language.SMTLib2.Internals
data SMTRequest response
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 :: Maybe String -> Proxy arg -> ArgAnnotation arg -> SMTExpr res -> SMTRequest Integer
SMTDeclareFun :: FunInfo -> SMTRequest Integer
SMTGetValue :: SMTExpr t -> SMTRequest t
SMTGetModel :: SMTRequest SMTModel
SMTGetProof :: SMTRequest (SMTExpr Bool)
SMTGetUnsatCore :: SMTRequest [ClauseId]
SMTSimplify :: 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 :: String -> SMTExpr t -> SMTRequest Integer
SMTNewInterpolationGroup :: SMTRequest InterpolationGroup
SMTNewClauseId :: SMTRequest ClauseId
data SMTModel
SMTModel :: Map Integer (Integer, [ProxyArg], SMTExpr Untyped) -> SMTModel
[modelFunctions] :: SMTModel -> Map Integer (Integer, [ProxyArg], SMTExpr Untyped)

-- | Describe limits on the ressources that an SMT-solver can use
data CheckSatLimits
CheckSatLimits :: Maybe Integer -> Maybe Integer -> CheckSatLimits

-- | A limit on the amount of time the solver can spend on the problem (in
--   milliseconds)
[limitTime] :: CheckSatLimits -> Maybe Integer

-- | A limit on the amount of memory the solver can use (in megabytes)
[limitMemory] :: CheckSatLimits -> Maybe Integer

-- | The result of a check-sat query
data CheckSatResult

-- | The formula is satisfiable
Sat :: CheckSatResult

-- | The formula is unsatisfiable
Unsat :: CheckSatResult

-- | The solver cannot determine the satisfiability of a formula
Unknown :: CheckSatResult
class Monad m => SMTBackend a m
smtHandle :: (SMTBackend a m, Typeable response) => a -> SMTRequest response -> m (response, a)
smtGetNames :: SMTBackend a m => a -> m (Integer -> String)
smtNextName :: SMTBackend a m => a -> m (Maybe String -> String)

-- | Haskell types which can be represented in SMT
class (Ord t, Typeable t, Ord (SMTAnnotation t), Typeable (SMTAnnotation t), Show (SMTAnnotation t)) => SMTType t where type family SMTAnnotation t asDataType _ _ = Nothing getProxyArgs _ _ = [] additionalConstraints _ _ = Nothing
getSort :: SMTType t => t -> SMTAnnotation t -> Sort
asDataType :: SMTType t => t -> SMTAnnotation t -> Maybe (String, TypeCollection)
asValueType :: SMTType t => t -> SMTAnnotation t -> (forall v. SMTValue v => v -> SMTAnnotation v -> r) -> Maybe r
getProxyArgs :: SMTType t => t -> SMTAnnotation t -> [ProxyArg]
additionalConstraints :: SMTType t => t -> SMTAnnotation t -> Maybe (SMTExpr t -> [SMTExpr Bool])
annotationFromSort :: SMTType t => t -> Sort -> SMTAnnotation t
defaultExpr :: SMTType t => SMTAnnotation t -> SMTExpr t
data ArgumentSort' a
ArgumentSort :: Integer -> ArgumentSort' a
NormalSort :: (Sort' a) -> ArgumentSort' a
type ArgumentSort = Fix ArgumentSort'
data Unmangling a
PrimitiveUnmangling :: (Value -> SMTAnnotation a -> Maybe a) -> Unmangling 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)) -> Unmangling a
data Mangling a
PrimitiveMangling :: (a -> SMTAnnotation a -> Value) -> Mangling a
ComplexMangling :: (a -> SMTAnnotation a -> SMTExpr a) -> Mangling a

-- | Haskell values which can be represented as SMT constants
class (SMTType t, Show t) => SMTValue t
unmangle :: SMTValue t => Unmangling t
mangle :: SMTValue t => Mangling t

-- | A type class for all types which support arithmetic operations in SMT
class (SMTValue t, Num t, SMTAnnotation t ~ ()) => SMTArith t

-- | Lifts the <a>Ord</a> class into SMT
class (SMTType t) => SMTOrd t
(.<.) :: SMTOrd t => SMTExpr t -> SMTExpr t -> SMTExpr Bool
(.>=.) :: SMTOrd t => SMTExpr t -> SMTExpr t -> SMTExpr Bool
(.>.) :: SMTOrd t => SMTExpr t -> SMTExpr t -> SMTExpr Bool
(.<=.) :: SMTOrd t => SMTExpr t -> SMTExpr t -> SMTExpr Bool

-- | An array which maps indices of type <i>i</i> to elements of type
--   <i>v</i>.
data SMTArray (i :: *) (v :: *)
SMTArray :: SMTArray
data FunInfo
FunInfo :: Proxy (arg, r) -> ArgAnnotation arg -> SMTAnnotation r -> Maybe String -> FunInfo
[funInfoProxy] :: FunInfo -> Proxy (arg, r)
[funInfoArgAnn] :: FunInfo -> ArgAnnotation arg
[funInfoResAnn] :: FunInfo -> SMTAnnotation r
[funInfoName] :: FunInfo -> Maybe String
data AnyBackend m
AnyBackend :: b -> AnyBackend m

-- | The SMT monad used for communating with the SMT solver
data SMT' m a
SMT :: (forall b. SMTBackend b m => b -> m (a, b)) -> SMT' m a
[runSMT] :: SMT' m a -> forall b. SMTBackend b m => b -> m (a, b)
type SMT = SMT' IO
smtBackend :: Monad m => (forall b. SMTBackend b m => b -> m (res, b)) -> SMT' m res
data Untyped
Untyped :: t -> Untyped
data UntypedValue
UntypedValue :: t -> UntypedValue

-- | An abstract SMT expression
data SMTExpr t
Var :: Integer -> SMTAnnotation t -> SMTExpr t
QVar :: Integer -> Integer -> SMTAnnotation t -> SMTExpr t
FunArg :: Integer -> SMTAnnotation t -> SMTExpr t
Const :: t -> SMTAnnotation t -> SMTExpr t
AsArray :: 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 :: SMTFunction arg res -> arg -> SMTExpr res
Named :: SMTExpr a -> Integer -> SMTExpr a
InternalObj :: a -> SMTAnnotation t -> SMTExpr t
UntypedExpr :: SMTExpr t -> SMTExpr Untyped
UntypedExprValue :: SMTExpr t -> SMTExpr UntypedValue
data Sort' a
BoolSort :: Sort' a
IntSort :: Sort' a
RealSort :: Sort' a
BVSort :: Integer -> Bool -> Sort' a
[bvSortWidth] :: Sort' a -> Integer
[bvSortUntyped] :: Sort' a -> Bool
ArraySort :: [a] -> a -> Sort' a
NamedSort :: String -> [a] -> Sort' a
type Sort = Fix Sort'
data Value
BoolValue :: Bool -> Value
IntValue :: Integer -> Value
RealValue :: (Ratio Integer) -> Value
BVValue :: Integer -> Integer -> Value
[bvValueWidth] :: Value -> Integer
[bvValueValue] :: Value -> Integer
ConstrValue :: String -> [Value] -> (Maybe (String, [Sort])) -> Value
data SMTFunction arg res
SMTEq :: SMTFunction [SMTExpr a] Bool
SMTMap :: SMTFunction arg res -> SMTFunction (Lifted arg i) (SMTArray i res)
SMTFun :: Integer -> SMTAnnotation res -> SMTFunction arg res
SMTBuiltIn :: String -> SMTAnnotation res -> SMTFunction arg res
SMTOrd :: SMTOrdOp -> SMTFunction (SMTExpr a, SMTExpr a) Bool
SMTArith :: SMTArithOp -> SMTFunction [SMTExpr a] a
SMTMinus :: SMTFunction (SMTExpr a, SMTExpr a) a
SMTIntArith :: SMTIntArithOp -> SMTFunction (SMTExpr Integer, SMTExpr Integer) Integer
SMTDivide :: SMTFunction (SMTExpr Rational, SMTExpr Rational) Rational
SMTNeg :: SMTFunction (SMTExpr a) a
SMTAbs :: SMTFunction (SMTExpr a) a
SMTNot :: SMTFunction (SMTExpr Bool) Bool
SMTLogic :: SMTLogicOp -> SMTFunction [SMTExpr Bool] Bool
SMTDistinct :: SMTFunction [SMTExpr a] Bool
SMTToReal :: SMTFunction (SMTExpr Integer) Rational
SMTToInt :: SMTFunction (SMTExpr Rational) Integer
SMTITE :: SMTFunction (SMTExpr Bool, SMTExpr a, SMTExpr a) a
SMTBVComp :: SMTBVCompOp -> SMTFunction (SMTExpr (BitVector a), SMTExpr (BitVector a)) Bool
SMTBVBin :: SMTBVBinOp -> SMTFunction (SMTExpr (BitVector a), SMTExpr (BitVector a)) (BitVector a)
SMTBVUn :: SMTBVUnOp -> SMTFunction (SMTExpr (BitVector a)) (BitVector a)
SMTSelect :: SMTFunction (SMTExpr (SMTArray i v), i) v
SMTStore :: SMTFunction (SMTExpr (SMTArray i v), i, SMTExpr v) (SMTArray i v)
SMTConstArray :: ArgAnnotation i -> SMTFunction (SMTExpr v) (SMTArray i v)
SMTConcat :: SMTFunction (SMTExpr (BitVector a), SMTExpr (BitVector b)) (BitVector (ConcatResult a b))
SMTExtract :: Proxy start -> Proxy len -> SMTFunction (SMTExpr (BitVector from)) (BitVector len')
SMTConstructor :: Constructor arg dt -> SMTFunction arg dt
SMTConTest :: Constructor arg dt -> SMTFunction (SMTExpr dt) Bool
SMTFieldSel :: Field a f -> SMTFunction (SMTExpr a) f
SMTDivisible :: Integer -> SMTFunction (SMTExpr Integer) Bool
class (SMTValue (BitVector a)) => IsBitVector a
getBVSize :: IsBitVector a => Proxy a -> SMTAnnotation (BitVector a) -> Integer
class (IsBitVector a, IsBitVector b, IsBitVector (ConcatResult a b)) => Concatable a b where type family ConcatResult a b
concatAnnotation :: Concatable a b => a -> b -> SMTAnnotation (BitVector a) -> SMTAnnotation (BitVector b) -> SMTAnnotation (BitVector (ConcatResult a b))
class (IsBitVector a, IsBitVector b) => Extractable a b
extractAnn :: Extractable a b => a -> b -> Integer -> SMTAnnotation (BitVector a) -> SMTAnnotation (BitVector b)
getExtractLen :: Extractable a b => a -> b -> SMTAnnotation (BitVector b) -> Integer

-- | Represents a constructor of a datatype <i>a</i> Can be obtained by
--   using the template haskell extension module
data Constructor arg res
Constructor :: [ProxyArg] -> DataType -> Constr -> Constructor arg res

-- | Represents a field of the datatype <i>a</i> of the type <i>f</i>
data Field a f
Field :: [ProxyArg] -> DataType -> Constr -> DataField -> Field a f
newtype InterpolationGroup
InterpolationGroup :: Integer -> InterpolationGroup

-- | Identifies a clause in an unsatisfiable core
newtype ClauseId
ClauseId :: Integer -> ClauseId

-- | Options controling the behaviour of the SMT solver
data SMTOption

-- | Whether or not to print "success" after each operation
PrintSuccess :: Bool -> SMTOption

-- | Produce a satisfying assignment after each successful checkSat
ProduceModels :: Bool -> SMTOption

-- | Produce a proof of unsatisfiability after each failed checkSat
ProduceProofs :: Bool -> SMTOption

-- | Enable the querying of unsatisfiable cores after a failed checkSat
ProduceUnsatCores :: Bool -> SMTOption

-- | Enable the generation of craig interpolants
ProduceInterpolants :: Bool -> SMTOption
data SMTInfo i
SMTSolverName :: SMTInfo String
SMTSolverVersion :: SMTInfo String

-- | Instances of this class may be used as arguments for constructed
--   functions and quantifiers.
class (Ord a, Typeable a, Show a, Ord (ArgAnnotation a), Typeable (ArgAnnotation a), Show (ArgAnnotation a)) => Args a where type family ArgAnnotation a foldExprs f s x ann = do { (s', _, r) <- foldsExprs (\ cs [(expr, _)] ann' -> do { (cs', cr) <- f cs expr ann'; return (cs', [cr], cr) }) s [(x, ())] ann; return (s', r) } fromArgs arg = fst $ foldExprsId (\ lst expr ann -> (lst ++ [UntypedExpr expr], expr)) [] arg (extractArgAnnotation arg)
foldExprs :: (Args a, Monad m) => (forall t. SMTType t => s -> SMTExpr t -> SMTAnnotation t -> m (s, SMTExpr t)) -> s -> a -> ArgAnnotation a -> m (s, a)
foldsExprs :: (Args a, 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 :: Args a => a -> ArgAnnotation a
toArgs :: Args a => ArgAnnotation a -> [SMTExpr Untyped] -> Maybe (a, [SMTExpr Untyped])
fromArgs :: Args a => a -> [SMTExpr Untyped]
getTypes :: Args a => a -> ArgAnnotation a -> [ProxyArg]
getArgAnnotation :: Args a => a -> [Sort] -> (ArgAnnotation a, [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 type family Lifted a i
getLiftedArgumentAnn :: Liftable a => a -> i -> ArgAnnotation a -> ArgAnnotation i -> ArgAnnotation (Lifted a i)
inferLiftedAnnotation :: Liftable a => a -> i -> ArgAnnotation (Lifted a i) -> (ArgAnnotation i, ArgAnnotation a)
getConstraint :: (Liftable a, 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)

-- | An extension of the <a>Args</a> class: Instances of this class can be
--   represented as native haskell data types.
class Args a => LiftArgs a where type family Unpacked a

-- | Converts a haskell value into its SMT representation.
liftArgs :: LiftArgs a => Unpacked a -> ArgAnnotation a -> a

-- | Converts a SMT representation back into a haskell value.
unliftArgs :: (LiftArgs a, Monad m) => a -> (forall t. SMTValue t => SMTExpr t -> m t) -> m (Unpacked a)
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
DataTypeInfo :: [TypeCollection] -> Map String (DataType, TypeCollection) -> Map String (Constr, DataType, TypeCollection) -> Map String (DataField, Constr, DataType, TypeCollection) -> DataTypeInfo
[structures] :: DataTypeInfo -> [TypeCollection]
[datatypes] :: DataTypeInfo -> Map String (DataType, TypeCollection)
[constructors] :: DataTypeInfo -> Map String (Constr, DataType, TypeCollection)
[fields] :: DataTypeInfo -> Map String (DataField, Constr, DataType, TypeCollection)
data TypeCollection
TypeCollection :: Integer -> [DataType] -> TypeCollection
[argCount] :: TypeCollection -> Integer
[dataTypes] :: TypeCollection -> [DataType]
data ProxyArg
ProxyArg :: t -> (SMTAnnotation t) -> ProxyArg
data ProxyArgValue
ProxyArgValue :: t -> (SMTAnnotation t) -> ProxyArgValue
withProxyArg :: ProxyArg -> (forall t. SMTType t => t -> SMTAnnotation t -> a) -> a
withProxyArgValue :: ProxyArgValue -> (forall t. SMTValue t => t -> SMTAnnotation t -> a) -> a
data AnyValue
AnyValue :: [ProxyArg] -> t -> (SMTAnnotation t) -> AnyValue
withAnyValue :: AnyValue -> (forall t. SMTType t => [ProxyArg] -> t -> SMTAnnotation t -> a) -> a
castAnyValue :: SMTType t => AnyValue -> Maybe (t, SMTAnnotation t)
data DataType
DataType :: String -> [Constr] -> (forall r. [ProxyArg] -> (forall t. SMTType t => t -> SMTAnnotation t -> r) -> r) -> DataType
[dataTypeName] :: DataType -> String
[dataTypeConstructors] :: DataType -> [Constr]
[dataTypeGetUndefined] :: DataType -> forall r. [ProxyArg] -> (forall t. SMTType t => t -> SMTAnnotation t -> r) -> r
data Constr
Constr :: String -> [DataField] -> (forall r. [Maybe ProxyArg] -> [AnyValue] -> (forall t. SMTType t => [ProxyArg] -> t -> SMTAnnotation t -> r) -> r) -> (forall r. [ProxyArg] -> (forall arg. Args arg => arg -> ArgAnnotation arg -> r) -> r) -> (forall t. SMTType t => [ProxyArg] -> t -> Bool) -> Constr
[conName] :: Constr -> String
[conFields] :: Constr -> [DataField]
[construct] :: Constr -> forall r. [Maybe ProxyArg] -> [AnyValue] -> (forall t. SMTType t => [ProxyArg] -> t -> SMTAnnotation t -> r) -> r
[conUndefinedArgs] :: Constr -> forall r. [ProxyArg] -> (forall arg. Args arg => arg -> ArgAnnotation arg -> r) -> r
[conTest] :: Constr -> forall t. SMTType t => [ProxyArg] -> t -> Bool
data DataField
DataField :: String -> ArgumentSort -> (forall r t. SMTType t => [ProxyArg] -> t -> (forall f. SMTType f => f -> SMTAnnotation f -> r) -> r) -> DataField
[fieldName] :: DataField -> String
[fieldSort] :: DataField -> ArgumentSort
[fieldGet] :: DataField -> 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

-- | Get all the type collections which are not yet declared from a type.
getNewTypeCollections :: SMTType t => Proxy t -> SMTAnnotation t -> DataTypeInfo -> ([TypeCollection], DataTypeInfo)
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
SMTState :: Integer -> Integer -> Integer -> Map Integer (FunInfo, Integer) -> Map (String, Integer) Integer -> Map String Integer -> DataTypeInfo -> SMTState
[nextVar] :: SMTState -> Integer
[nextInterpolationGroup] :: SMTState -> Integer
[nextClauseId] :: SMTState -> Integer
[allVars] :: SMTState -> Map Integer (FunInfo, Integer)
[namedVars] :: SMTState -> Map (String, Integer) Integer
[nameCount] :: SMTState -> Map String Integer
[declaredDataTypes] :: SMTState -> DataTypeInfo
emptySMTState :: SMTState
smtStateAddFun :: FunInfo -> SMTState -> (Integer, String, SMTState)
data Z
Z :: Z
data S a
S :: S a
class Typeable a => TypeableNat a
reflectNat :: TypeableNat a => Proxy a -> Integer -> Integer
data BVUntyped
BVUntyped :: BVUntyped
data BVTyped n
BVTyped :: BVTyped n
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 :: *)
BitVector :: Integer -> BitVector
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
Bound :: Integer -> Bound
showExpr :: Int -> SMTExpr t -> ShowS
noLimits :: CheckSatLimits
newtype Quantified
Quantified :: Integer -> Quantified
quantificationLevel :: SMTExpr t -> Integer
inferSorts :: ArgumentSort -> Sort -> Map Integer Sort -> Map Integer Sort
valueSort :: DataTypeInfo -> Value -> Sort
instance GHC.Classes.Ord Language.SMTLib2.Internals.Quantified
instance GHC.Classes.Eq Language.SMTLib2.Internals.Quantified
instance GHC.Show.Show Language.SMTLib2.Internals.Quantified
instance GHC.Show.Show Language.SMTLib2.Internals.Bound
instance GHC.Classes.Ord Language.SMTLib2.Internals.Bound
instance GHC.Classes.Eq Language.SMTLib2.Internals.Bound
instance GHC.Show.Show Language.SMTLib2.Internals.SMTModel
instance GHC.Classes.Ord (Language.SMTLib2.Internals.BitVector b)
instance GHC.Classes.Eq (Language.SMTLib2.Internals.BitVector b)
instance GHC.Show.Show (Language.SMTLib2.Internals.BVTyped n)
instance GHC.Classes.Ord (Language.SMTLib2.Internals.BVTyped n)
instance GHC.Classes.Eq (Language.SMTLib2.Internals.BVTyped n)
instance GHC.Show.Show Language.SMTLib2.Internals.BVUntyped
instance GHC.Classes.Ord Language.SMTLib2.Internals.BVUntyped
instance GHC.Classes.Eq Language.SMTLib2.Internals.BVUntyped
instance GHC.Classes.Ord Language.SMTLib2.Internals.SMTOption
instance GHC.Classes.Eq Language.SMTLib2.Internals.SMTOption
instance GHC.Show.Show Language.SMTLib2.Internals.SMTOption
instance GHC.Show.Show Language.SMTLib2.Internals.ClauseId
instance GHC.Classes.Ord Language.SMTLib2.Internals.ClauseId
instance GHC.Classes.Eq Language.SMTLib2.Internals.ClauseId
instance GHC.Show.Show Language.SMTLib2.Internals.InterpolationGroup
instance GHC.Classes.Ord Language.SMTLib2.Internals.InterpolationGroup
instance GHC.Classes.Eq Language.SMTLib2.Internals.InterpolationGroup
instance GHC.Show.Show Language.SMTLib2.Internals.Value
instance GHC.Classes.Ord Language.SMTLib2.Internals.Value
instance GHC.Classes.Eq Language.SMTLib2.Internals.Value
instance Data.Traversable.Traversable Language.SMTLib2.Internals.Sort'
instance Data.Foldable.Foldable Language.SMTLib2.Internals.Sort'
instance GHC.Base.Functor Language.SMTLib2.Internals.Sort'
instance GHC.Show.Show a => GHC.Show.Show (Language.SMTLib2.Internals.Sort' a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Language.SMTLib2.Internals.Sort' a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Language.SMTLib2.Internals.Sort' a)
instance GHC.Classes.Ord (Language.SMTLib2.Internals.SMTArray i v)
instance GHC.Classes.Eq (Language.SMTLib2.Internals.SMTArray i v)
instance GHC.Classes.Ord Language.SMTLib2.Internals.CheckSatResult
instance GHC.Classes.Eq Language.SMTLib2.Internals.CheckSatResult
instance GHC.Show.Show Language.SMTLib2.Internals.CheckSatResult
instance GHC.Classes.Ord Language.SMTLib2.Internals.CheckSatLimits
instance GHC.Classes.Eq Language.SMTLib2.Internals.CheckSatLimits
instance GHC.Show.Show Language.SMTLib2.Internals.CheckSatLimits
instance GHC.Base.Functor m => GHC.Base.Functor (Language.SMTLib2.Internals.SMT' m)
instance GHC.Base.Monad m => GHC.Base.Monad (Language.SMTLib2.Internals.SMT' m)
instance Control.Monad.IO.Class.MonadIO m => Control.Monad.IO.Class.MonadIO (Language.SMTLib2.Internals.SMT' m)
instance Control.Monad.Fix.MonadFix m => Control.Monad.Fix.MonadFix (Language.SMTLib2.Internals.SMT' m)
instance (GHC.Base.Monad m, GHC.Base.Functor m) => GHC.Base.Applicative (Language.SMTLib2.Internals.SMT' m)
instance Control.Monad.Trans.Class.MonadTrans Language.SMTLib2.Internals.SMT'
instance GHC.Classes.Eq Language.SMTLib2.Internals.Untyped
instance GHC.Classes.Ord Language.SMTLib2.Internals.Untyped
instance GHC.Classes.Eq Language.SMTLib2.Internals.UntypedValue
instance GHC.Classes.Ord Language.SMTLib2.Internals.UntypedValue
instance GHC.Show.Show Language.SMTLib2.Internals.UntypedValue
instance Language.SMTLib2.Internals.Args ()
instance GHC.Show.Show Language.SMTLib2.Internals.ProxyArg
instance GHC.Classes.Eq Language.SMTLib2.Internals.ProxyArg
instance GHC.Classes.Ord Language.SMTLib2.Internals.ProxyArg
instance GHC.Show.Show Language.SMTLib2.Internals.ProxyArgValue
instance GHC.Classes.Eq Language.SMTLib2.Internals.ProxyArgValue
instance GHC.Classes.Ord Language.SMTLib2.Internals.ProxyArgValue
instance Language.SMTLib2.Internals.TypeableNat Language.SMTLib2.Internals.Z
instance Language.SMTLib2.Internals.TypeableNat n => Language.SMTLib2.Internals.TypeableNat (Language.SMTLib2.Internals.S n)
instance GHC.Show.Show (Language.SMTLib2.Internals.BitVector a)
instance GHC.Enum.Enum (Language.SMTLib2.Internals.BitVector a)
instance GHC.Base.Monad m => Language.SMTLib2.Internals.SMTBackend (Language.SMTLib2.Internals.AnyBackend m) m
instance GHC.Show.Show (Language.SMTLib2.Internals.SMTExpr t)
instance GHC.Show.Show (Language.SMTLib2.Internals.SMTFunction arg res)
instance GHC.Show.Show (Language.SMTLib2.Internals.Field a f)
instance GHC.Show.Show (Language.SMTLib2.Internals.Constructor arg res)


-- | Implements various instance declarations for <a>SMTType</a>,
--   <a>SMTValue</a>, etc.
module Language.SMTLib2.Internals.Instances
valueToHaskell :: DataTypeInfo -> (forall t. SMTType t => [ProxyArg] -> t -> SMTAnnotation t -> r) -> Maybe Sort -> Value -> r

-- | Reconstruct the type annotation for a given SMT expression.
extractAnnotation :: SMTExpr a -> SMTAnnotation a
inferResAnnotation :: SMTFunction arg res -> ArgAnnotation arg -> SMTAnnotation res
entype :: (forall a. SMTType a => SMTExpr a -> b) -> SMTExpr Untyped -> b
entypeValue :: (forall a. SMTValue a => SMTExpr a -> b) -> SMTExpr UntypedValue -> b
castUntypedExpr :: SMTType t => SMTExpr Untyped -> SMTExpr t
castUntypedExprValue :: SMTType t => SMTExpr UntypedValue -> SMTExpr t
dtMaybe :: DataType
conNothing :: Constr
conJust :: Constr
nothing' :: SMTType a => SMTAnnotation a -> Constructor () (Maybe a)
just' :: SMTType a => SMTAnnotation a -> Constructor (SMTExpr a) (Maybe a)
fieldFromJust :: DataField

-- | Get an undefined value of the type argument of a type.
undefArg :: b a -> a
dtList :: DataType
conNil :: Constr
conInsert :: Constr
insert' :: SMTType a => SMTAnnotation a -> Constructor (SMTExpr a, SMTExpr [a]) [a]
nil' :: SMTType a => SMTAnnotation a -> Constructor () [a]
fieldHead :: DataField
fieldTail :: DataField
bvUnsigned :: IsBitVector a => BitVector a -> SMTAnnotation (BitVector a) -> Integer
bvSigned :: IsBitVector a => BitVector a -> SMTAnnotation (BitVector a) -> Integer
bvRestrict :: IsBitVector a => BitVector a -> SMTAnnotation (BitVector a) -> BitVector a
withSort :: DataTypeInfo -> Sort -> (forall t. SMTType t => t -> SMTAnnotation t -> r) -> r
withNumSort :: DataTypeInfo -> Sort -> (forall t. (SMTArith t) => t -> SMTAnnotation t -> r) -> Maybe r
withSorts :: DataTypeInfo -> [Sort] -> (forall arg. Liftable arg => arg -> ArgAnnotation arg -> r) -> r
withArraySort :: DataTypeInfo -> [Sort] -> Sort -> (forall i v. (Liftable i, SMTType v) => SMTArray i v -> (ArgAnnotation i, SMTAnnotation v) -> a) -> a

-- | Recursively fold a monadic function over all sub-expressions of this
--   expression
foldExprM :: (SMTType a, Monad m) => (forall t. SMTType t => s -> SMTExpr t -> m (s, [SMTExpr t])) -> s -> SMTExpr a -> m (s, [SMTExpr a])

-- | Recursively fold a monadic function over all sub-expressions of the
--   argument
foldArgsM :: (Args a, Monad m) => (forall t. SMTType t => s -> SMTExpr t -> m (s, [SMTExpr t])) -> s -> a -> m (s, [a])

-- | Recursively fold a function over all sub-expressions of this
--   expression. It is implemented as a special case of <a>foldExprM</a>.
foldExpr :: SMTType a => (forall t. SMTType t => s -> SMTExpr t -> (s, SMTExpr t)) -> s -> SMTExpr a -> (s, SMTExpr a)
foldExprMux :: SMTType a => (forall t. SMTType t => s -> SMTExpr t -> (s, [SMTExpr t])) -> s -> SMTExpr a -> (s, [SMTExpr a])

-- | Recursively fold a function over all sub-expressions of the argument.
--   It is implemented as a special case of <a>foldArgsM</a>.
foldArgs :: Args a => (forall t. SMTType t => s -> SMTExpr t -> (s, SMTExpr t)) -> s -> a -> (s, a)
foldArgsMux :: Args a => (forall t. SMTType t => s -> SMTExpr t -> (s, [SMTExpr t])) -> s -> a -> (s, [a])
compareFun :: (Args a1, Args a2) => SMTFunction a1 r1 -> SMTFunction a2 r2 -> Ordering
compareConstructor :: Constructor arg1 res1 -> Constructor arg2 res2 -> Ordering
compareField :: Field a1 f1 -> Field a2 f2 -> Ordering
compareArgs :: (Args a1, Args a2) => a1 -> a2 -> Ordering
compareExprs :: (SMTType t1, SMTType t2) => SMTExpr t1 -> SMTExpr t2 -> Ordering
eqExpr :: SMTExpr a -> SMTExpr a -> Maybe Bool
valueToConst :: DataTypeInfo -> Value -> (forall a. SMTType a => [ProxyArg] -> a -> SMTAnnotation a -> b) -> b
instance Language.SMTLib2.Internals.SMTType Language.SMTLib2.Internals.Untyped
instance Language.SMTLib2.Internals.SMTType Language.SMTLib2.Internals.UntypedValue
instance Language.SMTLib2.Internals.SMTValue Language.SMTLib2.Internals.UntypedValue
instance Language.SMTLib2.Internals.SMTType GHC.Types.Bool
instance Language.SMTLib2.Internals.SMTValue GHC.Types.Bool
instance Language.SMTLib2.Internals.SMTType GHC.Integer.Type.Integer
instance Language.SMTLib2.Internals.SMTValue GHC.Integer.Type.Integer
instance Language.SMTLib2.Internals.SMTArith GHC.Integer.Type.Integer
instance GHC.Num.Num (Language.SMTLib2.Internals.SMTExpr GHC.Integer.Type.Integer)
instance Language.SMTLib2.Internals.SMTOrd GHC.Integer.Type.Integer
instance GHC.Enum.Enum (Language.SMTLib2.Internals.SMTExpr GHC.Integer.Type.Integer)
instance Language.SMTLib2.Internals.SMTType (GHC.Real.Ratio GHC.Integer.Type.Integer)
instance Language.SMTLib2.Internals.SMTValue (GHC.Real.Ratio GHC.Integer.Type.Integer)
instance Language.SMTLib2.Internals.SMTArith (GHC.Real.Ratio GHC.Integer.Type.Integer)
instance GHC.Num.Num (Language.SMTLib2.Internals.SMTExpr (GHC.Real.Ratio GHC.Integer.Type.Integer))
instance GHC.Real.Fractional (Language.SMTLib2.Internals.SMTExpr (GHC.Real.Ratio GHC.Integer.Type.Integer))
instance Language.SMTLib2.Internals.SMTOrd (GHC.Real.Ratio GHC.Integer.Type.Integer)
instance (Language.SMTLib2.Internals.Args idx, Language.SMTLib2.Internals.SMTType val) => Language.SMTLib2.Internals.SMTType (Language.SMTLib2.Internals.SMTArray idx val)
instance Language.SMTLib2.Internals.SMTType a => Language.SMTLib2.Internals.Liftable (Language.SMTLib2.Internals.SMTExpr a)
instance Language.SMTLib2.Internals.SMTType a => Language.SMTLib2.Internals.Liftable [Language.SMTLib2.Internals.SMTExpr a]
instance (Language.SMTLib2.Internals.Liftable a, Language.SMTLib2.Internals.Liftable b) => Language.SMTLib2.Internals.Liftable (a, b)
instance (Language.SMTLib2.Internals.Liftable a, Language.SMTLib2.Internals.Liftable b, Language.SMTLib2.Internals.Liftable c) => Language.SMTLib2.Internals.Liftable (a, b, c)
instance (Language.SMTLib2.Internals.Liftable a, Language.SMTLib2.Internals.Liftable b, Language.SMTLib2.Internals.Liftable c, Language.SMTLib2.Internals.Liftable d) => Language.SMTLib2.Internals.Liftable (a, b, c, d)
instance (Language.SMTLib2.Internals.Liftable a, Language.SMTLib2.Internals.Liftable b, Language.SMTLib2.Internals.Liftable c, Language.SMTLib2.Internals.Liftable d, Language.SMTLib2.Internals.Liftable e) => Language.SMTLib2.Internals.Liftable (a, b, c, d, e)
instance (Language.SMTLib2.Internals.Liftable a, Language.SMTLib2.Internals.Liftable b, Language.SMTLib2.Internals.Liftable c, Language.SMTLib2.Internals.Liftable d, Language.SMTLib2.Internals.Liftable e, Language.SMTLib2.Internals.Liftable f) => Language.SMTLib2.Internals.Liftable (a, b, c, d, e, f)
instance (Language.SMTLib2.Internals.TypeableNat n1, Language.SMTLib2.Internals.TypeableNat n2, Language.SMTLib2.Internals.TypeableNat (Language.SMTLib2.Internals.Add n1 n2)) => Language.SMTLib2.Internals.Concatable (Language.SMTLib2.Internals.BVTyped n1) (Language.SMTLib2.Internals.BVTyped n2)
instance Language.SMTLib2.Internals.TypeableNat n2 => Language.SMTLib2.Internals.Concatable Language.SMTLib2.Internals.BVUntyped (Language.SMTLib2.Internals.BVTyped n2)
instance Language.SMTLib2.Internals.TypeableNat n1 => Language.SMTLib2.Internals.Concatable (Language.SMTLib2.Internals.BVTyped n1) Language.SMTLib2.Internals.BVUntyped
instance Language.SMTLib2.Internals.Concatable Language.SMTLib2.Internals.BVUntyped Language.SMTLib2.Internals.BVUntyped
instance Language.SMTLib2.Internals.SMTType a => Language.SMTLib2.Internals.Args (Language.SMTLib2.Internals.SMTExpr a)
instance (Language.SMTLib2.Internals.Args a, Language.SMTLib2.Internals.Args b) => Language.SMTLib2.Internals.Args (a, b)
instance Language.SMTLib2.Internals.SMTValue a => Language.SMTLib2.Internals.LiftArgs (Language.SMTLib2.Internals.SMTExpr a)
instance (Language.SMTLib2.Internals.LiftArgs a, Language.SMTLib2.Internals.LiftArgs b) => Language.SMTLib2.Internals.LiftArgs (a, b)
instance (Language.SMTLib2.Internals.Args a, Language.SMTLib2.Internals.Args b, Language.SMTLib2.Internals.Args c) => Language.SMTLib2.Internals.Args (a, b, c)
instance (Language.SMTLib2.Internals.LiftArgs a, Language.SMTLib2.Internals.LiftArgs b, Language.SMTLib2.Internals.LiftArgs c) => Language.SMTLib2.Internals.LiftArgs (a, b, c)
instance (Language.SMTLib2.Internals.Args a, Language.SMTLib2.Internals.Args b, Language.SMTLib2.Internals.Args c, Language.SMTLib2.Internals.Args d) => Language.SMTLib2.Internals.Args (a, b, c, d)
instance (Language.SMTLib2.Internals.LiftArgs a, Language.SMTLib2.Internals.LiftArgs b, Language.SMTLib2.Internals.LiftArgs c, Language.SMTLib2.Internals.LiftArgs d) => Language.SMTLib2.Internals.LiftArgs (a, b, c, d)
instance (Language.SMTLib2.Internals.Args a, Language.SMTLib2.Internals.Args b, Language.SMTLib2.Internals.Args c, Language.SMTLib2.Internals.Args d, Language.SMTLib2.Internals.Args e) => Language.SMTLib2.Internals.Args (a, b, c, d, e)
instance (Language.SMTLib2.Internals.LiftArgs a, Language.SMTLib2.Internals.LiftArgs b, Language.SMTLib2.Internals.LiftArgs c, Language.SMTLib2.Internals.LiftArgs d, Language.SMTLib2.Internals.LiftArgs e) => Language.SMTLib2.Internals.LiftArgs (a, b, c, d, e)
instance (Language.SMTLib2.Internals.Args a, Language.SMTLib2.Internals.Args b, Language.SMTLib2.Internals.Args c, Language.SMTLib2.Internals.Args d, Language.SMTLib2.Internals.Args e, Language.SMTLib2.Internals.Args f) => Language.SMTLib2.Internals.Args (a, b, c, d, e, f)
instance (Language.SMTLib2.Internals.LiftArgs a, Language.SMTLib2.Internals.LiftArgs b, Language.SMTLib2.Internals.LiftArgs c, Language.SMTLib2.Internals.LiftArgs d, Language.SMTLib2.Internals.LiftArgs e, Language.SMTLib2.Internals.LiftArgs f) => Language.SMTLib2.Internals.LiftArgs (a, b, c, d, e, f)
instance Language.SMTLib2.Internals.Args a => Language.SMTLib2.Internals.Args [a]
instance (Data.Typeable.Internal.Typeable a, GHC.Show.Show a, Language.SMTLib2.Internals.Args b, GHC.Classes.Ord a) => Language.SMTLib2.Internals.Args (Data.Map.Base.Map a b)
instance (Language.SMTLib2.Internals.Args a, Language.SMTLib2.Internals.Args b) => Language.SMTLib2.Internals.Args (Data.Either.Either a b)
instance Language.SMTLib2.Internals.Args a => Language.SMTLib2.Internals.Args (GHC.Base.Maybe a)
instance Language.SMTLib2.Internals.LiftArgs a => Language.SMTLib2.Internals.LiftArgs [a]
instance (Data.Typeable.Internal.Typeable a, GHC.Show.Show a, GHC.Classes.Ord a, Language.SMTLib2.Internals.LiftArgs b) => Language.SMTLib2.Internals.LiftArgs (Data.Map.Base.Map a b)
instance (Language.SMTLib2.Internals.LiftArgs a, Language.SMTLib2.Internals.LiftArgs b) => Language.SMTLib2.Internals.LiftArgs (Data.Either.Either a b)
instance Language.SMTLib2.Internals.LiftArgs a => Language.SMTLib2.Internals.LiftArgs (GHC.Base.Maybe a)
instance Language.SMTLib2.Internals.SMTType a => Language.SMTLib2.Internals.SMTType (GHC.Base.Maybe a)
instance Language.SMTLib2.Internals.SMTValue a => Language.SMTLib2.Internals.SMTValue (GHC.Base.Maybe a)
instance (Data.Typeable.Internal.Typeable a, Language.SMTLib2.Internals.SMTType a) => Language.SMTLib2.Internals.SMTType [a]
instance (Data.Typeable.Internal.Typeable a, Language.SMTLib2.Internals.SMTValue a) => Language.SMTLib2.Internals.SMTValue [a]
instance Language.SMTLib2.Internals.SMTType (Language.SMTLib2.Internals.BitVector Language.SMTLib2.Internals.BVUntyped)
instance Language.SMTLib2.Internals.IsBitVector Language.SMTLib2.Internals.BVUntyped
instance Language.SMTLib2.Internals.SMTValue (Language.SMTLib2.Internals.BitVector Language.SMTLib2.Internals.BVUntyped)
instance Language.SMTLib2.Internals.TypeableNat n => Language.SMTLib2.Internals.SMTType (Language.SMTLib2.Internals.BitVector (Language.SMTLib2.Internals.BVTyped n))
instance Language.SMTLib2.Internals.TypeableNat n => Language.SMTLib2.Internals.IsBitVector (Language.SMTLib2.Internals.BVTyped n)
instance Language.SMTLib2.Internals.TypeableNat n => Language.SMTLib2.Internals.SMTValue (Language.SMTLib2.Internals.BitVector (Language.SMTLib2.Internals.BVTyped n))
instance Language.SMTLib2.Internals.TypeableNat n => GHC.Num.Num (Language.SMTLib2.Internals.BitVector (Language.SMTLib2.Internals.BVTyped n))
instance Language.SMTLib2.Internals.TypeableNat n => GHC.Num.Num (Language.SMTLib2.Internals.SMTExpr (Language.SMTLib2.Internals.BitVector (Language.SMTLib2.Internals.BVTyped n)))
instance Language.SMTLib2.Internals.Extractable Language.SMTLib2.Internals.BVUntyped Language.SMTLib2.Internals.BVUntyped
instance Language.SMTLib2.Internals.TypeableNat n => Language.SMTLib2.Internals.Extractable (Language.SMTLib2.Internals.BVTyped n) Language.SMTLib2.Internals.BVUntyped
instance Language.SMTLib2.Internals.TypeableNat n => Language.SMTLib2.Internals.Extractable Language.SMTLib2.Internals.BVUntyped (Language.SMTLib2.Internals.BVTyped n)
instance (Language.SMTLib2.Internals.TypeableNat n1, Language.SMTLib2.Internals.TypeableNat n2) => Language.SMTLib2.Internals.Extractable (Language.SMTLib2.Internals.BVTyped n1) (Language.SMTLib2.Internals.BVTyped n2)
instance Language.SMTLib2.Internals.Args arg => GHC.Classes.Eq (Language.SMTLib2.Internals.SMTFunction arg res)
instance Language.SMTLib2.Internals.Args arg => GHC.Classes.Ord (Language.SMTLib2.Internals.SMTFunction arg res)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Language.SMTLib2.Internals.SMTExpr a)
instance Language.SMTLib2.Internals.SMTType t => GHC.Classes.Ord (Language.SMTLib2.Internals.SMTExpr t)
instance GHC.Classes.Eq (Language.SMTLib2.Internals.Constructor arg res)
instance GHC.Classes.Ord (Language.SMTLib2.Internals.Constructor arg res)
instance GHC.Classes.Eq (Language.SMTLib2.Internals.Field a f)
instance GHC.Classes.Ord (Language.SMTLib2.Internals.Field a f)

module Language.SMTLib2.Internals.Optimize
optimizeBackend :: b -> OptimizeBackend b
optimizeExpr :: SMTExpr t -> Maybe (SMTExpr t)
instance Language.SMTLib2.Internals.SMTBackend b m => Language.SMTLib2.Internals.SMTBackend (Language.SMTLib2.Internals.Optimize.OptimizeBackend b) m


-- | Defines the user-accessible interface of the smtlib2 library
module Language.SMTLib2.Internals.Interface

-- | Check if the model is satisfiable (e.g. if there is a value for each
--   variable so that every assertion holds)
checkSat :: Monad m => SMT' m Bool

-- | Check if the model is satisfiable using a given tactic. (Works only
--   with Z3)
checkSatUsing :: Monad m => Tactic -> SMT' m Bool

-- | Like <a>checkSat</a>, but gives you more options like choosing a
--   tactic (Z3 only) or providing memory/time-limits
checkSat' :: Monad m => Maybe Tactic -> CheckSatLimits -> SMT' m CheckSatResult
isSat :: CheckSatResult -> Bool

-- | Apply the given tactic to the current assertions. (Works only with Z3)
apply :: Monad m => Tactic -> SMT' m [SMTExpr Bool]

-- | Push a new context on the stack
push :: Monad m => SMT' m ()

-- | Pop a new context from the stack
pop :: Monad m => SMT' m ()

-- | Perform a stacked operation, meaning that every assertion and
--   declaration made in it will be undone after the operation.
stack :: Monad m => SMT' m a -> SMT' m a

-- | Insert a comment into the SMTLib2 command stream. If you aren't
--   looking at the command stream for debugging, this will do nothing.
comment :: Monad m => String -> SMT' m ()

-- | Create a new named variable
varNamed :: (SMTType t, Typeable t, Unit (SMTAnnotation t), Monad m) => String -> SMT' m (SMTExpr t)

-- | Create a named and annotated variable.
varNamedAnn :: (SMTType t, Typeable t, Monad m) => String -> SMTAnnotation t -> SMT' m (SMTExpr t)

-- | Create a annotated variable
varAnn :: (SMTType t, Typeable t, Monad m) => SMTAnnotation t -> SMT' m (SMTExpr t)

-- | Create a fresh new variable
var :: (SMTType t, Typeable t, Unit (SMTAnnotation t), Monad m) => SMT' m (SMTExpr t)

-- | Create a fresh untyped variable with a name
untypedNamedVar :: Monad m => String -> Sort -> SMT' m (SMTExpr Untyped)

-- | Create a fresh untyped variable
untypedVar :: Monad m => Sort -> SMT' m (SMTExpr Untyped)

-- | Like <a>argVarsAnnNamed</a>, but defaults the name to "var"
argVarsAnn :: (Args a, Monad m) => ArgAnnotation a -> SMT' m a

-- | Create annotated named SMT variables of the <a>Args</a> class. If more
--   than one variable is needed, they get a numerical suffix.
argVarsAnnNamed :: (Args a, Monad m) => String -> ArgAnnotation a -> SMT' m a
argVarsAnnNamed' :: (Args a, Monad m) => Maybe String -> ArgAnnotation a -> SMT' m a

-- | Like <a>argVarsAnn</a>, but can only be used for unit type
--   annotations.
argVars :: (Args a, Unit (ArgAnnotation a), Monad m) => SMT' m a

-- | A constant expression.
constant :: (SMTValue t, Unit (SMTAnnotation t)) => t -> SMTExpr t

-- | An annotated constant expression.
constantAnn :: SMTValue t => t -> SMTAnnotation t -> SMTExpr t
getValue :: (SMTValue t, Monad m) => SMTExpr t -> SMT' m t
getValues :: (LiftArgs arg, Monad m) => arg -> SMT' m (Unpacked arg)

-- | Extract all assigned values of the model
getModel :: Monad m => SMT' m SMTModel

-- | Extract all values of an array by giving the range of indices.
unmangleArray :: (Liftable i, LiftArgs i, Ix (Unpacked i), SMTValue v, Unit (ArgAnnotation i), Monad m) => (Unpacked i, Unpacked i) -> SMTExpr (SMTArray i v) -> SMT' m (Array (Unpacked i) v)

-- | Define a new function with a body
defFun :: (Args a, SMTType r, Unit (ArgAnnotation a), Monad m) => (a -> SMTExpr r) -> SMT' m (SMTFunction a r)

-- | Define a new constant.
defConst :: (SMTType r, Monad m) => SMTExpr r -> SMT' m (SMTExpr r)

-- | Define a new constant with a name
defConstNamed :: (SMTType r, Monad m) => String -> SMTExpr r -> SMT' m (SMTExpr r)
defConstNamed' :: (SMTType r, Monad m) => Maybe String -> SMTExpr r -> SMT' m (SMTExpr r)

-- | Define a new function with a body and custom type annotations for
--   arguments and result.
defFunAnnNamed :: (Args a, SMTType r, Monad m) => String -> ArgAnnotation a -> (a -> SMTExpr r) -> SMT' m (SMTFunction a r)
defFunAnnNamed' :: (Args a, SMTType r, Monad m) => Maybe String -> ArgAnnotation a -> (a -> SMTExpr r) -> SMT' m (SMTFunction a r)

-- | Like <a>defFunAnnNamed</a>, but defaults the function name to "fun".
defFunAnn :: (Args a, SMTType r, Monad m) => ArgAnnotation a -> (a -> SMTExpr r) -> SMT' m (SMTFunction a r)

-- | Boolean conjunction
and' :: SMTFunction [SMTExpr Bool] Bool
(.&&.) :: SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool

-- | Boolean disjunction
or' :: SMTFunction [SMTExpr Bool] Bool
(.||.) :: SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool

-- | Create a boolean expression that encodes that the array is equal to
--   the supplied constant array.
arrayEquals :: (LiftArgs i, Liftable i, SMTValue v, Ix (Unpacked i), Unit (ArgAnnotation i), Unit (SMTAnnotation v)) => SMTExpr (SMTArray i v) -> Array (Unpacked i) v -> SMTExpr Bool

-- | Asserts that a boolean expression is true
assert :: Monad m => SMTExpr Bool -> SMT' m ()

-- | Create a new interpolation group
interpolationGroup :: Monad m => SMT' m InterpolationGroup

-- | Assert a boolean expression and track it for an unsat core call later
assertId :: Monad m => SMTExpr Bool -> SMT' m ClauseId

-- | Assert a boolean expression to be true and assign it to an
--   interpolation group
assertInterp :: Monad m => SMTExpr Bool -> InterpolationGroup -> SMT' m ()
getInterpolant :: Monad m => [InterpolationGroup] -> SMT' m (SMTExpr Bool)
interpolate :: Monad m => [SMTExpr Bool] -> SMT' m [SMTExpr Bool]

-- | Set an option for the underlying SMT solver
setOption :: Monad m => SMTOption -> SMT' m ()

-- | Get information about the underlying SMT solver
getInfo :: (Monad m, Typeable i) => SMTInfo i -> SMT' m i

-- | Create a new uniterpreted function with annotations for the argument
--   and the return type.
funAnn :: (Liftable a, SMTType r, Monad m) => ArgAnnotation a -> SMTAnnotation r -> SMT' m (SMTFunction a r)

-- | Create a new uninterpreted named function with annotation for the
--   argument and the return type.
funAnnNamed :: (Liftable a, SMTType r, Monad m) => String -> ArgAnnotation a -> SMTAnnotation r -> SMT' m (SMTFunction a r)
funAnnNamed' :: (Liftable a, SMTType r, Monad m) => Maybe String -> ArgAnnotation a -> SMTAnnotation r -> SMT' m (SMTFunction a r)

-- | funAnn with an annotation only for the return type.
funAnnRet :: (Liftable a, SMTType r, Unit (ArgAnnotation a), Monad m) => SMTAnnotation r -> SMT' m (SMTFunction a r)

-- | Create a new uninterpreted function.
fun :: (Liftable a, SMTType r, SMTAnnotation r ~ (), Unit (ArgAnnotation a), Monad m) => SMT' m (SMTFunction a r)

-- | Apply a function to an argument
app :: (Args arg, SMTType res) => SMTFunction arg res -> arg -> SMTExpr res

-- | Lift a function to arrays
map' :: (Liftable arg, Args i, SMTType res) => SMTFunction arg res -> SMTFunction (Lifted arg i) (SMTArray i res)

-- | Two expressions shall be equal
(.==.) :: SMTType a => SMTExpr a -> SMTExpr a -> SMTExpr Bool

-- | A generalized version of <a>.==.</a>
argEq :: Args a => a -> a -> SMTExpr Bool

-- | Declares all arguments to be distinct
distinct :: SMTType a => [SMTExpr a] -> SMTExpr Bool

-- | Calculate the sum of arithmetic expressions
plus :: (SMTArith a) => SMTFunction [SMTExpr a] a

-- | Calculate the product of arithmetic expressions
mult :: (SMTArith a) => SMTFunction [SMTExpr a] a

-- | Subtracts two expressions
minus :: (SMTArith a) => SMTFunction (SMTExpr a, SMTExpr a) a

-- | Divide an arithmetic expression by another
div' :: SMTExpr Integer -> SMTExpr Integer -> SMTExpr Integer
div'' :: SMTFunction (SMTExpr Integer, SMTExpr Integer) Integer

-- | Perform a modulo operation on an arithmetic expression
mod' :: SMTExpr Integer -> SMTExpr Integer -> SMTExpr Integer
mod'' :: SMTFunction (SMTExpr Integer, SMTExpr Integer) Integer

-- | Calculate the remainder of the division of two integer expressions
rem' :: SMTExpr Integer -> SMTExpr Integer -> SMTExpr Integer
rem'' :: SMTFunction (SMTExpr Integer, SMTExpr Integer) Integer

-- | Divide a rational expression by another one
divide :: SMTExpr Rational -> SMTExpr Rational -> SMTExpr Rational
divide' :: SMTFunction (SMTExpr Rational, SMTExpr Rational) Rational

-- | For an expression <tt>x</tt>, this returns the expression <tt>-x</tt>.
neg :: SMTArith a => SMTFunction (SMTExpr a) a

-- | Convert an integer expression to a real expression
toReal :: SMTExpr Integer -> SMTExpr Rational

-- | Convert a real expression into an integer expression
toInt :: SMTExpr Rational -> SMTExpr Integer

-- | If-then-else construct
ite :: (SMTType a) => SMTExpr Bool -> SMTExpr a -> SMTExpr a -> SMTExpr a

-- | Exclusive or: Return true if exactly one argument is true.
xor :: SMTFunction [SMTExpr Bool] Bool

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

-- | Negates a boolean expression
not' :: SMTExpr Bool -> SMTExpr Bool
not'' :: SMTFunction (SMTExpr Bool) Bool

-- | Extracts an element of an array by its index
select :: (Liftable i, SMTType v) => SMTExpr (SMTArray i v) -> i -> SMTExpr v

-- | The expression <tt>store arr i v</tt> stores the value <i>v</i> in the
--   array <i>arr</i> at position <i>i</i> and returns the resulting new
--   array.
store :: (Liftable i, SMTType v) => SMTExpr (SMTArray i v) -> i -> SMTExpr v -> SMTExpr (SMTArray i v)

-- | Interpret a function <i>f</i> from <i>i</i> to <i>v</i> as an array
--   with indices <i>i</i> and elements <i>v</i>. Such that: <tt>f `app` j
--   .==. select (asArray f) j</tt> for all indices j.
asArray :: (Args arg, Unit (ArgAnnotation arg), SMTType res) => SMTFunction arg res -> SMTExpr (SMTArray arg res)

-- | Create an array where each element is the same.
constArray :: (Args i, SMTType v) => SMTExpr v -> ArgAnnotation i -> SMTExpr (SMTArray i v)

-- | Bitvector and
bvand :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector or
bvor :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector or
bvxor :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector not
bvnot :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector signed negation
bvneg :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector addition
bvadd :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector subtraction
bvsub :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector multiplication
bvmul :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector unsigned remainder
bvurem :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector signed remainder
bvsrem :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector unsigned division
bvudiv :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector signed division
bvsdiv :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector unsigned less-or-equal
bvule :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

-- | Bitvector unsigned less-than
bvult :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

-- | Bitvector unsigned greater-or-equal
bvuge :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

-- | Bitvector unsigned greater-than
bvugt :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

-- | Bitvector signed less-or-equal
bvsle :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

-- | Bitvector signed less-than
bvslt :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

-- | Bitvector signed greater-or-equal
bvsge :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

-- | Bitvector signed greater-than
bvsgt :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

-- | Bitvector shift left
bvshl :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector logical right shift
bvlshr :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector arithmetical right shift
bvashr :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Concats two bitvectors into one.
bvconcat :: (Concatable t1 t2) => SMTExpr (BitVector t1) -> SMTExpr (BitVector t2) -> SMTExpr (BitVector (ConcatResult t1 t2))

-- | Extract a sub-vector out of a given bitvector.
bvextract :: (TypeableNat start, TypeableNat len, Extractable tp len') => Proxy start -> Proxy len -> SMTExpr (BitVector tp) -> SMTExpr (BitVector len')
bvextract' :: Integer -> Integer -> SMTExpr (BitVector BVUntyped) -> SMTExpr (BitVector BVUntyped)

-- | Safely split a 16-bit bitvector into two 8-bit bitvectors.
bvsplitu16to8 :: SMTExpr BV16 -> (SMTExpr BV8, SMTExpr BV8)

-- | Safely split a 32-bit bitvector into two 16-bit bitvectors.
bvsplitu32to16 :: SMTExpr BV32 -> (SMTExpr BV16, SMTExpr BV16)

-- | Safely split a 32-bit bitvector into four 8-bit bitvectors.
bvsplitu32to8 :: SMTExpr BV32 -> (SMTExpr BV8, SMTExpr BV8, SMTExpr BV8, SMTExpr BV8)

-- | Safely split a 64-bit bitvector into two 32-bit bitvectors.
bvsplitu64to32 :: SMTExpr BV64 -> (SMTExpr BV32, SMTExpr BV32)

-- | Safely split a 64-bit bitvector into four 16-bit bitvectors.
bvsplitu64to16 :: SMTExpr BV64 -> (SMTExpr BV16, SMTExpr BV16, SMTExpr BV16, SMTExpr BV16)

-- | Safely split a 64-bit bitvector into eight 8-bit bitvectors.
bvsplitu64to8 :: SMTExpr BV64 -> (SMTExpr BV8, SMTExpr BV8, SMTExpr BV8, SMTExpr BV8, SMTExpr BV8, SMTExpr BV8, SMTExpr BV8, SMTExpr BV8)
mkQuantified :: (Args a, SMTType b) => (Integer -> [ProxyArg] -> SMTExpr b -> SMTExpr b) -> ArgAnnotation a -> (a -> SMTExpr b) -> SMTExpr b

-- | If the supplied function returns true for all possible values, the
--   forall quantification returns true.
forAll :: (Args a, Unit (ArgAnnotation a)) => (a -> SMTExpr Bool) -> SMTExpr Bool

-- | An annotated version of <a>forAll</a>.
forAllAnn :: Args a => ArgAnnotation a -> (a -> SMTExpr Bool) -> SMTExpr Bool

-- | If the supplied function returns true for at least one possible value,
--   the exists quantification returns true.
exists :: (Args a, Unit (ArgAnnotation a)) => (a -> SMTExpr Bool) -> SMTExpr Bool

-- | An annotated version of <a>exists</a>.
existsAnn :: Args a => ArgAnnotation a -> (a -> SMTExpr Bool) -> SMTExpr Bool

-- | Binds an expression to a variable. Can be used to prevent blowups in
--   the command stream if expressions are used multiple times. <tt>let' x
--   f</tt> is functionally equivalent to <tt>f x</tt>.
let' :: (Args a, Unit (ArgAnnotation a), SMTType b) => a -> (a -> SMTExpr b) -> SMTExpr b

-- | Like <a>let'</a>, but can be given an additional type annotation for
--   the argument of the function.
letAnn :: (Args a, SMTType b) => ArgAnnotation a -> a -> (a -> SMTExpr b) -> SMTExpr b

-- | Like <a>let'</a>, but can define multiple variables of the same type.
lets :: (Args a, Unit (ArgAnnotation a), SMTType b) => [a] -> ([a] -> SMTExpr b) -> SMTExpr b

-- | Like <a>forAll</a>, but can quantify over more than one variable (of
--   the same type).
forAllList :: (Args a, Unit (ArgAnnotation a)) => Integer -> ([a] -> SMTExpr Bool) -> SMTExpr Bool

-- | Like <a>exists</a>, but can quantify over more than one variable (of
--   the same type).
existsList :: (Args a, Unit (ArgAnnotation a)) => Integer -> ([a] -> SMTExpr Bool) -> SMTExpr Bool

-- | Checks if the expression is formed a specific constructor.
is :: (Args arg, SMTType dt) => SMTExpr dt -> Constructor arg dt -> SMTExpr Bool

-- | Access a field of an expression
(.#) :: (SMTType a, SMTType f) => SMTExpr a -> Field a f -> SMTExpr f

-- | Takes the first element of a list
head' :: (SMTType a, Unit (SMTAnnotation a)) => SMTExpr [a] -> SMTExpr a

-- | Drops the first element from a list
tail' :: (SMTType a, Unit (SMTAnnotation a)) => SMTExpr [a] -> SMTExpr [a]

-- | Checks if a list is empty.
isNil :: (SMTType a) => SMTExpr [a] -> SMTExpr Bool

-- | Checks if a list is non-empty.
isInsert :: (SMTType a, Unit (SMTAnnotation a)) => SMTExpr [a] -> SMTExpr Bool

-- | Sets the logic used for the following program (Not needed for many
--   solvers).
setLogic :: Monad m => String -> SMT' m ()

-- | Given an arbitrary expression, this creates a named version of it and
--   a name to reference it later on.
named :: (SMTType a, SMTAnnotation a ~ (), Monad m) => String -> SMTExpr a -> SMT' m (SMTExpr a, SMTExpr a)

-- | Like <a>named</a>, but defaults the name to "named".
named' :: (SMTType a, SMTAnnotation a ~ (), Monad m) => SMTExpr a -> SMT' m (SMTExpr a, SMTExpr a)

-- | After an unsuccessful <a>checkSat</a> this method extracts a proof
--   from the SMT solver that the instance is unsatisfiable.
getProof :: Monad m => SMT' m (SMTExpr Bool)

-- | Use the SMT solver to simplify a given expression. Currently only
--   works with Z3.
simplify :: (SMTType t, Monad m) => SMTExpr t -> SMT' m (SMTExpr t)

-- | After an unsuccessful <a>checkSat</a>, return a list of clauses which
--   make the instance unsatisfiable.
getUnsatCore :: Monad m => SMT' m [ClauseId]
optimizeExpr' :: SMTExpr a -> SMTExpr a

module Language.SMTLib2.Pipe

-- | An SMT backend which uses process pipes to communicate with an SMT
--   solver process.
data SMTPipe
newtype FunctionParser
FunctionParser :: (Lisp -> FunctionParser -> DataTypeInfo -> Maybe FunctionParser') -> FunctionParser
[parseFun] :: FunctionParser -> Lisp -> FunctionParser -> DataTypeInfo -> Maybe FunctionParser'

-- | Spawn a new SMT solver process and create a pipe to communicate with
--   it.
createSMTPipe :: String -> [String] -> IO SMTPipe
withPipe :: MonadIO m => String -> [String] -> SMT' m a -> m a
exprToLisp :: SMTExpr t -> (Integer -> String) -> DataTypeInfo -> Lisp
exprToLispWith :: (forall a. (Typeable a, Ord a, Show a) => a -> Lisp) -> SMTExpr t -> (Integer -> String) -> DataTypeInfo -> Lisp

-- | Parse a lisp expression into an SMT expression. Since we cannot know
--   what type the expression might have, we pass a general function which
--   may take any SMT expression and produce the desired result.
lispToExpr :: FunctionParser -> (Text -> Maybe (SMTExpr Untyped)) -> DataTypeInfo -> (forall a. SMTType a => SMTExpr a -> b) -> Maybe Sort -> Integer -> Lisp -> Maybe b
lispToExprWith :: (forall b. FunctionParser -> (Text -> Maybe (SMTExpr Untyped)) -> DataTypeInfo -> (forall a. SMTType a => SMTExpr a -> b) -> Maybe Sort -> Integer -> Lisp -> Maybe b) -> FunctionParser -> (Text -> Maybe (SMTExpr Untyped)) -> DataTypeInfo -> (forall a. SMTType a => SMTExpr a -> b) -> Maybe Sort -> Integer -> Lisp -> Maybe b
sortToLisp :: Sort -> Lisp

-- | Parse a lisp expression into an SMT sort.
lispToSort :: Lisp -> Maybe Sort
renderExpr :: (SMTType t, Monad m) => SMTExpr t -> SMT' m String
renderExpr' :: SMTType t => (Integer -> String) -> DataTypeInfo -> SMTExpr t -> String
renderSMTRequest :: (Maybe String -> String) -> (Integer -> String) -> DataTypeInfo -> SMTRequest r -> Either Lisp String
renderSMTResponse :: (Integer -> String) -> DataTypeInfo -> SMTRequest response -> response -> Maybe String

-- | A parser for all available SMT logics.
commonFunctions :: FunctionParser

-- | A map which contains signatures for a few common theorems which can be
--   used in the proofs which <tt>getProof</tt> returns.
commonTheorems :: FunctionParser
simpleParser :: (Liftable arg, SMTType res, Unit (ArgAnnotation arg), Unit (SMTAnnotation res)) => SMTFunction arg res -> FunctionParser
data FunctionParser'
OverloadedParser :: ([Sort] -> Bool) -> ([Sort] -> Maybe Sort) -> (forall a. [Sort] -> Sort -> (forall arg res. (Liftable arg, SMTType res) => SMTFunction arg res -> a) -> Maybe a) -> FunctionParser'
[sortConstraint] :: FunctionParser' -> [Sort] -> Bool
[deriveRetSort] :: FunctionParser' -> [Sort] -> Maybe Sort
[parseOverloaded] :: FunctionParser' -> forall a. [Sort] -> Sort -> (forall arg res. (Liftable arg, SMTType res) => SMTFunction arg res -> a) -> Maybe a
DefinedParser :: [Sort] -> Sort -> (forall a. (forall arg res. (Liftable arg, SMTType res) => SMTFunction arg res -> a) -> Maybe a) -> FunctionParser'
[definedArgSig] :: FunctionParser' -> [Sort]
[definedRetSig] :: FunctionParser' -> Sort
[parseDefined] :: FunctionParser' -> forall a. (forall arg res. (Liftable arg, SMTType res) => SMTFunction arg res -> a) -> Maybe a
instance Control.Monad.IO.Class.MonadIO m => Language.SMTLib2.Internals.SMTBackend Language.SMTLib2.Pipe.SMTPipe m
instance GHC.Base.Monoid Language.SMTLib2.Pipe.FunctionParser


-- | This module can be used if the simple <a>withSMTSolver</a>-interface
--   isn't sufficient, e.g. if you don't want to wrap your whole program
--   into one big <a>MonadSMT</a> or you want to run multiple solvers side
--   by side.
module Language.SMTLib2.Connection

-- | Represents a connection to an SMT solver. The SMT solver runs in a
--   seperate thread and communication is handled via handles.
data SMTConnection b

-- | Create a new connection to a SMT solver by spawning a shell command.
--   The solver must be able to read from stdin and write to stdout.
open :: (MonadIO m, SMTBackend b m) => b -> m (SMTConnection b)

-- | Closes an open SMT connection. Do not use the connection afterwards.
close :: (MonadIO m, SMTBackend b m) => SMTConnection b -> m ()
withConnection :: MonadIO m => SMTConnection b -> (b -> m (a, b)) -> m a

-- | Perform an action in the SMT solver associated with this connection
--   and return the result.
performSMT :: (MonadIO m, SMTBackend b m) => SMTConnection b -> SMT' m a -> m a
performSMTExitCleanly :: SMTBackend b IO => SMTConnection b -> SMT' IO a -> IO a


-- | Example usage: This program tries to find two numbers greater than
--   zero which sum up to 5.
--   
--   <pre>
--   import Language.SMTLib2
--   import Language.SMTLib2.Solver
--   
--   program :: SMT (Integer,Integer)
--   program = do
--     x &lt;- var
--     y &lt;- var
--     assert $ (plus [x,y]) .==. (constant 5)
--     assert $ x .&gt;. (constant 0)
--     assert $ y .&gt;. (constant 0)
--     checkSat
--     vx &lt;- getValue x
--     vy &lt;- getValue y
--     return (vx,vy)
--   
--   main = withZ3 program &gt;&gt;= print
--        
--   </pre>
module Language.SMTLib2

-- | The SMT monad used for communating with the SMT solver
data SMT' m a
type SMT = SMT' IO
class Monad m => SMTBackend a m
data AnyBackend m
AnyBackend :: b -> AnyBackend m

-- | Haskell types which can be represented in SMT
class (Ord t, Typeable t, Ord (SMTAnnotation t), Typeable (SMTAnnotation t), Show (SMTAnnotation t)) => SMTType t where type family SMTAnnotation t asDataType _ _ = Nothing getProxyArgs _ _ = [] additionalConstraints _ _ = Nothing

-- | Haskell values which can be represented as SMT constants
class (SMTType t, Show t) => SMTValue t

-- | A type class for all types which support arithmetic operations in SMT
class (SMTValue t, Num t, SMTAnnotation t ~ ()) => SMTArith t

-- | Lifts the <a>Ord</a> class into SMT
class (SMTType t) => SMTOrd t
(.<.) :: SMTOrd t => SMTExpr t -> SMTExpr t -> SMTExpr Bool
(.>=.) :: SMTOrd t => SMTExpr t -> SMTExpr t -> SMTExpr Bool
(.>.) :: SMTOrd t => SMTExpr t -> SMTExpr t -> SMTExpr Bool
(.<=.) :: SMTOrd t => SMTExpr t -> SMTExpr t -> SMTExpr Bool

-- | An abstract SMT expression
data SMTExpr t
data SMTFunction arg res

-- | Options controling the behaviour of the SMT solver
data SMTOption

-- | Whether or not to print "success" after each operation
PrintSuccess :: Bool -> SMTOption

-- | Produce a satisfying assignment after each successful checkSat
ProduceModels :: Bool -> SMTOption

-- | Produce a proof of unsatisfiability after each failed checkSat
ProduceProofs :: Bool -> SMTOption

-- | Enable the querying of unsatisfiable cores after a failed checkSat
ProduceUnsatCores :: Bool -> SMTOption

-- | Enable the generation of craig interpolants
ProduceInterpolants :: Bool -> SMTOption

-- | An array which maps indices of type <i>i</i> to elements of type
--   <i>v</i>.
data SMTArray (i :: *) (v :: *)

-- | Represents a constructor of a datatype <i>a</i> Can be obtained by
--   using the template haskell extension module
data Constructor arg res

-- | Represents a field of the datatype <i>a</i> of the type <i>f</i>
data Field a f

-- | Instances of this class may be used as arguments for constructed
--   functions and quantifiers.
class (Ord a, Typeable a, Show a, Ord (ArgAnnotation a), Typeable (ArgAnnotation a), Show (ArgAnnotation a)) => Args a where type family ArgAnnotation a foldExprs f s x ann = do { (s', _, r) <- foldsExprs (\ cs [(expr, _)] ann' -> do { (cs', cr) <- f cs expr ann'; return (cs', [cr], cr) }) s [(x, ())] ann; return (s', r) } fromArgs arg = fst $ foldExprsId (\ lst expr ann -> (lst ++ [UntypedExpr expr], expr)) [] arg (extractArgAnnotation arg)
foldExprs :: (Args a, Monad m) => (forall t. SMTType t => s -> SMTExpr t -> SMTAnnotation t -> m (s, SMTExpr t)) -> s -> a -> ArgAnnotation a -> m (s, a)
foldsExprs :: (Args a, 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 :: Args a => a -> ArgAnnotation a
toArgs :: Args a => ArgAnnotation a -> [SMTExpr Untyped] -> Maybe (a, [SMTExpr Untyped])
fromArgs :: Args a => a -> [SMTExpr Untyped]
getTypes :: Args a => a -> ArgAnnotation a -> [ProxyArg]
getArgAnnotation :: Args a => a -> [Sort] -> (ArgAnnotation a, [Sort])

-- | An extension of the <a>Args</a> class: Instances of this class can be
--   represented as native haskell data types.
class Args a => LiftArgs a where type family Unpacked a

-- | Converts a haskell value into its SMT representation.
liftArgs :: LiftArgs a => Unpacked a -> ArgAnnotation a -> a

-- | Converts a SMT representation back into a haskell value.
unliftArgs :: (LiftArgs a, Monad m) => a -> (forall t. SMTValue t => SMTExpr t -> m t) -> m (Unpacked a)
withSMTBackend :: SMTBackend a m => a -> SMT' m b -> m b
withSMTBackendExitCleanly :: SMTBackend b IO => b -> SMT a -> IO a

-- | Set an option for the underlying SMT solver
setOption :: Monad m => SMTOption -> SMT' m ()

-- | Get information about the underlying SMT solver
getInfo :: (Monad m, Typeable i) => SMTInfo i -> SMT' m i

-- | Sets the logic used for the following program (Not needed for many
--   solvers).
setLogic :: Monad m => String -> SMT' m ()
data SMTInfo i
SMTSolverName :: SMTInfo String
SMTSolverVersion :: SMTInfo String

-- | Asserts that a boolean expression is true
assert :: Monad m => SMTExpr Bool -> SMT' m ()

-- | Push a new context on the stack
push :: Monad m => SMT' m ()

-- | Pop a new context from the stack
pop :: Monad m => SMT' m ()

-- | Perform a stacked operation, meaning that every assertion and
--   declaration made in it will be undone after the operation.
stack :: Monad m => SMT' m a -> SMT' m a

-- | Check if the model is satisfiable (e.g. if there is a value for each
--   variable so that every assertion holds)
checkSat :: Monad m => SMT' m Bool

-- | Like <a>checkSat</a>, but gives you more options like choosing a
--   tactic (Z3 only) or providing memory/time-limits
checkSat' :: Monad m => Maybe Tactic -> CheckSatLimits -> SMT' m CheckSatResult

-- | Check if the model is satisfiable using a given tactic. (Works only
--   with Z3)
checkSatUsing :: Monad m => Tactic -> SMT' m Bool

-- | Apply the given tactic to the current assertions. (Works only with Z3)
apply :: Monad m => Tactic -> SMT' m [SMTExpr Bool]

-- | The result of a check-sat query
data CheckSatResult

-- | The formula is satisfiable
Sat :: CheckSatResult

-- | The formula is unsatisfiable
Unsat :: CheckSatResult

-- | The solver cannot determine the satisfiability of a formula
Unknown :: CheckSatResult

-- | Describe limits on the ressources that an SMT-solver can use
data CheckSatLimits
CheckSatLimits :: Maybe Integer -> Maybe Integer -> CheckSatLimits

-- | A limit on the amount of time the solver can spend on the problem (in
--   milliseconds)
[limitTime] :: CheckSatLimits -> Maybe Integer

-- | A limit on the amount of memory the solver can use (in megabytes)
[limitMemory] :: CheckSatLimits -> Maybe Integer
noLimits :: CheckSatLimits
getValue :: (SMTValue t, Monad m) => SMTExpr t -> SMT' m t
getValues :: (LiftArgs arg, Monad m) => arg -> SMT' m (Unpacked arg)

-- | Extract all assigned values of the model
getModel :: Monad m => SMT' m SMTModel

-- | Insert a comment into the SMTLib2 command stream. If you aren't
--   looking at the command stream for debugging, this will do nothing.
comment :: Monad m => String -> SMT' m ()

-- | After an unsuccessful <a>checkSat</a> this method extracts a proof
--   from the SMT solver that the instance is unsatisfiable.
getProof :: Monad m => SMT' m (SMTExpr Bool)

-- | Use the SMT solver to simplify a given expression. Currently only
--   works with Z3.
simplify :: (SMTType t, Monad m) => SMTExpr t -> SMT' m (SMTExpr t)

-- | Identifies a clause in an unsatisfiable core
data ClauseId

-- | Assert a boolean expression and track it for an unsat core call later
assertId :: Monad m => SMTExpr Bool -> SMT' m ClauseId

-- | After an unsuccessful <a>checkSat</a>, return a list of clauses which
--   make the instance unsatisfiable.
getUnsatCore :: Monad m => SMT' m [ClauseId]
data InterpolationGroup

-- | Create a new interpolation group
interpolationGroup :: Monad m => SMT' m InterpolationGroup

-- | Assert a boolean expression to be true and assign it to an
--   interpolation group
assertInterp :: Monad m => SMTExpr Bool -> InterpolationGroup -> SMT' m ()
getInterpolant :: Monad m => [InterpolationGroup] -> SMT' m (SMTExpr Bool)
interpolate :: Monad m => [SMTExpr Bool] -> SMT' m [SMTExpr Bool]

-- | Create a fresh new variable
var :: (SMTType t, Typeable t, Unit (SMTAnnotation t), Monad m) => SMT' m (SMTExpr t)

-- | Create a new named variable
varNamed :: (SMTType t, Typeable t, Unit (SMTAnnotation t), Monad m) => String -> SMT' m (SMTExpr t)

-- | Create a named and annotated variable.
varNamedAnn :: (SMTType t, Typeable t, Monad m) => String -> SMTAnnotation t -> SMT' m (SMTExpr t)

-- | Create a annotated variable
varAnn :: (SMTType t, Typeable t, Monad m) => SMTAnnotation t -> SMT' m (SMTExpr t)

-- | Like <a>argVarsAnn</a>, but can only be used for unit type
--   annotations.
argVars :: (Args a, Unit (ArgAnnotation a), Monad m) => SMT' m a

-- | Like <a>argVarsAnnNamed</a>, but defaults the name to "var"
argVarsAnn :: (Args a, Monad m) => ArgAnnotation a -> SMT' m a

-- | Create annotated named SMT variables of the <a>Args</a> class. If more
--   than one variable is needed, they get a numerical suffix.
argVarsAnnNamed :: (Args a, Monad m) => String -> ArgAnnotation a -> SMT' m a

-- | Create a fresh untyped variable
untypedVar :: Monad m => Sort -> SMT' m (SMTExpr Untyped)

-- | Create a fresh untyped variable with a name
untypedNamedVar :: Monad m => String -> Sort -> SMT' m (SMTExpr Untyped)

-- | A constant expression.
constant :: (SMTValue t, Unit (SMTAnnotation t)) => t -> SMTExpr t

-- | An annotated constant expression.
constantAnn :: SMTValue t => t -> SMTAnnotation t -> SMTExpr t

-- | Reconstruct the type annotation for a given SMT expression.
extractAnnotation :: SMTExpr a -> SMTAnnotation a

-- | Binds an expression to a variable. Can be used to prevent blowups in
--   the command stream if expressions are used multiple times. <tt>let' x
--   f</tt> is functionally equivalent to <tt>f x</tt>.
let' :: (Args a, Unit (ArgAnnotation a), SMTType b) => a -> (a -> SMTExpr b) -> SMTExpr b

-- | Like <a>let'</a>, but can define multiple variables of the same type.
lets :: (Args a, Unit (ArgAnnotation a), SMTType b) => [a] -> ([a] -> SMTExpr b) -> SMTExpr b

-- | Like <a>let'</a>, but can be given an additional type annotation for
--   the argument of the function.
letAnn :: (Args a, SMTType b) => ArgAnnotation a -> a -> (a -> SMTExpr b) -> SMTExpr b

-- | Given an arbitrary expression, this creates a named version of it and
--   a name to reference it later on.
named :: (SMTType a, SMTAnnotation a ~ (), Monad m) => String -> SMTExpr a -> SMT' m (SMTExpr a, SMTExpr a)

-- | Like <a>named</a>, but defaults the name to "named".
named' :: (SMTType a, SMTAnnotation a ~ (), Monad m) => SMTExpr a -> SMT' m (SMTExpr a, SMTExpr a)
optimizeExpr :: SMTExpr t -> Maybe (SMTExpr t)
optimizeExpr' :: SMTExpr a -> SMTExpr a

-- | Recursively fold a function over all sub-expressions of this
--   expression. It is implemented as a special case of <a>foldExprM</a>.
foldExpr :: SMTType a => (forall t. SMTType t => s -> SMTExpr t -> (s, SMTExpr t)) -> s -> SMTExpr a -> (s, SMTExpr a)

-- | Recursively fold a monadic function over all sub-expressions of this
--   expression
foldExprM :: (SMTType a, Monad m) => (forall t. SMTType t => s -> SMTExpr t -> m (s, [SMTExpr t])) -> s -> SMTExpr a -> m (s, [SMTExpr a])

-- | Recursively fold a function over all sub-expressions of the argument.
--   It is implemented as a special case of <a>foldArgsM</a>.
foldArgs :: Args a => (forall t. SMTType t => s -> SMTExpr t -> (s, SMTExpr t)) -> s -> a -> (s, a)

-- | Recursively fold a monadic function over all sub-expressions of the
--   argument
foldArgsM :: (Args a, Monad m) => (forall t. SMTType t => s -> SMTExpr t -> m (s, [SMTExpr t])) -> s -> a -> m (s, [a])

-- | Two expressions shall be equal
(.==.) :: SMTType a => SMTExpr a -> SMTExpr a -> SMTExpr Bool

-- | A generalized version of <a>.==.</a>
argEq :: Args a => a -> a -> SMTExpr Bool

-- | Declares all arguments to be distinct
distinct :: SMTType a => [SMTExpr a] -> SMTExpr Bool

-- | If-then-else construct
ite :: (SMTType a) => SMTExpr Bool -> SMTExpr a -> SMTExpr a -> SMTExpr a
(.&&.) :: SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool
(.||.) :: SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool

-- | Boolean conjunction
and' :: SMTFunction [SMTExpr Bool] Bool

-- | Boolean disjunction
or' :: SMTFunction [SMTExpr Bool] Bool

-- | Exclusive or: Return true if exactly one argument is true.
xor :: SMTFunction [SMTExpr Bool] Bool

-- | Negates a boolean expression
not' :: SMTExpr Bool -> SMTExpr Bool
not'' :: SMTFunction (SMTExpr Bool) Bool

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

-- | If the supplied function returns true for all possible values, the
--   forall quantification returns true.
forAll :: (Args a, Unit (ArgAnnotation a)) => (a -> SMTExpr Bool) -> SMTExpr Bool

-- | If the supplied function returns true for at least one possible value,
--   the exists quantification returns true.
exists :: (Args a, Unit (ArgAnnotation a)) => (a -> SMTExpr Bool) -> SMTExpr Bool

-- | An annotated version of <a>forAll</a>.
forAllAnn :: Args a => ArgAnnotation a -> (a -> SMTExpr Bool) -> SMTExpr Bool

-- | An annotated version of <a>exists</a>.
existsAnn :: Args a => ArgAnnotation a -> (a -> SMTExpr Bool) -> SMTExpr Bool

-- | Like <a>forAll</a>, but can quantify over more than one variable (of
--   the same type).
forAllList :: (Args a, Unit (ArgAnnotation a)) => Integer -> ([a] -> SMTExpr Bool) -> SMTExpr Bool

-- | Like <a>exists</a>, but can quantify over more than one variable (of
--   the same type).
existsList :: (Args a, Unit (ArgAnnotation a)) => Integer -> ([a] -> SMTExpr Bool) -> SMTExpr Bool

-- | Calculate the sum of arithmetic expressions
plus :: (SMTArith a) => SMTFunction [SMTExpr a] a

-- | Subtracts two expressions
minus :: (SMTArith a) => SMTFunction (SMTExpr a, SMTExpr a) a

-- | Calculate the product of arithmetic expressions
mult :: (SMTArith a) => SMTFunction [SMTExpr a] a

-- | Divide an arithmetic expression by another
div' :: SMTExpr Integer -> SMTExpr Integer -> SMTExpr Integer

-- | Perform a modulo operation on an arithmetic expression
mod' :: SMTExpr Integer -> SMTExpr Integer -> SMTExpr Integer

-- | Calculate the remainder of the division of two integer expressions
rem' :: SMTExpr Integer -> SMTExpr Integer -> SMTExpr Integer

-- | For an expression <tt>x</tt>, this returns the expression <tt>-x</tt>.
neg :: SMTArith a => SMTFunction (SMTExpr a) a

-- | Divide a rational expression by another one
divide :: SMTExpr Rational -> SMTExpr Rational -> SMTExpr Rational

-- | Convert an integer expression to a real expression
toReal :: SMTExpr Integer -> SMTExpr Rational

-- | Convert a real expression into an integer expression
toInt :: SMTExpr Rational -> SMTExpr Integer

-- | Extracts an element of an array by its index
select :: (Liftable i, SMTType v) => SMTExpr (SMTArray i v) -> i -> SMTExpr v

-- | The expression <tt>store arr i v</tt> stores the value <i>v</i> in the
--   array <i>arr</i> at position <i>i</i> and returns the resulting new
--   array.
store :: (Liftable i, SMTType v) => SMTExpr (SMTArray i v) -> i -> SMTExpr v -> SMTExpr (SMTArray i v)

-- | Create a boolean expression that encodes that the array is equal to
--   the supplied constant array.
arrayEquals :: (LiftArgs i, Liftable i, SMTValue v, Ix (Unpacked i), Unit (ArgAnnotation i), Unit (SMTAnnotation v)) => SMTExpr (SMTArray i v) -> Array (Unpacked i) v -> SMTExpr Bool

-- | Extract all values of an array by giving the range of indices.
unmangleArray :: (Liftable i, LiftArgs i, Ix (Unpacked i), SMTValue v, Unit (ArgAnnotation i), Monad m) => (Unpacked i, Unpacked i) -> SMTExpr (SMTArray i v) -> SMT' m (Array (Unpacked i) v)

-- | Interpret a function <i>f</i> from <i>i</i> to <i>v</i> as an array
--   with indices <i>i</i> and elements <i>v</i>. Such that: <tt>f `app` j
--   .==. select (asArray f) j</tt> for all indices j.
asArray :: (Args arg, Unit (ArgAnnotation arg), SMTType res) => SMTFunction arg res -> SMTExpr (SMTArray arg res)

-- | Create an array where each element is the same.
constArray :: (Args i, SMTType v) => SMTExpr v -> ArgAnnotation i -> SMTExpr (SMTArray i v)

-- | Bitvector and
bvand :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector or
bvor :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector or
bvxor :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector not
bvnot :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector signed negation
bvneg :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector addition
bvadd :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector subtraction
bvsub :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector multiplication
bvmul :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector unsigned remainder
bvurem :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector signed remainder
bvsrem :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector unsigned division
bvudiv :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector signed division
bvsdiv :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector unsigned less-or-equal
bvule :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

-- | Bitvector unsigned less-than
bvult :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

-- | Bitvector unsigned greater-or-equal
bvuge :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

-- | Bitvector unsigned greater-than
bvugt :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

-- | Bitvector signed less-or-equal
bvsle :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

-- | Bitvector signed less-than
bvslt :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

-- | Bitvector signed greater-or-equal
bvsge :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

-- | Bitvector signed greater-than
bvsgt :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool

-- | Bitvector shift left
bvshl :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector logical right shift
bvlshr :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)

-- | Bitvector arithmetical right shift
bvashr :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)
data BitVector (b :: *)
BitVector :: Integer -> BitVector
data BVTyped n
data BVUntyped
type BV8 = BitVector (BVTyped N8)
type BV16 = BitVector (BVTyped N16)
type BV32 = BitVector (BVTyped N32)
type BV64 = BitVector (BVTyped N64)
type N0 = Z
type N1 = S N0
type N2 = S N1
type N3 = S N2
type N4 = S N3
type N5 = S N4
type N6 = S N5
type N7 = S N6
type N8 = S N7
type N9 = S N8
type N10 = S N9
type N11 = S N10
type N12 = S N11
type N13 = S N12
type N14 = S N13
type N15 = S N14
type N16 = S N15
type N17 = S N16
type N18 = S N17
type N19 = S N18
type N20 = S N19
type N21 = S N20
type N22 = S N21
type N23 = S N22
type N24 = S N23
type N25 = S N24
type N26 = S N25
type N27 = S N26
type N28 = S N27
type N29 = S N28
type N30 = S N29
type N31 = S N30
type N32 = S N31
type N33 = S N32
type N34 = S N33
type N35 = S N34
type N36 = S N35
type N37 = S N36
type N38 = S N37
type N39 = S N38
type N40 = S N39
type N41 = S N40
type N42 = S N41
type N43 = S N42
type N44 = S N43
type N45 = S N44
type N46 = S N45
type N47 = S N46
type N48 = S N47
type N49 = S N48
type N50 = S N49
type N51 = S N50
type N52 = S N51
type N53 = S N52
type N54 = S N53
type N55 = S N54
type N56 = S N55
type N57 = S N56
type N58 = S N57
type N59 = S N58
type N60 = S N59
type N61 = S N60
type N62 = S N61
type N63 = S N62
type N64 = S N63

-- | Concats two bitvectors into one.
bvconcat :: (Concatable t1 t2) => SMTExpr (BitVector t1) -> SMTExpr (BitVector t2) -> SMTExpr (BitVector (ConcatResult t1 t2))

-- | Safely split a 16-bit bitvector into two 8-bit bitvectors.
bvsplitu16to8 :: SMTExpr BV16 -> (SMTExpr BV8, SMTExpr BV8)

-- | Safely split a 32-bit bitvector into two 16-bit bitvectors.
bvsplitu32to16 :: SMTExpr BV32 -> (SMTExpr BV16, SMTExpr BV16)

-- | Safely split a 32-bit bitvector into four 8-bit bitvectors.
bvsplitu32to8 :: SMTExpr BV32 -> (SMTExpr BV8, SMTExpr BV8, SMTExpr BV8, SMTExpr BV8)

-- | Safely split a 64-bit bitvector into two 32-bit bitvectors.
bvsplitu64to32 :: SMTExpr BV64 -> (SMTExpr BV32, SMTExpr BV32)

-- | Safely split a 64-bit bitvector into four 16-bit bitvectors.
bvsplitu64to16 :: SMTExpr BV64 -> (SMTExpr BV16, SMTExpr BV16, SMTExpr BV16, SMTExpr BV16)

-- | Safely split a 64-bit bitvector into eight 8-bit bitvectors.
bvsplitu64to8 :: SMTExpr BV64 -> (SMTExpr BV8, SMTExpr BV8, SMTExpr BV8, SMTExpr BV8, SMTExpr BV8, SMTExpr BV8, SMTExpr BV8, SMTExpr BV8)

-- | Extract a sub-vector out of a given bitvector.
bvextract :: (TypeableNat start, TypeableNat len, Extractable tp len') => Proxy start -> Proxy len -> SMTExpr (BitVector tp) -> SMTExpr (BitVector len')
bvextract' :: Integer -> Integer -> SMTExpr (BitVector BVUntyped) -> SMTExpr (BitVector BVUntyped)

-- | Create a new uniterpreted function with annotations for the argument
--   and the return type.
funAnn :: (Liftable a, SMTType r, Monad m) => ArgAnnotation a -> SMTAnnotation r -> SMT' m (SMTFunction a r)

-- | Create a new uninterpreted named function with annotation for the
--   argument and the return type.
funAnnNamed :: (Liftable a, SMTType r, Monad m) => String -> ArgAnnotation a -> SMTAnnotation r -> SMT' m (SMTFunction a r)

-- | funAnn with an annotation only for the return type.
funAnnRet :: (Liftable a, SMTType r, Unit (ArgAnnotation a), Monad m) => SMTAnnotation r -> SMT' m (SMTFunction a r)

-- | Create a new uninterpreted function.
fun :: (Liftable a, SMTType r, SMTAnnotation r ~ (), Unit (ArgAnnotation a), Monad m) => SMT' m (SMTFunction a r)

-- | Apply a function to an argument
app :: (Args arg, SMTType res) => SMTFunction arg res -> arg -> SMTExpr res

-- | Define a new function with a body
defFun :: (Args a, SMTType r, Unit (ArgAnnotation a), Monad m) => (a -> SMTExpr r) -> SMT' m (SMTFunction a r)

-- | Define a new constant.
defConst :: (SMTType r, Monad m) => SMTExpr r -> SMT' m (SMTExpr r)

-- | Define a new constant with a name
defConstNamed :: (SMTType r, Monad m) => String -> SMTExpr r -> SMT' m (SMTExpr r)

-- | Like <a>defFunAnnNamed</a>, but defaults the function name to "fun".
defFunAnn :: (Args a, SMTType r, Monad m) => ArgAnnotation a -> (a -> SMTExpr r) -> SMT' m (SMTFunction a r)

-- | Define a new function with a body and custom type annotations for
--   arguments and result.
defFunAnnNamed :: (Args a, SMTType r, Monad m) => String -> ArgAnnotation a -> (a -> SMTExpr r) -> SMT' m (SMTFunction a r)

-- | Lift a function to arrays
map' :: (Liftable arg, Args i, SMTType res) => SMTFunction arg res -> SMTFunction (Lifted arg i) (SMTArray i res)

-- | Checks if the expression is formed a specific constructor.
is :: (Args arg, SMTType dt) => SMTExpr dt -> Constructor arg dt -> SMTExpr Bool

-- | Access a field of an expression
(.#) :: (SMTType a, SMTType f) => SMTExpr a -> Field a f -> SMTExpr f

-- | Takes the first element of a list
head' :: (SMTType a, Unit (SMTAnnotation a)) => SMTExpr [a] -> SMTExpr a

-- | Drops the first element from a list
tail' :: (SMTType a, Unit (SMTAnnotation a)) => SMTExpr [a] -> SMTExpr [a]
insert' :: SMTType a => SMTAnnotation a -> Constructor (SMTExpr a, SMTExpr [a]) [a]

-- | Checks if a list is empty.
isNil :: (SMTType a) => SMTExpr [a] -> SMTExpr Bool

-- | Checks if a list is non-empty.
isInsert :: (SMTType a, Unit (SMTAnnotation a)) => SMTExpr [a] -> SMTExpr Bool
data Untyped
data UntypedValue
entype :: (forall a. SMTType a => SMTExpr a -> b) -> SMTExpr Untyped -> b
entypeValue :: (forall a. SMTValue a => SMTExpr a -> b) -> SMTExpr UntypedValue -> b
castUntypedExpr :: SMTType t => SMTExpr Untyped -> SMTExpr t
castUntypedExprValue :: SMTType t => SMTExpr UntypedValue -> SMTExpr t


-- | Gives interfaces to some common SMT solvers.
module Language.SMTLib2.Solver

-- | Z3 is a solver by Microsoft
--   <a>http://research.microsoft.com/en-us/um/redmond/projects/z3</a>.
withZ3 :: MonadIO m => SMT' m a -> m a

-- | MathSAT <a>http://mathsat.fbk.eu</a>.
withMathSat :: MonadIO m => SMT' m a -> m a

-- | CVC4 is an open-source SMT solver <a>http://cs.nyu.edu/acsys/cvc4</a>
withCVC4 :: MonadIO m => SMT' m a -> m a

-- | SMTInterpol is an experimental interpolating SMT solver
--   <a>http://ultimate.informatik.uni-freiburg.de/smtinterpol</a>
withSMTInterpol :: MonadIO m => SMT' m a -> m a