Copyright	(c) Galois Inc 2014-2020.
License	BSD3
Maintainer	Joe Hendrix <jhendrix@galois.com>
Safe Haskell	None
Language	Haskell2010

What4.Protocol.SMTWriter

Contents

Type classes
Terms
SMTWriter
SMTWriter operations
Reexports

Description

This defines common definitions used in writing SMTLIB (2.0 and later), and yices outputs from Expr values.

The writer is designed to support solvers with arithmetic, propositional logic, bitvector, tuples (aka. structs), and arrays.

It maps complex Expr values to either structs or arrays depending on what the solver supports (structs are preferred if both are supported).

It maps multi-dimensional arrays to either arrays with structs as indices if structs are supported or nested arrays if they are not.

The solver should detect when something is not supported and give an error rather than sending invalid output to a file.

Synopsis

class Num v => SupportTermOps v where
- boolExpr :: Bool -> v
- notExpr :: v -> v
- andAll :: [v] -> v
- orAll :: [v] -> v
- (.&&) :: v -> v -> v
- (.||) :: v -> v -> v
- (.==) :: v -> v -> v
- (./=) :: v -> v -> v
- impliesExpr :: v -> v -> v
- letExpr :: [(Text, v)] -> v -> v
- ite :: v -> v -> v -> v
- sumExpr :: [v] -> v
- termIntegerToReal :: v -> v
- termRealToInteger :: v -> v
- integerTerm :: Integer -> v
- rationalTerm :: Rational -> v
- (.<=) :: v -> v -> v
- (.<) :: v -> v -> v
- (.>) :: v -> v -> v
- (.>=) :: v -> v -> v
- intAbs :: v -> v
- intDiv :: v -> v -> v
- intMod :: v -> v -> v
- intDivisible :: v -> Natural -> v
- bvTerm :: NatRepr w -> BV w -> v
- bvNeg :: v -> v
- bvAdd :: v -> v -> v
- bvSub :: v -> v -> v
- bvMul :: v -> v -> v
- bvSLe :: v -> v -> v
- bvULe :: v -> v -> v
- bvSLt :: v -> v -> v
- bvULt :: v -> v -> v
- bvUDiv :: v -> v -> v
- bvURem :: v -> v -> v
- bvSDiv :: v -> v -> v
- bvSRem :: v -> v -> v
- bvAnd :: v -> v -> v
- bvOr :: v -> v -> v
- bvXor :: v -> v -> v
- bvNot :: v -> v
- bvShl :: v -> v -> v
- bvLshr :: v -> v -> v
- bvAshr :: v -> v -> v
- bvConcat :: v -> v -> v
- bvExtract :: NatRepr w -> Natural -> Natural -> v -> v
- bvTestBit :: NatRepr w -> Natural -> v -> v
- bvSumExpr :: NatRepr w -> [v] -> v
- floatTerm :: FloatPrecisionRepr fpp -> BigFloat -> v
- floatNeg :: v -> v
- floatAbs :: v -> v
- floatSqrt :: RoundingMode -> v -> v
- floatAdd :: RoundingMode -> v -> v -> v
- floatSub :: RoundingMode -> v -> v -> v
- floatMul :: RoundingMode -> v -> v -> v
- floatDiv :: RoundingMode -> v -> v -> v
- floatRem :: v -> v -> v
- floatFMA :: RoundingMode -> v -> v -> v -> v
- floatEq :: v -> v -> v
- floatFpEq :: v -> v -> v
- floatLe :: v -> v -> v
- floatLt :: v -> v -> v
- floatIsNaN :: v -> v
- floatIsInf :: v -> v
- floatIsZero :: v -> v
- floatIsPos :: v -> v
- floatIsNeg :: v -> v
- floatIsSubnorm :: v -> v
- floatIsNorm :: v -> v
- floatCast :: FloatPrecisionRepr fpp -> RoundingMode -> v -> v
- floatRound :: RoundingMode -> v -> v
- floatFromBinary :: FloatPrecisionRepr fpp -> v -> v
- bvToFloat :: FloatPrecisionRepr fpp -> RoundingMode -> v -> v
- sbvToFloat :: FloatPrecisionRepr fpp -> RoundingMode -> v -> v
- realToFloat :: FloatPrecisionRepr fpp -> RoundingMode -> v -> v
- floatToBV :: Natural -> RoundingMode -> v -> v
- floatToSBV :: Natural -> RoundingMode -> v -> v
- floatToReal :: v -> v
- realIsInteger :: v -> v
- realDiv :: v -> v -> v
- realSin :: v -> v
- realCos :: v -> v
- realATan2 :: v -> v -> v
- realSinh :: v -> v
- realCosh :: v -> v
- realExp :: v -> v
- realLog :: v -> v
- smtFnApp :: v -> [v] -> v
- smtFnUpdate :: Maybe (v -> [v] -> v -> v)
- lambdaTerm :: Maybe ([(Text, Some TypeMap)] -> v -> v)
- fromText :: Text -> v
type ArrayConstantFn v = [Some TypeMap] -> Some TypeMap -> v -> v
class SupportTermOps (Term h) => SMTWriter h where
- forallExpr :: [(Text, Some TypeMap)] -> Term h -> Term h
- existsExpr :: [(Text, Some TypeMap)] -> Term h -> Term h
- arrayConstant :: Maybe (ArrayConstantFn (Term h))
- arraySelect :: Term h -> [Term h] -> Term h
- arrayUpdate :: Term h -> [Term h] -> Term h -> Term h
- commentCommand :: f h -> Builder -> Command h
- assertCommand :: f h -> Term h -> Command h
- assertNamedCommand :: f h -> Term h -> Text -> Command h
- pushCommand :: f h -> Command h
- popCommand :: f h -> Command h
- popManyCommands :: f h -> Int -> [Command h]
- resetCommand :: f h -> Command h
- checkCommands :: f h -> [Command h]
- checkWithAssumptionsCommands :: f h -> [Text] -> [Command h]
- getUnsatAssumptionsCommand :: f h -> Command h
- getUnsatCoreCommand :: f h -> Command h
- setOptCommand :: f h -> Text -> Text -> Command h
- declareCommand :: f h -> Text -> Assignment TypeMap args -> TypeMap rtp -> Command h
- defineCommand :: f h -> Text -> [(Text, Some TypeMap)] -> TypeMap rtp -> Term h -> Command h
- declareStructDatatype :: WriterConn t h -> Assignment TypeMap args -> IO ()
- structCtor :: Assignment TypeMap args -> [Term h] -> Term h
- structProj :: Assignment TypeMap args -> Index args tp -> Term h -> Term h
- stringTerm :: ByteString -> Term h
- stringLength :: Term h -> Term h
- stringIndexOf :: Term h -> Term h -> Term h -> Term h
- stringContains :: Term h -> Term h -> Term h
- stringIsPrefixOf :: Term h -> Term h -> Term h
- stringIsSuffixOf :: Term h -> Term h -> Term h
- stringSubstring :: Term h -> Term h -> Term h -> Term h
- stringAppend :: [Term h] -> Term h
- resetDeclaredStructs :: WriterConn t h -> IO ()
- writeCommand :: WriterConn t h -> Command h -> IO ()
class SMTWriter h => SMTReadWriter h where
- smtEvalFuns :: WriterConn t h -> InputStream Text -> SMTEvalFunctions h
- smtSatResult :: f h -> InputStream Text -> IO (SatResult () ())
- smtUnsatCoreResult :: f h -> InputStream Text -> IO [Text]
- smtUnsatAssumptionsResult :: f h -> InputStream Text -> IO [(Bool, Text)]
type SMTEvalBVArrayFn h w v = (1 <= w, 1 <= v) => NatRepr w -> NatRepr v -> Term h -> IO (Maybe (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v)))
newtype SMTEvalBVArrayWrapper h = SMTEvalBVArrayWrapper {
- unEvalBVArrayWrapper :: forall w v. SMTEvalBVArrayFn h w v
}
type family Term (h :: Type) :: Type
app :: Builder -> [Builder] -> Builder
app_list :: Builder -> [Builder] -> Builder
builder_list :: [Builder] -> Builder
data WriterConn t (h :: Type)
connState :: WriterConn t h -> h
newWriterConn :: OutputStream Text -> InputStream Text -> AcknowledgementAction t cs -> String -> ProblemFeatures -> SymbolVarBimap t -> cs -> IO (WriterConn t cs)
resetEntryStack :: WriterConn t h -> IO ()
popEntryStackToTop :: WriterConn t h -> IO Int
entryStackHeight :: WriterConn t h -> IO Int
pushEntryStack :: WriterConn t h -> IO ()
popEntryStack :: WriterConn t h -> IO ()
type family Command (h :: Type) :: Type
addCommand :: SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommandNoAck :: SMTWriter h => WriterConn t h -> Command h -> IO ()
addCommands :: SMTWriter h => WriterConn t h -> [Command h] -> IO ()
mkFreeVar :: SMTWriter h => WriterConn t h -> Assignment TypeMap args -> TypeMap rtp -> IO Text
bindVarAsFree :: SMTWriter h => WriterConn t h -> ExprBoundVar t tp -> IO ()
data TypeMap (tp :: BaseType) where
- BoolTypeMap :: TypeMap BaseBoolType
- IntegerTypeMap :: TypeMap BaseIntegerType
- RealTypeMap :: TypeMap BaseRealType
- BVTypeMap :: 1 <= w => !(NatRepr w) -> TypeMap (BaseBVType w)
- FloatTypeMap :: !(FloatPrecisionRepr fpp) -> TypeMap (BaseFloatType fpp)
- Char8TypeMap :: TypeMap (BaseStringType Char8)
- ComplexToStructTypeMap :: TypeMap BaseComplexType
- ComplexToArrayTypeMap :: TypeMap BaseComplexType
- PrimArrayTypeMap :: !(Assignment TypeMap (idxl ::> idx)) -> !(TypeMap tp) -> TypeMap (BaseArrayType (idxl ::> idx) tp)
- FnArrayTypeMap :: !(Assignment TypeMap (idxl ::> idx)) -> TypeMap tp -> TypeMap (BaseArrayType (idxl ::> idx) tp)
- StructTypeMap :: !(Assignment TypeMap idx) -> TypeMap (BaseStructType idx)
typeMap :: WriterConn t h -> BaseTypeRepr tp -> Either BaseTypeError (TypeMap tp)
freshBoundVarName :: SMTWriter h => WriterConn t h -> DefineStyle -> [(Text, Some TypeMap)] -> TypeMap rtp -> Term h -> IO Text
assumeFormula :: SMTWriter h => WriterConn t h -> Term h -> IO ()
assumeFormulaWithName :: SMTWriter h => WriterConn t h -> Term h -> Text -> IO ()
assumeFormulaWithFreshName :: SMTWriter h => WriterConn t h -> Term h -> IO Text
data DefineStyle
- = FunctionDefinition
- | EqualityDefinition
newtype AcknowledgementAction t h = AckAction {
- runAckAction :: WriterConn t h -> Command h -> IO ()
}
nullAcknowledgementAction :: AcknowledgementAction t h
assume :: SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
mkSMTTerm :: SMTWriter h => WriterConn t h -> Expr t tp -> IO (Term h)
mkFormula :: SMTWriter h => WriterConn t h -> BoolExpr t -> IO (Term h)
mkAtomicFormula :: SMTWriter h => WriterConn t h -> BoolExpr t -> IO Text
data SMTEvalFunctions h = SMTEvalFunctions {
- smtEvalBool :: Term h -> IO Bool
- smtEvalBV :: forall w. NatRepr w -> Term h -> IO (BV w)
- smtEvalReal :: Term h -> IO Rational
- smtEvalFloat :: forall fpp. FloatPrecisionRepr fpp -> Term h -> IO (BV (FloatPrecisionBits fpp))
- smtEvalBvArray :: Maybe (SMTEvalBVArrayWrapper h)
- smtEvalString :: Term h -> IO ByteString
}
smtExprGroundEvalFn :: forall t h. SMTWriter h => WriterConn t h -> SMTEvalFunctions h -> IO (GroundEvalFn t)
data CollectorResults h a = CollectorResults {
- crResult :: !a
- crBindings :: ![(Text, Term h)]
- crFreeConstants :: ![(Text, Some TypeMap)]
- crSideConds :: ![Term h]
}
mkBaseExpr :: SMTWriter h => Expr t tp -> SMTCollector t h (Term h)
runInSandbox :: SupportTermOps (Term h) => WriterConn t h -> SMTCollector t h a -> IO (CollectorResults h a)
data RoundingMode
- = RNE
- | RNA
- | RTP
- | RTN
- | RTZ

