>@      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~           Safe-Inferred!"+-./2346HMThe 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 . Constructs a unit type Safe-Inferred!"+-./2346HM+  !"#$%&'()*+,-./012+  !"#$%&'()*+,-./012+.210/+-,'*)("&%$#!      ! "&%$#'*)(+-,.210/ Safe-Inferred!"+-./2346HM;3456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklm83456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghij;ajihgfedcb<`_^]\[ZYXWVUTSRQPONMLKJIHGFEDCBA@?>=8;:957634mlk345768;:9<$`_^]\[ZYXWVUTSRQPONMLKJIHGFEDCBA@?>=a jihgfedcbklmNone!"+-./2346=BHKMAn extension of the P class: Instances of this class can be represented as native haskell data types.5Converts a haskell value into its SMT representation.8Converts a SMT representation back into a haskell value.[Instances of this class may be used as arguments for constructed functions and quantifiers.2Options controling the behaviour of the SMT solver+Enable the generation of craig interpolantsBEnable the querying of unsatisfiable cores after a failed checkSat>Produce a proof of unsatisfiability after each failed checkSat>Produce a satisfying assignment after each successful checkSat6Whether or not to print "success" after each operation ,Identifies a clause in an unsatisfiable core #Represents a field of the datatype a of the type f'Represents a constructor of a datatype aB Can be obtained by using the template haskell extension moduleIAn abstract SMT expression\6The SMT monad used for communating with the SMT solverg$An array which maps indices of type i to elements of type v.i Lifts the  class into SMTnEA type class for all types which support arithmetic operations in SMTo8Haskell values which can be represented as SMT constants|-Haskell types which can be represented in SMTThe result of a check-sat query;The solver cannot determine the satisfiability of a formulaThe formula is unsatisfiableThe formula is satisfiable<Describe limits on the ressources that an SMT-solver can useSA limit on the amount of time the solver can spend on the problem (in milliseconds)AA limit on the amount of memory the solver can use (in megabytes)DGet all the type collections which are not yet declared from a type.nopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~inopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~|}~y{zxuwvrtsopqnijklmghabcdef_`\]^[YZWXIVUTSRQPONMLKJ@HGFCBADE?7>=<98:;6543210/.-,+*)('&%$#"!      ~}|{zyxwvutsrpqnonopqrstuvwxyz{|}~     6543210/.-,+*)('&%$#"! 7>=<98:;?@HGFCBADEI VUTSRQPONMLKJWXYZ[\]^_`abcdefghijklmnopqrtsuwvxy{z|}~jklmNone!"+-./2346=BHJKM;Reconstruct the type annotation for a given SMT expression.6Get an undefined value of the type argument of a type.ORecursively fold a monadic function over all sub-expressions of this expressionLRecursively fold a monadic function over all sub-expressions of the argumentsRecursively fold a function over all sub-expressions of this expression. It is implemented as a special case of .pRecursively fold a function over all sub-expressions of the argument. It is implemented as a special case of .r      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abc)     rcba`_^]\[ZYXWVUTSRQPONMLKJIHGFEDCBA@?>=<;:9876543210/.-,+*) ('&%$#    "! r      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcNone!"+-./2346HMdedede deNone !"+-./2346=HKMrflCheck if the model is satisfiable (e.g. if there is a value for each variable so that every assertion holds)gLCheck if the model is satisfiable using a given tactic. (Works only with Z3)hLike f], but gives you more options like choosing a tactic (Z3 only) or providing memory/time-limitsjFApply the given tactic to the current assertions. (Works only with Z3)kPush a new context on the stackl Pop a new context from the stackmxPerform a stacked operation, meaning that every assertion and declaration made in it will be undone after the operation.nInsert a comment into the SMTLib2 command stream. If you aren't looking at the command stream for debugging, this will do nothing.oCreate a new named variablep&Create a named and annotated variable.qCreate a annotated variablerCreate a fresh new variables+Create a fresh untyped variable with a nametCreate a fresh untyped variableuLike v , but defaults the name to "var"v,Create annotated named SMT variables of the L class. If more than one variable is needed, they get a numerical suffix.xLike u1, but can only be used for unit type annotations.yA constant expression.z!An annotated constant expression.}(Extract all assigned values of the model~>Extract all values of an array by giving the range of indices.!Define a new function with a bodyDefine a new constant.!Define a new constant with a nameWDefine a new function with a body and custom type annotations for arguments and result.Like *, but defaults the function name to "fun".Boolean conjunctionBoolean disjunction`Create a boolean expression that encodes that the array is equal to the supplied constant array.)Asserts that a boolean expression is true Create a new interpolation groupEAssert a boolean expression and track it for an unsat core call laterNAssert a boolean expression to be true and assign it to an interpolation group+Set an option for the underlying SMT solver/Get information about the underlying SMT solver\Create a new uniterpreted function with annotations for the argument and the return type.bCreate a new uninterpreted named function with annotation for the argument and the return type.3funAnn with an annotation only for the return type.$Create a new uninterpreted function.Apply a function to an argumentLift a function to arraysTwo expressions shall be equalA generalized version of %Declares all arguments to be distinct+Calculate the sum of arithmetic expressions/Calculate the product of arithmetic expressionsSubtracts two expressions*Divide an arithmetic expression by another6Perform a modulo operation on an arithmetic expressionBCalculate the remainder of the division of two integer expressions+Divide a rational expression by another oneFor an expression x, this returns the expression -x.2Convert an integer expression to a real expression4Convert a real expression into an integer expressionIf-then-else construct:Exclusive or: Return true if exactly one argument is true. ImplicationNegates a boolean expression,Extracts an element of an array by its indexThe expression  store arr i v stores the value v in the array arr at position i% and returns the resulting new array.Interpret a function f from i to v as an array with indices i and elements v. Such that: #f `app` j .==. select (asArray f) j for all indices j./Create an array where each element is the same. Bitvector and Bitvector or Bitvector or Bitvector notBitvector signed negationBitvector additionBitvector subtractionBitvector multiplicationBitvector unsigned remainderBitvector signed remainderBitvector unsigned divisionBitvector signed division Bitvector unsigned less-or-equalBitvector unsigned less-than#Bitvector unsigned greater-or-equalBitvector unsigned greater-thanBitvector signed less-or-equalBitvector signed less-than!Bitvector signed greater-or-equalBitvector signed greater-thanBitvector shift leftBitvector logical right shift"Bitvector arithmetical right shift Concats two bitvectors into one..Extract a sub-vector out of a given bitvector.:Safely split a 16-bit bitvector into two 8-bit bitvectors.;Safely split a 32-bit bitvector into two 16-bit bitvectors.;Safely split a 32-bit bitvector into four 8-bit bitvectors.;Safely split a 64-bit bitvector into two 32-bit bitvectors.<Safely split a 64-bit bitvector into four 16-bit bitvectors.<Safely split a 64-bit bitvector into eight 8-bit bitvectors.fIf the supplied function returns true for all possible values, the forall quantification returns true.An annotated version of .nIf the supplied function returns true for at least one possible value, the exists quantification returns true.An annotated version of .Binds an expression to a variable. Can be used to prevent blowups in the command stream if expressions are used multiple times. let' x f is functionally equivalent to f x.Like R, but can be given an additional type annotation for the argument of the function.Like 5, but can define multiple variables of the same type.Like B, but can quantify over more than one variable (of the same type).Like B, but can quantify over more than one variable (of the same type).:Checks if the expression is formed a specific constructor.Access a field of an expression!Takes the first element of a list#Drops the first element from a listChecks if a list is empty.Checks if a list is non-empty.LSets the logic used for the following program (Not needed for many solvers).fGiven an arbitrary expression, this creates a named version of it and a name to reference it later on.Like #, but defaults the name to "named".After an unsuccessful fU this method extracts a proof from the SMT solver that the instance is unsatisfiable.SUse the SMT solver to simplify a given expression. Currently only works with Z3.After an unsuccessful fD, return a list of clauses which make the instance unsatisfiable.fghijklmnopqrstuvwxyz{|}~If this expression is trueThen return this expression Else this oneIf this expression is trueThis one must be as well0This element will be at every index of the arrayAnnotations of the index type!The start of the extracted regionThe bitvector to extract fromNumber of variables to quantify7Function which takes a list of the quantified variablesNumber of variables to quantify7Function which takes a list of the quantified variablesfghijklmnopqrstuvwxyz{|}~fghijklmnopqrstuvwxyz{|}~fghijklmnopqrstuvwxyz{|}~None !"+-./2346HMXAn SMT backend which uses process pipes to communicate with an SMT solver process. HSpawn a new SMT solver process and create a pipe to communicate with it.)Parse a lisp expression into an SMT sort.`A map which contains signatures for a few common theorems which can be used in the proofs which getProof returns.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.&A parser for all available SMT logics.W !"#$$Path to the binary of the SMT solver5Command line arguments to be passed to the SMT solver%&'()*+,-./01234&The parser to use for function symbolsHow to handle variable names%Information about declared data types3A function to apply to the resulting SMT expression=If you know the sort of the expression, you can pass it here. The current quantification levelThe lisp expression to parse56789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYH !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXY None!"+-./2346HMRepresents a connection to an SMT solver. The SMT solver runs in a seperate thread and communication is handled via handles.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.DCloses an open SMT connection. Do not use the connection afterwards. ZPerform an action in the SMT solver associated with this connection and return the result.Z[The backend for the SMT solver. 'The connection to the SMT solver to useThe action to perform     Z[  None!"+-./2346HMrstuvwxyz{|}~   IWY[\_`gijklmno|}efghjklmnopqrstuvxyz{|}~\[_`|}onijklmIg klmfhgj{|}n  ropqxuvtsyze~utsr~}|{zyxwvYW None!"+-./2346HM Z3 is a solver by Microsoft  :http://research.microsoft.com/en-us/um/redmond/projects/z3. MathSAT  http://mathsat.fbk.eu. "CVC4 is an open-source SMT solver http://cs.nyu.edu/acsys/cvc48SMTInterpol is an experimental interpolating SMT solver 6http://ultimate.informatik.uni-freiburg.de/smtinterpol            \   !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyzz{{|}~MO      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMMNNOPOQRRSSTUVWXX(YZ[\']^_`abcdefghfijklmnopqrstuvwxyzz{|}}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                !"#$%&'()*+,-./0123456789:;<=>?@ABCD  EF smtlib2-0.2 Data.Unit$Language.SMTLib2.Internals.OperatorsLanguage.SMTLib2.StrategyLanguage.SMTLib2.Internals$Language.SMTLib2.Internals.Instances#Language.SMTLib2.Internals.Optimize$Language.SMTLib2.Internals.InterfaceLanguage.SMTLib2.PipeLanguage.SMTLib2.ConnectionLanguage.SMTLib2.SolverLanguage.SMTLib2Unitunit $fUnit(,,,,,) $fUnit(,,,,) $fUnit(,,,) $fUnit(,,) $fUnit(,)$fUnit() SMTBVUnOpBVNegBVNot SMTBVBinOpBVOrBVAndBVXorBVASHRBVLSHRBVSHLBVSDivBVUDivBVSRemBVURemBVMulBVSubBVAdd SMTBVCompOpBVSGTBVSGEBVSLTBVSLEBVUGTBVUGEBVULTBVULE SMTLogicOpImpliesXOrOrAnd SMTIntArithOpRemModDiv SMTArithOpMultPlusSMTOrdOpLtLeGtGe QFLRATacticPArithBranchCutRatio BuiltInTactic CustomTactic QFLRATacticAnyPar ParDoubleParIntParBoolProbeIsQFBVEQIsQFBVIsPropositional HasPatternsProduceUnsatCores ProduceModel ProduceProofs NumBVConstsNumArithConsts NumBoolConsts NumConstsNumExprsSizeDepthMemory IsUnboundedIsNRAIsNIAIsQFNRAIsQFNIAIsILPIsQFLIRAIsQFLRAIsQFLIA ArithAvgBW ArithMaxBW ArithAvgDeg ArithMaxDegIsPB ProbeCompareProbeEqProbeNotProbeOrProbeAnd ProbeIntConstProbeBoolConstTactic UsingParamsFailIfIfTryForParThenParOrOrElseAndThenSkip $fShowProbe$fShowBuiltInTactic $fShowTactic QuantifiedBoundBV64BV32BV16BV8N64N63N62N61N60N59N58N57N56N55N54N53N52N51N50N49N48N47N46N45N44N43N42N41N40N39N38N37N36N35N34N33N32N31N30N29N28N27N26N25N24N23N22N21N20N19N18N17N16N15N14N13N12N11N10N9N8N7N6N5N4N3N2N1N0 BitVectorBVTyped BVUntypedAdd TypeableNat reflectNatSZSMTStatenextVarnextInterpolationGroup nextClauseIdallVars namedVars nameCountdeclaredDataTypes DataField fieldName fieldSortfieldGetConstrconName conFields constructconUndefinedArgsconTestDataType dataTypeNamedataTypeConstructorsdataTypeGetUndefinedAnyValue ProxyArgValueProxyArgTypeCollectionargCount dataTypes DataTypeInfo structures datatypes constructorsfieldsLiftArgsUnpackedliftArgs unliftArgsLiftableLiftedgetLiftedArgumentAnninferLiftedAnnotation getConstraintArgs ArgAnnotation foldExprs foldsExprsextractArgAnnotationtoArgsfromArgsgetTypesgetArgAnnotationSMTInfoSMTSolverVersion SMTSolverName SMTOptionProduceInterpolants ProduceModels PrintSuccessClauseIdInterpolationGroupField Constructor Extractable extractAnn getExtractLen Concatable ConcatResultconcatAnnotation IsBitVector getBVSize SMTFunction SMTDivisible SMTFieldSel SMTConTestSMTConstructor SMTExtract SMTConcat SMTConstArraySMTStore SMTSelectSMTBVUnSMTBVBin SMTBVCompSMTITESMTToInt SMTToReal SMTDistinctSMTLogicSMTNotSMTAbsSMTNeg SMTDivide SMTIntArithSMTMinusSMTArithSMTOrd SMTBuiltInSMTFunSMTMapSMTEqValue ConstrValueBVValue bvValueWidth bvValueValue RealValueIntValue BoolValueSortSort' NamedSort ArraySortBVSort bvSortWidth bvSortUntypedRealSortIntSortBoolSortSMTExprUntypedExprValue UntypedExpr InternalObjNamedAppLetExistsForallAsArrayConstFunArgQVarVar UntypedValueUntypedSMTSMT'runSMT AnyBackendFunInfo funInfoProxy funInfoArgAnn funInfoResAnn funInfoNameSMTArray.<..>=..>..<=.SMTValueunmanglemangleManglingComplexManglingPrimitiveMangling UnmanglingComplexUnmanglingPrimitiveUnmangling ArgumentSort ArgumentSort' NormalSortSMTType SMTAnnotationgetSort asDataType asValueType getProxyArgsadditionalConstraintsannotationFromSort defaultExpr SMTBackend smtHandle smtGetNames smtNextNameCheckSatResultUnknownUnsatSatCheckSatLimits limitTime limitMemorySMTModelmodelFunctions SMTRequestSMTNewClauseIdSMTNewInterpolationGroup SMTNameExprSMTApplySMTExit SMTCommentSMTGetInterpolant SMTSimplifySMTGetUnsatCore SMTGetProof SMTGetModel SMTGetValue SMTDeclareFun SMTDefineFunSMTPopSMTPushSMTDeclareSortSMTDeclareDataTypesSMTDeclaredDataTypes SMTCheckSat SMTAssert SMTSetOption SMTGetInfo SMTSetLogic smtBackendgetSorts foldExprsId foldsExprsIdargSorts unpackArgs firstJustgetUndef getFunUndef getArrayUndefwithSMTBackendExitCleanlywithSMTBackendwithSMTBackend' funInfoSortfunInfoArgSorts argsSignatureargumentSortToSortsortToArgumentSort declareType withProxyArgwithProxyArgValue withAnyValue castAnyValueemptyDataTypeInfocontainsTypeCollectionaddDataTypeStructuregetNewTypeCollections asNamedSort escapeName escapeName' unescapeName unescapeName' emptySMTStatesmtStateAddFunreifyNatreifySum reifyExtractshowExprnoLimitsquantificationLevel inferSorts valueSort$fShowConstructor $fShowField$fShowSMTFunction $fShowSMTExpr$fSMTBackendAnyBackendm$fEnumBitVector$fShowBitVector$fTypeableNatS$fTypeableNatZ$fOrdProxyArgValue$fEqProxyArgValue$fShowProxyArgValue $fOrdProxyArg $fEqProxyArg$fShowProxyArg$fArgs()$fShowUntypedValue$fOrdUntypedValue$fEqUntypedValue $fOrdUntyped $fEqUntyped$fMonadTransSMT'$fApplicativeSMT'$fMonadFixSMT' $fMonadIOSMT' $fMonadSMT' $fFunctorSMT'valueToHaskellextractAnnotationinferResAnnotationentype entypeValuecastUntypedExprcastUntypedExprValuedtMaybe conNothingconJustnothing'just' fieldFromJustundefArgdtListconNil conInsertinsert'nil' fieldHead fieldTail bvUnsignedbvSigned bvRestrictwithSort withNumSort withSorts withArraySort foldExprM foldArgsMfoldExpr foldExprMuxfoldArgs foldArgsMux compareFuncompareConstructor compareField compareArgs compareExprseqExpr valueToConst $fOrdField $fEqField$fOrdConstructor$fEqConstructor $fOrdSMTExpr $fEqSMTExpr$fOrdSMTFunction$fEqSMTFunction$fExtractableBVTypedBVTyped$fExtractableBVUntypedBVTyped$fExtractableBVTypedBVUntyped$fExtractableBVUntypedBVUntyped $fNumSMTExpr$fNumBitVector$fSMTValueBitVector$fIsBitVectorBVTyped$fSMTTypeBitVector$fSMTValueBitVector0$fIsBitVectorBVUntyped$fSMTTypeBitVector0 $fSMTValue[] $fSMTType[]$fSMTValueMaybe$fSMTTypeMaybe$fLiftArgsMaybe$fLiftArgsEither $fLiftArgsMap $fLiftArgs[] $fArgsMaybe $fArgsEither $fArgsMap$fArgs[]$fLiftArgs(,,,,,) $fArgs(,,,,,)$fLiftArgs(,,,,) $fArgs(,,,,)$fLiftArgs(,,,) $fArgs(,,,)$fLiftArgs(,,) $fArgs(,,) $fLiftArgs(,)$fLiftArgsSMTExpr $fArgs(,) $fArgsSMTExpr$fConcatableBVUntypedBVUntyped$fConcatableBVTypedBVUntyped$fConcatableBVUntypedBVTyped$fConcatableBVTypedBVTyped$fLiftable(,,,,,)$fLiftable(,,,,)$fLiftable(,,,)$fLiftable(,,) $fLiftable(,) $fLiftable[]$fLiftableSMTExpr$fSMTTypeSMTArray $fSMTOrdRatio$fFractionalSMTExpr $fNumSMTExpr0$fSMTArithRatio$fSMTValueRatio$fSMTTypeRatio $fEnumSMTExpr$fSMTOrdInteger $fNumSMTExpr1$fSMTArithInteger$fSMTValueInteger$fSMTTypeInteger$fSMTValueBool $fSMTTypeBool$fSMTValueUntypedValue$fSMTTypeUntypedValue$fSMTTypeUntypedoptimizeBackend optimizeExprcheckSat checkSatUsing checkSat'isSatapplypushpopstackcommentvarNamed varNamedAnnvarAnnvaruntypedNamedVar untypedVar argVarsAnnargVarsAnnNamedargVarsAnnNamed'argVarsconstant constantAnngetValue getValuesgetModel unmangleArraydefFundefConst defConstNameddefConstNamed'defFunAnnNameddefFunAnnNamed' defFunAnnand'.&&.or'.||. arrayEqualsassertinterpolationGroupassertId assertInterpgetInterpolant setOptiongetInfofunAnn funAnnNamed funAnnNamed' funAnnRetfunappmap'.==.argEqdistinctplusmultminusdiv'div''mod'mod''rem'rem''dividedivide'negtoRealtoIntitexor.=>.not'not''selectstoreasArray constArraybvandbvorbvxorbvnotbvnegbvaddbvsubbvmulbvurembvsrembvudivbvsdivbvulebvultbvugebvugtbvslebvsltbvsgebvsgtbvshlbvlshrbvashrbvconcat bvextract bvextract' bvsplitu16to8bvsplitu32to16 bvsplitu32to8bvsplitu64to32bvsplitu64to16 bvsplitu64to8 mkQuantifiedforAll forAllAnnexists existsAnnlet'letAnnlets forAllList existsListis.#head'tail'isNilisInsertsetLogicnamednamed'getProofsimplify getUnsatCore optimizeExpr'FunctionParser' DefinedParser definedArgSig definedRetSig parseDefinedOverloadedParsersortConstraint deriveRetSortparseOverloadedFunctionParserparseFunSMTPipe renderExpr renderExpr'renderSMTRequestrenderSMTResponse createSMTPipe sortToLisp lispToSort exprToLispexprToLispWithcommonTheorems lispToExpr simpleParsercommonFunctionswithPipe SMTConnectionopenclosewithConnection performSMTperformSMTExitCleanlywithZ3 withMathSatwithCVC4withSMTInterpolghc-prim GHC.ClassesOrd TFCo:R:AddSn2 TFCo:R:AddZnOptimizeBackendOptB optimizeCallremoveConstsOf removeItems splitLastbvBinOpOptimizebvCompOptimizeintArithOptimizeintMinusOptimizeintCmpOptimize$fSMTBackendOptimizeBackendm channelIn channelOut processHandlesmtState handleNormal handleRequestargumentSortToLisp sortToLisp'findName mkUntyped isOverloadedfunctionSignaturefunctionGetSymbol clearInput putRequest parseResponseargs removeLets lispToValue lispToValue' lispToConstr valueToLispgeneralizeSortgeneralizeSortsexprSort quantToExprparseLetwithFirstArgSort nameParserallEqConstrainteqParser mapParser ordOpParser arithOpParser minusParserintArithParser divideParser absParser logicParserdistinctParser toRealParser toIntParser iteParser bvCompParser bvBinOpParser bvUnOpParser selectParser storeParserconstArrayParser concatParser extractParser sigParserdivisibleParserconstructorParser fieldParser tacticToLisp probeToLisp$fMonoidFunctionParser$fSMTBackendSMTPipembackend