Type classes

class Num v => SupportTermOps v where Source #

A class of values containing rational and operations.

Minimal complete definition

boolExpr, notExpr, andAll, orAll, (.==), letExpr, ite, termIntegerToReal, termRealToInteger, integerTerm, rationalTerm, (.<=), intAbs, intDiv, intMod, intDivisible, bvTerm, bvNeg, bvAdd, bvSub, bvMul, bvSLe, bvULe, bvSLt, bvULt, bvUDiv, bvURem, bvSDiv, bvSRem, bvAnd, bvOr, bvXor, bvNot, bvShl, bvLshr, bvAshr, bvConcat, bvExtract, floatTerm, floatNeg, floatAbs, floatSqrt, floatAdd, floatSub, floatMul, floatDiv, floatRem, floatFMA, floatEq, floatFpEq, floatLe, floatLt, floatIsNaN, floatIsInf, floatIsZero, floatIsPos, floatIsNeg, floatIsSubnorm, floatIsNorm, floatCast, floatRound, floatFromBinary, bvToFloat, sbvToFloat, realToFloat, floatToBV, floatToSBV, floatToReal, realIsInteger, realDiv, realSin, realCos, realATan2, realSinh, realCosh, realExp, realLog, smtFnApp, fromText

Methods

boolExpr :: Bool -> v Source #

notExpr :: v -> v Source #

andAll :: [v] -> v Source #

orAll :: [v] -> v Source #

(.&&) :: v -> v -> v infixr 3 Source #

(.||) :: v -> v -> v infixr 2 Source #

(.==) :: v -> v -> v infix 4 Source #

Compare two elements for equality.

(./=) :: v -> v -> v infix 4 Source #

Compare two elements for in-equality.

impliesExpr :: v -> v -> v Source #

letExpr :: [(Text, v)] -> v -> v Source #

Create a let expression. This is a "sequential" let, which is syntactic sugar for a nested series of single let bindings. As a consequence, bound variables are in scope for the right-hand-sides of subsequent bindings.

ite :: v -> v -> v -> v Source #

Create an if-then-else expression.

sumExpr :: [v] -> v Source #

Add a list of values together.

termIntegerToReal :: v -> v Source #

Convert an integer expression to a real.

termRealToInteger :: v -> v Source #

Convert a real expression to an integer.

integerTerm :: Integer -> v Source #

Convert an integer to a term.

rationalTerm :: Rational -> v Source #

Convert a rational to a term.

(.<=) :: v -> v -> v infix 4 Source #

Less-then-or-equal

(.<) :: v -> v -> v infix 4 Source #

Less-then

(.>) :: v -> v -> v infix 4 Source #

Greater then

(.>=) :: v -> v -> v infix 4 Source #

Greater then or equal

intAbs :: v -> v Source #

Integer theory terms

intDiv :: v -> v -> v Source #

intMod :: v -> v -> v Source #

intDivisible :: v -> Natural -> v Source #

bvTerm :: NatRepr w -> BV w -> v Source #

Create expression from bitvector.

bvNeg :: v -> v Source #

bvAdd :: v -> v -> v Source #

bvSub :: v -> v -> v Source #

bvMul :: v -> v -> v Source #

bvSLe :: v -> v -> v Source #

bvULe :: v -> v -> v Source #

bvSLt :: v -> v -> v Source #

bvULt :: v -> v -> v Source #

bvUDiv :: v -> v -> v Source #

bvURem :: v -> v -> v Source #

bvSDiv :: v -> v -> v Source #

bvSRem :: v -> v -> v Source #

bvAnd :: v -> v -> v Source #

bvOr :: v -> v -> v Source #

bvXor :: v -> v -> v Source #

bvNot :: v -> v Source #

bvShl :: v -> v -> v Source #

bvLshr :: v -> v -> v Source #

bvAshr :: v -> v -> v Source #

bvConcat :: v -> v -> v Source #

Concatenate two bitvectors together.

bvExtract :: NatRepr w -> Natural -> Natural -> v -> v Source #

bvExtract w i n v extracts bits [i..i+n) from v as a new bitvector. v must contain at least w elements, and i+n must be less than or equal to w. The result has n elements. The least significant bit of v should have index 0.

bvTestBit :: NatRepr w -> Natural -> v -> v Source #

bvTestBit w i x returns predicate that holds if bit i in x is set to true. w should be the number of bits in x.

bvSumExpr :: NatRepr w -> [v] -> v Source #

floatTerm :: FloatPrecisionRepr fpp -> BigFloat -> v Source #

floatNeg :: v -> v Source #

floatAbs :: v -> v Source #

floatSqrt :: RoundingMode -> v -> v Source #

floatAdd :: RoundingMode -> v -> v -> v Source #

floatSub :: RoundingMode -> v -> v -> v Source #

floatMul :: RoundingMode -> v -> v -> v Source #

floatDiv :: RoundingMode -> v -> v -> v Source #

floatRem :: v -> v -> v Source #

floatFMA :: RoundingMode -> v -> v -> v -> v Source #

floatEq :: v -> v -> v Source #

floatFpEq :: v -> v -> v Source #

floatLe :: v -> v -> v Source #

floatLt :: v -> v -> v Source #

floatIsNaN :: v -> v Source #

floatIsInf :: v -> v Source #

floatIsZero :: v -> v Source #

floatIsPos :: v -> v Source #

floatIsNeg :: v -> v Source #

floatIsSubnorm :: v -> v Source #

floatIsNorm :: v -> v Source #

floatCast :: FloatPrecisionRepr fpp -> RoundingMode -> v -> v Source #

floatRound :: RoundingMode -> v -> v Source #

floatFromBinary :: FloatPrecisionRepr fpp -> v -> v Source #

bvToFloat :: FloatPrecisionRepr fpp -> RoundingMode -> v -> v Source #

sbvToFloat :: FloatPrecisionRepr fpp -> RoundingMode -> v -> v Source #

realToFloat :: FloatPrecisionRepr fpp -> RoundingMode -> v -> v Source #

floatToBV :: Natural -> RoundingMode -> v -> v Source #

floatToSBV :: Natural -> RoundingMode -> v -> v Source #

floatToReal :: v -> v Source #

realIsInteger :: v -> v Source #

Predicate that holds if a real number is an integer.

realDiv :: v -> v -> v Source #

realSin :: v -> v Source #

realCos :: v -> v Source #

realATan2 :: v -> v -> v Source #

realSinh :: v -> v Source #

realCosh :: v -> v Source #

realExp :: v -> v Source #

realLog :: v -> v Source #

smtFnApp :: v -> [v] -> v Source #

Apply the arguments to the given function.

smtFnUpdate :: Maybe (v -> [v] -> v -> v) Source #

Update a function value to return a new value at the given point.

This may be Nothing if solver has no builtin function for update.

lambdaTerm :: Maybe ([(Text, Some TypeMap)] -> v -> v) Source #

Function for creating a lambda term if output supports it.

Yices support lambda expressions, but SMTLIB2 does not. The function takes arguments and the expression.

fromText :: Text -> v Source #

Instances

Instances details

SupportTermOps Term Source #

Instance details

Defined in What4.Protocol.SMTLib2

Methods

boolExpr :: Bool -> Term Source #

notExpr :: Term -> Term Source #

andAll :: [Term] -> Term Source #

orAll :: [Term] -> Term Source #

(.&&) :: Term -> Term -> Term Source #

(.||) :: Term -> Term -> Term Source #

(.==) :: Term -> Term -> Term Source #

(./=) :: Term -> Term -> Term Source #

impliesExpr :: Term -> Term -> Term Source #

letExpr :: [(Text, Term)] -> Term -> Term Source #

ite :: Term -> Term -> Term -> Term Source #

sumExpr :: [Term] -> Term Source #

termIntegerToReal :: Term -> Term Source #

termRealToInteger :: Term -> Term Source #

integerTerm :: Integer -> Term Source #

rationalTerm :: Rational -> Term Source #

(.<=) :: Term -> Term -> Term Source #

(.<) :: Term -> Term -> Term Source #

(.>) :: Term -> Term -> Term Source #

(.>=) :: Term -> Term -> Term Source #

intAbs :: Term -> Term Source #

intDiv :: Term -> Term -> Term Source #

intMod :: Term -> Term -> Term Source #

intDivisible :: Term -> Natural -> Term Source #

bvTerm :: forall (w :: Nat). NatRepr w -> BV w -> Term Source #

bvNeg :: Term -> Term Source #

bvAdd :: Term -> Term -> Term Source #

bvSub :: Term -> Term -> Term Source #

bvMul :: Term -> Term -> Term Source #

bvSLe :: Term -> Term -> Term Source #

bvULe :: Term -> Term -> Term Source #

bvSLt :: Term -> Term -> Term Source #

bvULt :: Term -> Term -> Term Source #

bvUDiv :: Term -> Term -> Term Source #

bvURem :: Term -> Term -> Term Source #

bvSDiv :: Term -> Term -> Term Source #

bvSRem :: Term -> Term -> Term Source #

bvAnd :: Term -> Term -> Term Source #

bvOr :: Term -> Term -> Term Source #

bvXor :: Term -> Term -> Term Source #

bvNot :: Term -> Term Source #

bvShl :: Term -> Term -> Term Source #

bvLshr :: Term -> Term -> Term Source #

bvAshr :: Term -> Term -> Term Source #

bvConcat :: Term -> Term -> Term Source #

bvExtract :: forall (w :: Nat). NatRepr w -> Natural -> Natural -> Term -> Term Source #

bvTestBit :: forall (w :: Nat). NatRepr w -> Natural -> Term -> Term Source #

bvSumExpr :: forall (w :: Nat). NatRepr w -> [Term] -> Term Source #

floatTerm :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> BigFloat -> Term Source #

floatNeg :: Term -> Term Source #

floatAbs :: Term -> Term Source #

floatSqrt :: RoundingMode -> Term -> Term Source #

floatAdd :: RoundingMode -> Term -> Term -> Term Source #

floatSub :: RoundingMode -> Term -> Term -> Term Source #

floatMul :: RoundingMode -> Term -> Term -> Term Source #

floatDiv :: RoundingMode -> Term -> Term -> Term Source #

floatRem :: Term -> Term -> Term Source #

floatFMA :: RoundingMode -> Term -> Term -> Term -> Term Source #

floatEq :: Term -> Term -> Term Source #

floatFpEq :: Term -> Term -> Term Source #

floatLe :: Term -> Term -> Term Source #

floatLt :: Term -> Term -> Term Source #

floatIsNaN :: Term -> Term Source #

floatIsInf :: Term -> Term Source #

floatIsZero :: Term -> Term Source #

floatIsPos :: Term -> Term Source #

floatIsNeg :: Term -> Term Source #

floatIsSubnorm :: Term -> Term Source #

floatIsNorm :: Term -> Term Source #

floatCast :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

floatRound :: RoundingMode -> Term -> Term Source #

floatFromBinary :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> Term -> Term Source #

bvToFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

sbvToFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

realToFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

floatToBV :: Natural -> RoundingMode -> Term -> Term Source #

floatToSBV :: Natural -> RoundingMode -> Term -> Term Source #

floatToReal :: Term -> Term Source #

realIsInteger :: Term -> Term Source #

realDiv :: Term -> Term -> Term Source #

realSin :: Term -> Term Source #

realCos :: Term -> Term Source #

realATan2 :: Term -> Term -> Term Source #

realSinh :: Term -> Term Source #

realCosh :: Term -> Term Source #

realExp :: Term -> Term Source #

realLog :: Term -> Term Source #

smtFnApp :: Term -> [Term] -> Term Source #

smtFnUpdate :: Maybe (Term -> [Term] -> Term -> Term) Source #

lambdaTerm :: Maybe ([(Text, Some TypeMap)] -> Term -> Term) Source #

fromText :: Text -> Term Source #

type ArrayConstantFn v Source #

Arguments

= [Some TypeMap]	Type for indices
-> Some TypeMap	Type for value.
-> v	Constant to assign all values.
-> v

class SupportTermOps (Term h) => SMTWriter h where Source #

Typeclass need to generate SMTLIB commands.

Methods

forallExpr :: [(Text, Some TypeMap)] -> Term h -> Term h Source #

Create a forall expression

existsExpr :: [(Text, Some TypeMap)] -> Term h -> Term h Source #

Create an exists expression

arrayConstant :: Maybe (ArrayConstantFn (Term h)) Source #

Create a constant array

This may return Nothing if the solver does not support constant arrays.

arraySelect :: Term h -> [Term h] -> Term h Source #

Select an element from an array

arrayUpdate :: Term h -> [Term h] -> Term h -> Term h Source #

'arrayUpdate a i v' returns an array that contains value v at index i, and the same value as in a at every other index.

commentCommand :: f h -> Builder -> Command h Source #

Create a command that just defines a comment.

assertCommand :: f h -> Term h -> Command h Source #

Create a command that asserts a formula.

assertNamedCommand :: f h -> Term h -> Text -> Command h Source #

Create a command that asserts a formula and attaches the given name to it (primarily for the purposes of later reporting unsatisfiable cores).

pushCommand :: f h -> Command h Source #

Push 1 new scope

popCommand :: f h -> Command h Source #

Pop 1 existing scope

popManyCommands :: f h -> Int -> [Command h] Source #

Pop several scopes.

resetCommand :: f h -> Command h Source #

Reset the solver state, forgetting all pushed frames and assertions

checkCommands :: f h -> [Command h] Source #

Check if the current set of assumption is satisfiable. May require multiple commands. The intial commands require an ack. The last one does not.

checkWithAssumptionsCommands :: f h -> [Text] -> [Command h] Source #

Check if a collection of assumptions is satisfiable in the current context. The assumptions must be given as the names of literals already in scope.

getUnsatAssumptionsCommand :: f h -> Command h Source #

Ask the solver to return an unsatisfiable core from among the assumptions passed into the previous "check with assumptions" command.

getUnsatCoreCommand :: f h -> Command h Source #

Ask the solver to return an unsatisfiable core from among the named assumptions previously asserted using the assertNamedCommand after an unsatisfiable checkCommand.

setOptCommand :: f h -> Text -> Text -> Command h Source #

Set an option/parameter.

declareCommand :: f h -> Text -> Assignment TypeMap args -> TypeMap rtp -> Command h Source #

Declare a new symbol with the given name, arguments types, and result type.

defineCommand Source #

Arguments

:: f h
-> Text	Name of variable
-> [(Text, Some TypeMap)]
-> TypeMap rtp
-> Term h
-> Command h

Define a new symbol with the given name, arguments, result type, and associated expression.

The argument contains the variable name and the type of the variable.

declareStructDatatype :: WriterConn t h -> Assignment TypeMap args -> IO () Source #

Declare a struct datatype if is has not been already given the number of arguments in the struct.

structCtor :: Assignment TypeMap args -> [Term h] -> Term h Source #

Build a struct term with the given types and fields

structProj :: Assignment TypeMap args -> Index args tp -> Term h -> Term h Source #

Project a field from a struct with the given types

stringTerm :: ByteString -> Term h Source #

Produce a term representing a string literal

stringLength :: Term h -> Term h Source #

Compute the length of a term

stringIndexOf :: Term h -> Term h -> Term h -> Term h Source #

stringIndexOf s t i computes the first index following or at i where t appears within s as a substring, or -1 if no such index exists

stringContains :: Term h -> Term h -> Term h Source #

Test if the first string contains the second string

stringIsPrefixOf :: Term h -> Term h -> Term h Source #

Test if the first string is a prefix of the second string

stringIsSuffixOf :: Term h -> Term h -> Term h Source #

Test if the first string is a suffix of the second string

stringSubstring :: Term h -> Term h -> Term h -> Term h Source #

stringSubstring s off len extracts the substring of s starting at index off and having length len. The result of this operation is undefined if off and len to not specify a valid substring of s; in particular, we must have off+len <= length(s).

stringAppend :: [Term h] -> Term h Source #

Append the given strings

resetDeclaredStructs :: WriterConn t h -> IO () Source #

Forget all previously-declared struct types.

writeCommand :: WriterConn t h -> Command h -> IO () Source #

Write a command to the connection.

Instances

Instances details

SMTWriter Connection Source #
Instance details Defined in What4.Solver.Yices Methods forallExpr :: [(Text, Some TypeMap)] -> Term Connection -> Term Connection Source # existsExpr :: [(Text, Some TypeMap)] -> Term Connection -> Term Connection Source # arrayConstant :: Maybe (ArrayConstantFn (Term Connection)) Source # arraySelect :: Term Connection -> [Term Connection] -> Term Connection Source # arrayUpdate :: Term Connection -> [Term Connection] -> Term Connection -> Term Connection Source # commentCommand :: f Connection -> Builder -> Command Connection Source # assertCommand :: f Connection -> Term Connection -> Command Connection Source # assertNamedCommand :: f Connection -> Term Connection -> Text -> Command Connection Source # pushCommand :: f Connection -> Command Connection Source # popCommand :: f Connection -> Command Connection Source # popManyCommands :: f Connection -> Int -> [Command Connection] Source # resetCommand :: f Connection -> Command Connection Source # checkCommands :: f Connection -> [Command Connection] Source # checkWithAssumptionsCommands :: f Connection -> [Text] -> [Command Connection] Source # getUnsatAssumptionsCommand :: f Connection -> Command Connection Source # getUnsatCoreCommand :: f Connection -> Command Connection Source # setOptCommand :: f Connection -> Text -> Text -> Command Connection Source # declareCommand :: forall f (args :: Ctx BaseType) (rtp :: BaseType). f Connection -> Text -> Assignment TypeMap args -> TypeMap rtp -> Command Connection Source # defineCommand :: forall f (rtp :: BaseType). f Connection -> Text -> [(Text, Some TypeMap)] -> TypeMap rtp -> Term Connection -> Command Connection Source # declareStructDatatype :: forall t (args :: Ctx BaseType). WriterConn t Connection -> Assignment TypeMap args -> IO () Source # structCtor :: forall (args :: Ctx BaseType). Assignment TypeMap args -> [Term Connection] -> Term Connection Source # structProj :: forall (args :: Ctx BaseType) (tp :: BaseType). Assignment TypeMap args -> Index args tp -> Term Connection -> Term Connection Source # stringTerm :: ByteString -> Term Connection Source # stringLength :: Term Connection -> Term Connection Source # stringIndexOf :: Term Connection -> Term Connection -> Term Connection -> Term Connection Source # stringContains :: Term Connection -> Term Connection -> Term Connection Source # stringIsPrefixOf :: Term Connection -> Term Connection -> Term Connection Source # stringIsSuffixOf :: Term Connection -> Term Connection -> Term Connection Source # stringSubstring :: Term Connection -> Term Connection -> Term Connection -> Term Connection Source # stringAppend :: [Term Connection] -> Term Connection Source # resetDeclaredStructs :: WriterConn t Connection -> IO () Source # writeCommand :: WriterConn t Connection -> Command Connection -> IO () Source #
SMTLib2Tweaks a => SMTWriter (Writer a) Source #
Instance details Defined in What4.Protocol.SMTLib2 Methods forallExpr :: [(Text, Some TypeMap)] -> Term (Writer a) -> Term (Writer a) Source # existsExpr :: [(Text, Some TypeMap)] -> Term (Writer a) -> Term (Writer a) Source # arrayConstant :: Maybe (ArrayConstantFn (Term (Writer a))) Source # arraySelect :: Term (Writer a) -> [Term (Writer a)] -> Term (Writer a) Source # arrayUpdate :: Term (Writer a) -> [Term (Writer a)] -> Term (Writer a) -> Term (Writer a) Source # commentCommand :: f (Writer a) -> Builder -> Command (Writer a) Source # assertCommand :: f (Writer a) -> Term (Writer a) -> Command (Writer a) Source # assertNamedCommand :: f (Writer a) -> Term (Writer a) -> Text -> Command (Writer a) Source # pushCommand :: f (Writer a) -> Command (Writer a) Source # popCommand :: f (Writer a) -> Command (Writer a) Source # popManyCommands :: f (Writer a) -> Int -> [Command (Writer a)] Source # resetCommand :: f (Writer a) -> Command (Writer a) Source # checkCommands :: f (Writer a) -> [Command (Writer a)] Source # checkWithAssumptionsCommands :: f (Writer a) -> [Text] -> [Command (Writer a)] Source # getUnsatAssumptionsCommand :: f (Writer a) -> Command (Writer a) Source # getUnsatCoreCommand :: f (Writer a) -> Command (Writer a) Source # setOptCommand :: f (Writer a) -> Text -> Text -> Command (Writer a) Source # declareCommand :: forall f (args :: Ctx BaseType) (rtp :: BaseType). f (Writer a) -> Text -> Assignment TypeMap args -> TypeMap rtp -> Command (Writer a) Source # defineCommand :: forall f (rtp :: BaseType). f (Writer a) -> Text -> [(Text, Some TypeMap)] -> TypeMap rtp -> Term (Writer a) -> Command (Writer a) Source # declareStructDatatype :: forall t (args :: Ctx BaseType). WriterConn t (Writer a) -> Assignment TypeMap args -> IO () Source # structCtor :: forall (args :: Ctx BaseType). Assignment TypeMap args -> [Term (Writer a)] -> Term (Writer a) Source # structProj :: forall (args :: Ctx BaseType) (tp :: BaseType). Assignment TypeMap args -> Index args tp -> Term (Writer a) -> Term (Writer a) Source # stringTerm :: ByteString -> Term (Writer a) Source # stringLength :: Term (Writer a) -> Term (Writer a) Source # stringIndexOf :: Term (Writer a) -> Term (Writer a) -> Term (Writer a) -> Term (Writer a) Source # stringContains :: Term (Writer a) -> Term (Writer a) -> Term (Writer a) Source # stringIsPrefixOf :: Term (Writer a) -> Term (Writer a) -> Term (Writer a) Source # stringIsSuffixOf :: Term (Writer a) -> Term (Writer a) -> Term (Writer a) Source # stringSubstring :: Term (Writer a) -> Term (Writer a) -> Term (Writer a) -> Term (Writer a) Source # stringAppend :: [Term (Writer a)] -> Term (Writer a) Source # resetDeclaredStructs :: WriterConn t (Writer a) -> IO () Source # writeCommand :: WriterConn t (Writer a) -> Command (Writer a) -> IO () Source #

class SMTWriter h => SMTReadWriter h where Source #

Used when we need two way communication with the solver.

Methods

smtEvalFuns :: WriterConn t h -> InputStream Text -> SMTEvalFunctions h Source #

Get functions for parsing values out of the solver.

smtSatResult :: f h -> InputStream Text -> IO (SatResult () ()) Source #

Parse a set result from the solver's response.

smtUnsatCoreResult :: f h -> InputStream Text -> IO [Text] Source #

Parse a list of names of assumptions that form an unsatisfiable core. These correspond to previously-named assertions.

smtUnsatAssumptionsResult :: f h -> InputStream Text -> IO [(Bool, Text)] Source #

Parse a list of names of assumptions that form an unsatisfiable core. The boolean indicates the polarity of the atom: true for an ordinary atom, false for a negated atom.

Instances

Instances details

SMTReadWriter Connection Source #
Instance details Defined in What4.Solver.Yices Methods smtEvalFuns :: WriterConn t Connection -> InputStream Text -> SMTEvalFunctions Connection Source # smtSatResult :: f Connection -> InputStream Text -> IO (SatResult () ()) Source # smtUnsatCoreResult :: f Connection -> InputStream Text -> IO [Text] Source # smtUnsatAssumptionsResult :: f Connection -> InputStream Text -> IO [(Bool, Text)] Source #
SMTLib2Tweaks a => SMTReadWriter (Writer a) Source #
Instance details Defined in What4.Protocol.SMTLib2 Methods smtEvalFuns :: WriterConn t (Writer a) -> InputStream Text -> SMTEvalFunctions (Writer a) Source # smtSatResult :: f (Writer a) -> InputStream Text -> IO (SatResult () ()) Source # smtUnsatCoreResult :: f (Writer a) -> InputStream Text -> IO [Text] Source # smtUnsatAssumptionsResult :: f (Writer a) -> InputStream Text -> IO [(Bool, Text)] Source #

type SMTEvalBVArrayFn h w v = (1 <= w, 1 <= v) => NatRepr w -> NatRepr v -> Term h -> IO (Maybe (GroundArray (SingleCtx (BaseBVType w)) (BaseBVType v))) Source #

newtype SMTEvalBVArrayWrapper h Source #

Constructors

SMTEvalBVArrayWrapper
Fields unEvalBVArrayWrapper :: forall w v. SMTEvalBVArrayFn h w v

Terms

type family Term (h :: Type) :: Type Source #

A term in the output language.

Instances

Instances details

type Term Connection Source #
Instance details Defined in What4.Solver.Yices type Term Connection
type Term (Writer a) Source #
Instance details Defined in What4.Protocol.SMTLib2 type Term (Writer a) = Term

app :: Builder -> [Builder] -> Builder Source #

app_list :: Builder -> [Builder] -> Builder Source #

builder_list :: [Builder] -> Builder Source #

SMTWriter

data WriterConn t (h :: Type) Source #

connState :: WriterConn t h -> h Source #

The specific connection information.

newWriterConn Source #

Arguments

:: OutputStream Text	Stream to write queries onto
-> InputStream Text	Input stream to read responses from (may be the `nullInput` stream if no responses are expected)
-> AcknowledgementAction t cs	An action to consume solver acknowledgement responses
-> String	Name of solver for reporting purposes.
-> ProblemFeatures	Indicates what features are supported by the solver.
-> SymbolVarBimap t	A bijective mapping between variables and their canonical name (if any).
-> cs	State information specific to the type of connection
-> IO (WriterConn t cs)

resetEntryStack :: WriterConn t h -> IO () Source #

Clear the entry stack, and start with a fresh one.

popEntryStackToTop :: WriterConn t h -> IO Int Source #

Pop all but the topmost stack entry. Return the number of entries on the stack prior to popping.

entryStackHeight :: WriterConn t h -> IO Int Source #

Return the number of pushed stack frames. Note, this is one fewer than the number of entries in the stack beacuse the base entry is the top-level context that is not in the scope of any push.

pushEntryStack :: WriterConn t h -> IO () Source #

Push a new frame to the stack for maintaining the writer cache.

popEntryStack :: WriterConn t h -> IO () Source #

type family Command (h :: Type) :: Type Source #

Instances

Instances details

type Command Connection Source #
Instance details Defined in What4.Solver.Yices type Command Connection
type Command (Writer a) Source #
Instance details Defined in What4.Protocol.SMTLib2 type Command (Writer a) = Command

addCommand :: SMTWriter h => WriterConn t h -> Command h -> IO () Source #

Write a command to the connection along with position information if it differs from the last position.

addCommandNoAck :: SMTWriter h => WriterConn t h -> Command h -> IO () Source #

addCommands :: SMTWriter h => WriterConn t h -> [Command h] -> IO () Source #

Write a sequence of commands. All but the last should have acknowledgement.

mkFreeVar :: SMTWriter h => WriterConn t h -> Assignment TypeMap args -> TypeMap rtp -> IO Text Source #

Create a new variable with the given name.

bindVarAsFree :: SMTWriter h => WriterConn t h -> ExprBoundVar t tp -> IO () Source #

Consider the bound variable as free within the current assumption frame.

data TypeMap (tp :: BaseType) where Source #

TypeMap defines how a given BaseType maps to an SMTLIB type.

It is necessary as there may be several ways in which a base type can be encoded.

Constructors

BoolTypeMap :: TypeMap BaseBoolType
IntegerTypeMap :: TypeMap BaseIntegerType
RealTypeMap :: TypeMap BaseRealType
BVTypeMap :: 1 <= w => !(NatRepr w) -> TypeMap (BaseBVType w)
FloatTypeMap :: !(FloatPrecisionRepr fpp) -> TypeMap (BaseFloatType fpp)
Char8TypeMap :: TypeMap (BaseStringType Char8)
ComplexToStructTypeMap :: TypeMap BaseComplexType
ComplexToArrayTypeMap :: TypeMap BaseComplexType
PrimArrayTypeMap :: !(Assignment TypeMap (idxl ::> idx)) -> !(TypeMap tp) -> TypeMap (BaseArrayType (idxl ::> idx) tp)
FnArrayTypeMap :: !(Assignment TypeMap (idxl ::> idx)) -> TypeMap tp -> TypeMap (BaseArrayType (idxl ::> idx) tp)
StructTypeMap :: !(Assignment TypeMap idx) -> TypeMap (BaseStructType idx)

Instances

Instances details

TestEquality TypeMap Source #
Instance details Defined in What4.Protocol.SMTWriter Methods testEquality :: forall (a :: k) (b :: k). TypeMap a -> TypeMap b -> Maybe (a :~: b) #
ShowF TypeMap Source #
Instance details Defined in What4.Protocol.SMTWriter Methods withShow :: forall p q (tp :: k) a. p TypeMap -> q tp -> (Show (TypeMap tp) => a) -> a # showF :: forall (tp :: k). TypeMap tp -> String # showsPrecF :: forall (tp :: k). Int -> TypeMap tp -> String -> String #
Eq (TypeMap tp) Source #
Instance details Defined in What4.Protocol.SMTWriter Methods (==) :: TypeMap tp -> TypeMap tp -> Bool # (/=) :: TypeMap tp -> TypeMap tp -> Bool #
Show (TypeMap a) Source #
Instance details Defined in What4.Protocol.SMTWriter Methods showsPrec :: Int -> TypeMap a -> ShowS # show :: TypeMap a -> String # showList :: [TypeMap a] -> ShowS #

typeMap :: WriterConn t h -> BaseTypeRepr tp -> Either BaseTypeError (TypeMap tp) Source #

Given a solver connection and a base type repr, typeMap attempts to find the best encoding for a variable of that type supported by teh solver.

freshBoundVarName Source #

Arguments

:: SMTWriter h
=> WriterConn t h
-> DefineStyle
-> [(Text, Some TypeMap)]	Names of variables in term and associated type.
-> TypeMap rtp	Type of expression.
-> Term h
-> IO Text

Create a variable name eqivalent to the given expression.

assumeFormula :: SMTWriter h => WriterConn t h -> Term h -> IO () Source #

Assume that the given formula holds.

assumeFormulaWithName :: SMTWriter h => WriterConn t h -> Term h -> Text -> IO () Source #

assumeFormulaWithFreshName :: SMTWriter h => WriterConn t h -> Term h -> IO Text Source #

data DefineStyle Source #

Constructors

FunctionDefinition
EqualityDefinition

Instances

Instances details

Eq DefineStyle Source #
Instance details Defined in What4.Protocol.SMTWriter Methods (==) :: DefineStyle -> DefineStyle -> Bool # (/=) :: DefineStyle -> DefineStyle -> Bool #
Show DefineStyle Source #
Instance details Defined in What4.Protocol.SMTWriter Methods showsPrec :: Int -> DefineStyle -> ShowS # show :: DefineStyle -> String # showList :: [DefineStyle] -> ShowS #

newtype AcknowledgementAction t h Source #

An action for consuming an acknowledgement message from the solver, if it is configured to produce ack messages.

Constructors

AckAction
Fields runAckAction :: WriterConn t h -> Command h -> IO ()

nullAcknowledgementAction :: AcknowledgementAction t h Source #

An acknowledgement action that does nothing

SMTWriter operations

assume :: SMTWriter h => WriterConn t h -> BoolExpr t -> IO () Source #

Write assume formula predicates for asserting predicate holds.

mkSMTTerm :: SMTWriter h => WriterConn t h -> Expr t tp -> IO (Term h) Source #

Write a expression to SMT

mkFormula :: SMTWriter h => WriterConn t h -> BoolExpr t -> IO (Term h) Source #

Write a logical expression.

mkAtomicFormula :: SMTWriter h => WriterConn t h -> BoolExpr t -> IO Text Source #

data SMTEvalFunctions h Source #

Constructors

SMTEvalFunctions

Fields

smtEvalBool :: Term h -> IO Bool
Given a SMT term for a Boolean value, this should whether the term is assigned true or false.
smtEvalBV :: forall w. NatRepr w -> Term h -> IO (BV w)
Given a bitwidth, and a SMT term for a bitvector with that bitwidth, this should return an unsigned integer with the value of that bitvector.
smtEvalReal :: Term h -> IO Rational
Given a SMT term for real value, this should return a rational value for that term.
smtEvalFloat :: forall fpp. FloatPrecisionRepr fpp -> Term h -> IO (BV (FloatPrecisionBits fpp))
Given floating point format, and an SMT term for a floating-point value in that format, this returns an unsigned integer with the bits of the IEEE-754 representation.
smtEvalBvArray :: Maybe (SMTEvalBVArrayWrapper h)
If Just, a function to read arrays whose domain and codomain are both bitvectors. If Nothing, signifies that we should fall back to index-selection representation of arrays.
smtEvalString :: Term h -> IO ByteString
Given a SMT term representing as sequence of bytes, return the value as a bytestring.

smtExprGroundEvalFn Source #

Arguments

:: forall t h. SMTWriter h
=> WriterConn t h	Connection to SMT solver.
-> SMTEvalFunctions h
-> IO (GroundEvalFn t)

The function creates a function for evaluating elts to concrete values given a connection to an SMT solver along with some functions for evaluating different types of terms to concrete values.

data CollectorResults h a Source #

This describes the result that was collected from the solver.

Constructors

CollectorResults
Fields crResult :: !a Result from sandboxed computation. crBindings :: ![(Text, Term h)] List of bound variables. crFreeConstants :: ![(Text, Some TypeMap)] Constants added during generation. crSideConds :: ![Term h] List of Boolean predicates asserted by collector.

mkBaseExpr :: SMTWriter h => Expr t tp -> SMTCollector t h (Term h) Source #

Convert an element to a base expression.

runInSandbox :: SupportTermOps (Term h) => WriterConn t h -> SMTCollector t h a -> IO (CollectorResults h a) Source #

This runs the side collector and collects the results.

Reexports

data RoundingMode Source #

Rounding modes for IEEE-754 floating point operations.

Constructors

RNE	Round to nearest even.
RNA	Round to nearest away.
RTP	Round toward plus Infinity.
RTN	Round toward minus Infinity.
RTZ	Round toward zero.

Instances

Instances details

Enum RoundingMode Source #
Instance details Defined in What4.Utils.FloatHelpers Methods succ :: RoundingMode -> RoundingMode # pred :: RoundingMode -> RoundingMode # toEnum :: Int -> RoundingMode # fromEnum :: RoundingMode -> Int # enumFrom :: RoundingMode -> [RoundingMode] # enumFromThen :: RoundingMode -> RoundingMode -> [RoundingMode] # enumFromTo :: RoundingMode -> RoundingMode -> [RoundingMode] # enumFromThenTo :: RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode] #
Eq RoundingMode Source #
Instance details Defined in What4.Utils.FloatHelpers Methods (==) :: RoundingMode -> RoundingMode -> Bool # (/=) :: RoundingMode -> RoundingMode -> Bool #
Ord RoundingMode Source #
Instance details Defined in What4.Utils.FloatHelpers Methods compare :: RoundingMode -> RoundingMode -> Ordering # (<) :: RoundingMode -> RoundingMode -> Bool # (<=) :: RoundingMode -> RoundingMode -> Bool # (>) :: RoundingMode -> RoundingMode -> Bool # (>=) :: RoundingMode -> RoundingMode -> Bool # max :: RoundingMode -> RoundingMode -> RoundingMode # min :: RoundingMode -> RoundingMode -> RoundingMode #
Show RoundingMode Source #
Instance details Defined in What4.Utils.FloatHelpers Methods showsPrec :: Int -> RoundingMode -> ShowS # show :: RoundingMode -> String # showList :: [RoundingMode] -> ShowS #
Generic RoundingMode Source #
Instance details Defined in What4.Utils.FloatHelpers Associated Types type Rep RoundingMode :: Type -> Type # Methods from :: RoundingMode -> Rep RoundingMode x # to :: Rep RoundingMode x -> RoundingMode #
Hashable RoundingMode Source #
Instance details Defined in What4.Utils.FloatHelpers Methods hashWithSalt :: Int -> RoundingMode -> Int # hash :: RoundingMode -> Int #
type Rep RoundingMode Source #
Instance details Defined in What4.Utils.FloatHelpers type Rep RoundingMode = D1 ('MetaData "RoundingMode" "What4.Utils.FloatHelpers" "what4-1.1-F6JmVDCUG2e4tsAmUzrLc2" 'False) ((C1 ('MetaCons "RNE" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RNA" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RTP" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "RTN" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RTZ" 'PrefixI 'False) (U1 :: Type -> Type))))